mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-09-11 20:40:38 +03:00
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.
3 lines
116 B
Plaintext
3 lines
116 B
Plaintext
Bool.lemma.notnot
|
|
: ∀(b: Bool) (Equal Bool (Bool.not (Bool.not b)) b)
|
|
= λb (~b _ ?a (Equal.refl Bool Bool.false)) |