blob: 1d122cf590dde8d9ad8372dc8598758104d22dd3 (
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
|
T14040a.hs:21:18: error:
• Cannot generalise type; skolem ‘z’ would escape its scope
if I tried to quantify (_1 :: WeirdList z) in this type:
forall a1 (wl :: WeirdList a1)
(p :: forall x. x -> WeirdList x -> *).
Sing @(WeirdList a1) wl
-> (forall y. p @x0 _0 ('WeirdNil @x0))
-> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing @z x
-> Sing @(WeirdList (WeirdList z)) xs
-> p @(WeirdList z) _1 xs
-> p @z _2 ('WeirdCons @z x xs))
-> p @a1 _3 wl
(Indeed, I sometimes struggle even printing this correctly,
due to its ill-scoped nature.)
• 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
|
