Improve detection of unsatisfiable unification problems

[fblanqui]

Currently, the file tests/OK/gaspard.dk is accepted. Its LP version is:

constant symbol U : TYPE;
constant symbol foo : U;
constant symbol e : U → TYPE;
constant symbol c : Π x : U, e x;
symbol aux : (Π x : U, e x) → U;
rule aux (λ _, c $_) ↪ foo;

LP checks that the rule preserves typing but doesn't detect that the LHS is in fact not typable. This can also be seen by asking:

type aux (λ _, c ?M);

This is not actually an issue as LP ends with a constraint that it cannot solve, but it would be better to detect and tell the user that the constraint is not satisfiable.