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
ADTs can be defined with the syntax:
data Vector T (len: Nat)
| cons (len: Nat) (head: T) (tail: (Vector T len)) : (Vector T (Nat.succ len))
| nil : (Vector T Nat.zero)
Which will convert to the equivalent inductive λ-encoding (via self).
Pattern-matching has the syntax:
match x = expr with (a: A) (b: B) ... {
ctr0: ret0
ctr1: ret1
}: motive
The 'with' syntax is used to explicitly move values down the cases,
crating lambdas for them. This linearizes them (which avoids cloning)
and specializes their type w.r.t. the matched value, for proving.
We also allow a shorthand for top-level definitions, as:
foo (a: A) (b: B) ... : R =
body
This will auto-add lambdas before 'body'. If 'body' is a pattern-match,
the lambdas will be automatically moved down, so this has the effect of
linearizing top-level args, without needing explicit 'with' annotations.
Now, there are two local binders:
let x = ...
use x = ...
The 'let' binder will create a local definition, type-check it, and
assign a name to it. When compiled, it will create 'dup' nodes.
The 'use' binder is just an alias. It will not bind a new variable, and,
when compiled, will create inline copies. Also, for type-checking, it
allows creating aliases that are definitionaly equal for the checker.
on the `infer` function, we usually have something like this:
infer (App f x) ctx =
infer <- infer f ctx
case infer of
All a b -> do
check x a ctx
return $ out arg
otherwise ->
fail
this causes `x : a` to be happen before `infer (f x)` returns `b x`.
this is generally fine, but, in situations such as dependent
eliminations:
λx (bool-elim ?A x t f) : (P x)
we really want `(elim ...)` to return `P x` BEFORE we check `t : ?A
true` and `t : ?A false`. that would allow the unification problem `?A x
== P x` to generate the solution `?A = λx (P x)` **before** the `t : ?A
true` check possibly fails.
being able to fill that metavar is very important for Kind2, since that
would allow us to omit motives in pattern-matches. because of that, I
think that the more sensible order is for infer to return its result
first, and then its inner checks occur. this is via a very lightweight
mechanism that consists of a list of suspended checks (`susp`), which we
push to inside `infer`, and fully consume inside `check`.
this is a middle-ground between checking in order (from left-to-right)
and a more complex suspension mechanism (involving dependency graphs).
with this simple solution, we're able to use metavars inside the motive
of dependent eliminations, greatly reducing the need for annotations in
practical code.
