blob: f359155dbd02ea514e1409c74ca85cf2e6648489 (
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
|
T15370.hs:14:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
• Couldn't match type ‘n’ with ‘j’
Expected: n :~: j
Actual: n :~: n
‘n’ is a rigid type variable bound by
the type signature for:
mkRefl :: forall {k} (n :: k) (j :: k). n :~: j
at T15370.hs:13:1-17
‘j’ is a rigid type variable bound by
the type signature for:
mkRefl :: forall {k} (n :: k) (j :: k). n :~: j
at T15370.hs:13:1-17
• In the expression: Refl
In an equation for ‘mkRefl’: mkRefl = Refl
• Relevant bindings include
mkRefl :: n :~: j (bound at T15370.hs:14:1)
T15370.hs:20:13: warning: [-Wdeferred-type-errors (in -Wdefault)]
• Couldn't match type ‘S r’ with ‘()’
Expected: ()
Actual: S r
• In the expression: no + _
In a case alternative: Refl -> no + _
In the expression: case mkRefl @x @y of { Refl -> no + _ }
• Relevant bindings include
no :: S r (bound at T15370.hs:18:7)
right :: S r -> () (bound at T15370.hs:18:1)
T15370.hs:20:18: warning: [-Wtyped-holes (in -Wdefault)]
• Found hole: _ :: S r
Where: ‘r’, ‘y’, ‘x’ are rigid type variables bound by
the type signature for:
right :: forall x y (r :: Either x y). S r -> ()
at T15370.hs:(16,1)-(17,18)
• In the second argument of ‘(+)’, namely ‘_’
In the expression: no + _
In a case alternative: Refl -> no + _
• Relevant bindings include
no :: S r (bound at T15370.hs:18:7)
right :: S r -> () (bound at T15370.hs:18:1)
Constraints include y ~ x (from T15370.hs:20:5-8)
|
