class b, c, d, e, f, g < Type;

class Type < Type;

class Type < Type;

class Type < Type;

class d < Type;

class a < d;

class a < a;

class a < b;

class b < d;

class d < d;

class d < a;

type t : a

class h < a;

class h < c;

type [__] : a -> b

var x : a; y : Type; x : y

var

var x : b

var x < t

sort

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

a < (b, d)

b < d

c < Type

d < Type

e < Type

f < Type

g < Type

h < (c, a)

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

[__] : a -> b

t : a

%% Type Variables --------------------------------------------------------

x < t : a %(var_4)%

y : Type %(var_2)%

%% Variables -------------------------------------------------------------

x : y

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

### Warning 3.7, void universe class declaration 'Type'

### Warning 4.7, void universe class declaration 'Type'

### Warning 6.7, void universe class declaration 'Type'

*** Error 8.11, not a class 'a'

### Warning 8.7, unchanged class 'd'

*** Error 13.7, cyclic class 'a'

### Hint 15.7, refined class 'a'

### Hint 16.7, refined class 'b'

*** Error 18.7, cyclic class 'd'

*** Error 19.7, cyclic class 'd'

### Hint 24.7, refined class 'h'

*** Error 26.7, illegal type pattern argument '__'

### Hint 28.5, is type variable 'x'

### Hint 28.12, is type variable 'y'

### Hint 28.24, not a class 'y'

### Hint 30.7, not a class 's'

*** Error 30.9, unknown type 's'

### Hint 32.5, is type variable 'x'

### Hint 32.5, rebound type variable 'x'

### Hint 34.5, rebound type variable 'x'

*** Error 36.8, illegal type pattern argument '__'