Weird error message

[francoisthire]

On this example

#NAME bug.

type : Type.
def term : type -> Type.

pi : A : type -> (term A -> type) -> type.
[A,B] term (pi A B) --> a : term A -> term (B a).

def i (A : type) (B : term A -> type) : term (pi A B) := z : term A => z.

The error given is

Cannot type the definition of i test.dk, 9:4-5

Why?

[fblanqui]

Your example is tests/KO/francois.dk . The error message is now:

Cannot solve constraint [term A] ~ [term (B z)]
Cannot type the definition of [i] at [tests/KO/francois.dk, 7:4-5].
Error at [tests/KO/francois.dk, 7:0-72].