blob: be667ec3a635f907a6c6294bf47d5177cc7541b5 (
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
|
T14040a.hs:26:46: error:
• Couldn't match kind ‘k1’ with ‘WeirdList z’
Expected kind ‘WeirdList k1’,
but ‘xs’ has kind ‘WeirdList (WeirdList z)’
because kind variable ‘z’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)’
at T14040a.hs:(25,19)-(27,41)
• In the second argument of ‘p’, namely ‘xs’
In the type ‘Sing wl
-> (forall (y :: Type). p _ WeirdNil)
-> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
-> p _ wl’
In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x -> WeirdList x -> Type).
Sing wl
-> (forall (y :: Type). p _ WeirdNil)
-> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
-> p _ wl
T14040a.hs:27:27: error:
• Couldn't match kind ‘k0’ with ‘z’
Expected kind ‘WeirdList k0’,
but ‘WeirdCons x xs’ has kind ‘WeirdList z’
because kind variable ‘z’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)’
at T14040a.hs:(25,19)-(27,41)
• In the second argument of ‘p’, namely ‘(WeirdCons x xs)’
In the type ‘Sing wl
-> (forall (y :: Type). p _ WeirdNil)
-> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
-> p _ wl’
In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x -> WeirdList x -> Type).
Sing wl
-> (forall (y :: Type). p _ WeirdNil)
-> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
-> p _ wl
|
