Spurious unification error when checking Dedukti file

[rish987]

The following Dedukti file contains a syntax error, but also reports a unification error that only appears when the syntax error (or any other error) is present:

A: Type.
B: Type.

a: A.

def f : B -> A -> A.

[] f _ (f _ _) --> a.

[] f _ _ --> a.

: (; produces error ;)

This is the error:

$ lambdapi check test.dk --lib-root=.
Checking "test.dk" ...
[test.dk:12:0-1] [A] and [B] are not unifiable.
Unexpected token ":".

dk check only reports the syntax error (and succeeds when it is removed):

$ dk check test.dk
[ERROR CODE:702]  [test.dk] [line:12 column:0] 
Parsing error: Unexpected token ':'.

[fblanqui]

I cannot reproduce your error. I works for me with lambdapi 2.4.0 and master. Which version of lambdapi do you use? Perhaps you have some hidden invalid character in your file?

[rish987]

That's odd. I just updated to lambdapi 2.4.0 from lambdapi 2.1.0, but was still able to reproduce the error. I also was able to reproduce it with a fresh install of lambdapi 2.4.0 on a separate machine.

[fblanqui]

I see now. The problem is caused by the colon at the end. This is strange indeed.

[rish987]

Yes, in fact, any error that results in error output will show it (syntax error, typing error, etc.).