Kill derived constraints

Co-authored by: Sam Derbyshire

Previously, GHC had three flavours of constraint:
Wanted, Given, and Derived. This removes Derived constraints.

Though serving a number of purposes, the most important role
of Derived constraints was to enable better error messages.
This job has been taken over by the new RewriterSets, as explained
in Note [Wanteds rewrite wanteds] in GHC.Tc.Types.Constraint.

Other knock-on effects:
 - Various new Notes as I learned about under-described bits of GHC

 - A reshuffling around the AST for implicit-parameter bindings,
   with better integration with TTG.

 - Various improvements around fundeps. These were caused by the
   fact that, previously, fundep constraints were all Derived,
   and Derived constraints would get dropped. Thus, an unsolved
   Derived didn't stop compilation. Without Derived, this is no
   longer possible, and so we have to be considerably more careful
   around fundeps.

 - A nice little refactoring in GHC.Tc.Errors to center the work
   on a new datatype called ErrorItem. Constraints are converted
   into ErrorItems at the start of processing, and this allows for
   a little preprocessing before the main classification.

 - This commit also cleans up the behavior in generalisation around
   functional dependencies. Now, if a variable is determined by
   functional dependencies, it will not be quantified. This change
   is user facing, but it should trim down GHC's strange behavior
   around fundeps.

 - Previously, reportWanteds did quite a bit of work, even on an empty
   WantedConstraints. This commit adds a fast path.

 - Now, GHC will unconditionally re-simplify constraints during
   quantification. See Note [Unconditionally resimplify constraints when
   quantifying], in GHC.Tc.Solver.

Close #18398.
Close #18406.
Solve the fundep-related non-confluence in #18851.
Close #19131.
Close #19137.
Close #20922.
Close #20668.
Close #19665.

-------------------------
Metric Decrease:
    LargeRecord
    T9872b
    T9872b_defer
    T9872d
    TcPlugin_RewritePerf
-------------------------

64 files changed, 749 insertions, 191 deletions

diff --git a/testsuite/tests/typecheck/should_fail/AmbigFDs.hs b/testsuite/tests/typecheck/should_fail/AmbigFDs.hs
new file mode 100644
index 0000000000..d9ebdbbb7c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/AmbigFDs.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE FunctionalDependencies, NoPolyKinds #-}
+-- NB: No AllowAmbiguousTypes. The type isn't ambiguous, because of the fundeps.
+-- But it is confusing, because we don't know whether b1 and b2 are really the
+-- same or not.
+
+module AmbigFDs where
+
+class C a b | a -> b
+
+foo :: (C a b1, C a b2) => a -> Int
+foo = undefined
diff --git a/testsuite/tests/typecheck/should_fail/AmbigFDs.stderr b/testsuite/tests/typecheck/should_fail/AmbigFDs.stderr
new file mode 100644
index 0000000000..c95578268e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/AmbigFDs.stderr
@@ -0,0 +1,23 @@
+
+AmbigFDs.hs:10:8: error:
+    • Couldn't match type ‘b1’ with ‘b2’
+        arising from a functional dependency between constraints:
+          ‘C a b2’
+            arising from a type ambiguity check for
+            the type signature for ‘foo’ at AmbigFDs.hs:10:8-35
+          ‘C a b1’
+            arising from the type signature for:
+                           foo :: forall a b1 b2.
+                                  (C a b1, C a b2) =>
+                                  a -> Int at AmbigFDs.hs:10:8-35
+      ‘b1’ is a rigid type variable bound by
+        the type signature for:
+          foo :: forall a b1 b2. (C a b1, C a b2) => a -> Int
+        at AmbigFDs.hs:10:8-35
+      ‘b2’ is a rigid type variable bound by
+        the type signature for:
+          foo :: forall a b1 b2. (C a b1, C a b2) => a -> Int
+        at AmbigFDs.hs:10:8-35
+    • In the ambiguity check for ‘foo’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      In the type signature: foo :: (C a b1, C a b2) => a -> Int
diff --git a/testsuite/tests/typecheck/should_fail/FD1.hs b/testsuite/tests/typecheck/should_fail/FD1.hs
new file mode 100644
index 0000000000..39c45bfdb4
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/FD1.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
+{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
+
+-- #1781
+-- This one should really succeed, because 'plus' can only
+-- be called with a = Int->Int, but the old fundep story
+-- certainly made it fail, and so that's what we expect for now
+-- We may become more liberal later
+
+module ShouldCompile where
+
+class E a b | a -> b, b -> a
+instance E a a
+
+plus :: (E a (Int -> Int)) => Int -> a
+plus x y = x + y
diff --git a/testsuite/tests/typecheck/should_fail/FD1.stderr b/testsuite/tests/typecheck/should_fail/FD1.stderr
new file mode 100644
index 0000000000..64a01c43e1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/FD1.stderr
@@ -0,0 +1,10 @@
+
+FD1.hs:16:1: error:
+    • Couldn't match expected type ‘a’ with actual type ‘Int -> Int’
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          plus :: forall a. E a (Int -> Int) => Int -> a
+        at FD1.hs:15:1-38
+    • The equation(s) for ‘plus’ have two value arguments,
+        but its type ‘Int -> a’ has only one
+    • Relevant bindings include plus :: Int -> a (bound at FD1.hs:16:1)
diff --git a/testsuite/tests/typecheck/should_fail/FD2.hs b/testsuite/tests/typecheck/should_fail/FD2.hs
new file mode 100644
index 0000000000..f8732c846d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/FD2.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
+{-# LANGUAGE ScopedTypeVariables, FlexibleContexts #-}
+
+-- #1783
+-- Like #1781 you could argue that this one should succeed
+-- but we stick with the old behaviour for now.  When we do
+-- fundeps properly it'll probably start to work
+
+module ShouldCompile where
+
+import Prelude hiding (foldr, foldr1)
+
+import Data.Maybe
+
+class Elem a e | a -> e
+
+class Foldable a where
+  foldr :: Elem a e => (e -> b -> b) -> b -> a -> b
+
+--  foldr1 :: forall e. Elem a e => (e -> e -> e) -> a -> e  -- WORKS!
+  foldr1 :: Elem a e => (e -> e -> e) -> a -> e
+  foldr1 f xs = fromMaybe (error "foldr1: empty structure")
+                  (foldr mf Nothing xs)
+     where mf :: Elem a e => (e -> Maybe e -> Maybe e)
+           mf x Nothing  = Just x
+           mf x (Just y) = Just (f x y)
diff --git a/testsuite/tests/typecheck/should_fail/FD2.stderr b/testsuite/tests/typecheck/should_fail/FD2.stderr
new file mode 100644
index 0000000000..a5462aa94e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/FD2.stderr
@@ -0,0 +1,20 @@
+
+FD2.hs:26:34: error:
+    • Couldn't match expected type ‘e1’ with actual type ‘e’
+      ‘e1’ is a rigid type variable bound by
+        the type signature for:
+          mf :: forall e1. Elem a e1 => e1 -> Maybe e1 -> Maybe e1
+        at FD2.hs:24:12-54
+      ‘e’ is a rigid type variable bound by
+        the type signature for:
+          foldr1 :: forall e. Elem a e => (e -> e -> e) -> a -> e
+        at FD2.hs:21:13-47
+    • In the first argument of ‘Just’, namely ‘(f x y)’
+      In the expression: Just (f x y)
+      In an equation for ‘mf’: mf x (Just y) = Just (f x y)
+    • Relevant bindings include
+        y :: e1 (bound at FD2.hs:26:23)
+        x :: e1 (bound at FD2.hs:26:15)
+        mf :: e1 -> Maybe e1 -> Maybe e1 (bound at FD2.hs:25:12)
+        f :: e -> e -> e (bound at FD2.hs:22:10)
+        foldr1 :: (e -> e -> e) -> a -> e (bound at FD2.hs:22:3)
diff --git a/testsuite/tests/typecheck/should_fail/FD3.hs b/testsuite/tests/typecheck/should_fail/FD3.hs
new file mode 100644
index 0000000000..475e379c10
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/FD3.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances #-}
+
+-- #1795
+
+module ShouldCompile where
+
+data A a = A
+
+class MkA a b | a -> b where
+   mkA :: a -> A b
+
+instance MkA a a where
+
+translate :: (String, a) -> A a
+translate a = mkA a
+
+{- From the call to mkA
+
+[W] MkA alpha beta
+[W] alpha ~ (String,a)
+[W] A beta ~ A a
+
+==>  beta:=a, alpha:=(String,a)
+-}
diff --git a/testsuite/tests/typecheck/should_fail/FD3.stderr b/testsuite/tests/typecheck/should_fail/FD3.stderr
new file mode 100644
index 0000000000..d7ac728b6c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/FD3.stderr
@@ -0,0 +1,15 @@
+
+FD3.hs:15:15: error:
+    • Couldn't match type ‘a’ with ‘(String, a)’
+        arising from a functional dependency between:
+          constraint ‘MkA (String, a) a’ arising from a use of ‘mkA’
+          instance ‘MkA a1 a1’ at FD3.hs:12:10-16
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          translate :: forall a. (String, a) -> A a
+        at FD3.hs:14:1-31
+    • In the expression: mkA a
+      In an equation for ‘translate’: translate a = mkA a
+    • Relevant bindings include
+        a :: (String, a) (bound at FD3.hs:15:11)
+        translate :: (String, a) -> A a (bound at FD3.hs:15:1)
diff --git a/testsuite/tests/typecheck/should_fail/FunDepOrigin1b.hs b/testsuite/tests/typecheck/should_fail/FunDepOrigin1b.hs
new file mode 100644
index 0000000000..dfd807d463
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/FunDepOrigin1b.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts #-}
+
+module FunDepOrigin1b where
+
+class C a b | a -> b where
+  op :: a -> b -> b
+
+-- foo :: (C Bool (Maybe a), C Bool [b]) => x -> (Maybe a, [b])
+foo _ = (op True Nothing, op False [])
+
+-- See Note [Suppressing confusing errors] in GHC.Tc.Errors
diff --git a/testsuite/tests/typecheck/should_fail/FunDepOrigin1b.stderr b/testsuite/tests/typecheck/should_fail/FunDepOrigin1b.stderr
new file mode 100644
index 0000000000..a67bf17955
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/FunDepOrigin1b.stderr
@@ -0,0 +1,12 @@
+
+FunDepOrigin1b.hs:9:10: error:
+    • No instance for (C Bool (Maybe a0)) arising from a use of ‘op’
+    • In the expression: op True Nothing
+      In the expression: (op True Nothing, op False [])
+      In an equation for ‘foo’: foo _ = (op True Nothing, op False [])
+
+FunDepOrigin1b.hs:9:27: error:
+    • No instance for (C Bool [a1]) arising from a use of ‘op’
+    • In the expression: op False []
+      In the expression: (op True Nothing, op False [])
+      In an equation for ‘foo’: foo _ = (op True Nothing, op False [])
diff --git a/testsuite/tests/typecheck/should_fail/T11947a.stderr b/testsuite/tests/typecheck/should_fail/T11947a.stderr
index 9ca1da0ee0..c63c745e44 100644
--- a/testsuite/tests/typecheck/should_fail/T11947a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T11947a.stderr
@@ -6,6 +6,9 @@ T11947a.hs:4:19: error:
                    theFloatDigits :: forall a. RealFloat a => Int
         at T11947a.hs:4:19-46
       The type variable ‘a0’ is ambiguous
+      Potentially matching instances:
+        instance RealFloat Double -- Defined in ‘GHC.Float’
+        instance RealFloat Float -- Defined in ‘GHC.Float’
     • In the ambiguity check for ‘theFloatDigits’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       In the type signature:
diff --git a/testsuite/tests/typecheck/should_fail/T14325.stderr b/testsuite/tests/typecheck/should_fail/T14325.stderr
index 1508c4a689..6cf71b5e08 100644
--- a/testsuite/tests/typecheck/should_fail/T14325.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14325.stderr
@@ -1,9 +1,14 @@
 
 T14325.hs:11:9: error:
-    • Could not deduce (C b (f b)) arising from a use of ‘foo’
-      from the context: C (f b) b
-        bound by the type signature for:
-                   hm3 :: forall (f :: * -> *) b. C (f b) b => b -> f b
+    • Couldn't match type ‘b’ with ‘f b’
+        arising from a superclass required to satisfy ‘C b (f b)’,
+        arising from a use of ‘foo’
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          hm3 :: forall (f :: * -> *) b. C (f b) b => b -> f b
         at T14325.hs:10:1-28
     • In the expression: foo x
       In an equation for ‘hm3’: hm3 x = foo x
+    • Relevant bindings include
+        x :: b (bound at T14325.hs:11:5)
+        hm3 :: b -> f b (bound at T14325.hs:11:1)
diff --git a/testsuite/tests/typecheck/should_fail/T15648.stderr b/testsuite/tests/typecheck/should_fail/T15648.stderr
index 7de4bc9e18..acfcaf8d1c 100644
--- a/testsuite/tests/typecheck/should_fail/T15648.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15648.stderr
@@ -11,13 +11,20 @@ T15648.hs:23:21: error:
         legitToJank :: LegitEquality a b -> JankyEquality a b
           (bound at T15648.hs:23:1)
 
-T15648.hs:30:10: error:
-    • Couldn't match expected type: (a GHC.Prim.~# b)
-                                    -> b GHC.Prim.~# a
-                  with actual type: b GHC.Prim.~# a
-    • In the expression: unJank $ legitToJank $ mkLegit @b @a
-      In an equation for ‘ueqSym’:
-          ueqSym = unJank $ legitToJank $ mkLegit @b @a
+T15648.hs:30:33: error:
+    • Couldn't match expected type ‘a’ with actual type ‘b’
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          ueqSym :: forall a b. (a GHC.Prim.~# b) -> b GHC.Prim.~# a
+        at T15648.hs:(28,1)-(29,32)
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          ueqSym :: forall a b. (a GHC.Prim.~# b) -> b GHC.Prim.~# a
+        at T15648.hs:(28,1)-(29,32)
+    • In the second argument of ‘($)’, namely ‘mkLegit @b @a’
+      In the second argument of ‘($)’, namely
+        ‘legitToJank $ mkLegit @b @a’
+      In the expression: unJank $ legitToJank $ mkLegit @b @a
     • Relevant bindings include
         ueqSym :: (a GHC.Prim.~# b) -> b GHC.Prim.~# a
           (bound at T15648.hs:30:1)
diff --git a/testsuite/tests/typecheck/should_fail/T15767.stderr b/testsuite/tests/typecheck/should_fail/T15767.stderr
index 2c20dd200f..9724eca0da 100644
--- a/testsuite/tests/typecheck/should_fail/T15767.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15767.stderr
@@ -1,6 +1,6 @@
 
 T15767.hs:7:5: error:
-    • No instance for (C () b) arising from a use of ‘x’
+    • No instance for (C () b0) arising from a use of ‘x’
     • In the expression: x
       In an equation for ‘y’:
           y = x
diff --git a/testsuite/tests/typecheck/should_fail/T16204c.stderr b/testsuite/tests/typecheck/should_fail/T16204c.stderr
index 6ad532a4ea..731a873423 100644
--- a/testsuite/tests/typecheck/should_fail/T16204c.stderr
+++ b/testsuite/tests/typecheck/should_fail/T16204c.stderr
@@ -1,12 +1,8 @@
 
 T16204c.hs:16:8: error:
-    • Couldn't match kind ‘Rep’ with ‘*’
-      When matching types
-        a0 :: Rep
-        a :: *
-      Expected: Sing a
-        Actual: Sing a0
+    • Couldn't match type ‘Rep’ with ‘*’
+      Expected: Sing @(*) a
+        Actual: Sing @Rep a0
     • In the first argument of ‘id’, namely ‘sTo’
       In the expression: id sTo
       In an equation for ‘x’: x = id sTo
-    • Relevant bindings include x :: Sing a (bound at T16204c.hs:16:1)
diff --git a/testsuite/tests/typecheck/should_fail/T16512a.stderr b/testsuite/tests/typecheck/should_fail/T16512a.stderr
index a799bcca21..a4d979948f 100644
--- a/testsuite/tests/typecheck/should_fail/T16512a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T16512a.stderr
@@ -1,9 +1,14 @@
 
 T16512a.hs:41:25: error:
-    • Couldn't match type: ListVariadic as (a -> b)
-                     with: a -> ListVariadic as b
+    • Couldn't match type ‘as’ with ‘a : as’
       Expected: AST (ListVariadic (a : as) b)
         Actual: AST (ListVariadic as (a -> b))
+      ‘as’ is a rigid type variable bound by
+        a pattern with constructor:
+          AnApplication :: forall (as :: [*]) b.
+                           AST (ListVariadic as b) -> ASTs as -> AnApplication b,
+        in a case alternative
+        at T16512a.hs:40:9-26
     • In the first argument of ‘AnApplication’, namely ‘g’
       In the expression: AnApplication g (a `ConsAST` as)
       In a case alternative:
@@ -13,4 +18,3 @@ T16512a.hs:41:25: error:
         g :: AST (ListVariadic as (a -> b)) (bound at T16512a.hs:40:23)
         a :: AST a (bound at T16512a.hs:38:15)
         f :: AST (a -> b) (bound at T16512a.hs:38:10)
-        unapply :: AST b -> AnApplication b (bound at T16512a.hs:38:1)
diff --git a/testsuite/tests/typecheck/should_fail/T16946.hs b/testsuite/tests/typecheck/should_fail/T16946.hs
index e824f7cec8..7144c0e1b2 100644
--- a/testsuite/tests/typecheck/should_fail/T16946.hs
+++ b/testsuite/tests/typecheck/should_fail/T16946.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE RankNTypes, TypeFamilies, PolyKinds, FunctionalDependencies #-}
+{-# LANGUAGE AllowAmbiguousTypes, RankNTypes, TypeFamilies, PolyKinds, FunctionalDependencies #-}
 module T16946 where
 
 import Data.Kind
diff --git a/testsuite/tests/typecheck/should_fail/T17139.stderr b/testsuite/tests/typecheck/should_fail/T17139.stderr
index 7da4635a61..d89b166fdc 100644
--- a/testsuite/tests/typecheck/should_fail/T17139.stderr
+++ b/testsuite/tests/typecheck/should_fail/T17139.stderr
@@ -1,21 +1,4 @@
 
-T17139.hs:15:10: error:
-    • Couldn't match type ‘f’ with ‘(->) a’
-      Expected: TypeFam f (a -> b)
-        Actual: (a -> a) -> f a -> TypeFam f b0
-      ‘f’ is a rigid type variable bound by
-        the type signature for:
-          lift :: forall a b (f :: * -> *). (a -> b) -> TypeFam f (a -> b)
-        at T17139.hs:14:1-38
-    • The lambda expression ‘\ x -> _ (f <*> x)’
-      has one value argument,
-        but its type ‘TypeFam f (a -> b)’ has none
-      In the expression: \ x -> _ (f <*> x)
-      In an equation for ‘lift’: lift f = \ x -> _ (f <*> x)
-    • Relevant bindings include
-        f :: a -> b (bound at T17139.hs:15:6)
-        lift :: (a -> b) -> TypeFam f (a -> b) (bound at T17139.hs:15:1)
-
 T17139.hs:15:16: error:
     • Found hole: _ :: (a -> b0) -> f a -> TypeFam f b0
       Where: ‘b0’ is an ambiguous type variable
diff --git a/testsuite/tests/typecheck/should_fail/T18398.hs b/testsuite/tests/typecheck/should_fail/T18398.hs
new file mode 100644
index 0000000000..80b21c715f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18398.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
+             ExistentialQuantification, GADTSyntax, FlexibleContexts #-}
+{-# OPTIONS_GHC -ddump-types #-}
+
+module FloatFDs2 where
+
+class C a b | a -> b where
+  meth :: a -> b -> ()
+
+data Ex where
+  MkEx :: a -> Ex
+
+f x = (\y -> case x of MkEx _ -> meth x y, \z -> case x of MkEx _ -> meth x z)
diff --git a/testsuite/tests/typecheck/should_fail/T18398.stderr b/testsuite/tests/typecheck/should_fail/T18398.stderr
new file mode 100644
index 0000000000..00a1f14804
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18398.stderr
@@ -0,0 +1,12 @@
+
+T18398.hs:13:34: error:
+    • No instance for (C Ex p0) arising from a use of ‘meth’
+    • In the expression: meth x y
+      In a case alternative: MkEx _ -> meth x y
+      In the expression: case x of MkEx _ -> meth x y
+
+T18398.hs:13:70: error:
+    • No instance for (C Ex p0) arising from a use of ‘meth’
+    • In the expression: meth x z
+      In a case alternative: MkEx _ -> meth x z
+      In the expression: case x of MkEx _ -> meth x z
diff --git a/testsuite/tests/typecheck/should_fail/T18406.hs b/testsuite/tests/typecheck/should_fail/T18406.hs
new file mode 100644
index 0000000000..7ebcc278fc
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18406.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts #-}
+
+module Bug where
+
+class C a b | a -> b where
+  op :: a -> b -> ()
+
+f x = op True x
+
+{- We could accept this, quantifying over a C Bool b constraint. But this is a
+bit silly, actually, because the b is fixed by the fundep. We don't know what
+it's fix to, but it's definitely fixed. So, in the end, we choose not to
+Henry Ford polymorphism ("it works for any b as long as b is ???") and not
+to quantify. Users can quantify manually if they want.
+-}
diff --git a/testsuite/tests/typecheck/should_fail/T18406.stderr b/testsuite/tests/typecheck/should_fail/T18406.stderr
new file mode 100644
index 0000000000..aa786df13e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18406.stderr
@@ -0,0 +1,5 @@
+
+T18406.hs:8:7: error:
+    • No instance for (C Bool b0) arising from a use of ‘op’
+    • In the expression: op True x
+      In an equation for ‘f’: f x = op True x
diff --git a/testsuite/tests/typecheck/should_fail/T18851.hs b/testsuite/tests/typecheck/should_fail/T18851.hs
new file mode 100644
index 0000000000..bba609a5ce
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18851.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE FunctionalDependencies, FlexibleInstances, UndecidableInstances,
+             ScopedTypeVariables, TypeFamilies, TypeApplications,
+             FlexibleContexts, AllowAmbiguousTypes, ExtendedDefaultRules #-}
+
+module T18851 where
+
+default (Int)
+
+type family C_FD a
+class C_FD a ~ b => C a b
+
+type instance C_FD Int = Bool -- just for Show (C_FD Int)
+instance C Int b => C Int b
+
+class IsInt int
+instance int ~ Int => IsInt int
+
+data A
+instance Show A where
+  show _ = "A"
+data B
+instance Show B where
+  show _ = "B"
+
+f :: forall a b c int
+  .  ( Show c, Num int
+     , C int a, C int b, C int c
+     -- , c ~ C_FD int -- add this to get rid of ambiguity error
+     )
+  => String
+f = show (undefined :: c)
+
+-- blows up at run time once type checks
+g :: String
+g = f @A @B
diff --git a/testsuite/tests/typecheck/should_fail/T18851.stderr b/testsuite/tests/typecheck/should_fail/T18851.stderr
new file mode 100644
index 0000000000..613435041c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18851.stderr
@@ -0,0 +1,7 @@
+
+T18851.hs:35:5: error:
+    • Couldn't match type ‘B’ with ‘A’
+        arising from a superclass required to satisfy ‘C int0 A’,
+        arising from a use of ‘f’
+    • In the expression: f @A @B
+      In an equation for ‘g’: g = f @A @B
diff --git a/testsuite/tests/typecheck/should_fail/T18851b.hs b/testsuite/tests/typecheck/should_fail/T18851b.hs
new file mode 100644
index 0000000000..0618c792ce
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18851b.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE FunctionalDependencies, FlexibleInstances, UndecidableInstances,
+             ScopedTypeVariables, TypeFamilies, TypeApplications, NoPolyKinds,
+             FlexibleContexts, AllowAmbiguousTypes #-}
+
+module T18851b where
+
+-- NB: -XNoPolyKinds is important. Otherwise, we get IsInt :: forall k. k -> Constraint,
+-- but its instance specializes k to Type. The [W] IsInt int doesn't match the instance
+-- then, and so we get no int ~ Int equality.
+
+class C a b | a -> b
+instance C Int b => C Int b
+
+class IsInt int
+instance int ~ Int => IsInt int
+
+data A
+instance Show A where
+  show _ = "A"
+data B
+instance Show B where
+  show _ = "B"
+
+f :: forall a b c int. (Show a, Show b, Show c, C int a, C int b, C int c, IsInt int) => String
+f = show (undefined :: c)
+
+g = f @A @B
diff --git a/testsuite/tests/typecheck/should_fail/T18851b.stderr b/testsuite/tests/typecheck/should_fail/T18851b.stderr
new file mode 100644
index 0000000000..3b8dd1d801
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18851b.stderr
@@ -0,0 +1,8 @@
+
+T18851b.hs:27:5: error:
+    • Couldn't match type ‘A’ with ‘B’
+        arising from a functional dependency between constraints:
+          ‘C Int B’ arising from a use of ‘f’ at T18851b.hs:27:5
+          ‘C Int A’ arising from a use of ‘f’ at T18851b.hs:27:5
+    • In the expression: f @A @B
+      In an equation for ‘g’: g = f @A @B
diff --git a/testsuite/tests/typecheck/should_fail/T18851c.hs b/testsuite/tests/typecheck/should_fail/T18851c.hs
new file mode 100644
index 0000000000..f633d4674d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18851c.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE DataKinds                #-}
+{-# LANGUAGE GADTs                    #-}
+{-# LANGUAGE PolyKinds                #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilyDependencies   #-}
+{-# LANGUAGE TypeOperators            #-}
+
+-- from https://gitlab.haskell.org/ghc/ghc/-/merge_requests/5899#note_407871
+
+module T18851c where
+
+-- base
+import           Data.Kind (Type)
+
+data Nat
+type Plus1 :: Nat -> Nat
+type family Plus1 n = r | r -> n
+
+data V (n :: Nat) = V
+
+data VSucc n where
+  VSucc :: V n -> VSucc (Plus1 n)
+
+foo :: VSucc n -> VSucc n -> VSucc n
+foo (VSucc _) (VSucc _) = VSucc V
diff --git a/testsuite/tests/typecheck/should_fail/T18851c.stderr b/testsuite/tests/typecheck/should_fail/T18851c.stderr
new file mode 100644
index 0000000000..4360fb16d2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18851c.stderr
@@ -0,0 +1,33 @@
+
+T18851c.hs:25:27: error:
+    • Could not deduce (n2 ~ n1)
+        arising from reasoning about an injective type family using constraints:
+          ‘Plus1 n2 ~ n’
+            arising from a type equality
+              VSucc (Plus1 n2) ~ VSucc n at T18851c.hs:25:27-33
+          ‘Plus1 n1 ~ n’
+            arising from a pattern with constructor:
+                           VSucc :: forall (n :: Nat). V n -> VSucc (Plus1 n),
+                         in an equation for ‘foo’ at T18851c.hs:25:6-12
+      from the context: n ~ Plus1 n1
+        bound by a pattern with constructor:
+                   VSucc :: forall (n :: Nat). V n -> VSucc (Plus1 n),
+                 in an equation for ‘foo’
+        at T18851c.hs:25:6-12
+      or from: n ~ Plus1 n2
+        bound by a pattern with constructor:
+                   VSucc :: forall (n :: Nat). V n -> VSucc (Plus1 n),
+                 in an equation for ‘foo’
+        at T18851c.hs:25:16-22
+      ‘n2’ is a rigid type variable bound by
+        a pattern with constructor:
+          VSucc :: forall (n :: Nat). V n -> VSucc (Plus1 n),
+        in an equation for ‘foo’
+        at T18851c.hs:25:16-22
+      ‘n1’ is a rigid type variable bound by
+        a pattern with constructor:
+          VSucc :: forall (n :: Nat). V n -> VSucc (Plus1 n),
+        in an equation for ‘foo’
+        at T18851c.hs:25:6-12
+    • In the expression: VSucc V
+      In an equation for ‘foo’: foo (VSucc _) (VSucc _) = VSucc V
diff --git a/testsuite/tests/typecheck/should_fail/T1897a.hs b/testsuite/tests/typecheck/should_fail/T1897a.hs
index e4ec66afd0..435b985e6f 100644
--- a/testsuite/tests/typecheck/should_fail/T1897a.hs
+++ b/testsuite/tests/typecheck/should_fail/T1897a.hs
@@ -7,5 +7,5 @@ class Wob a b where
    from :: b -> a
 
 foo x = [x, to (from x)]
--- Ambiguous type:  Wob a b => b -> [b]
+-- Ambiguous type:  Wob a0 b => b -> [b]
 -- Should be rejected
diff --git a/testsuite/tests/typecheck/should_fail/T1899.stderr b/testsuite/tests/typecheck/should_fail/T1899.stderr
index ceb5f69c66..451a4444e1 100644
--- a/testsuite/tests/typecheck/should_fail/T1899.stderr
+++ b/testsuite/tests/typecheck/should_fail/T1899.stderr
@@ -1,15 +1,14 @@
 
-T1899.hs:15:26: error:
+T1899.hs:12:29: error:
     • Couldn't match expected type ‘a’
                   with actual type ‘Proposition a0’
       ‘a’ is a rigid type variable bound by
         the type signature for:
           transRHS :: forall a. [a] -> Int -> Constraint a
         at T1899.hs:9:2-39
-    • In the first argument of ‘Prop’, namely ‘(Auxiliary varSet)’
-      In the expression: Prop (Auxiliary varSet)
-      In the expression:
-        [Prop (Auxiliary varSet), Prop (Auxiliary varSet)]
+    • In the first argument of ‘Prop’, namely ‘(Auxiliary undefined)’
+      In the expression: Prop (Auxiliary undefined)
+      In the expression: [Prop (Auxiliary undefined)]
     • Relevant bindings include
         varSet :: [a] (bound at T1899.hs:10:11)
         transRHS :: [a] -> Int -> Constraint a (bound at T1899.hs:10:2)
diff --git a/testsuite/tests/typecheck/should_fail/T19977a.hs b/testsuite/tests/typecheck/should_fail/T19977a.hs
new file mode 100644
index 0000000000..e9e3a1dce1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19977a.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE Haskell2010 #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module T19977a where
+
+-- See Note [Inferring principal types] in Ghc.Tc.Solver
+
+f x = show [x]
+
+g :: Show [a] => a -> String
+g x = f x
diff --git a/testsuite/tests/typecheck/should_fail/T19977a.stderr b/testsuite/tests/typecheck/should_fail/T19977a.stderr
new file mode 100644
index 0000000000..296a8c90a6
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19977a.stderr
@@ -0,0 +1,13 @@
+
+T19977a.hs:11:7: error:
+    • Could not deduce (Show a) arising from a use of ‘f’
+      from the context: Show [a]
+        bound by the type signature for:
+                   g :: forall a. Show [a] => a -> String
+        at T19977a.hs:10:1-28
+      Possible fix:
+        add (Show a) to the context of
+          the type signature for:
+            g :: forall a. Show [a] => a -> String
+    • In the expression: f x
+      In an equation for ‘g’: g x = f x
diff --git a/testsuite/tests/typecheck/should_fail/T19977b.hs b/testsuite/tests/typecheck/should_fail/T19977b.hs
new file mode 100644
index 0000000000..6f7bf0f033
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19977b.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE Haskell2010 #-}
+{-# LANGUAGE
+  FlexibleContexts,
+  FlexibleInstances,
+  UndecidableInstances,
+  NoMonomorphismRestriction
+#-}
+
+module T19977b where
+
+-- See Note [Inferring principal types] in Ghc.Tc.Solver
+
+class C a
+class D a where
+  d :: a
+instance C a => D a where
+  d = undefined
+h = d
+
+g :: D a => a
+g = h
diff --git a/testsuite/tests/typecheck/should_fail/T19977b.stderr b/testsuite/tests/typecheck/should_fail/T19977b.stderr
new file mode 100644
index 0000000000..988dc5faf6
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19977b.stderr
@@ -0,0 +1,13 @@
+
+T19977b.hs:21:5: error:
+    • Could not deduce (C a) arising from a use of ‘h’
+      from the context: D a
+        bound by the type signature for:
+                   g :: forall a. D a => a
+        at T19977b.hs:20:1-13
+      Possible fix:
+        add (C a) to the context of
+          the type signature for:
+            g :: forall a. D a => a
+    • In the expression: h
+      In an equation for ‘g’: g = h
diff --git a/testsuite/tests/typecheck/should_fail/T20064.hs b/testsuite/tests/typecheck/should_fail/T20064.hs
new file mode 100644
index 0000000000..2466081278
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20064.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE FlexibleContexts, FunctionalDependencies, NoMonomorphismRestriction #-}
+
+module T20064 where
+
+data AB a b = AB
+
+class C a b | a -> b where
+  meth :: AB a b -> b
+
+ab :: AB Int b
+ab = AB
+
+--foo :: C Int b => b
+foo = meth ab
diff --git a/testsuite/tests/typecheck/should_fail/T20064.stderr b/testsuite/tests/typecheck/should_fail/T20064.stderr
new file mode 100644
index 0000000000..eb63a9a283
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20064.stderr
@@ -0,0 +1,5 @@
+
+T20064.hs:14:7: error:
+    • No instance for (C Int b0) arising from a use of ‘meth’
+    • In the expression: meth ab
+      In an equation for ‘foo’: foo = meth ab
diff --git a/testsuite/tests/typecheck/should_fail/T5684.hs b/testsuite/tests/typecheck/should_fail/T5684.hs
index d1addf399f..61b72e4817 100644
--- a/testsuite/tests/typecheck/should_fail/T5684.hs
+++ b/testsuite/tests/typecheck/should_fail/T5684.hs
@@ -26,33 +26,6 @@ flop1 =  [ op False False    -- (3) Creates a functional dependency which kicks
                              -- which immediately becomes [S] B Bool alpha
          ]
 
-flop2 =  [ op False False
-         , op True undefined
-         , op 'c' undefined
-         ]
-
-
-flop3 =  [ op 'c' undefined
-         , op True undefined
-         , op False False
-         ]
-
-flop4 =  [ op 'c' undefined
-         , op False False
-         , op True undefined
-         ]
-
-
-flop5 =  [ op True undefined
-         , op 'c' undefined
-         , op False False
-         ]
-
-
-flop6 =  [ op True undefined
-         , op False False
-         , op 'c' undefined
-         ]
 
 
 {- Now, in HEAD we no longer have cached GivenSolved goals in the inerts and hence
diff --git a/testsuite/tests/typecheck/should_fail/T5684.stderr b/testsuite/tests/typecheck/should_fail/T5684.stderr
index ed2af704f4..854cd8b498 100644
--- a/testsuite/tests/typecheck/should_fail/T5684.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5684.stderr
@@ -8,89 +8,9 @@ T5684.hs:20:12: error:
           flop1 = [op False False, op 'c' undefined, op True undefined]
 
 T5684.hs:24:12: error:
-    • No instance for (B Char b5) arising from a use of ‘op’
+    • No instance for (B Char b0) arising from a use of ‘op’
     • In the expression: op 'c' undefined
       In the expression:
         [op False False, op 'c' undefined, op True undefined]
       In an equation for ‘flop1’:
           flop1 = [op False False, op 'c' undefined, op True undefined]
-
-T5684.hs:29:12: error:
-    • No instance for (A Bool) arising from a use of ‘op’
-    • In the expression: op False False
-      In the expression:
-        [op False False, op True undefined, op 'c' undefined]
-      In an equation for ‘flop2’:
-          flop2 = [op False False, op True undefined, op 'c' undefined]
-
-T5684.hs:31:12: error:
-    • No instance for (B Char b4) arising from a use of ‘op’
-    • In the expression: op 'c' undefined
-      In the expression:
-        [op False False, op True undefined, op 'c' undefined]
-      In an equation for ‘flop2’:
-          flop2 = [op False False, op True undefined, op 'c' undefined]
-
-T5684.hs:35:12: error:
-    • No instance for (B Char b3) arising from a use of ‘op’
-    • In the expression: op 'c' undefined
-      In the expression:
-        [op 'c' undefined, op True undefined, op False False]
-      In an equation for ‘flop3’:
-          flop3 = [op 'c' undefined, op True undefined, op False False]
-
-T5684.hs:37:12: error:
-    • No instance for (A Bool) arising from a use of ‘op’
-    • In the expression: op False False
-      In the expression:
-        [op 'c' undefined, op True undefined, op False False]
-      In an equation for ‘flop3’:
-          flop3 = [op 'c' undefined, op True undefined, op False False]
-
-T5684.hs:40:12: error:
-    • No instance for (B Char b2) arising from a use of ‘op’
-    • In the expression: op 'c' undefined
-      In the expression:
-        [op 'c' undefined, op False False, op True undefined]
-      In an equation for ‘flop4’:
-          flop4 = [op 'c' undefined, op False False, op True undefined]
-
-T5684.hs:41:12: error:
-    • No instance for (A Bool) arising from a use of ‘op’
-    • In the expression: op False False
-      In the expression:
-        [op 'c' undefined, op False False, op True undefined]
-      In an equation for ‘flop4’:
-          flop4 = [op 'c' undefined, op False False, op True undefined]
-
-T5684.hs:47:12: error:
-    • No instance for (B Char b1) arising from a use of ‘op’
-    • In the expression: op 'c' undefined
-      In the expression:
-        [op True undefined, op 'c' undefined, op False False]
-      In an equation for ‘flop5’:
-          flop5 = [op True undefined, op 'c' undefined, op False False]
-
-T5684.hs:48:12: error:
-    • No instance for (A Bool) arising from a use of ‘op’
-    • In the expression: op False False
-      In the expression:
-        [op True undefined, op 'c' undefined, op False False]
-      In an equation for ‘flop5’:
-          flop5 = [op True undefined, op 'c' undefined, op False False]
-
-T5684.hs:53:12: error:
-    • No instance for (A Bool) arising from a use of ‘op’
-    • In the expression: op False False
-      In the expression:
-        [op True undefined, op False False, op 'c' undefined]
-      In an equation for ‘flop6’:
-          flop6 = [op True undefined, op False False, op 'c' undefined]
-
-T5684.hs:54:12: error:
-    • No instance for (B Char b0) arising from a use of ‘op’
-    • In the expression: op 'c' undefined
-      In the expression:
-        [op True undefined, op False False, op 'c' undefined]
-      In an equation for ‘flop6’:
-          flop6 = [op True undefined, op False False, op 'c' undefined]
diff --git a/testsuite/tests/typecheck/should_fail/T5684b.hs b/testsuite/tests/typecheck/should_fail/T5684b.hs
new file mode 100644
index 0000000000..37d3acaa35
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T5684b.hs
@@ -0,0 +1,15 @@
+{-# OPTIONS -XFunctionalDependencies -XUndecidableInstances -XFlexibleInstances #-}
+
+module T5684b where
+
+class B a b | a -> b where
+  op :: a -> b -> ()
+
+class A a | -> a
+
+instance A b => B Bool b
+
+flop2 =  [ op False False
+         , op True undefined
+         , op 'c' undefined
+         ]
diff --git a/testsuite/tests/typecheck/should_fail/T5684b.stderr b/testsuite/tests/typecheck/should_fail/T5684b.stderr
new file mode 100644
index 0000000000..68c6e38b5f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T5684b.stderr
@@ -0,0 +1,16 @@
+
+T5684b.hs:12:12: error:
+    • No instance for (A Bool) arising from a use of ‘op’
+    • In the expression: op False False
+      In the expression:
+        [op False False, op True undefined, op 'c' undefined]
+      In an equation for ‘flop2’:
+          flop2 = [op False False, op True undefined, op 'c' undefined]
+
+T5684b.hs:14:12: error:
+    • No instance for (B Char b0) arising from a use of ‘op’
+    • In the expression: op 'c' undefined
+      In the expression:
+        [op False False, op True undefined, op 'c' undefined]
+      In an equation for ‘flop2’:
+          flop2 = [op False False, op True undefined, op 'c' undefined]
diff --git a/testsuite/tests/typecheck/should_fail/T5684c.hs b/testsuite/tests/typecheck/should_fail/T5684c.hs
new file mode 100644
index 0000000000..e176266fdc
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T5684c.hs
@@ -0,0 +1,15 @@
+{-# OPTIONS -XFunctionalDependencies -XUndecidableInstances -XFlexibleInstances #-}
+
+module T5684 where
+
+class B a b | a -> b where
+  op :: a -> b -> ()
+
+class A a | -> a
+
+instance A b => B Bool b
+
+flop3 =  [ op 'c' undefined
+         , op True undefined
+         , op False False
+         ]
diff --git a/testsuite/tests/typecheck/should_fail/T5684c.stderr b/testsuite/tests/typecheck/should_fail/T5684c.stderr
new file mode 100644
index 0000000000..69577811c4
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T5684c.stderr
@@ -0,0 +1,16 @@
+
+T5684c.hs:12:12: error:
+    • No instance for (B Char b0) arising from a use of ‘op’
+    • In the expression: op 'c' undefined
+      In the expression:
+        [op 'c' undefined, op True undefined, op False False]
+      In an equation for ‘flop3’:
+          flop3 = [op 'c' undefined, op True undefined, op False False]
+
+T5684c.hs:13:12: error:
+    • No instance for (A Bool) arising from a use of ‘op’
+    • In the expression: op True undefined
+      In the expression:
+        [op 'c' undefined, op True undefined, op False False]
+      In an equation for ‘flop3’:
+          flop3 = [op 'c' undefined, op True undefined, op False False]
diff --git a/testsuite/tests/typecheck/should_fail/T5684d.hs b/testsuite/tests/typecheck/should_fail/T5684d.hs
new file mode 100644
index 0000000000..f18ae68a74
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T5684d.hs
@@ -0,0 +1,15 @@
+{-# OPTIONS -XFunctionalDependencies -XUndecidableInstances -XFlexibleInstances #-}
+
+module T5684 where
+
+class B a b | a -> b where
+  op :: a -> b -> ()
+
+class A a | -> a
+
+instance A b => B Bool b
+
+flop4 =  [ op 'c' undefined
+         , op False False
+         , op True undefined
+         ]
diff --git a/testsuite/tests/typecheck/should_fail/T5684d.stderr b/testsuite/tests/typecheck/should_fail/T5684d.stderr
new file mode 100644
index 0000000000..eeec8c071b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T5684d.stderr
@@ -0,0 +1,16 @@
+
+T5684d.hs:12:12: error:
+    • No instance for (B Char b0) arising from a use of ‘op’
+    • In the expression: op 'c' undefined
+      In the expression:
+        [op 'c' undefined, op False False, op True undefined]
+      In an equation for ‘flop4’:
+          flop4 = [op 'c' undefined, op False False, op True undefined]
+
+T5684d.hs:13:12: error:
+    • No instance for (A Bool) arising from a use of ‘op’
+    • In the expression: op False False
+      In the expression:
+        [op 'c' undefined, op False False, op True undefined]
+      In an equation for ‘flop4’:
+          flop4 = [op 'c' undefined, op False False, op True undefined]
diff --git a/testsuite/tests/typecheck/should_fail/T5684e.hs b/testsuite/tests/typecheck/should_fail/T5684e.hs
new file mode 100644
index 0000000000..080c81cbbf
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T5684e.hs
@@ -0,0 +1,15 @@
+{-# OPTIONS -XFunctionalDependencies -XUndecidableInstances -XFlexibleInstances #-}
+
+module T5684 where
+
+class B a b | a -> b where
+  op :: a -> b -> ()
+
+class A a | -> a
+
+instance A b => B Bool b
+
+flop5 =  [ op True undefined
+         , op 'c' undefined
+         , op False False
+         ]
diff --git a/testsuite/tests/typecheck/should_fail/T5684e.stderr b/testsuite/tests/typecheck/should_fail/T5684e.stderr
new file mode 100644
index 0000000000..388f69720d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T5684e.stderr
@@ -0,0 +1,16 @@
+
+T5684e.hs:12:12: error:
+    • No instance for (A Bool) arising from a use of ‘op’
+    • In the expression: op True undefined
+      In the expression:
+        [op True undefined, op 'c' undefined, op False False]
+      In an equation for ‘flop5’:
+          flop5 = [op True undefined, op 'c' undefined, op False False]
+
+T5684e.hs:13:12: error:
+    • No instance for (B Char b0) arising from a use of ‘op’
+    • In the expression: op 'c' undefined
+      In the expression:
+        [op True undefined, op 'c' undefined, op False False]
+      In an equation for ‘flop5’:
+          flop5 = [op True undefined, op 'c' undefined, op False False]
diff --git a/testsuite/tests/typecheck/should_fail/T5684f.hs b/testsuite/tests/typecheck/should_fail/T5684f.hs
new file mode 100644
index 0000000000..beaa300798
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T5684f.hs
@@ -0,0 +1,15 @@
+{-# OPTIONS -XFunctionalDependencies -XUndecidableInstances -XFlexibleInstances #-}
+
+module T5684 where
+
+class B a b | a -> b where
+  op :: a -> b -> ()
+
+class A a | -> a
+
+instance A b => B Bool b
+
+flop6 =  [ op True undefined
+         , op False False
+         , op 'c' undefined
+         ]
diff --git a/testsuite/tests/typecheck/should_fail/T5684f.stderr b/testsuite/tests/typecheck/should_fail/T5684f.stderr
new file mode 100644
index 0000000000..e0b19c6a2b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T5684f.stderr
@@ -0,0 +1,16 @@
+
+T5684f.hs:12:12: error:
+    • No instance for (A Bool) arising from a use of ‘op’
+    • In the expression: op True undefined
+      In the expression:
+        [op True undefined, op False False, op 'c' undefined]
+      In an equation for ‘flop6’:
+          flop6 = [op True undefined, op False False, op 'c' undefined]
+
+T5684f.hs:14:12: error:
+    • No instance for (B Char b0) arising from a use of ‘op’
+    • In the expression: op 'c' undefined
+      In the expression:
+        [op True undefined, op False False, op 'c' undefined]
+      In an equation for ‘flop6’:
+          flop6 = [op True undefined, op False False, op 'c' undefined]
diff --git a/testsuite/tests/typecheck/should_fail/T7279.stderr b/testsuite/tests/typecheck/should_fail/T7279.stderr
index eed8878170..985d23804d 100644
--- a/testsuite/tests/typecheck/should_fail/T7279.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7279.stderr
@@ -6,6 +6,12 @@ T7279.hs:6:10: error:
                    forall a b. (Eq a, Show b) => Eq (T a)
         at T7279.hs:6:10-35
       The type variable ‘b0’ is ambiguous
+      Potentially matching instances:
+        instance Show Ordering -- Defined in ‘GHC.Show’
+        instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
+        ...plus 25 others
+        ...plus 12 instances involving out-of-scope types
+        (use -fprint-potential-instances to see them all)
     • In the ambiguity check for an instance declaration
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       In the instance declaration for ‘Eq (T a)’
diff --git a/testsuite/tests/typecheck/should_fail/T7696.hs b/testsuite/tests/typecheck/should_fail/T7696.hs
index f2dbdde4ee..70e17c94d5 100644
--- a/testsuite/tests/typecheck/should_fail/T7696.hs
+++ b/testsuite/tests/typecheck/should_fail/T7696.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE NoPolyKinds #-}
+
 module T7696 where
 
 f1 :: (m a, t m)
@@ -14,4 +16,4 @@ w :: * -> *
 
 m a ~ ()
 t m ~ w ()
--}
\ No newline at end of file
+-}
diff --git a/testsuite/tests/typecheck/should_fail/T7696.stderr b/testsuite/tests/typecheck/should_fail/T7696.stderr
index 945312094d..cc8885c372 100644
--- a/testsuite/tests/typecheck/should_fail/T7696.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7696.stderr
@@ -1,7 +1,12 @@
 
-T7696.hs:7:6: error:
-    • Couldn't match type ‘m0 a0’ with ‘()’
+T7696.hs:9:6: error:
+    • Couldn't match kind ‘*’ with ‘* -> *’
+      When matching types
+        t0 :: (* -> *) -> *
+        w :: * -> *
       Expected: ((), w ())
         Actual: (m0 a0, t0 m0)
     • In the expression: f1
       In an equation for ‘f2’: f2 = f1
+    • Relevant bindings include
+        f2 :: ((), w ()) (bound at T7696.hs:9:1)
diff --git a/testsuite/tests/typecheck/should_fail/T7748a.stderr b/testsuite/tests/typecheck/should_fail/T7748a.stderr
index ed9df46d15..c187edd01d 100644
--- a/testsuite/tests/typecheck/should_fail/T7748a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7748a.stderr
@@ -1,13 +1,13 @@
 
-T7748a.hs:16:24: error:
+T7748a.hs:14:24: error:
     • Couldn't match expected type ‘a’
                   with actual type ‘Maybe (Maybe (r -> ()))’
       ‘a’ is a rigid type variable bound by
         the type signature for:
           test :: forall a r. a -> r -> ()
         at T7748a.hs:11:1-20
-    • In the pattern: Just (Just p)
-      In a case alternative: Just (Just p) -> p
+    • In the pattern: Nothing
+      In a case alternative: Nothing -> const ()
       In the expression:
         case zd of
           Nothing -> const ()
diff --git a/testsuite/tests/typecheck/should_fail/T7869.stderr b/testsuite/tests/typecheck/should_fail/T7869.stderr
index c599b276d9..15e9cc4658 100644
--- a/testsuite/tests/typecheck/should_fail/T7869.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7869.stderr
@@ -1,18 +1,16 @@
 
 T7869.hs:3:12: error:
-    • Couldn't match type ‘a1’ with ‘a’
+    • Couldn't match type ‘b1’ with ‘b’
       Expected: [a1] -> b1
         Actual: [a] -> b
-      ‘a1’ is a rigid type variable bound by
+      ‘b1’ is a rigid type variable bound by
         an expression type signature:
           forall a1 b1. [a1] -> b1
         at T7869.hs:3:20-27
-      ‘a’ is a rigid type variable bound by
+      ‘b’ is a rigid type variable bound by
         the inferred type of f :: [a] -> b
         at T7869.hs:3:1-27
     • In the expression: f x
       In the expression: (\ x -> f x) :: [a] -> b
       In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b
-    • Relevant bindings include
-        x :: [a1] (bound at T7869.hs:3:7)
-        f :: [a] -> b (bound at T7869.hs:3:1)
+    • Relevant bindings include f :: [a] -> b (bound at T7869.hs:3:1)
diff --git a/testsuite/tests/typecheck/should_fail/T8603.stderr b/testsuite/tests/typecheck/should_fail/T8603.stderr
index e202ca2610..e4febcfb4c 100644
--- a/testsuite/tests/typecheck/should_fail/T8603.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8603.stderr
@@ -2,28 +2,14 @@
 T8603.hs:33:17: error:
     • Couldn't match kind ‘*’ with ‘* -> *’
       When matching types
-        (->) [a1] :: * -> *
+        m0 :: * -> *
         [a2] :: *
       Expected: [a2] -> StateT s RV a0
-        Actual: t0 ((->) [a1]) (StateT s RV a0)
+        Actual: t0 m0 (StateT s RV a0)
     • The function ‘lift’ is applied to two value arguments,
-        but its type ‘([a1] -> StateT s RV a0)
-                      -> t0 ((->) [a1]) (StateT s RV a0)’
+        but its type ‘m0 (StateT s RV a0) -> t0 m0 (StateT s RV a0)’
         has only one
       In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3]
       In the expression:
         do prize <- lift uniform [1, 2, ....]
            return False
-
-T8603.hs:33:22: error:
-    • Couldn't match type: RV a1
-                     with: StateT s RV a0
-      Expected: [a1] -> StateT s RV a0
-        Actual: [a1] -> RV a1
-    • In the first argument of ‘lift’, namely ‘uniform’
-      In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3]
-      In the expression:
-        do prize <- lift uniform [1, 2, ....]
-           return False
-    • Relevant bindings include
-        testRVState1 :: RVState s Bool (bound at T8603.hs:32:1)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index ff092df478..2febea800d 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -76,7 +76,7 @@ test('tcfail088', normal, compile_fail, [''])
 test('tcfail089', normal, compile_fail, [''])
 test('tcfail090', normal, compile_fail, [''])
 test('tcfail092', normal, compile_fail, [''])
-test('tcfail093', normal, compile, [''])
+test('tcfail093', normal, compile_fail, [''])
 test('tcfail094', normal, compile_fail, [''])
 test('tcfail095', normal, compile_fail, [''])
 test('tcfail096', normal, compile_fail, [''])
@@ -189,6 +189,9 @@ test('tcfail203a', normal, compile_fail, [''])
 test('tcfail204', normal, compile_fail, [''])
 test('tcfail206', normal, compile_fail, [''])
 
+test('tc168', normal, compile_fail, [''])
+test('tc168b', normal, compile_fail, [''])
+
 test('T1595', normal, compile_fail, [''])
 test('T1899', normal, compile_fail, [''])
 test('T2126', normal, compile_fail, [''])
@@ -266,6 +269,11 @@ test('T5570', normal, compile_fail, [''])
 test('T5691', normal, compile_fail, [''])
 test('T5689', normal, compile_fail, [''])
 test('T5684', normal, compile_fail, [''])
+test('T5684b', normal, compile_fail, [''])
+test('T5684c', normal, compile_fail, [''])
+test('T5684d', normal, compile_fail, [''])
+test('T5684e', normal, compile_fail, [''])
+test('T5684f', normal, compile_fail, [''])
 test('T5858', normal, compile_fail, [''])
 test('T5957', normal, compile_fail, [''])
 test('T6001', normal, compile_fail, [''])
@@ -550,6 +558,9 @@ test('T16512b', normal, compile_fail, [''])
 test('T17213', [extra_files(['T17213a.hs'])], multimod_compile_fail, ['T17213', '-v0'])
 test('T17355', normal, compile_fail, [''])
 test('T17563', normal, compile_fail, [''])
+test('T18851', normal, compile_fail, [''])
+test('T18851b', normal, compile_fail, [''])
+test('T18851c', normal, compile_fail, [''])
 test('T16946', normal, compile_fail, [''])
 test('T16502', expect_broken(12854), compile, [''])
 test('T17566b', normal, compile_fail, [''])
@@ -618,6 +629,8 @@ test('T19397E3', extra_files(['T19397S.hs']), multimod_compile_fail,
 test('T19397E4', extra_files(['T19397S.hs']), multimod_compile_fail,
     ['T19397E4.hs', '-v0 -main-is foo'])
 test('T19415', normal, compile_fail, [''])
+test('T19977a', normal, compile_fail, [''])
+test('T19977b', normal, compile_fail, [''])
 test('T19978', normal, compile_fail, [''])
 test('T20043', normal, compile_fail, [''])
 test('T20122', normal, compile_fail, [''])
@@ -629,3 +642,11 @@ test('T20588', [extra_files(['T20588.hs', 'T20588.hs-boot', 'T20588_aux.hs'])],
 test('T20588c', [extra_files(['T20588c.hs', 'T20588c.hs-boot', 'T20588c_aux.hs'])], multimod_compile_fail, ['T20588c_aux.hs', '-v0'])
 test('T20189', normal, compile_fail, [''])
 test('T20873c', normal, compile_fail, [''])
+test('FunDepOrigin1b', normal, compile_fail, [''])
+test('FD1', normal, compile_fail, [''])
+test('FD2', normal, compile_fail, [''])
+test('FD3', normal, compile_fail, [''])
+test('T18398', normal, compile_fail, [''])
+test('T18406', normal, compile_fail, [''])
+test('AmbigFDs', normal, compile_fail, [''])
+test('T20064', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tc168.hs b/testsuite/tests/typecheck/should_fail/tc168.hs
new file mode 100644
index 0000000000..48c765bdbf
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/tc168.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}
+
+-- We want to get the type
+--      g :: forall a b c.  C a (b,c) => a -> b
+--but GHC 6.0 bogusly gets
+--      g :: forall a b.  C a (b,()) => a -> b
+
+-- Having done this, we reject f on the grounds
+-- that its type is ambiguous: adding the type
+-- signature   g :: C a (b,c) => a -> b
+-- would fail
+
+module ShouldFail where
+
+class C a b where { op :: a -> b }
+
+g x = fst (op x)
diff --git a/testsuite/tests/typecheck/should_fail/tc168.stderr b/testsuite/tests/typecheck/should_fail/tc168.stderr
new file mode 100644
index 0000000000..082cf3d96d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/tc168.stderr
@@ -0,0 +1,12 @@
+
+tc168.hs:17:1: error:
+    • Could not deduce (C a1 (a2, b0))
+      from the context: C a1 (a2, b)
+        bound by the inferred type for ‘g’:
+                   forall {a1} {a2} {b}. C a1 (a2, b) => a1 -> a2
+        at tc168.hs:17:1-16
+      The type variable ‘b0’ is ambiguous
+    • In the ambiguity check for the inferred type for ‘g’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      When checking the inferred type
+        g :: forall {a1} {a2} {b}. C a1 (a2, b) => a1 -> a2
diff --git a/testsuite/tests/typecheck/should_fail/tc168b.hs b/testsuite/tests/typecheck/should_fail/tc168b.hs
new file mode 100644
index 0000000000..052d0ab979
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/tc168b.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}
+
+module ShouldFail where
+
+class C a b where { op :: a -> b }
+
+g a = get (op a)
+
+get :: (u,v,w,x,y,z) -> u
+get (u,_,_,_,_,_) = u
diff --git a/testsuite/tests/typecheck/should_fail/tc168b.stderr b/testsuite/tests/typecheck/should_fail/tc168b.stderr
new file mode 100644
index 0000000000..6b9619ec36
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/tc168b.stderr
@@ -0,0 +1,16 @@
+
+tc168b.hs:7:1: error:
+    • Could not deduce (C a (u, v0, w0, x0, y0, z0))
+      from the context: C a (u, v, w, x, y, z)
+        bound by the inferred type for ‘g’:
+                   forall {a} {u} {v} {w} {x} {y} {z}.
+                   C a (u, v, w, x, y, z) =>
+                   a -> u
+        at tc168b.hs:7:1-16
+      The type variables ‘v0’, ‘w0’, ‘x0’, ‘y0’, ‘z0’ are ambiguous
+    • In the ambiguity check for the inferred type for ‘g’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      When checking the inferred type
+        g :: forall {a} {u} {v} {w} {x} {y} {z}.
+             C a (u, v, w, x, y, z) =>
+             a -> u
diff --git a/testsuite/tests/typecheck/should_fail/tcfail093.hs b/testsuite/tests/typecheck/should_fail/tcfail093.hs
index 2329bfa2ff..9d6556786d 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail093.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail093.hs
@@ -11,11 +11,15 @@ module ShouldFail where
 
 -- July 07: I'm changing this from "should fail" to "should succeed"
 -- See Note [Important subtlety in oclose] in GHC.Tc.Instance.FunDeps
+--
+-- June 2021: Changing this back to "should fail".
+-- See https://gitlab.haskell.org/ghc/ghc/-/issues/20064
 
 
 primDup :: Int -> IO Int
 primDup = undefined
 
+--dup :: Call (IO Int) h => () -> Int -> h
 dup () = call primDup
 
 --      call :: Call c h => c -> h
diff --git a/testsuite/tests/typecheck/should_fail/tcfail093.stderr b/testsuite/tests/typecheck/should_fail/tcfail093.stderr
new file mode 100644
index 0000000000..4909623a52
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/tcfail093.stderr
@@ -0,0 +1,5 @@
+
+tcfail093.hs:23:10: error:
+    • No instance for (Call (IO Int) h0) arising from a use of ‘call’
+    • In the expression: call primDup
+      In an equation for ‘dup’: dup () = call primDup
diff --git a/testsuite/tests/typecheck/should_fail/tcfail097.stderr b/testsuite/tests/typecheck/should_fail/tcfail097.stderr
index bc8d9a0cf1..f00af20700 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail097.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail097.stderr
@@ -6,6 +6,12 @@ tcfail097.hs:5:6: error:
                    f :: forall a. Eq a => Int -> Int
         at tcfail097.hs:5:6-23
       The type variable ‘a0’ is ambiguous
+      Potentially matching instances:
+        instance Eq Ordering -- Defined in ‘GHC.Classes’
+        instance Eq Integer -- Defined in ‘GHC.Num.Integer’
+        ...plus 23 others
+        ...plus four instances involving out-of-scope types
+        (use -fprint-potential-instances to see them all)
     • In the ambiguity check for ‘f’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       In the type signature: f :: Eq a => Int -> Int
diff --git a/testsuite/tests/typecheck/should_fail/tcfail102.stderr b/testsuite/tests/typecheck/should_fail/tcfail102.stderr
index 60a101df0c..fdfedf7ebb 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail102.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail102.stderr
@@ -2,12 +2,12 @@
 tcfail102.hs:1:14: warning: [-Wdeprecated-flags (in -Wdefault)]
     -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language.
 
-tcfail102.hs:9:15: error:
-    • Could not deduce (Integral (Ratio a)) arising from a use of ‘p’
+tcfail102.hs:9:7: error:
+    • Could not deduce (Integral (Ratio a))
+        arising from a record update
       from the context: Integral a
         bound by the type signature for:
                    f :: forall a. Integral a => P (Ratio a) -> P (Ratio a)
         at tcfail102.hs:8:1-45
-    • In the ‘p’ field of a record
-      In the expression: x {p = p x}
+    • In the expression: x {p = p x}
       In an equation for ‘f’: f x = x {p = p x}
diff --git a/testsuite/tests/typecheck/should_fail/tcfail201.stderr b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
index 023772c775..088c2be671 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail201.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
@@ -1,5 +1,5 @@
 
-tcfail201.hs:17:58: error:
+tcfail201.hs:17:27: error:
     • Couldn't match expected type ‘a’ with actual type ‘HsDoc id0’
       ‘a’ is a rigid type variable bound by
         the type signature for:
@@ -7,9 +7,9 @@ tcfail201.hs:17:58: error:
                      (forall a1 b. c (a1 -> b) -> a1 -> c b)
                      -> (forall g. g -> c g) -> a -> c a
         at tcfail201.hs:15:1-85
-    • In the first argument of ‘z’, namely ‘DocEmpty’
-      In the expression: z DocEmpty
+    • In the pattern: DocEmpty
       In a case alternative: DocEmpty -> z DocEmpty
+      In the expression: case hsDoc of DocEmpty -> z DocEmpty
     • Relevant bindings include
         hsDoc :: a (bound at tcfail201.hs:16:13)
         gfoldl' :: (forall a1 b. c (a1 -> b) -> a1 -> c b)