blob: 31e5c8c4e78054381535987b85fe8331941938a6 (
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
|
T14040a.hs:34:8: error:
• Cannot apply expression of type ‘Sing wl0
-> (forall y. p0 _0 'WeirdNil)
-> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
-> Sing xs
-> p0 GHC.Types.Any xs
-> p0 GHC.Types.Any ('WeirdCons x xs))
-> p0 GHC.Types.Any wl0’
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)
|
