blob: 8aaf3b581f0156d91d806c8c056173e5d7404228 (
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
|
T15577.hs:20:18: error:
• Expecting one more argument to ‘f’
Expected a type, but ‘f’ has kind ‘* -> *’
• In the type ‘f’
In a stmt of a pattern guard for
an equation for ‘g’:
Refl <- f @f @a @r r
In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
T15577.hs:20:21: error:
• Expected kind ‘f1 a1 -> *’, but ‘a’ has kind ‘*’
• In the type ‘a’
In a stmt of a pattern guard for
an equation for ‘g’:
Refl <- f @f @a @r r
In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
• Relevant bindings include
r :: Proxy r1 (bound at T15577.hs:18:3)
g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
T15577.hs:20:26: error:
• Couldn't match kind ‘GHC.Types.RuntimeRep’ with ‘*’
When matching kinds
f1 :: * -> *
TYPE :: GHC.Types.RuntimeRep -> *
• In the fourth argument of ‘f’, namely ‘r’
In a stmt of a pattern guard for
an equation for ‘g’:
Refl <- f @f @a @r r
In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
• Relevant bindings include
r :: Proxy r1 (bound at T15577.hs:18:3)
g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
T15577.hs:21:7: error:
• Could not deduce: F r1 ~ r1
from the context: r0 ~ F r0
bound by a pattern with constructor:
Refl :: forall {k} (a :: k). a :~: a,
in a pattern binding in
a pattern guard for
an equation for ‘g’
at T15577.hs:18:7-10
Expected: F r1 :~: r1
Actual: r1 :~: r1
‘r1’ is a rigid type variable bound by
the type signature for:
g :: forall (f1 :: * -> *) a1 (r1 :: f1 a1).
Proxy r1 -> F r1 :~: r1
at T15577.hs:17:1-76
• In the expression: Refl
In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
• Relevant bindings include
r :: Proxy r1 (bound at T15577.hs:18:3)
g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
|
