lambdapi
lambdapi copied to clipboard
Deducteam
Improve type checking error messages
The error messages from Lambdapi could be more informative.
Let us consider a simple example:
We want to define functions fst and snd:
symbol const Type : TYPE
symbol injective eta : Type ⇒ TYPE
// function type
symbol const Ar : Type ⇒ Type ⇒ Type
set infix right 6 ">" ≔ Ar
rule eta (&a > &b) → eta &a ⇒ eta &b
definition fst : ∀ (A B : Type), eta (A > B > A) ≔
λ A B a b, a
All is good so far.
Now we introduce snd, where we change the type signature,
but forget to change the defining term:
definition snd : ∀ (A B : Type), eta (A > B > B) ≔
λ A B a b, a
We get an error from Lambdapi:
[errors-ex.lp, 12:0-13:14] Term [λA B a b, a] does not have type [∀(A:Type) (B:Type), eta (A > (B > B))].
This error message is correct, but it could be more helpful. Something along the lines:
[errors-ex.lp, 12:0-13:14] Term [a] does not have type [B].
(Inspiration could come from articles such as "Improving Type Error Messages in OCaml" by Arthur Charguéraud.)
For toy examples like this, one can of course spot the error easily, but with more involved proofs, this becomes increasingly difficult.
Yet another example:
symbol const Type : TYPE
symbol injective eta : Type ⇒ TYPE
symbol o : Type
symbol const neg : eta o ⇒ eta o
type neg o
Error message:
[typeinfer.lp, 7:5-10] Cannot infer the type of [neg o].
43c547dc684135542b8159885514b8219e062844 provides slightly more information.
One extreme case of guiding error messages: https://elm-lang.org/news/the-syntax-cliff Not necessarily what would be appropriate for Lambdapi, I agree, but the intention is interesting, I believe.