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.

24 files changed, 173 insertions, 74 deletions

diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 823244ebca..6cc9f12bca 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -54,13 +54,9 @@ test('T15419', normal, compile, [''])
 test('T14066h', normal, compile, [''])
 test('T15666', normal, compile, [''])
 test('T15725', normal, compile, [''])
-test('T14880', normal, compile, [''])
-test('T14880-2', normal, compile, [''])
 test('T15743', normal, compile, ['-ddump-types -fprint-explicit-foralls'])
 test('InferDependency', normal, compile, [''])
 test('T15743e', normal, compile, ['-ddump-types -fprint-explicit-foralls'])
-test('T15076', normal, compile, [''])
-test('T15076b', normal, compile, [''])
 test('T15076c', normal, compile, [''])
 test('T15829', normal, compile, [''])
 test('T14729', normal, compile, ['-ddump-types -fprint-typechecker-elaboration -fprint-explicit-coercions'])
diff --git a/testsuite/tests/dependent/should_compile/T14880-2.hs b/testsuite/tests/dependent/should_fail/T14880-2.hs
index e7057a3f00..e7057a3f00 100644
--- a/testsuite/tests/dependent/should_compile/T14880-2.hs
+++ b/testsuite/tests/dependent/should_fail/T14880-2.hs
diff --git a/testsuite/tests/dependent/should_fail/T14880-2.stderr b/testsuite/tests/dependent/should_fail/T14880-2.stderr
new file mode 100644
index 0000000000..2082ca6c34
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14880-2.stderr
@@ -0,0 +1,8 @@
+
+T14880-2.hs:12:9: error:
+    • Cannot generalise type; skolem ‘arg’ would escape its scope
+      if I tried to quantify (a0 :: arg) in this type:
+        forall arg. Proxy @{Proxy @{arg} a0 -> *} (Foo arg @a0) -> ()
+      (Indeed, I sometimes struggle even printing this correctly,
+       due to its ill-scoped nature.)
+    • In the type signature: quux :: forall arg. Proxy (Foo arg) -> ()
diff --git a/testsuite/tests/dependent/should_compile/T14880.hs b/testsuite/tests/dependent/should_fail/T14880.hs
index 91cfb20a4a..91cfb20a4a 100644
--- a/testsuite/tests/dependent/should_compile/T14880.hs
+++ b/testsuite/tests/dependent/should_fail/T14880.hs
diff --git a/testsuite/tests/dependent/should_fail/T14880.stderr b/testsuite/tests/dependent/should_fail/T14880.stderr
new file mode 100644
index 0000000000..a5aa1df8d2
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14880.stderr
@@ -0,0 +1,12 @@
+
+T14880.hs:12:5: error:
+    • Cannot generalise type; skolem ‘arg’ would escape its scope
+      if I tried to quantify (a0 :: arg) in this type:
+        forall x arg.
+        ((Foo arg @a0 :: (Proxy @{arg} a0 -> *))
+         ~ (Foo arg @a0 :: (Proxy @{arg} a0 -> *))) =>
+        Bar x
+      (Indeed, I sometimes struggle even printing this correctly,
+       due to its ill-scoped nature.)
+    • In the definition of data constructor ‘MkBar’
+      In the data declaration for ‘Bar’
diff --git a/testsuite/tests/dependent/should_compile/T15076.hs b/testsuite/tests/dependent/should_fail/T15076.hs
index 0890cf9eab..0890cf9eab 100644
--- a/testsuite/tests/dependent/should_compile/T15076.hs
+++ b/testsuite/tests/dependent/should_fail/T15076.hs
diff --git a/testsuite/tests/dependent/should_fail/T15076.stderr b/testsuite/tests/dependent/should_fail/T15076.stderr
new file mode 100644
index 0000000000..814d459c3c
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15076.stderr
@@ -0,0 +1,11 @@
+
+T15076.hs:10:8: error:
+    • Cannot generalise type; skolem ‘a’ would escape its scope
+      if I tried to quantify (x0 :: a) in this type:
+        forall a (f :: forall (x :: a). Proxy @{a} x -> *).
+        Proxy @{Proxy @{a} x0 -> *} (f @x0) -> ()
+      (Indeed, I sometimes struggle even printing this correctly,
+       due to its ill-scoped nature.)
+    • In the type signature:
+        foo :: forall (a :: Type) (f :: forall (x :: a). Proxy x -> Type).
+               Proxy f -> ()
diff --git a/testsuite/tests/dependent/should_compile/T15076b.hs b/testsuite/tests/dependent/should_fail/T15076b.hs
index 15fce826c0..15fce826c0 100644
--- a/testsuite/tests/dependent/should_compile/T15076b.hs
+++ b/testsuite/tests/dependent/should_fail/T15076b.hs
diff --git a/testsuite/tests/dependent/should_fail/T15076b.stderr b/testsuite/tests/dependent/should_fail/T15076b.stderr
new file mode 100644
index 0000000000..3ee27a82b3
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15076b.stderr
@@ -0,0 +1,11 @@
+
+T15076b.hs:8:8: error:
+    • Cannot generalise type; skolem ‘a’ would escape its scope
+      if I tried to quantify (x0 :: a) in this type:
+        forall a (f :: forall (x :: a). Proxy @{a} x -> *).
+        Proxy @{Proxy @{a} x0 -> *} (f @x0) -> ()
+      (Indeed, I sometimes struggle even printing this correctly,
+       due to its ill-scoped nature.)
+    • In the type signature:
+        foo :: forall (a :: Type) (f :: forall (x :: a). Proxy x -> Type).
+               Proxy f -> ()
diff --git a/testsuite/tests/dependent/should_fail/T15825.stderr b/testsuite/tests/dependent/should_fail/T15825.stderr
index 97582ba952..5d989303a6 100644
--- a/testsuite/tests/dependent/should_fail/T15825.stderr
+++ b/testsuite/tests/dependent/should_fail/T15825.stderr
@@ -1,6 +1,8 @@
 
-T15825.hs:14:31: error:
-    • Illegal type synonym family application ‘GHC.Types.Any
-                                                 @k’ in instance:
-        X (a @(GHC.Types.Any @k))
+T15825.hs:14:10: error:
+    • Cannot generalise type; skolem ‘k’ would escape its scope
+      if I tried to quantify (x0 :: k) in this type:
+        forall k (a :: C k). X (a @x0)
+      (Indeed, I sometimes struggle even printing this correctly,
+       due to its ill-scoped nature.)
     • In the instance declaration for ‘X (a :: *)’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 8ff5a88961..dde686af7a 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -60,3 +60,7 @@ test('T16418', normal, compile_fail, [''])
 test('T17541', normal, compile_fail, [''])
 test('T17541b', normal, compile_fail, [''])
 test('T17131', normal, compile_fail, [''])
+test('T14880', normal, compile_fail, [''])
+test('T14880-2', normal, compile_fail, [''])
+test('T15076', normal, compile_fail, [''])
+test('T15076b', normal, compile_fail, [''])
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
diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T
index 2ac343f635..6ef1928768 100644
--- a/testsuite/tests/patsyn/should_compile/all.T
+++ b/testsuite/tests/patsyn/should_compile/all.T
@@ -75,7 +75,6 @@ test('T14058', [extra_files(['T14058.hs', 'T14058a.hs'])],
                multimod_compile, ['T14058', '-v0'])
 test('T14326', normal, compile, [''])
 test('T14394', normal, ghci_script, ['T14394.script'])
-test('T14552', normal, compile, [''])
 test('T14498', normal, compile, [''])
 test('T16682', [extra_files(['T16682.hs', 'T16682a.hs'])],
                multimod_compile, ['T16682', '-v0 -fwarn-incomplete-patterns -fno-code'])
diff --git a/testsuite/tests/patsyn/should_compile/T14552.hs b/testsuite/tests/patsyn/should_fail/T14552.hs
index a4a7493530..a4a7493530 100644
--- a/testsuite/tests/patsyn/should_compile/T14552.hs
+++ b/testsuite/tests/patsyn/should_fail/T14552.hs
diff --git a/testsuite/tests/patsyn/should_fail/T14552.stderr b/testsuite/tests/patsyn/should_fail/T14552.stderr
new file mode 100644
index 0000000000..b9b6b8448b
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T14552.stderr
@@ -0,0 +1,8 @@
+
+T14552.hs:22:9: error:
+    • Cannot generalise type; skolem ‘k’ would escape its scope
+      if I tried to quantify (aa0 :: k) in this type:
+        forall k (w :: k --> *). Exp a0 (F @k @(*) w aa0)
+      (Indeed, I sometimes struggle even printing this correctly,
+       due to its ill-scoped nature.)
+    • In the declaration for pattern synonym ‘FOO’
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index 27ebc8bdd4..02cc2cec2c 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -46,3 +46,4 @@ test('T15685', normal, compile_fail, [''])
 test('T15692', normal, compile, [''])   # It has -fdefer-type-errors inside
 test('T15694', normal, compile_fail, [''])
 test('T16900', normal, compile_fail, ['-fdiagnostics-show-caret'])
+test('T14552', normal, compile_fail, [''])
diff --git a/testsuite/tests/polykinds/T15795.stderr b/testsuite/tests/polykinds/T15795.stderr
new file mode 100644
index 0000000000..65bfdddecc
--- /dev/null
+++ b/testsuite/tests/polykinds/T15795.stderr
@@ -0,0 +1,9 @@
+
+T15795.hs:12:3: error:
+    • Cannot generalise type; skolem ‘k’ would escape its scope
+      if I tried to quantify (a0 :: k) in this type:
+        forall k (b :: k). T @k @a0 b
+      (Indeed, I sometimes struggle even printing this correctly,
+       due to its ill-scoped nature.)
+    • In the definition of data constructor ‘MkT’
+      In the data declaration for ‘T’
diff --git a/testsuite/tests/polykinds/T15795a.stderr b/testsuite/tests/polykinds/T15795a.stderr
new file mode 100644
index 0000000000..f4757137ce
--- /dev/null
+++ b/testsuite/tests/polykinds/T15795a.stderr
@@ -0,0 +1,9 @@
+
+T15795a.hs:9:3: error:
+    • Cannot generalise type; skolem ‘u’ would escape its scope
+      if I tried to quantify (cat10 :: u) in this type:
+        forall u (a :: u). F @u @cat10 a
+      (Indeed, I sometimes struggle even printing this correctly,
+       due to its ill-scoped nature.)
+    • In the definition of data constructor ‘Prod’
+      In the data declaration for ‘F’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 74ab266308..4312691755 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -204,8 +204,8 @@ test('T15817', normal, compile, [''])
 test('T15874', normal, compile, [''])
 test('T14887a', normal, compile, [''])
 test('T14847', normal, compile, [''])
-test('T15795', normal, compile, [''])
-test('T15795a', normal, compile, [''])
+test('T15795', normal, compile_fail, [''])
+test('T15795a', normal, compile_fail, [''])
 test('T16247', normal, compile_fail, [''])
 test('T16247a', normal, compile_fail, [''])
 test('KindVarOrder', normal, ghci_script, ['KindVarOrder.script'])
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index c51ff0b36b..80b11ca851 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -685,7 +685,6 @@ test('UnlifNewUnify', normal, compile, [''])
 test('UnliftedNewtypesLPFamily', normal, compile, [''])
 test('UnliftedNewtypesDifficultUnification', normal, compile, [''])
 test('T16832', normal, ghci_script, ['T16832.script'])
-test('T16946', normal, compile, [''])
 test('T16995', normal, compile, [''])
 test('T17007', normal, compile, [''])
 test('T17067', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T14350.stderr b/testsuite/tests/typecheck/should_fail/T14350.stderr
index eb80d3ec80..955554ab8d 100644
--- a/testsuite/tests/typecheck/should_fail/T14350.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14350.stderr
@@ -1,30 +1,52 @@
 
-T14350.hs:59:15: error:
-    • Couldn't match expected type ‘Proxy a1
-                                    -> Apply (Apply c 'Proxy) (Apply g 'Proxy)’
-                  with actual type ‘Sing (f @@ t0)’
-    • The function ‘applySing’ is applied to three arguments,
-      but its type ‘Sing f -> Sing t0 -> Sing (f @@ t0)’ has only two
-      In the expression: applySing f Proxy Proxy
-      In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy
-    • Relevant bindings include
-        x :: Sing x (bound at T14350.hs:59:11)
-        g :: Sing g (bound at T14350.hs:59:9)
-        f :: Sing f (bound at T14350.hs:59:7)
-        dcomp :: Sing f
-                 -> Sing g -> Sing x -> (c @@ 'Proxy) @@ (g @@ 'Proxy)
-          (bound at T14350.hs:59:1)
-
-T14350.hs:59:27: error:
-    • Couldn't match expected type ‘Sing t0’
-                  with actual type ‘Proxy a0’
-    • In the second argument of ‘applySing’, namely ‘Proxy’
-      In the expression: applySing f Proxy Proxy
-      In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy
-    • Relevant bindings include
-        x :: Sing x (bound at T14350.hs:59:11)
-        g :: Sing g (bound at T14350.hs:59:9)
-        f :: Sing f (bound at T14350.hs:59:7)
-        dcomp :: Sing f
-                 -> Sing g -> Sing x -> (c @@ 'Proxy) @@ (g @@ 'Proxy)
-          (bound at T14350.hs:59:1)
+T14350.hs:49:10: error:
+    • Cannot generalise type; skolem ‘a’ would escape its scope
+      if I tried to quantify (x0 :: a) in this type:
+        forall a (b1 :: a ~> *)
+               (c :: forall (x :: a). Proxy @{a} x ~> ((@@) @{*} @{a} b1 x ~> *))
+               (f :: forall (x :: a) (y :: (@@) @{*} @{a} b1 x).
+                     Proxy @{a} x
+                     ~> (Proxy @{Apply @a @(*) b1 x} y
+                         ~> (@@)
+                              @{*}
+                              @{Apply @a @(*) b1 x}
+                              ((@@)
+                                 @{Apply @a @(*) b1 x ~> *} @{Proxy @{a} x} (c @x) ('Proxy @{a} @x))
+                              y))
+               (g :: forall (x :: a). Proxy @{a} x ~> (@@) @{*} @{a} b1 x)
+               (x :: a).
+        Sing
+          @(Proxy @{a} x0
+            ~> (Proxy @{Apply @a @(*) b1 x0} y0
+                ~> Apply
+                     @(Apply @a @(*) b1 x0)
+                     @(*)
+                     (Apply
+                        @(Proxy @{a} x0)
+                        @(Apply @a @(*) b1 x0 ~> *)
+                        (c @x0)
+                        ('Proxy @{a} @x0))
+                     y0))
+          (f @x0 @y0)
+        -> Sing @(Proxy @{a} x1 ~> Apply @a @(*) b1 x1) (g @x1)
+        -> Sing @a x
+        -> (@@)
+             @{*}
+             @{Apply @a @(*) b1 x}
+             ((@@)
+                @{Apply @a @(*) b1 x ~> *} @{Proxy @{a} x} (c @x) ('Proxy @{a} @x))
+             ((@@)
+                @{Apply @a @(*) b1 x} @{Proxy @{a} x} (g @x) ('Proxy @{a} @x))
+      (Indeed, I sometimes struggle even printing this correctly,
+       due to its ill-scoped nature.)
+    • In the type signature:
+        dcomp :: forall (a :: Type)
+                        (b :: a ~> Type)
+                        (c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
+                        (f :: forall (x :: a) (y :: b @@ x).
+                              Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
+                        (g :: forall (x :: a). Proxy x ~> b @@ x)
+                        (x :: a).
+                 Sing f
+                 -> Sing g
+                    -> Sing x -> c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x))
diff --git a/testsuite/tests/typecheck/should_compile/T16946.hs b/testsuite/tests/typecheck/should_fail/T16946.hs
index e824f7cec8..e824f7cec8 100644
--- a/testsuite/tests/typecheck/should_compile/T16946.hs
+++ b/testsuite/tests/typecheck/should_fail/T16946.hs
diff --git a/testsuite/tests/typecheck/should_fail/T16946.stderr b/testsuite/tests/typecheck/should_fail/T16946.stderr
new file mode 100644
index 0000000000..a923fe778e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16946.stderr
@@ -0,0 +1,16 @@
+
+T16946.hs:11:9: error:
+    • Cannot generalise type; skolem ‘k’ would escape its scope
+      if I tried to quantify (y0 :: k) in this type:
+        forall k (c :: k -> k -> *)
+               (m :: forall (x :: k) (y :: k). c x y -> * -> *) a.
+        CatMonad @k c m =>
+        a -> m @y0 @y0 (Id @{k} @y0 c) a
+      (Indeed, I sometimes struggle even printing this correctly,
+       due to its ill-scoped nature.)
+    • In the type signature:
+        boom :: forall k
+                       (c :: k -> k -> Type)
+                       (m :: forall (x :: k) (y :: k). c x y -> Type -> Type)
+                       a.
+                CatMonad c m => a -> m (Id c) a
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index e46f694dd3..e11c239742 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -549,3 +549,4 @@ test('T17213', [extra_files(['T17213a.hs'])], multimod_compile_fail, ['T17213',
 test('T17355', normal, compile_fail, [''])
 test('T17360', normal, compile_fail, [''])
 test('T17563', normal, compile_fail, [''])
+test('T16946', normal, compile_fail, [''])