Improve error reporting

[smimram]

Please improve error reporting. For instance,

coh comp (x : *) (y : *) (f : x -> y) (z : *) (g : y -> z) : x -> z.

let test (x : *) (y : *) (f : x -> y) = comp f f.

results in

=^.^= let comp = x -> z
=I.I= defined.

Fatal error: exception Common.NotEqual("x", "y")

I would expect the line and character number of the error and the fact that the second f is expected to be of type y -> ... but is of type x -> y.

[smimram]

Another one:

coh comp (x : *) (y : *) (f : x -> y) (z : *) (g : y -> z) : x -> z.

coh test (x : *) (x : *) (f : x -> y) : comp f f -> f.

gives

=^.^= let comp = x -> z
=I.I= defined.

=^.^= let test = (comp f f) -> f
Fatal error: exception Common.DoubleDef("x")