OpWithInst.hascasl.output revision 678e45c045799ce271c4719123ecd9cf4f456d4b
type s
op a : s
vars a, b : Type
op __=[s]__ : forall a . a * a -> Unit
. (op __=[s]__ : forall a : Type . a * a -> Unit) (a, a)
. a =[s] a
. a =e=[s : Type] a;
op f[a] : a -> Unit
op g[b,a] : a * b -> Unit
op h[b,a] : a -> b
op j[a,b] : a -> b
class Funct < Type -> Type
vars f, F : Funct
%% order of var declarations counts
op k[a,f] : f a
op k[b,a,f] : b -> f a
op k[a,b,f] : b -> f a
op l[F,a] : F a
%% or explicit forall order
op k[G,b,a] : forall G : Funct; b : Type; a : Type . b -> G a
. (op __=[s]__ : forall a : Type . a * a -> Unit)[s] (a, a)
. (__=[s]__ : s * s -> Unit) (a, a)
. (__ =[s][s : Type] __ : s * s -> Unit) (a, a)
. (op __=[s][a : Type]__ : a * a -> Unit)[s] (a, a);
op if__then__else[a][a : Type]__ : a * a * a -> a
op if__then__else[s][a : Type]__ : a * a * a -> a
op if__then__else[a : Type]__ : a * a * a -> a
class
Funct < Type -> Type
type
s : Type
vars
F : Funct %(var_8)%;
a : Type %(var_1)%;
b : Type %(var_2)%;
f : Funct %(var_7)%
op __=[s]__ : forall a : Type . a * a -> Unit
op a : s
op f[a] : forall a : Type . a -> Unit
op g[b,a] : forall a : Type; b : Type . a * b -> Unit
op h[b,a] : forall a : Type; b : Type . a -> b
op if__then__else__ : forall a : Type . a * a * a -> a
op if__then__else[a]__ : forall a : Type . a * a * a -> a
op if__then__else[s]__ : forall a : Type . a * a * a -> a
op j[a,b] : forall a : Type; b : Type . a -> b
op k[G,b,a] : forall G : Funct; b : Type; a : Type . b -> G a
op k[a,b,f] : forall a : Type; b : Type; f : Funct . b -> f a
op k[a,f] : forall a : Type; f : Funct . f a
op k[b,a,f] : forall a : Type; b : Type; f : Funct . b -> f a
op l[F,a] : forall a : Type; F : Funct . F a
. a =[s] a
. a =[s] a
. a =e= a
. a =[s] a
. (__=[s]__ : s * s -> Unit) (a, a)
. (__ =[s][s : Type] __ : s * s -> Unit) (a, a)
. a =[s] a
### Hint 4.5, is type variable 'a'
### Hint 4.8, is type variable 'b'
### Hint 6.26,
no kind found for 'a'
expected: {Cpo}
found: {Type}
### Hint 6.26,
no kind found for 'a'
expected: {Cppo}
found: {Type}
### Hint 6.4-6.11, is polymorphic compound identifier '__=[s]__'
### Hint 8.29,
no kind found for 'a'
expected: {Cpo}
found: {Type}
### Hint 8.29,
no kind found for 'a'
expected: {Cppo}
found: {Type}
### Hint 8.7-8.14, is polymorphic compound identifier '__=[s]__'
### Hint 10.6-10.8, is compound list '[s]'
### Hint 11.8-11.15, is type list '[s : Type]'
### Hint 13.4-13.7, is polymorphic compound identifier 'f[a]'
### Hint 15.13,
no kind found for 'a'
expected: {Cpo}
found: {Type}
### Hint 15.13,
no kind found for 'a'
expected: {Cppo}
found: {Type}
### Warning 15.6, unexpected identifier in compound list 'b'
### Hint 15.4-15.9, is polymorphic compound identifier 'g[b,a]'
### Warning 17.6, unexpected identifier in compound list 'b'
### Hint 17.4-17.9, is polymorphic compound identifier 'h[b,a]'
### Warning 19.8, unexpected identifier in compound list 'b'
### Hint 19.4-19.9, is polymorphic compound identifier 'j[a,b]'
### Hint 23.5, is type variable 'f'
### Hint 23.8, is type variable 'F'
### Warning 25.9, unexpected identifier in compound list 'f'
### Hint 25.4-25.10, is polymorphic compound identifier 'k[a,f]'
### Warning 26.6, unexpected identifier in compound list 'b'
### Warning 26.12, unexpected identifier in compound list 'f'
### Hint 26.4-26.13, is polymorphic compound identifier 'k[b,a,f]'
### Warning 27.9, unexpected identifier in compound list 'b'
### Warning 27.12, unexpected identifier in compound list 'f'
### Hint 27.4-27.13, is polymorphic compound identifier 'k[a,b,f]'
### Warning 29.6, unexpected identifier in compound list 'F'
### Hint 29.4-29.10, is polymorphic compound identifier 'l[F,a]'
### Hint 32.34, rebound type variable 'b'
### Hint 32.37, rebound type variable 'a'
### Warning 32.6, unexpected identifier in compound list 'G'
### Warning 32.9, unexpected identifier in compound list 'b'
### Hint 32.4-32.13, is polymorphic compound identifier 'k[G,b,a]'
### Hint 34.44, is type list '[s]'
### Hint 34.29,
no kind found for 'a'
expected: {Cpo}
found: {Type}
### Hint 34.29,
no kind found for 'a'
expected: {Cppo}
found: {Type}
### Hint 34.7-34.14, is polymorphic compound identifier '__=[s]__'
### Hint 35.44-35.46, is type list '[s, s]'
### Hint 35.29,
no kind found for 'a'
expected: {Cpo}
found: {Type}
### Hint 35.29,
no kind found for 'a'
expected: {Cppo}
found: {Type}
### Hint 35.7-35.14, is polymorphic compound identifier '__=[s]__'
### Hint 35.44-35.46,
for type scheme 'a * a -> Unit' wrong length of instantiation list
'[s, s]'
### Hint 35.4-35.16,
untypeable term
'(op __=[s]__ : forall a : Type . a * a -> Unit)[s, s]'
*** Error 35.4-35.52,
no typing for
'(op __=[s]__ : forall a : Type . a * a -> Unit)[s, s] (a, a)'
### Hint 36.7-36.9, is compound list '[s]'
### Hint 36.10-36.22, is type list '[s, s : Type]'
### Hint 36.28,
no kind found for 's'
expected: {Cpo}
found: {Type}
### Hint 36.28,
no kind found for 's'
expected: {Cppo}
found: {Type}
### Hint 36.11-36.16,
for type scheme 'a * a -> Unit' wrong length of instantiation list
'[s, s : Type]'
### Hint 36.4-36.23, no type found for '__=[s]__'
### Hint 36.6-36.26,
untypeable term '__ =[s][s, s : Type] __ : s * s -> Unit'
*** Error 36.6-36.46,
no typing for '(__ =[s][s, s : Type] __ : s * s -> Unit) (a, a)'
### Hint 37.7-37.9, is compound list '[s]'
### Hint 37.15,
no kind found for 's'
expected: {Cpo}
found: {Type}
### Hint 37.15,
no kind found for 's'
expected: {Cppo}
found: {Type}
### Hint 37.29-37.31, is compound list '[s]'
*** Error 37.30, unexpected mixfix token: s
### Hint 38.7-38.9, is compound list '[s]'
### Hint 38.10-38.12, is compound list '[s]'
### Hint 38.18,
no kind found for 's'
expected: {Cpo}
found: {Type}
### Hint 38.18,
no kind found for 's'
expected: {Cppo}
found: {Type}
### Hint 38.32-38.34, is compound list '[s]'
*** Error 38.10, unexpected mixfix token: [
### Hint 39.7-39.9, is compound list '[s]'
### Hint 39.15,
no kind found for 's'
expected: {Cpo}
found: {Type}
### Hint 39.15,
no kind found for 's'
expected: {Cppo}
found: {Type}
### Hint 40.7-40.9, is compound list '[s]'
### Hint 40.10-40.19, is type list '[s : Type]'
### Hint 40.25,
no kind found for 's'
expected: {Cpo}
found: {Type}
### Hint 40.25,
no kind found for 's'
expected: {Cppo}
found: {Type}
### Hint 41.43, is type list '[s]'
### Hint 41.14, rebound type variable 'a'
### Hint 41.28,
no kind found for 'a'
expected: {Cpo}
found: {Type}
### Hint 41.28,
no kind found for 'a'
expected: {Cppo}
found: {Type}
### Hint 41.7-41.24, is polymorphic compound identifier '__=[s]__'
### Hint 43.22, rebound type variable 'a'
### Hint 43.35,
no kind found for 'a'
expected: {Cpo}
found: {Type}
### Hint 43.35,
no kind found for 'a'
expected: {Cppo}
found: {Type}
### Hint 43.4-43.31,
is polymorphic compound identifier 'if__then__else[a]__'
### Hint 44.22, rebound type variable 'a'
### Hint 44.35,
no kind found for 'a'
expected: {Cpo}
found: {Type}
### Hint 44.35,
no kind found for 'a'
expected: {Cppo}
found: {Type}
### Hint 44.4-44.31,
is polymorphic compound identifier 'if__then__else[s]__'
### Hint 45.19, rebound type variable 'a'
### Hint 45.32,
no kind found for 'a'
expected: {Cpo}
found: {Type}
### Hint 45.32,
no kind found for 'a'
expected: {Cppo}
found: {Type}