diff options
Diffstat (limited to 'testsuite/tests/partial-sigs/should_fail/T14040a.stderr')
| -rw-r--r-- | testsuite/tests/partial-sigs/should_fail/T14040a.stderr | 57 |
1 files changed, 24 insertions, 33 deletions
diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr index d03d0dc32b..1d122cf590 100644 --- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr +++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr @@ -1,34 +1,25 @@ -T14040a.hs:34:8: error: - • Cannot apply expression of type ‘Sing wl - -> (forall y. p _0 'WeirdNil) - -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)). - Sing x - -> Sing xs - -> p GHC.Types.Any xs - -> p GHC.Types.Any ('WeirdCons x xs)) - -> p _1 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) +T14040a.hs:21:18: error: + • Cannot generalise type; skolem ‘z’ would escape its scope + if I tried to quantify (_1 :: WeirdList z) in this type: + forall a1 (wl :: WeirdList a1) + (p :: forall x. x -> WeirdList x -> *). + Sing @(WeirdList a1) wl + -> (forall y. p @x0 _0 ('WeirdNil @x0)) + -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)). + Sing @z x + -> Sing @(WeirdList (WeirdList z)) xs + -> p @(WeirdList z) _1 xs + -> p @z _2 ('WeirdCons @z x xs)) + -> p @a1 _3 wl + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the type signature: + elimWeirdList :: forall (a :: Type) + (wl :: WeirdList a) + (p :: forall (x :: Type). x -> WeirdList x -> Type). + Sing wl + -> (forall (y :: Type). p _ WeirdNil) + -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). + Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) + -> p _ wl |