%% Classes ---------------------------------------------------------------

TYPE = Type

a < d

b < d

c < d

d

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

Data1 : Type %[type __ ::=

a : -> __

b : -> __

c : -> __]%

Data2 : Type %[type __ ::=

Cons21 : Data1 �

Data2 -> __ (%(Data2.Cons21.sel_[1,1])% :? Data1)(%(Data2.Cons21.sel_[2,1])% :? Data2)

Cons22 : Data2 �

Data1 -> __ (%(Data2.Cons22.sel_[1,1])% :? Data2)(%(Data2.Cons22.sel_[2,1])% :? Data1)]%

Data3 : Type %[type __ ::=

Cons31 : Data1 � Data2 -> __ (sel1 :? Data1)(sel2 :? Data2)

Cons32 : Data2 � Data1 -> __ (sel2 :? Data2)(sel1 :? Data1)]%

Data4 : Type %[type __ ::=

Cons41 : Data1 � Data2 ->? __ (sel1 :? Data1)(sel2 :? Data2)

Cons42 : Data2 � Data1 ->? __ (sel2 :? Data2)(sel1 :? Data1)]%

Pred : Type- -> Type

Pred__ : Type- -> Type

Unit : TYPE

s : (c, Type) < ? s

t : Type %(var)%

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

%(Data2.Cons21.sel_[1,1])% : Data2 ->? Data1 %(select from Data2 constructed by

Cons21 : Data1 � Data2 -> Data2)%

%(Data2.Cons21.sel_[2,1])% : Data2 ->? Data2 %(select from Data2 constructed by

Cons21 : Data1 � Data2 -> Data2)%

%(Data2.Cons22.sel_[1,1])% : Data2 ->? Data2 %(select from Data2 constructed by

Cons22 : Data2 � Data1 -> Data2)%

%(Data2.Cons22.sel_[2,1])% : Data2 ->? Data1 %(select from Data2 constructed by

Cons22 : Data2 � Data1 -> Data2)%

Cons21 : Data1 � Data2 -> Data2 %(construct Data2)%

Cons22 : Data2 � Data1 -> Data2 %(construct Data2)%

Cons31 : Data1 � Data2 -> Data3 %(construct Data3)%

Cons32 : Data2 � Data1 -> Data3 %(construct Data3)%

Cons41 : Data1 � Data2 ->? Data4 %(construct Data4)%

Cons42 : Data2 � Data1 ->? Data4 %(construct Data4)%

a : Data1 %(construct Data1)%

: ? s

b : Data1 %(construct Data1)%

c : Data1 %(construct Data1)%

eq : s � s ->? Unit

sel1 : Data4 ->? Data1 %(select from Data4 constructed by

(Cons41 : Data1 � Data2 ->? Data4,

Cons42 : Data2 � Data1 ->? Data4))%

: Data3 ->? Data1 %(select from Data3 constructed by

(Cons31 : Data1 � Data2 -> Data3,

Cons32 : Data2 � Data1 -> Data3))%

sel2 : Data4 ->? Data2 %(select from Data4 constructed by

(Cons41 : Data1 � Data2 ->? Data4,

Cons42 : Data2 � Data1 ->? Data4))%

: Data3 ->? Data2 %(select from Data3 constructed by

(Cons31 : Data1 � Data2 -> Data3,

Cons32 : Data2 � Data1 -> Data3))%

tt : s ->? Unit = \ x : s . ()

x : s %(var)%

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

Error (line 1, column 7) illegal universe class declaration 'Type'

Warning (line 5, column 32) unchecked type 't'

Warning (line 5, column 20) redeclared class 'TYPE'

Error (line 5, column 20) inconsistent redefinition of 'TYPE'

Warning (line 11, column 16) implicit declaration of superclass 'd'

Warning (line 11, column 7) redeclared class 'a'

Warning (line 11, column 10) redeclared class 'b'

Warning (line 11, column 13) redeclared class 'c'

Warning (line 11, column 19) redeclared class 'a'

Error (line 11, column 19) class cannot become an alias class 'a'

Hint (line 16, column 9) not a class 's'

Error (line 20, column 12) unexpected mixfix token 'res'

Error (line 21, column 5) unexpected mixfix token '('

Error (line 22, column 5) unexpected mixfix token '('

Error (line 28, column 13) unexpected mixfix token '('

Error (line 30, column 13) unexpected mixfix token '('

Error (line 32, column 12) unexpected mixfix token 'impl'

Error (line 34, column 12) unexpected mixfix token 'or'

Error (line 37, column 6) unexpected mixfix token '('

Error (line 40, column 6) unexpected mixfix token '('

Hint (line 45, column 11) not a class 't'

Error (line 45, column 8) wrong type scheme of 'x'

expected: s

found: t

Hint (line 45, column 18) not a class 't'

Error (line 47, column 5) unexpected mixfix token '='

Warning (line 57, column 11) redeclared type 's'

Error (line 61, column 36) undeclared type 'Data2'

Error (line 61, column 52) undeclared type 'Data2'

Warning (line 61, column 73) data subtype ignored

Error (line 66, column 8) unexpected mixfix token 'true'

Hint (line 66, column 23) not a class 's'

Error (line 66, column 25) unexpected mixfix token 'e'

Hint (line 67, column 10) not a class 's'

Error (line 67, column 12) unexpected mixfix token 'e'