Arr opt

[leissa]

Trying to fix #109.

[NeuralCoder3]

Does this branch solve the problem and is ready?

[leissa]

No, it's only half of the equation. One problem was whether checking for alpha-equiv happens only optimistic or not. I.e. t1 == t2 must yield true, otherwise sth is broken. But there is also this is_uniform thing, where alpha-equiv is only optionally but we rely on that.

Anyway, I'm currently working (again) on the type inference which is strongly geared into the alpha-equiv and I'm looking again at this issue from this angle.

[leissa]

After our recent discussion in Discord, I looked once again into the changes here. One change was the problematic rule:

(a, b) -> ‹2; a›    if alpha-equiv(a, b).

Which is replaced by this PR with:

(a, b)#i (x, y, z)
* a: A = .Cn [X, Y, Z]
* b: B = .Cn [X, Y, Z]

While this does not yet fully fixes #10, it makes things better.