blob: 97a3c5f17a271773ae5bfb0668c8f755210d6610 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
|
type error: can not unify
[32m'Bool[m
with
[32m'Int[m
in
------------ trace
'Data3 :: [32mType[39m[K
Data3 :: [32m'Bool -> 'Char -> 'Bool->'Data3[39m[K
Data31 :: [32m'Int -> 'String -> 'Int->'Data3[39m[K
'Data3Case :: [32m(b : 'Data3->Type) -> (c:'Bool -> d:'Char -> e:'Bool -> b (Data3 c d e)) -> (g:'Int -> h:'String -> i:'Int -> b (Data31 g h i)) -> k:'Data3 -> b k[39m[K
match'Data3 :: [32m(b : Type->Type) -> b 'Data3 -> d:Type -> b d -> b d[39m[K
infer: [47m\([32ma[39m : _:'Type) -> 'Data3Case (\_:'Type -> _:'Type) (\_:'Type _:'Type ([32me[39m : _:'Type) -> labelend e) (\_:'Type _:'Type ([32mh[39m : _:'Type) -> labelend h) a[49m[K
infer: \([32ma[39m : [47m_:'Type[49m : [32mType[39m) -> 'Data3Case (\_:'Type -> _:'Type) (\_:'Type _:'Type ([32me[39m : _:'Type) -> labelend e) (\_:'Type _:'Type ([32mh[39m : _:'Type) -> labelend h) a[K
infer: \([32mb[39m : (\[34ma[39m:[47m'Type[49m -> a) : [32mType[39m) -> 'Data3Case (\_:'Type -> _:'Type) (\_:'Type _:'Type ([32mf[39m : _:'Type) -> labelend f) (\_:'Type _:'Type ([32mi[39m : _:'Type) -> labelend i) b[K
focus: \([32mb[39m : (\[34ma[39m:[47m[32mType[39m[49m -> a) : [32mType[39m) -> 'Data3Case (\_:'Type -> _:'Type) (\_:'Type _:'Type ([32mf[39m : _:'Type) -> labelend f) (\_:'Type _:'Type ([32mi[39m : _:'Type) -> labelend i) b[K
infer: \([32mb[39m : \[34ma[39m->[47ma[49m : [32mType[39m) -> 'Data3Case (\_:'Type -> _:'Type) (\_:'Type _:'Type ([32mf[39m : _:'Type) -> labelend f) (\_:'Type _:'Type ([32mi[39m : _:'Type) -> labelend i) b[K
focus: \([32mb[39m : \[34ma[39m->[47m[32ma[39m[49m : [32mType[39m) -> 'Data3Case (\_:'Type -> _:'Type) (\_:'Type _:'Type ([32mf[39m : _:'Type) -> labelend f) (\_:'Type _:'Type ([32mi[39m : _:'Type) -> labelend i) b[K
focus: \([32mb[39m : (\[34ma[39m -> [47m[32ma[39m[49m:[32mType[39m)) -> 'Data3Case (\_:'Type -> _:'Type) (\_:'Type _:'Type ([32mf[39m : _:'Type) -> labelend f) (\_:'Type _:'Type ([32mi[39m : _:'Type) -> labelend i) b[K
focus: \([32mc[39m : (\[34ma[39m [34mb[39m:[32m'Unit[39m -> [47m[32ma[39m[49m)) -> 'Data3Case (\_:'Type -> _:'Type) (\_:'Type _:'Type ([32mg[39m : _:'Type) -> labelend g) (\_:'Type _:'Type ([32mj[39m : _:'Type) -> labelend j) c[K
focus: \([32mb[39m : \[34ma[39m->[47m[32ma[39m[49m) -> 'Data3Case (\_:'Type -> _:'Type) (\_:'Type _:'Type ([32mf[39m : _:'Type) -> labelend f) (\_:'Type _:'Type ([32mi[39m : _:'Type) -> labelend i) b[K
focus: \[34ma[39m [32mb[39m:[47m[32ma[39m[49m -> 'Data3Case (\_:'Type -> _:'Type) (\_:'Type _:'Type ([32mf[39m : _:'Type) -> labelend f) (\_:'Type _:'Type ([32mi[39m : _:'Type) -> labelend i) b[K
infer: \[34ma[39m [32mb[39m:[32ma[39m -> [47m'Data3Case (\_:'Type -> _:'Type) (\_:'Type _:'Type ([32mf[39m : _:'Type) -> labelend f) (\_:'Type _:'Type ([32mi[39m : _:'Type) -> labelend i) b[49m[K
infer: \[34ma[39m [32mb[39m:[32ma[39m -> [47m'Data3Case (\_:'Type -> _:'Type) (\_:'Type _:'Type ([32mf[39m : _:'Type) -> labelend f) (\_:'Type _:'Type ([32mi[39m : _:'Type) -> labelend i)[49m b[K
infer: \[34ma[39m [32mb[39m:[32ma[39m -> [47m'Data3Case (\_:'Type -> _:'Type) (\_:'Type _:'Type ([32mf[39m : _:'Type) -> labelend f)[49m (\_:'Type _:'Type ([32mi[39m : _:'Type) -> labelend i) b[K
infer: \[34ma[39m [32mb[39m:[32ma[39m -> [47m'Data3Case (\_:'Type -> _:'Type)[49m (\_:'Type _:'Type ([32mf[39m : _:'Type) -> labelend f) (\_:'Type _:'Type ([32mi[39m : _:'Type) -> labelend i) b[K
infer: \[34ma[39m [32mb[39m:[32ma[39m -> [47m'Data3Case[49m (\_:'Type -> _:'Type) (\_:'Type _:'Type ([32mf[39m : _:'Type) -> labelend f) (\_:'Type _:'Type ([32mi[39m : _:'Type) -> labelend i) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> ([47m[32m\c:Type d:Type e:Type f:Type -> 'Data3Case c d e f[39m[49m) (\_:'Type -> _:'Type) (\_:'Type _:'Type ([32mj[39m : _:'Type) -> labelend j) (\_:'Type _:'Type ([32mm[39m : _:'Type) -> labelend m) b[K
check: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type e:Type f:Type -> 'Data3Case c d e f[39m) ([47m(\_:'Type -> _:'Type) :: [32m'Data3->Type[39m[49m) (\_:'Type _:'Type ([32mi[39m : _:'Type) -> labelend i) (\_:'Type _:'Type ([32ml[39m : _:'Type) -> labelend l) b[K
check: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type e:Type f:Type -> 'Data3Case c d e f[39m) (\[32mg[39m:[32m'Data3[39m -> [47m_:'Type :: [32mType[39m[49m) (\_:'Type _:'Type ([32mj[39m : _:'Type) -> labelend j) (\_:'Type _:'Type ([32mm[39m : _:'Type) -> labelend m) b[K
infer: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type e:Type f:Type -> 'Data3Case c d e f[39m) (\[32mg[39m:[32m'Data3[39m -> [47m_:'Type[49m : [32mType[39m) (\_:'Type _:'Type ([32mj[39m : _:'Type) -> labelend j) (\_:'Type _:'Type ([32mm[39m : _:'Type) -> labelend m) b[K
infer: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type e:Type f:Type -> 'Data3Case c d e f[39m) (\[32mg[39m:[32m'Data3[39m -> (\[34mh[39m:[47m'Type[49m -> h) : [32mType[39m) (\_:'Type _:'Type ([32mk[39m : _:'Type) -> labelend k) (\_:'Type _:'Type ([32mn[39m : _:'Type) -> labelend n) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type e:Type f:Type -> 'Data3Case c d e f[39m) (\[32mg[39m:[32m'Data3[39m -> (\[34mh[39m:[47m[32mType[39m[49m -> h) : [32mType[39m) (\_:'Type _:'Type ([32mk[39m : _:'Type) -> labelend k) (\_:'Type _:'Type ([32mn[39m : _:'Type) -> labelend n) b[K
infer: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type e:Type f:Type -> 'Data3Case c d e f[39m) (\[32mg[39m:[32m'Data3[39m -> \[34mh[39m->[47mh[49m : [32mType[39m) (\_:'Type _:'Type ([32mk[39m : _:'Type) -> labelend k) (\_:'Type _:'Type ([32mn[39m : _:'Type) -> labelend n) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type e:Type f:Type -> 'Data3Case c d e f[39m) (\[32mg[39m:[32m'Data3[39m -> \[34mh[39m->[47m[32mh[39m[49m : [32mType[39m) (\_:'Type _:'Type ([32mk[39m : _:'Type) -> labelend k) (\_:'Type _:'Type ([32mn[39m : _:'Type) -> labelend n) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type e:Type f:Type -> 'Data3Case c d e f[39m) (\[32mg[39m:[32m'Data3[39m [34mh[39m -> [47m[32mh[39m[49m:[32mType[39m) (\_:'Type _:'Type ([32mk[39m : _:'Type) -> labelend k) (\_:'Type _:'Type ([32mn[39m : _:'Type) -> labelend n) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type e:Type f:Type -> 'Data3Case c d e f[39m) (\[32mg[39m:[32m'Data3[39m [34mh[39m [34mi[39m:[32m'Unit[39m -> [47m[32mh[39m[49m) (\_:'Type _:'Type ([32ml[39m : _:'Type) -> labelend l) (\_:'Type _:'Type ([32mo[39m : _:'Type) -> labelend o) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type e:Type f:Type -> 'Data3Case c d e f[39m) (\[32mg[39m:[32m'Data3[39m -> \[34mh[39m->[47m[32mh[39m[49m) (\_:'Type _:'Type ([32mk[39m : _:'Type) -> labelend k) (\_:'Type _:'Type ([32mn[39m : _:'Type) -> labelend n) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type e:Type f:Type -> 'Data3Case c d e f[39m) (\[34mg[39m [32mh[39m:[32m'Data3[39m -> [47m[32mg[39m[49m) (\_:'Type _:'Type ([32mk[39m : _:'Type) -> labelend k) (\_:'Type _:'Type ([32mn[39m : _:'Type) -> labelend n) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type e:Type f:Type -> 'Data3Case c d e f[39m) (\[34mg[39m [47m[32mh:Type -> g[39m[49m) (\_:'Type _:'Type ([32mk[39m : _:'Type) -> labelend k) (\_:'Type _:'Type ([32mn[39m : _:'Type) -> labelend n) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m -> ([32m\d:Type e:Type f:Type g:Type -> 'Data3Case d e f g[39m) ([47m[32m\h:Type -> c[39m[49m)) (\_:'Type _:'Type ([32mk[39m : _:'Type) -> labelend k) (\_:'Type _:'Type ([32mn[39m : _:'Type) -> labelend n) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m [47m[32md:Type e:Type f:Type -> 'Data3Case (\g:Type -> c) d e f[39m[49m) (\_:'Type _:'Type ([32mj[39m : _:'Type) -> labelend j) (\_:'Type _:'Type ([32mm[39m : _:'Type) -> labelend m) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m -> ([47m[32m\d:Type e:Type f:Type -> 'Data3Case (\g:Type -> c) d e f[39m[49m) (\_:'Type _:'Type ([32mj[39m : _:'Type) -> labelend j)) (\_:'Type _:'Type ([32mm[39m : _:'Type) -> labelend m) b[K
check: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m -> ([32m\d:Type e:Type f:Type -> 'Data3Case (\g:Type -> c) d e f[39m) ([47m(\_:'Type _:'Type ([32mj[39m : _:'Type) -> labelend j) :: [32m'Bool -> 'Char -> 'Bool->c[39m[49m)) (\_:'Type _:'Type ([32mj[39m : _:'Type) -> labelend j) b[K
check: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m -> ([32m\d:Type e:Type f:Type -> 'Data3Case (\g:Type -> c) d e f[39m) (\[32mh[39m:[32m'Bool[39m -> [47m(\_:'Type ([32mj[39m : _:'Type) -> labelend j) :: [32m'Char -> 'Bool->c[39m[49m)) (\_:'Type _:'Type ([32mk[39m : _:'Type) -> labelend k) b[K
check: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m -> ([32m\d:Type e:Type f:Type -> 'Data3Case (\g:Type -> c) d e f[39m) (\[32mh[39m:[32m'Bool[39m [32mi[39m:[32m'Char[39m -> [47m(\([32mj[39m : _:'Type) -> labelend j) :: [32m'Bool->c[39m[49m)) (\_:'Type _:'Type ([32ml[39m : _:'Type) -> labelend l) b[K
check: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m -> ([32m\d:Type e:Type f:Type -> 'Data3Case (\g:Type -> c) d e f[39m) (\[32mh[39m:[32m'Bool[39m [32mi[39m:[32m'Char[39m [32mj[39m:[32m'Bool[39m -> [47mlabelend j :: [32mc[39m[49m)) (\_:'Type _:'Type ([32mm[39m : _:'Type) -> labelend m) b[K
check: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m -> ([32m\d:Type e:Type f:Type -> 'Data3Case (\g:Type -> c) d e f[39m) (\[32mh[39m:[32m'Bool[39m [32mi[39m:[32m'Char[39m [32mj[39m:[32m'Bool[39m -> labEnd [47mj::[32mc[39m[49m)) (\_:'Type _:'Type ([32mm[39m : _:'Type) -> labelend m) b[K
infer: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m -> ([32m\d:Type e:Type f:Type -> 'Data3Case (\g:Type -> c) d e f[39m) (\[32mh[39m:[32m'Bool[39m [32mi[39m:[32m'Char[39m [32mj[39m:[32m'Bool[39m -> labEnd [47mj[49m:[32mc[39m)) (\_:'Type _:'Type ([32mm[39m : _:'Type) -> labelend m) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m -> ([32m\d:Type e:Type f:Type -> 'Data3Case (\g:Type -> c) d e f[39m) (\[32mh[39m:[32m'Bool[39m [32mi[39m:[32m'Char[39m [32mj[39m:[32m'Bool[39m -> labEnd [47m[32mj[39m[49m:[32mc[39m)) (\_:'Type _:'Type ([32mm[39m : _:'Type) -> labelend m) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m -> ([32m\d:Type e:Type f:Type -> 'Data3Case (\g:Type -> c) d e f[39m) (\[32mh[39m:[32m'Bool[39m [32mi[39m:[32m'Char[39m [32mj[39m:[32m'Bool[39m -> labEnd \([34mk[39m : [32mc~'Bool[39m)->[47m[32mj[39m[49m)) (\_:'Type _:'Type ([32mn[39m : _:'Type) -> labelend n) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m -> ([32m\d:Type e:Type f:Type -> 'Data3Case (\g:Type -> c) d e f[39m) (\[32mh[39m:[32m'Bool[39m [32mi[39m:[32m'Char[39m [32mj[39m:[32m'Bool[39m -> labEnd (\[34mc[39m:=[32m'Bool[39m -> [47m[32mj[39m[49m))) (\_:'Type _:'Type ([32mm[39m : _:'Type) -> labelend m) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m -> ([32m\d:Type e:Type f:Type -> 'Data3Case (\g:Type -> c) d e f[39m) (\[32mh[39m:[32m'Bool[39m [32mi[39m:[32m'Char[39m [32mj[39m:[32m'Bool[39m [34mc[39m:=[32m'Bool[39m -> labEnd [47m[32mj[39m[49m)) (\_:'Type _:'Type ([32mm[39m : _:'Type) -> labelend m) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m -> ([32m\d:Type e:Type f:Type -> 'Data3Case (\g:Type -> c) d e f[39m) (\[32mh[39m:[32m'Bool[39m [32mi[39m:[32m'Char[39m [32mj[39m:[32m'Bool[39m [34mc[39m:=[32m'Bool[39m -> [47m[32mlabend j[39m[49m)) (\_:'Type _:'Type ([32mm[39m : _:'Type) -> labelend m) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m -> ([32m\d:Type e:Type f:Type -> 'Data3Case (\g:Type -> c) d e f[39m) (\[32mh[39m:[32m'Bool[39m [32mi[39m:[32m'Char[39m [34mc[39m:=[32m'Bool[39m [32mj[39m:[32m'Bool[39m -> [47m[32mlabend j[39m[49m)) (\_:'Type _:'Type ([32mm[39m : _:'Type) -> labelend m) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m -> ([32m\d:Type e:Type f:Type -> 'Data3Case (\g:Type -> c) d e f[39m) (\[32mh[39m:[32m'Bool[39m [32mi[39m:[32m'Char[39m [34mc[39m:=[32m'Bool[39m [47m[32mj:Type -> labend j[39m[49m)) (\_:'Type _:'Type ([32mm[39m : _:'Type) -> labelend m) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m -> ([32m\d:Type e:Type f:Type -> 'Data3Case (\g:Type -> c) d e f[39m) (\[32mh[39m:[32m'Bool[39m [34mc[39m:=[32m'Bool[39m [32mi[39m:[32m'Char[39m [47m[32mj:Type -> labend j[39m[49m)) (\_:'Type _:'Type ([32mm[39m : _:'Type) -> labelend m) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m -> ([32m\d:Type e:Type f:Type -> 'Data3Case (\g:Type -> c) d e f[39m) (\[32mh[39m:[32m'Bool[39m [34mc[39m:=[32m'Bool[39m [47m[32mi:Type j:Type -> labend j[39m[49m)) (\_:'Type _:'Type ([32mm[39m : _:'Type) -> labelend m) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m -> ([32m\d:Type e:Type f:Type -> 'Data3Case (\g:Type -> c) d e f[39m) (\[34mc[39m:=[32m'Bool[39m [32mh[39m:[32m'Bool[39m [47m[32mi:Type j:Type -> labend j[39m[49m)) (\_:'Type _:'Type ([32mm[39m : _:'Type) -> labelend m) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m -> ([32m\d:Type e:Type f:Type -> 'Data3Case (\g:Type -> c) d e f[39m) (\[34mc[39m:=[32m'Bool[39m [47m[32mh:Type i:Type j:Type -> labend j[39m[49m)) (\_:'Type _:'Type ([32mm[39m : _:'Type) -> labelend m) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m [34mc[39m:=[32m'Bool[39m -> ([32m\d:Type e:Type f:Type -> 'Data3Case (\g:Type -> 'Bool) d e f[39m) ([47m[32m\h:Type i:Type j:Type -> labend j[39m[49m)) (\_:'Type _:'Type ([32mm[39m : _:'Type) -> labelend m) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> (\[34mc[39m [34mc[39m:=[32m'Bool[39m [47m[32md:Type e:Type -> 'Data3Case (\f:Type -> 'Bool) (\g:Type h:Type i:Type -> labend i) d e[39m[49m) (\_:'Type _:'Type ([32ml[39m : _:'Type) -> labelend l) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> ([47m[32m\c:Type d:Type -> 'Data3Case (\e:Type -> 'Bool) (\f:Type g:Type h:Type -> labend h) c d[39m[49m) (\_:'Type _:'Type ([32mk[39m : _:'Type) -> labelend k) b[K
check: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type -> 'Data3Case (\e:Type -> 'Bool) (\f:Type g:Type h:Type -> labend h) c d[39m) ([47m(\_:'Type _:'Type ([32mk[39m : _:'Type) -> labelend k) :: [32m'Int -> 'String -> 'Int->'Bool[39m[49m) b[K
check: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type -> 'Data3Case (\e:Type -> 'Bool) (\f:Type g:Type h:Type -> labend h) c d[39m) (\[32mi[39m:[32m'Int[39m -> [47m(\_:'Type ([32mk[39m : _:'Type) -> labelend k) :: [32m'String -> 'Int->'Bool[39m[49m) b[K
check: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type -> 'Data3Case (\e:Type -> 'Bool) (\f:Type g:Type h:Type -> labend h) c d[39m) (\[32mi[39m:[32m'Int[39m [32mj[39m:[32m'String[39m -> [47m(\([32mk[39m : _:'Type) -> labelend k) :: [32m'Int->'Bool[39m[49m) b[K
check: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type -> 'Data3Case (\e:Type -> 'Bool) (\f:Type g:Type h:Type -> labend h) c d[39m) (\[32mi[39m:[32m'Int[39m [32mj[39m:[32m'String[39m [32mk[39m:[32m'Int[39m -> [47mlabelend k :: [32m'Bool[39m[49m) b[K
check: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type -> 'Data3Case (\e:Type -> 'Bool) (\f:Type g:Type h:Type -> labend h) c d[39m) (\[32mi[39m:[32m'Int[39m [32mj[39m:[32m'String[39m [32mk[39m:[32m'Int[39m -> labEnd [47mk::[32m'Bool[39m[49m) b[K
infer: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type -> 'Data3Case (\e:Type -> 'Bool) (\f:Type g:Type h:Type -> labend h) c d[39m) (\[32mi[39m:[32m'Int[39m [32mj[39m:[32m'String[39m [32mk[39m:[32m'Int[39m -> labEnd [47mk[49m:[32m'Bool[39m) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type -> 'Data3Case (\e:Type -> 'Bool) (\f:Type g:Type h:Type -> labend h) c d[39m) (\[32mi[39m:[32m'Int[39m [32mj[39m:[32m'String[39m [32mk[39m:[32m'Int[39m -> labEnd [47m[32mk[39m[49m:[32m'Bool[39m) b[K
focus: \[34ma[39m [32mb[39m:[32ma[39m -> ([32m\c:Type d:Type -> 'Data3Case (\e:Type -> 'Bool) (\f:Type g:Type h:Type -> labend h) c d[39m) (\[32mi[39m:[32m'Int[39m [32mj[39m:[32m'String[39m [32mk[39m:[32m'Int[39m -> labEnd \([34ml[39m : [32m'Empty "can not unify\n\ESC[32m'Bool\ESC[m\nwith\n\ESC[32m'Int\ESC[m\n"[39m)->[47m[32mk[39m[49m) b[K
!type error: can not unify
[32m'Bool[m
with
[32m'Int[m
in
------------ tooltips
testdata/language-features/adt/adt02.reject.lc 2:6-2:11 Type
testdata/language-features/adt/adt02.reject.lc 2:6-5:25 Type
testdata/language-features/adt/adt02.reject.lc 2:6-7:11 Type
testdata/language-features/adt/adt02.reject.lc 2:6-10:20 Type
testdata/language-features/adt/adt02.reject.lc 3:5-3:10 Bool -> Char -> Bool->Data3 | Data3 | Type
testdata/language-features/adt/adt02.reject.lc 3:21-3:25 Type
testdata/language-features/adt/adt02.reject.lc 4:21-4:25 Type
testdata/language-features/adt/adt02.reject.lc 5:21-5:25 Type
testdata/language-features/adt/adt02.reject.lc 7:5-7:11 Data3 | Int -> String -> Int->Data3 | Type
testdata/language-features/adt/adt02.reject.lc 8:17-8:20 Type
testdata/language-features/adt/adt02.reject.lc 9:17-9:23 Type
testdata/language-features/adt/adt02.reject.lc 10:17-10:20 Type
|
