diff options
Diffstat (limited to 'testsuite/tests/typecheck/should_fail/T18851c.stderr')
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/T18851c.stderr | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/testsuite/tests/typecheck/should_fail/T18851c.stderr b/testsuite/tests/typecheck/should_fail/T18851c.stderr new file mode 100644 index 0000000000..4360fb16d2 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T18851c.stderr @@ -0,0 +1,33 @@ + +T18851c.hs:25:27: error: + • Could not deduce (n2 ~ n1) + arising from reasoning about an injective type family using constraints: + ‘Plus1 n2 ~ n’ + arising from a type equality + VSucc (Plus1 n2) ~ VSucc n at T18851c.hs:25:27-33 + ‘Plus1 n1 ~ 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:6-12 + 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 |