blob: cc0d0ca708df190854e2b244112d94467ee89670 (
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
|
T14040a.hs:21:18: error:
• Couldn't match type ‘k0’ with ‘a’
because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for:
elimWeirdList :: forall a1 (wl :: WeirdList a1) (p :: forall x.
x -> WeirdList x -> *).
Sing wl
-> (forall y. p k0 w0 'WeirdNil)
-> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
Sing x -> Sing xs -> p k1 w1 xs -> p k2 w2 ('WeirdCons x xs))
-> p k3 w3 wl
at T14040a.hs:(21,18)-(28,23)
Expected type: Sing wl
-> (forall y. p k1 w0 'WeirdNil)
-> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2 ('WeirdCons x xs))
-> p k3 w3 wl
Actual type: Sing wl
-> (forall y. p k1 w0 'WeirdNil)
-> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2 ('WeirdCons x xs))
-> p k3 w3 wl
• In the ambiguity check for ‘elimWeirdList’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
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:34:8: error:
• Cannot apply expression of type ‘Sing wl
-> (forall y. p k0 w0 'WeirdNil)
-> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
Sing x
-> Sing xs -> p k1 w1 xs -> p k2 w2 ('WeirdCons x xs))
-> p k3 w3 wl’
to a visible type argument ‘(WeirdList z)’
• In the sixth argument of ‘pWeirdCons’, namely
‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
In the expression:
pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
In an equation for ‘elimWeirdList’:
elimWeirdList
(SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil
pWeirdCons
= pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
|
