type s

op a : s

op __=[s]__ : forall a . a * a -> Unit

. (op __=[s]__[s] : forall a : Type . a * a -> Unit) (a, a);

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

s : Type

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

__=[s]__ : forall a : Type . a * a -> Unit %(op)%

a : s %(op)%

%% Sentences -------------------------------------------------------------

a =[s] a

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

*** Error 4.22, unknown type variable 'a'

*** Error 6.28, unknown type variable 'a'