blob: ebe5f8621d57b2d82bf4829b39e156b9bd32eed4 (
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
|
T18851c.hs:25:27: error: [GHC-25897]
• Could not deduce ‘n2 ~ n1’
arising from reasoning about an injective type family using constraints:
‘Plus1 n1 ~ n’
arising from a type equality
VSucc (Plus1 n1) ~ VSucc n at T18851c.hs:25:27-33
‘Plus1 n2 ~ n’
arising from a pattern with constructor:
VSucc :: forall (n :: Nat). V n -> VSucc (Plus1 n),
in an equation for ‘foo’ at T18851c.hs:25:16-22
from the context: n ~ Plus1 n1
bound by a pattern with constructor:
VSucc :: forall (n :: Nat). V n -> VSucc (Plus1 n),
in an equation for ‘foo’
at T18851c.hs:25:6-12
or from: n ~ Plus1 n2
bound by a pattern with constructor:
VSucc :: forall (n :: Nat). V n -> VSucc (Plus1 n),
in an equation for ‘foo’
at T18851c.hs:25:16-22
‘n2’ is a rigid type variable bound by
a pattern with constructor:
VSucc :: forall (n :: Nat). V n -> VSucc (Plus1 n),
in an equation for ‘foo’
at T18851c.hs:25:16-22
‘n1’ is a rigid type variable bound by
a pattern with constructor:
VSucc :: forall (n :: Nat). V n -> VSucc (Plus1 n),
in an equation for ‘foo’
at T18851c.hs:25:6-12
• In the expression: VSucc V
In an equation for ‘foo’: foo (VSucc _) (VSucc _) = VSucc V
|
