Gbury / dolmen

Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction
BSD 2-Clause "Simplified" License
80 stars 17 forks source link

Confusing error message with pattern matching on polymorphic type in ae's native language #215

Open Gbury opened 6 months ago

Gbury commented 6 months ago

Consider the following problem:

type 'a list = Cons of {elt : 'a; tail : 'a list} | Nil

function length (list : 'b) : int =
  match list with
  | Nil -> 0
  | Cons(_, l') -> length(l') + 1
end

This results in the following error message:

File "tmp.ae", line 5, character 4-7:
5 |   | Nil -> 0
        ^^^
Error The constructor Nil : ∀ 'a : Type . list('a) does not belong to type w1

Which might be surprising to users. To help clarify things, it would help if: