BTW, some of this recent stuff broke reading of `builtins.typer`, unless you have some corresponding changes to that which haven't been committed. I used `git bisect` (a rare treat) and found this is the first breaking commit:
``` fc6835a1c317e3bca4048fc19ee1525744bfa6d5 is the first bad commit commit fc6835a1c317e3bca4048fc19ee1525744bfa6d5 Author: Stefan Monnier monnier@iro.umontreal.ca Date: Fri Jul 7 16:30:42 2017 -0400
* btl/pervasive.typer: Let lambda_->_ infer the needed lambda_≡>_!
* btl/builtins.typer (Eq_comm): Same here. ```
and the (first) error is around `builtins.typer` line 57 (commutativity of equality):
``` Eq_comm : (l : TypeLevel) ≡> (t : Type_ l) ≡> (x : t) ≡> (y : t) ≡> (p : Eq (t := t) x y) -> Eq (t := t) y x; Eq_comm p = Eq_cast (f := lambda xy -> Eq (t := t) xy x) (p := p) Eq_refl; ```
where `unify_with_arrow` reports:
``` [Ln 57, cl 1] ./btl/builtins.typer [!] Error LPARSE Type
(l : TypeLevel[26]) ≡> (t : (##Type_ l[0])) ≡> (x : t[0]) ≡> (y : t[1]) ≡> (p : (Eq[40] l[3] t[2] x[1] y[0])) -> (Eq[41] l[4] t[3] y[1] x[2])
and
(p : ?tId[7]) -> ?tId[5]
does not match > Arrow:
(l : TypeLevel[26]) ≡> (t : (##Type_ l[0])) ≡> (x : t[0]) ≡> (y : t[1]) ≡> (p : (Eq[40] l[3] t[2] x[1] y [0])) -> (Eq[41] l[4] t[3] y[1] x[2]) ```
Christopher League league@contrapunctus.net writes:
Hey, this thread popped up as I was embarking on some travel, but now that I had a chance to read it, I just want to "+1" the solution you landed on! I'm not sure I liked the idea of a magic vs. literal equals in definitions (or is it 'cooked' vs. 'raw')? But having a 'λ' that adds extra 'Λ' as needed seems flexible and reasonable.
CL
Stefan Monnier monnier@IRO.UMontreal.CA writes:
*** Case 1 (easy): we want to be able to write
[...]
*** Case 2 (easy):
Since these depend on HM-style generalization and our inference alg doesn't let us (yet) compute efficiently the set of "free" metavars, this is still not implemented. [ Aka: *too* easy. ]
*** Case 3: We could also allow
This one even less.
*** Case 4: now comes the tricky part.
[...]
*** Case 5: sinking deeper.
These should now work. I ended up doing it not in `let` but in the `lambda_->_` special form. So this should work even for cases where we need to pass an anonymous polymorphic function but want to just write "lambda x -> ..." and skip writing the additional "lambda t ≡> ... "wrappers.
K : (a : Type) ≡> a -> (b : Type) ≡> b -> a; K x y = x;And yes, the new code also allows the above (tho currently, K is defined in pervasive.typer before we define multi-arg lambdas, so it can't be defined quite as above).
Stefan
Typer mailing list Typer@iro.umontreal.ca https://webmail.iro.umontreal.ca/mailman/listinfo/typer