11 files changed, 52 insertions, 8 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, [''])