%% Type Constructors -----------------------------------------------------

s : Type

t : Type

%% Assumptions -----------------------------------------------------------

__+__ : t -> t -> t

: t � t -> t

: s � s -> s

: s -> s -> s,idem, assoc, comm

a : t

: s

b : t

: s

c : s = a + b

%% Diagnostics -----------------------------------------------------------

Hint (line 5, column 14) type 's � s' is not unifiable with 's'

Hint (line 7, column 14) type 't' is not unifiable with 's'

Hint (line 5, column 14) type 't � t' is not unifiable with 's'

Hint (line 8, column 14) type 't' is not unifiable with 't � t'

Hint (line 7, column 14) type 't' is not unifiable with 's � s'

Hint (line 5, column 14) type 't' is not unifiable with 's'

Hint (line 3, column 12) type 't' is not unifiable with 's'

Hint (line 3, column 12) type 't' is not unifiable with 's'

Error (line 13, column 12) ambiguous mixfix term: a + b

(op __+ : s -> s -> s) (op a : s) (op b : s)

(op __+__ : s � s -> s) ((op a : s), (op b : s))