1. Previously, the following term wouldn't type-check:
match x = term {
true: ct
false: cf
}
When `term` isn't a variable.
The reason is that the `match` syntax was desugared to:
(~term _ ct cf)
Which, in general, results in the following check:
true : ∀(P: Bool -> *) ∀(t: P true) ∀(f: P false) (P term)
check _ :: Bool -> *
check ct :: (_ true)
check cf :: (_ false)
check () :: (_ term)
unify (_ term) == (P term)
This should generate the solution:
_ = λx(P x)
But, when `term` isn't a variable (it could be a function call, or a ref, for
example), this fails to satisfy the pattern unification criteria. To fix that,
we just use a `let` to always create a variable before unifying, so that the
`match` syntax is desugared to:
let x = term
(~x _ ct cf)
Which solves the issue.
2. Previously, the following term wouldn't type-check:
equal (a: Nat) (b: Nat) : Bool =
match a with (b: Nat) {
succ: match b {
succ: (equal a.pred b.pred)
zero: false
}
zero: match b {
succ: false
zero: true
}
}
After inspecting the type-checker output, I noticed the reason is due to how the
outer hole interacts with the inner hole. Specifically, after some computations
we eventually get to the following unification problem:
unify _2 == (_3 b)
Here, there are two ways to solve this:
_2 = (_3 b)
or
_3 = λx (_2)
Initially, it seems like both solutions are equivalent. Yet, by choosing the
first, we, later on, face the following problem:
- (_3 (succ x))
- Bool
Which violates the pattern unification requisites (for the same reason: `succ`
is a constructor, rather than a variable). A way to solve this problem would be
to simply invert the order, and use `_3 = λx (_2)` instead (done in the last
commit). That way, we'd have `(_3 (succ x))` reduce to just `_2`, which would
solve `_2 = Bool` and type-check fine. This is a quickfix though. I wonder if
there is a more principled approach that would let us avoid `(succ x)` to be
there at all.
Debug log: https://gist.github.com/VictorTaelin/6dd1a7167d5b7c8d5626c0f5b88c75a0
