diff options
| author | Richard Eisenberg <rae@richarde.dev> | 2019-12-11 15:58:56 +0000 |
|---|---|---|
| committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-01-12 21:29:27 -0500 |
| commit | 350e2b78788d47255d27489dfc62d664498b5de4 (patch) | |
| tree | 50f2f1982c9f120e6b8aac1970579d34333cd16a /testsuite/tests/partial-sigs | |
| parent | 9129210f7e9937c1065330295f06524661575839 (diff) | |
| download | haskell-350e2b78788d47255d27489dfc62d664498b5de4.tar.gz | |
Don't zap to Any; error instead
This changes GHC's treatment of so-called Naughty Quantification
Candidates to issue errors, instead of zapping to Any.
Close #16775.
No new test cases, because existing ones cover this well.
Diffstat (limited to 'testsuite/tests/partial-sigs')
| -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 |