blob: fc3c1e0c8b0f222bad4782882da5e276796aefb1 (
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: [GHC-46956]
• Couldn't match kind ‘k0’ with ‘WeirdList z’
Expected kind ‘WeirdList k0’,
but ‘xs’ has kind ‘WeirdList (WeirdList z)’
because kind variable ‘z’ would escape its scope
This (rigid, skolem) kind variable is bound by
an explicit forall (z :: Type) (x :: z)
(xs :: WeirdList (WeirdList z))
at T14040a.hs:25:26-77
• In the second argument of ‘p’, namely ‘xs’
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: [GHC-46956]
• Couldn't match kind ‘k1’ with ‘z’
Expected kind ‘WeirdList k1’,
but ‘WeirdCons x xs’ has kind ‘WeirdList z’
because kind variable ‘z’ would escape its scope
This (rigid, skolem) kind variable is bound by
an explicit forall (z :: Type) (x :: z)
(xs :: WeirdList (WeirdList z))
at T14040a.hs:25:26-77
• In the second argument of ‘p’, namely ‘(WeirdCons x xs)’
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
|