f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblettclass a, b, c, d < Type

167414650dc57c11c13ba85253f0211b3de0ecc5Christian Maedertype r : a; s : a; s : b; t : c

7ae67d07c8b605503c300a7da2d11974a2702904Christian Maedertype [__], {__} : a -> b

4eaeba586d49aa0761ee2bb6d20efba91562cef6Andy Gimblettvar u : [r]; v : {s}

4eaeba586d49aa0761ee2bb6d20efba91562cef6Andy Gimbletttype tuple3 : a -> b -> c -> d

4eaeba586d49aa0761ee2bb6d20efba91562cef6Andy Gimblettvar x : tuple3 r s t

7ae67d07c8b605503c300a7da2d11974a2702904Christian Maedervar y : tuple3 r s

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimbletttype tuple1 : b -> a

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimbletttype m : (a -> b) -> c

type List : a -> b

var w : m List

var o1 : m

var o2 : m tuple1

var o3 : m tuple3

var nt : a -> (b -> c) -> c -> d

var o4 : nt r List s

type s1, r1, t1 < t

type s2 = r2 = t2

type s3 = {x : t . ((fun __=__[t]

: forall a : Type . a_v-1 * a_v-1 ->? Unit) :

t * t ->? Unit)

(var x : t, var x : t) :

Unit}

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

a < Type

b < Type

c < Type

d < Type

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

List : a -> b

Logical : Type := Unit ->? Unit

Pred : -Type -> Type := \ a : -Type . a_v-1 ->? Unit

Unit : Type

[__] : a -> b

__*__ : +Type -> +Type -> Type

__*__*__ : +Type -> +Type -> +Type -> Type

__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type

__*__*__*__*__ : +Type -> +Type -> +Type -> +Type -> +Type -> Type

__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)

__-->?__ : -Type -> +Type -> Type < __->?__

__->__ : -Type -> +Type -> Type < __->?__

__->?__ : -Type -> +Type -> Type

m : (a -> b) -> c

r : a

r1 : c < t

r2 : Type < (t2, r2, s2)

s : (b, a)

s1 : c < t

s2 : Type < (t2, r2, s2)

s3

: Type < t

= {x : t . ((fun __=__[t]

: forall a : Type . a_v-1 * a_v-1 ->? Unit) :

t * t ->? Unit)

(var x : t, var x : t) :

Unit}

t : c

t1 : c < t

t2 : Type < (t2, r2, s2)

tuple1 : b -> a

tuple3 : a -> b -> c -> d

{__} : a -> b

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

nt : a -> (b -> c) -> c -> d %(var_1)%

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

__/\__ : ? Unit * ? Unit ->? Unit %(fun)%

__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%

__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

__=>__ : ? Unit * ? Unit ->? Unit %(fun)%

__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

__\/__ : ? Unit * ? Unit ->? Unit %(fun)%

__if__ : ? Unit * ? Unit ->? Unit %(fun)%

__when__else__

: forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%

bottom : forall a : Type . a_v-1 %(fun)%

def__ : forall a : Type . a_v-1 ->? Unit %(fun)%

false : Unit %(fun)%

not__ : ? Unit ->? Unit %(fun)%

true : Unit %(fun)%

�__ : ? Unit ->? Unit %(fun)%

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

o1 : m

o2 : m tuple1

o3 : m tuple3

o4 : nt r List s

u : [r]

v : {s}

w : m List

x : tuple3 r s t

y : tuple3 r s

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

*** Hint 7.6, not a kind '[r]'

*** Hint 7.14, not a kind '{s}'

*** Hint 11.7, not a kind 'tuple3 r s t'

*** Hint 12.7, not a kind 'tuple3 r s'

*** Error 12.9-12.18, no kind found for 'tuple3 r s'

expected: [ Type ]

found: [ c -> d ]

*** Hint 18.7, not a kind 'm [__]'

*** Error 18.12, unexpected place '__'

*** Hint 22.7, not a kind 'm List'

*** Hint 24.8, not a class 'm'

*** Error 24.10, no kind found for 'm'

expected: [ Type ]

found: [ (a -> b) -> c ]

*** Hint 26.8, not a kind 'm tuple1'

*** Hint 26.12, no kind found for 'tuple1'

expected: [ a -> b ]

found: [ b -> a ]

*** Error 26.10-26.12, no kind found for 'm tuple1'

*** Hint 28.8, not a kind 'm tuple3'

*** Hint 28.12, no kind found for 'tuple3'

expected: [ a -> b ]

found: [ a -> b -> c -> d ]

*** Error 28.10-28.12, no kind found for 'm tuple3'

*** Hint 30.5, is type variable 'nt'

*** Hint 32.8, not a kind 'nt r List s'

*** Hint 32.15, no kind found for 'List'

expected: [ b -> c ]

found: [ a -> b ]

*** Error 32.10-32.20, no kind found for 'nt r List s'

*** Hint 38.12, rebound variable 'x'