8 files changed, 58 insertions, 25 deletions
diff --git a/testsuite/tests/dependent/should_fail/T14066h.hs b/testsuite/tests/dependent/should_compile/T14066h.hs
index a20ae30958..df3db1c15d 100644
--- a/testsuite/tests/dependent/should_fail/T14066h.hs
+++ b/testsuite/tests/dependent/should_compile/T14066h.hs
@@ -7,5 +7,5 @@ import Data.Proxy
 f :: forall b. b -> (Proxy Int, Proxy Maybe)
 f x = (fst y :: Proxy Int, fst y :: Proxy Maybe)
   where
-    y :: (Proxy a, b)  -- MonoLocalBinds means this won't generalize over the kind of a
+    y :: (Proxy a, b)  -- this generalizes over the kind of a
     y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 4e096c1f71..418fba2d85 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -53,3 +53,4 @@ test('T15264', normal, compile, [''])
 test('DkNameRes', normal, compile, [''])
 test('T15346', normal, compile, [''])
 test('T15419', normal, compile, [''])
+test('T14066h', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/DepFail1.stderr b/testsuite/tests/dependent/should_fail/DepFail1.stderr
index 630f010fa3..a8e64d4e0c 100644
--- a/testsuite/tests/dependent/should_fail/DepFail1.stderr
+++ b/testsuite/tests/dependent/should_fail/DepFail1.stderr
@@ -2,11 +2,25 @@
 DepFail1.hs:7:6: error:
     • Expecting one more argument to ‘Proxy Bool’
       Expected a type, but ‘Proxy Bool’ has kind ‘Bool -> *’
-    • In the type signature:
-        z :: Proxy Bool
+    • In the type signature: z :: Proxy Bool
+
+DepFail1.hs:8:5: error:
+    • Couldn't match expected type ‘Proxy Bool’
+                  with actual type ‘Proxy k0 a1’
+    • In the expression: P
+      In an equation for ‘z’: z = P
 
 DepFail1.hs:10:16: error:
     • Expected kind ‘Int’, but ‘Bool’ has kind ‘*’
     • In the second argument of ‘Proxy’, namely ‘Bool’
-      In the type signature:
-        a :: Proxy Int Bool
+      In the type signature: a :: Proxy Int Bool
+
+DepFail1.hs:11:5: error:
+    • Couldn't match kind ‘*’ with ‘Int’
+      When matching types
+        a0 :: Int
+        Bool :: *
+      Expected type: Proxy Int Bool
+        Actual type: Proxy Int a0
+    • In the expression: P
+      In an equation for ‘a’: a = P
diff --git a/testsuite/tests/dependent/should_fail/T13895.stderr b/testsuite/tests/dependent/should_fail/T13895.stderr
index 0ae1710bf0..3e8bef6858 100644
--- a/testsuite/tests/dependent/should_fail/T13895.stderr
+++ b/testsuite/tests/dependent/should_fail/T13895.stderr
@@ -1,4 +1,28 @@
 
+T13895.hs:8:14: error:
+    • Could not deduce (Typeable (t dict0))
+      from the context: (Data a, Typeable (t dict))
+        bound by the type signature for:
+                   dataCast1 :: forall k (dict :: Typeable k) (dict1 :: Typeable
+                                                                          *) a (c :: *
+                                                                                     -> *) (t :: forall k1.
+                                                                                                 Typeable
+                                                                                                   k1 =>
+                                                                                                 k1
+                                                                                                 -> *).
+                                (Data a, Typeable (t dict)) =>
+                                (forall d. Data d => c (t dict1 d)) -> Maybe (c a)
+        at T13895.hs:(8,14)-(14,24)
+      The type variable ‘dict0’ is ambiguous
+    • In the ambiguity check for ‘dataCast1’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      In the type signature:
+        dataCast1 :: forall (a :: Type).
+                     Data a =>
+                     forall (c :: Type -> Type)
+                            (t :: forall (k :: Type). Typeable k => k -> Type).
+                     Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
+
 T13895.hs:12:23: error:
     • Illegal constraint in a kind: Typeable k0
     • In the first argument of ‘Typeable’, namely ‘t’
diff --git a/testsuite/tests/dependent/should_fail/T14066.stderr b/testsuite/tests/dependent/should_fail/T14066.stderr
index cd0142f5c1..e5179e510b 100644
--- a/testsuite/tests/dependent/should_fail/T14066.stderr
+++ b/testsuite/tests/dependent/should_fail/T14066.stderr
@@ -1,6 +1,6 @@
 
 T14066.hs:15:59: error:
-    • Expected kind ‘k0’, but ‘b’ has kind ‘k’
+    • Expected kind ‘k’, but ‘b’ has kind ‘k1’
     • In the second argument of ‘SameKind’, namely ‘b’
       In the type signature: g :: forall k (b :: k). SameKind a b
       In the expression:
@@ -8,4 +8,6 @@ T14066.hs:15:59: error:
           g :: forall k (b :: k). SameKind a b
           g = undefined
         in ()
-    • Relevant bindings include x :: Proxy a (bound at T14066.hs:15:4)
+    • Relevant bindings include
+        x :: Proxy a (bound at T14066.hs:15:4)
+        f :: Proxy a -> () (bound at T14066.hs:15:1)
diff --git a/testsuite/tests/dependent/should_fail/T14066e.stderr b/testsuite/tests/dependent/should_fail/T14066e.stderr
index 504ca5a80e..193c74d193 100644
--- a/testsuite/tests/dependent/should_fail/T14066e.stderr
+++ b/testsuite/tests/dependent/should_fail/T14066e.stderr
@@ -1,6 +1,15 @@
 
 T14066e.hs:13:59: error:
-    • Expected kind ‘c’, but ‘b'’ has kind ‘k0’
+    • Couldn't match kind ‘k1’ with ‘*’
+      ‘k1’ is a rigid type variable bound by
+        the type signature for:
+          j :: forall k k1 (c :: k1) (b :: k).
+               Proxy a -> Proxy b -> Proxy c -> Proxy b
+        at T14066e.hs:12:5-61
+      When matching kinds
+        k :: *
+        c :: k1
+      Expected kind ‘c’, but ‘b'’ has kind ‘k’
     • In the first argument of ‘Proxy’, namely ‘(b' :: c')’
       In an expression type signature: Proxy (b' :: c')
       In the expression: (p1 :: Proxy (b' :: c'))
diff --git a/testsuite/tests/dependent/should_fail/T14066h.stderr b/testsuite/tests/dependent/should_fail/T14066h.stderr
deleted file mode 100644
index bfd33693b6..0000000000
--- a/testsuite/tests/dependent/should_fail/T14066h.stderr
+++ /dev/null
@@ -1,16 +0,0 @@
-
-T14066h.hs:8:28: error:
-    • Couldn't match kind ‘* -> *’ with ‘*’
-      When matching types
-        a0 :: *
-        Maybe :: * -> *
-      Expected type: Proxy Maybe
-        Actual type: Proxy a0
-    • In the expression: fst y :: Proxy Maybe
-      In the expression: (fst y :: Proxy Int, fst y :: Proxy Maybe)
-      In an equation for ‘f’:
-          f x
-            = (fst y :: Proxy Int, fst y :: Proxy Maybe)
-            where
-                y :: (Proxy a, b)
-                y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 593b7787a1..0f7129020e 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -26,7 +26,6 @@ test('T14066d', normal, compile_fail, [''])
 test('T14066e', normal, compile_fail, [''])
 test('T14066f', normal, compile_fail, [''])
 test('T14066g', normal, compile_fail, [''])
-test('T14066h', normal, compile_fail, [''])
 test('T14845_fail1', normal, compile_fail, [''])
 test('T14845_fail2', normal, compile_fail, [''])
 test('InferDependency', normal, compile_fail, [''])