diff options
Diffstat (limited to 'testsuite/tests/partial-sigs/should_fail/T14040a.stderr')
| -rw-r--r-- | testsuite/tests/partial-sigs/should_fail/T14040a.stderr | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr new file mode 100644 index 0000000000..20a0fa51ca --- /dev/null +++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr @@ -0,0 +1,31 @@ + +T14040a.hs:34:8: error: + • Cannot apply expression of type ‘Sing wl + -> (forall y. p w0 'WeirdNil) + -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)). + Sing x -> Sing xs -> p w1 xs -> p w2 ('WeirdCons x xs)) + -> p w3 wl’ + to a visible type argument ‘(WeirdList z)’ + • In the sixth argument of ‘pWeirdCons’, namely + ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’ + In the expression: + pWeirdCons + @z + @x + @xs + x + xs + (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons) + In an equation for ‘elimWeirdList’: + elimWeirdList + (SWeirdCons (x :: Sing (x :: z)) + (xs :: Sing (xs :: WeirdList (WeirdList z)))) + pWeirdNil + pWeirdCons + = pWeirdCons + @z + @x + @xs + x + xs + (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons) |