blob: 20a0fa51ca44f714c923a863a6b4804434942bee (
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
|
T14040a.hs:34:8: error:
• Cannot apply expression of type ‘Sing wl
-> (forall y. p w0 'WeirdNil)
-> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
Sing x -> Sing xs -> p w1 xs -> p w2 ('WeirdCons x xs))
-> p 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)
|
