Why this term fails to typecheck?
VictorTaelin opened this issue · 4 comments
I'm trying to typecheck this term:
Lam (For Star (Pi (Var 0) (Var 1))) (Var 0)
Which, if I understand correctly, is equivalent to λ(p : (∀ (x : *) -> (x -> x))) -> p. I get a type mismatch error. Why?
Sorry for confusing notation. λ(p : (∀ (x : *) -> (x -> x))) -> p in Minimal.hs is written as (am "p" (pi "x" star $ "x" ==> "x") $ "p" in RawTerm or Lam (Pi Star $ Pi (Var 0) (Var 0)) $ Var 0 in Term.
That's because we use de Bruijn levels instead of indices, and also forAll is (confusingly, I admit) shorthand for λ(x : *) instead of ∀ (x : *).
Anyway, now I renamed forAll to tlam and defined forAll as ∀ (x : *).
Ahh. Of course. You said right on the post you was using Bruijn levels. Totally my fault for forgetting that.
Is there actually a simple way to convert to using bruijn indices (just for the fact I'm used to them), or would it be hard and/or problematic? On the Reddit thread someone claims I just need to change 2 lines, is that accurate?
Added DB indexed version, it's indeed a very small change.
Thank you!