blob: 955554ab8df7664739ef0567d03780510e24e587 (
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
|
T14350.hs:49:10: error:
• Cannot generalise type; skolem ‘a’ would escape its scope
if I tried to quantify (x0 :: a) in this type:
forall a (b1 :: a ~> *)
(c :: forall (x :: a). Proxy @{a} x ~> ((@@) @{*} @{a} b1 x ~> *))
(f :: forall (x :: a) (y :: (@@) @{*} @{a} b1 x).
Proxy @{a} x
~> (Proxy @{Apply @a @(*) b1 x} y
~> (@@)
@{*}
@{Apply @a @(*) b1 x}
((@@)
@{Apply @a @(*) b1 x ~> *} @{Proxy @{a} x} (c @x) ('Proxy @{a} @x))
y))
(g :: forall (x :: a). Proxy @{a} x ~> (@@) @{*} @{a} b1 x)
(x :: a).
Sing
@(Proxy @{a} x0
~> (Proxy @{Apply @a @(*) b1 x0} y0
~> Apply
@(Apply @a @(*) b1 x0)
@(*)
(Apply
@(Proxy @{a} x0)
@(Apply @a @(*) b1 x0 ~> *)
(c @x0)
('Proxy @{a} @x0))
y0))
(f @x0 @y0)
-> Sing @(Proxy @{a} x1 ~> Apply @a @(*) b1 x1) (g @x1)
-> Sing @a x
-> (@@)
@{*}
@{Apply @a @(*) b1 x}
((@@)
@{Apply @a @(*) b1 x ~> *} @{Proxy @{a} x} (c @x) ('Proxy @{a} @x))
((@@)
@{Apply @a @(*) b1 x} @{Proxy @{a} x} (g @x) ('Proxy @{a} @x))
(Indeed, I sometimes struggle even printing this correctly,
due to its ill-scoped nature.)
• In the type signature:
dcomp :: forall (a :: Type)
(b :: a ~> Type)
(c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
(f :: forall (x :: a) (y :: b @@ x).
Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
(g :: forall (x :: a). Proxy x ~> b @@ x)
(x :: a).
Sing f
-> Sing g
-> Sing x -> c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x))
|
