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 -------------------------
author: Richard Eisenberg <rae@richarde.dev> 2022-02-18 23:29:52 +0100
committer: Marge Bot <ben+marge-bot@smart-cactus.org> 2022-02-23 08:16:07 -0500
commit: a599abbad939820c666ced00ae9eb33706a4f360 (patch)
tree: 7b3811972a50da9e81018056cdcdeef158bc22e3 /testsuite/tests
parent: 558c7d554b9724abfaa2bcc1f42050e67b36a988 (diff)
download: haskell-a599abbad939820c666ced00ae9eb33706a4f360.tar.gz
139 files changed, 1629 insertions, 434 deletions
diff --git a/testsuite/tests/dependent/should_compile/LopezJuan.hs b/testsuite/tests/dependent/should_compile/LopezJuan.hs
new file mode 100644
index 0000000000..bc7cc89201
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/LopezJuan.hs
@@ -0,0 +1,73 @@
+{-
+
+This test is inspired by
+  Practical dependent type checking using twin types
+  Victor López Juan and Nils Anders Danielsson
+  TyDe '20
+  https://dl.acm.org/doi/10.1145/3406089.3409030
+
+The challenge is whether we can unify two types where the only
+way to know that the kinds are equal is to unify the types. This
+would fail in an algorithm that required kind unification before
+type unification.
+-}
+
+{-# LANGUAGE TypeOperators, TypeApplications, DataKinds,
+             StandaloneKindSignatures, PolyKinds, GADTs,
+             TypeFamilies, NamedWildCards, PartialTypeSignatures #-}
+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
+
+module LopezJuan where
+
+import Data.Type.Equality ( (:~~:)(..) )
+import Data.Kind ( Type )
+import Data.Proxy ( Proxy )
+
+-- amazingly, this worked without modification
+
+data SBool :: Bool -> Type where
+  SFalse :: SBool False
+  STrue  :: SBool True
+
+data BoolOp where
+  None :: Bool -> BoolOp
+  Some :: Bool -> BoolOp
+
+type F :: Bool -> Type
+type family F b
+
+get :: BoolOp -> Bool
+get (None _) = True
+get (Some x) = x
+
+type Get :: BoolOp -> Bool
+type family Get x where
+  Get (None _) = True
+  Get (Some x) = x
+
+type TyFun :: Type -> Type -> Type
+data TyFun arg res
+
+type (~>) :: Type -> Type -> Type
+type arg ~> res = TyFun arg res -> Type
+infixr 0 ~>
+
+data Const :: a -> (b ~> a)
+
+f :: SBool x -> (:~~:) @(F (Get (_alpha x)) ~> BoolOp)
+                       @(F True ~> BoolOp)
+                       (Const (None x))
+                       (Const (_alpha x))
+f _ = HRefl
+
+-- and something simpler:
+
+type family Idish guard a where
+  Idish True a = a
+  Idish False a = Int
+
+g :: (:~~:) @(Idish _alpha Type)
+            @Type
+            (Proxy _alpha)
+            (Proxy True)
+g = HRefl
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 5f947f5e37..93d9164768 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -72,3 +72,4 @@ test('T16344b', normal, compile, [''])
 test('T16347', normal, compile, [''])
 test('T18660', normal, compile, [''])
 test('T12174', normal, compile, [''])
+test('LopezJuan', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/T11471.stderr b/testsuite/tests/dependent/should_fail/T11471.stderr
index 7772850564..30bab29f4b 100644
--- a/testsuite/tests/dependent/should_fail/T11471.stderr
+++ b/testsuite/tests/dependent/should_fail/T11471.stderr
@@ -10,13 +10,3 @@ T11471.hs:15:10: error:
       In the expression: f (undefined :: Proxy Int#) 3#
       In an equation for ‘bad’: bad = f (undefined :: Proxy Int#) 3#
     • Relevant bindings include bad :: F a (bound at T11471.hs:15:1)
-
-T11471.hs:15:35: error:
-    • Couldn't match a lifted type with an unlifted type
-      When matching types
-        F a :: *
-        Int# :: TYPE 'IntRep
-    • In the second argument of ‘f’, namely ‘3#’
-      In the expression: f (undefined :: Proxy Int#) 3#
-      In an equation for ‘bad’: bad = f (undefined :: Proxy Int#) 3#
-    • Relevant bindings include bad :: F a (bound at T11471.hs:15:1)
diff --git a/testsuite/tests/dependent/should_fail/T13135_simple.hs b/testsuite/tests/dependent/should_fail/T13135_simple.hs
new file mode 100644
index 0000000000..576b923886
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13135_simple.hs
@@ -0,0 +1,115 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T13135_simple where
+
+import Data.Kind (Type)
+import GHC.Exts ( RuntimeRep(BoxedRep), Levity(Lifted) )
+
+{-
+NB: All the type applications and explicit quantification
+aren't necessary for the error
+to trigger, but they are helpful in reading this code.
+-}
+
+type Sig :: Type -> Type
+data Sig a = SigFun a (Sig a)
+-- SigFun :: forall (a :: Type). a -> Sig a -> Sig a
+
+type SmartFun :: forall (t :: Type). Sig t -> Type
+type family SmartFun sig = r | r -> sig where
+  forall (a :: Type) (sig :: Sig Type).
+    SmartFun @Type (SigFun @Type a sig) = a -> SmartFun @Type sig
+
+smartSym :: forall (k :: Type) (sig :: Sig k). SmartFun @k sig
+smartSym = error @(BoxedRep Lifted) @(SmartFun @k sig) "urk"
+
+problem :: Int -> Bool
+problem = smartSym
+
+{-
+problem arises in RHS of `problem`:
+
+instantiate smartSym:
+  kappa :: Type
+  sigma :: Sig kappa
+  smartSym :: SmartFun @kappa sigma
+
+[W] w1 :: SmartFun @kappa sigma ~ Int -> Bool
+
+injective type family says:
+beta :: Sig Type
+[W] w2 :: Type ~ kappa
+[W] w3 :: sigma ~ SigFun @Type Int beta
+
+then we have
+inert: [W] w1 :: SmartFun @kappa sigma ~ Int -> Bool
+work list: [W] w3 :: (SigFun @Type Int beta :: Sig Type) ~ (sigma :: Sig kappa)  (current item)
+           [W] w2 :: Type ~ kappa
+
+this is a hetero equality. So we get
+[W] w4 :: Type ~ kappa
+[W] w5 :: sigma ~ (SigFun @Type Int beta |> Sig w4)
+w3 is solved
+we cannot solve w5 by unification because of the coercion hole w4, so w5 becomes an inert,
+  kicking out w1
+
+next step.
+inert: [W] w5 :: sigma ~ (SigFun @Type Int beta |> Sig w4)
+work list: [W] w1 :: SmartFun @kappa sigma ~ Int -> Bool  (current item)
+           [W] w4 :: Type ~ kappa
+           [W] w2 :: Type ~ kappa
+
+LHS of w1 is rewritten, making it become
+  [W] w1 :: SmartFun @kappa (SigFun @Type Int beta |> Sig w4) ~ Int -> Bool
+
+injective type family says:
+gamma :: Sig Type
+[W] w6 :: Type ~ kappa
+[W] w7 :: (SigFun @Type Int gamma :: Sig Type)
+            ~
+          ((SigFun @Type Int beta |> Sig w4) :: Sig kappa)
+
+next step.
+inert: [W] w5 :: sigma ~ (SigFun @Type Int beta |> Sig w4)
+       [W] w1 :: SmartFun @kappa (SigFun @Type int beta |> Sig w4) ~ Int -> Bool
+work list: [W] w7 :: SigFun @Type Int gamma ~ (SigFun @Type Int beta |> Sig w4)  (current item)
+           [W] w6 :: Type ~ kappa
+           [W] w4 :: Type ~ kappa
+           [W] w2 :: Type ~ kappa
+
+we drop the cast on the work item, to get
+  [W] w7 :: SigFun @Type Int gamma ~ SigFun @Type Int beta
+this decomposes to
+  [W] w8 :: beta ~ gamma
+which gets added to the work list
+
+next step.
+inert: [W] w5 :: sigma ~ (SigFun @Type Int beta |> Sig w4)
+       [W] w1 :: SmartFun @kappa (SigFun @Type int beta |> Sig w4) ~ Int -> Bool
+work list: [W] w8 :: beta ~ gamma  (current item)
+           [W] w6 :: Type ~ kappa
+           [W] w4 :: Type ~ kappa
+           [W] w2 :: Type ~ kappa
+
+unify beta := gamma
+kick out w5 and w1
+
+next step.
+inert: none
+work list: [W] w5 :: sigma ~ (SigFun @Type Int beta |> Sig w4)   (current item)
+           [W] w1 :: SmartFun @kappa (SigFun @Type Int beta |> Sig w4) ~ Int -> Bool
+           [W] w6 :: Type ~ kappa
+           [W] w4 :: Type ~ kappa
+           [W] w2 :: Type ~ kappa
+
+w5 still cannot be solved by unification, and then when we see w1 again, we spit out
+new type-family injectivity equalities... and around and around we go.
+
+-}
diff --git a/testsuite/tests/dependent/should_fail/T13135_simple.stderr b/testsuite/tests/dependent/should_fail/T13135_simple.stderr
new file mode 100644
index 0000000000..52b1e848c0
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13135_simple.stderr
@@ -0,0 +1,8 @@
+
+T13135_simple.hs:34:11: error:
+    • Couldn't match type ‘SmartFun sig’ with ‘Bool’
+      Expected: Int -> Bool
+        Actual: SmartFun ('SigFun Int sig)
+      The type variable ‘sig’ is ambiguous
+    • In the expression: smartSym
+      In an equation for ‘problem’: problem = smartSym
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 255b20b7e0..5de2070a0e 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -65,6 +65,7 @@ test('T16344a', normal, compile_fail, [''])
 test('T16418', normal, compile_fail, [''])
 test('T17541', normal, compile_fail, [''])
 test('T17541b', normal, compile_fail, [''])
+test('T13135_simple', normal, compile_fail, [''])
 test('T17131', normal, compile_fail, [''])
 test('T14880', normal, compile_fail, [''])
 test('T14880-2', normal, compile_fail, [''])
diff --git a/testsuite/tests/deriving/should_fail/T5287.stderr b/testsuite/tests/deriving/should_fail/T5287.stderr
index 479f1f84b5..0dfedee061 100644
--- a/testsuite/tests/deriving/should_fail/T5287.stderr
+++ b/testsuite/tests/deriving/should_fail/T5287.stderr
@@ -6,6 +6,8 @@ T5287.hs:7:10: error:
                    forall a oops. A a oops => Read (D a)
         at T5287.hs:7:10-31
       The type variable ‘oops0’ is ambiguous
+      Potentially matching instance:
+        instance A Int Bool -- Defined at T5287.hs:13:10
     • In the ambiguity check for an instance declaration
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       In the instance declaration for ‘Read (D a)’
diff --git a/testsuite/tests/ghci/should_run/tc-plugin-ghci/TcPluginGHCi.hs b/testsuite/tests/ghci/should_run/tc-plugin-ghci/TcPluginGHCi.hs
index b194d8f2b5..fbaeaa4f0f 100644
--- a/testsuite/tests/ghci/should_run/tc-plugin-ghci/TcPluginGHCi.hs
+++ b/testsuite/tests/ghci/should_run/tc-plugin-ghci/TcPluginGHCi.hs
@@ -11,7 +11,7 @@ plugin = defaultPlugin { tcPlugin = Just . thePlugin }
 thePlugin :: [CommandLineOption] -> TcPlugin
 thePlugin opts = TcPlugin
   { tcPluginInit    = trace "TcPluginGHCi" (return ())
-  , tcPluginSolve   = \_ _ _ _ _ -> return $ TcPluginOk [] []
+  , tcPluginSolve   = \_ _ _ _ -> return $ TcPluginOk [] []
   , tcPluginRewrite = \_ -> emptyUFM
   , tcPluginStop    = \_ -> return ()
   }
diff --git a/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr b/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr
index 16078fd7fc..1a11c1f996 100644
--- a/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr
+++ b/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr
@@ -1,29 +1,23 @@
 
 PushedInAsGivens.hs:10:31: error:
-    • Could not deduce (a1 ~ a)
-      from the context: F Int ~ [a1]
-        bound by the type signature for:
-                   foo :: forall a1. (F Int ~ [a1]) => a1 -> Int
-        at PushedInAsGivens.hs:9:13-44
-      ‘a1’ is a rigid type variable bound by
+    • Couldn't match expected type ‘a’ with actual type ‘a0’
+        because type variable ‘a’ would escape its scope
+      This (rigid, skolem) type variable is bound by
         the type signature for:
-          foo :: forall a1. (F Int ~ [a1]) => a1 -> Int
+          foo :: forall a. (F Int ~ [a]) => a -> Int
         at PushedInAsGivens.hs:9:13-44
-      ‘a’ is a rigid type variable bound by
-        the inferred type of bar :: a -> (a, Int)
-        at PushedInAsGivens.hs:(9,1)-(11,20)
     • In the expression: y
       In the first argument of ‘length’, namely ‘[x, y]’
       In the expression: length [x, y]
     • Relevant bindings include
-        x :: a1 (bound at PushedInAsGivens.hs:10:17)
-        foo :: a1 -> Int (bound at PushedInAsGivens.hs:10:13)
-        y :: a (bound at PushedInAsGivens.hs:9:5)
-        bar :: a -> (a, Int) (bound at PushedInAsGivens.hs:9:1)
+        x :: a (bound at PushedInAsGivens.hs:10:17)
+        foo :: a -> Int (bound at PushedInAsGivens.hs:10:13)
+        y :: a0 (bound at PushedInAsGivens.hs:9:5)
+        bar :: a0 -> (a0, Int) (bound at PushedInAsGivens.hs:9:1)
 
 PushedInAsGivens.hs:11:15: error:
     • Couldn't match type: F Int
-                     with: [a]
+                     with: [a0]
         arising from a use of ‘foo’
     • In the expression: foo y
       In the expression: (y, foo y)
@@ -33,5 +27,5 @@ PushedInAsGivens.hs:11:15: error:
           foo x = length [...]
         in (y, foo y)
     • Relevant bindings include
-        y :: a (bound at PushedInAsGivens.hs:9:5)
-        bar :: a -> (a, Int) (bound at PushedInAsGivens.hs:9:1)
+        y :: a0 (bound at PushedInAsGivens.hs:9:5)
+        bar :: a0 -> (a0, Int) (bound at PushedInAsGivens.hs:9:1)
diff --git a/testsuite/tests/indexed-types/should_compile/T3208b.stderr b/testsuite/tests/indexed-types/should_compile/T3208b.stderr
index c1a09ebfcb..216b14f095 100644
--- a/testsuite/tests/indexed-types/should_compile/T3208b.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T3208b.stderr
@@ -1,6 +1,21 @@
 
+T3208b.hs:15:10: error:
+    • Could not deduce (OTerm o0 ~ STerm a) arising from a use of ‘fce’
+      from the context: (OTerm a ~ STerm a, OBJECT a, SUBST a)
+        bound by the type signature for:
+                   fce' :: forall a c.
+                           (OTerm a ~ STerm a, OBJECT a, SUBST a) =>
+                           a -> c
+        at T3208b.hs:14:1-56
+      The type variable ‘o0’ is ambiguous
+    • In the expression: fce (apply f)
+      In an equation for ‘fce'’: fce' f = fce (apply f)
+    • Relevant bindings include
+        f :: a (bound at T3208b.hs:15:6)
+        fce' :: a -> c (bound at T3208b.hs:15:1)
+
 T3208b.hs:15:15: error:
-    • Could not deduce (OTerm o0 ~ STerm a)
+    • Could not deduce (STerm o0 ~ STerm a)
         arising from a use of ‘apply’
       from the context: (OTerm a ~ STerm a, OBJECT a, SUBST a)
         bound by the type signature for:
@@ -8,6 +23,7 @@ T3208b.hs:15:15: error:
                            (OTerm a ~ STerm a, OBJECT a, SUBST a) =>
                            a -> c
         at T3208b.hs:14:1-56
+      NB: ‘STerm’ is a non-injective type family
       The type variable ‘o0’ is ambiguous
     • In the first argument of ‘fce’, namely ‘(apply f)’
       In the expression: fce (apply f)
diff --git a/testsuite/tests/indexed-types/should_fail/T4254.hs b/testsuite/tests/indexed-types/should_compile/T4254.hs
index b12ffb4f87..5e84318dfe 100644
--- a/testsuite/tests/indexed-types/should_fail/T4254.hs
+++ b/testsuite/tests/indexed-types/should_compile/T4254.hs
@@ -1,9 +1,9 @@
 {-# LANGUAGE TypeFamilies, FunctionalDependencies, RankNTypes, MultiParamTypeClasses #-}
 module T4254 where
 
-class FD a b | a -> b where 
-  op :: a -> b; 
-  op = undefined 
+class FD a b | a -> b where
+  op :: a -> b;
+  op = undefined
 
 instance FD Int Bool
 
@@ -14,8 +14,3 @@ ok1    = op
 ok2   :: forall a b. (a~Int,FD a b,b~Bool) => a -> Bool
 ok2    = op
 -- Should be OK: needs the b~Bool
-
-fails :: forall a b. (a~Int,FD a b) => a -> Bool 
-fails  = op
--- Could fail: no proof that b~Bool
--- But can also succeed; it's not a *wanted* constraint
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index d03de782c6..39f9b49b4e 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -306,3 +306,4 @@ test('T8707', normal, compile, ['-O'])
 test('T14111', normal, compile, ['-O'])
 test('T19336', normal, compile, ['-O'])
 test('T11715b', normal, ghci_script, ['T11715b.script'])
+test('T4254', normal, compile, [''])
diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs
index f8187e5878..6a19a172bf 100644
--- a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs
+++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs
@@ -22,7 +22,12 @@ class C a where
 
 instance C Int where
   type forall a b. CT [a] (a,a)     = Float
-  type forall b.   CT _ _           = Maybe b
-
   data forall a b. CD [a] (a,a)     = CD5 Float
+
+instance C Bool where
+  type forall b.   CT _ _           = Maybe b
   data forall b.   CD _ _           = CD6 (Maybe b)
+
+instance C Double where
+  type forall b. CT _ _ = Bool
+  data forall b. CD _ _ = CD7
diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr
index 7d8bd872ed..c12678c32a 100644
--- a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr
@@ -57,20 +57,14 @@ ExplicitForAllFams4b.hs:24:17: error:
     • In the type instance declaration for ‘CT’
       In the instance declaration for ‘C Int’
 
-ExplicitForAllFams4b.hs:25:15: error:
-    • Type variable ‘b’ is mentioned in the RHS,
-        but not bound on the LHS of the family instance
-    • In the type instance declaration for ‘CT’
-      In the instance declaration for ‘C Int’
-
-ExplicitForAllFams4b.hs:27:3: error:
+ExplicitForAllFams4b.hs:25:3: error:
     • Type indexes must match class instance head
       Expected: CD Int _
         Actual: CD [a] (a, a)
     • In the data instance declaration for ‘CD’
       In the instance declaration for ‘C Int’
 
-ExplicitForAllFams4b.hs:27:17: error:
+ExplicitForAllFams4b.hs:25:17: error:
     • Type variable ‘b’ is mentioned in the RHS,
         but not bound on the LHS of the family instance
     • In the data instance declaration for ‘CD’
@@ -79,5 +73,23 @@ ExplicitForAllFams4b.hs:27:17: error:
 ExplicitForAllFams4b.hs:28:15: error:
     • Type variable ‘b’ is mentioned in the RHS,
         but not bound on the LHS of the family instance
+    • In the type instance declaration for ‘CT’
+      In the instance declaration for ‘C Bool’
+
+ExplicitForAllFams4b.hs:29:15: error:
+    • Type variable ‘b’ is mentioned in the RHS,
+        but not bound on the LHS of the family instance
     • In the data instance declaration for ‘CD’
-      In the instance declaration for ‘C Int’
+      In the instance declaration for ‘C Bool’
+
+ExplicitForAllFams4b.hs:32:15: error:
+    • Type variable ‘b’ is bound by a forall,
+        but not used in the family instance
+    • In the type instance declaration for ‘CT’
+      In the instance declaration for ‘C Double’
+
+ExplicitForAllFams4b.hs:33:15: error:
+    • Type variable ‘b’ is mentioned in the RHS,
+        but not bound on the LHS of the family instance
+    • In the data instance declaration for ‘CD’
+      In the instance declaration for ‘C Double’
diff --git a/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr b/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
index 63f24fa268..e3ff20d973 100644
--- a/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
+++ b/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
@@ -1,18 +1,28 @@
 
 ExtraTcsUntch.hs:23:18: error:
     • Couldn't match expected type: F Int
-                  with actual type: [p]
+                  with actual type: [[a0]]
     • In the first argument of ‘h’, namely ‘[x]’
       In the expression: h [x]
       In an equation for ‘g1’: g1 _ = h [x]
     • Relevant bindings include
-        x :: p (bound at ExtraTcsUntch.hs:21:3)
-        f :: p -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
+        x :: [a0] (bound at ExtraTcsUntch.hs:21:3)
+        f :: [a0] -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
 
-ExtraTcsUntch.hs:25:38: error:
-    • Couldn't match expected type: F Int
-                  with actual type: [[a0]]
-      The type variable ‘a0’ is ambiguous
-    • In the first argument of ‘h’, namely ‘[[undefined]]’
-      In the expression: h [[undefined]]
+ExtraTcsUntch.hs:25:53: error:
+    • Couldn't match type ‘a0’ with ‘a’
+        arising from a functional dependency between:
+          constraint ‘C [a0] [a]’ arising from a use of ‘op’
+          instance ‘C [a1] [a1]’ at ExtraTcsUntch.hs:9:10-18
+        because type variable ‘a’ would escape its scope
+      This (rigid, skolem) type variable is bound by
+        a pattern with constructor: TEx :: forall a. a -> TEx,
+        in a case alternative
+        at ExtraTcsUntch.hs:25:26-30
+    • In the expression: op x [y]
       In the expression: (h [[undefined]], op x [y])
+      In a case alternative: TEx y -> (h [[undefined]], op x [y])
+    • Relevant bindings include
+        y :: a (bound at ExtraTcsUntch.hs:25:30)
+        x :: [a0] (bound at ExtraTcsUntch.hs:21:3)
+        f :: [a0] -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail16.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail16.stderr
index df131da8a3..d33d2f9535 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail16.stderr
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail16.stderr
@@ -2,7 +2,6 @@
 SimpleFail16.hs:10:12: error:
     • Couldn't match expected type: p0 a0
                   with actual type: F ()
-      The type variables ‘p0’, ‘a0’ are ambiguous
     • In the first argument of ‘foo’, namely ‘(undefined :: F ())’
       In the expression: foo (undefined :: F ())
       In an equation for ‘bar’: bar = foo (undefined :: F ())
diff --git a/testsuite/tests/indexed-types/should_fail/T13972.hs b/testsuite/tests/indexed-types/should_fail/T13972.hs
index 9a5af411e2..27e2b5563f 100644
--- a/testsuite/tests/indexed-types/should_fail/T13972.hs
+++ b/testsuite/tests/indexed-types/should_fail/T13972.hs
@@ -8,7 +8,7 @@ import Data.Kind
 class C (a :: k) where
   type T k :: Type
 
--- This used to fail, with a mysterious error messate
+-- This used to fail, with a mysterious error message
 --    Type indexes must match class instance head
 --      Expected: T (a1 -> Either a1 b1)
 --      Actual: T (a -> Either a b)
diff --git a/testsuite/tests/indexed-types/should_fail/T14230a.stderr b/testsuite/tests/indexed-types/should_fail/T14230a.stderr
index 726764a07f..886ee184d4 100644
--- a/testsuite/tests/indexed-types/should_fail/T14230a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T14230a.stderr
@@ -1,6 +1,7 @@
 
-T14230a.hs:13:14: error:
-    • Expected kind ‘k -> *’, but ‘a’ has kind ‘*’
-    • In the second argument of ‘CD’, namely ‘(a :: k -> *)’
-      In the data instance declaration for ‘CD’
+T14230a.hs:13:3: error:
+    • Type indexes must match class instance head
+      Expected: CD (*) (Maybe a)
+        Actual: CD k a
+    • In the data instance declaration for ‘CD’
       In the instance declaration for ‘C (Maybe a)’
diff --git a/testsuite/tests/indexed-types/should_fail/T14246.stderr b/testsuite/tests/indexed-types/should_fail/T14246.stderr
index a41f73efa5..292c49fb25 100644
--- a/testsuite/tests/indexed-types/should_fail/T14246.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T14246.stderr
@@ -5,8 +5,7 @@ T14246.hs:19:5: error:
       In the type family declaration for ‘KLN’
 
 T14246.hs:23:27: error:
-    • Couldn't match kind: 'S (KLN (f t))
-                     with: KLN f
+    • Couldn't match kind ‘*’ with ‘L’
       Expected kind ‘Vect (KLN f) L’,
         but ‘Cons (Label (t :: v)) l’ has kind ‘Vect ('S (KLN (f t))) (*)’
     • In the second argument of ‘Reveal’, namely
diff --git a/testsuite/tests/indexed-types/should_fail/T15870.stderr b/testsuite/tests/indexed-types/should_fail/T15870.stderr
index 198ec75797..54a2ea87e9 100644
--- a/testsuite/tests/indexed-types/should_fail/T15870.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T15870.stderr
@@ -1,10 +1,7 @@
 
 T15870.hs:32:34: error:
     • Couldn't match kind ‘k’ with ‘*’
-      When matching kinds
-        b :: *
-        a :: k
-      Expected kind ‘Optic a’, but ‘g2’ has kind ‘Optic b’
+      Expected kind ‘Optic @{k} a’, but ‘g2’ has kind ‘Optic @{*} b’
       ‘k’ is a rigid type variable bound by
         the instance declaration
         at T15870.hs:(27,1)-(32,35)
diff --git a/testsuite/tests/indexed-types/should_fail/T2693.stderr b/testsuite/tests/indexed-types/should_fail/T2693.stderr
index 57d4303849..f07905b570 100644
--- a/testsuite/tests/indexed-types/should_fail/T2693.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2693.stderr
@@ -2,7 +2,7 @@
 T2693.hs:12:15: error:
     • Couldn't match expected type: (a8, b1)
                   with actual type: TFn a6
-      The type variables ‘a6’, ‘a8’, ‘b1’ are ambiguous
+      The type variable ‘a6’ is ambiguous
     • In the first argument of ‘fst’, namely ‘x’
       In the first argument of ‘(+)’, namely ‘fst x’
       In the expression: fst x + fst x
@@ -11,7 +11,7 @@ T2693.hs:12:15: error:
 T2693.hs:12:23: error:
     • Couldn't match expected type: (a8, b2)
                   with actual type: TFn a7
-      The type variables ‘a7’, ‘a8’, ‘b2’ are ambiguous
+      The type variable ‘a7’ is ambiguous
     • In the first argument of ‘fst’, namely ‘x’
       In the second argument of ‘(+)’, namely ‘fst x’
       In the expression: fst x + fst x
@@ -20,7 +20,7 @@ T2693.hs:12:23: error:
 T2693.hs:19:15: error:
     • Couldn't match expected type: (a5, b0)
                   with actual type: TFn a2
-      The type variables ‘a2’, ‘a5’, ‘b0’ are ambiguous
+      The type variable ‘a2’ is ambiguous
     • In the first argument of ‘fst’, namely ‘x’
       In the first argument of ‘(+)’, namely ‘fst x’
       In the expression: fst x + snd x
@@ -29,7 +29,7 @@ T2693.hs:19:15: error:
 T2693.hs:19:23: error:
     • Couldn't match expected type: (a4, a5)
                   with actual type: TFn a3
-      The type variables ‘a3’, ‘a4’, ‘a5’ are ambiguous
+      The type variable ‘a3’ is ambiguous
     • In the first argument of ‘snd’, namely ‘x’
       In the second argument of ‘(+)’, namely ‘snd x’
       In the expression: fst x + snd x
@@ -40,7 +40,7 @@ T2693.hs:29:20: error:
                      with: PVR a1
       Expected: () -> Maybe (PVR a1)
         Actual: () -> Maybe (TFn a0)
-      The type variables ‘a0’, ‘a1’ are ambiguous
+      The type variable ‘a0’ is ambiguous
     • In the first argument of ‘mapM’, namely ‘g’
       In a stmt of a 'do' block: pvs <- mapM g undefined
       In the expression:
diff --git a/testsuite/tests/indexed-types/should_fail/T3330c.stderr b/testsuite/tests/indexed-types/should_fail/T3330c.stderr
index 3947abddb6..b661193655 100644
--- a/testsuite/tests/indexed-types/should_fail/T3330c.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T3330c.stderr
@@ -3,7 +3,7 @@ T3330c.hs:25:43: error:
     • Couldn't match kind ‘*’ with ‘* -> *’
       When matching types
         f1 :: * -> *
-        Der f1 x :: *
+        f1 x :: *
       Expected: Der ((->) x) (Der f1 x)
         Actual: R f1
     • In the first argument of ‘plug’, namely ‘rf’
diff --git a/testsuite/tests/indexed-types/should_fail/T4174.stderr b/testsuite/tests/indexed-types/should_fail/T4174.stderr
index 14156deaf0..a33dcf7222 100644
--- a/testsuite/tests/indexed-types/should_fail/T4174.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4174.stderr
@@ -1,16 +1,6 @@
 
 T4174.hs:45:12: error:
-    • Couldn't match type ‘a’ with ‘SmStep’
-      Expected: m (Field (Way (GHC6'8 minor) n t p) a b)
-        Actual: m (Field (WayOf m) SmStep RtsSpinLock)
-      ‘a’ is a rigid type variable bound by
-        the type signature for:
-          testcase :: forall (m :: * -> *) minor n t p a b.
-                      Monad m =>
-                      m (Field (Way (GHC6'8 minor) n t p) a b)
-        at T4174.hs:44:1-63
+    • Couldn't match type ‘False’ with ‘True’
+        arising from a use of ‘sync_large_objects’
     • In the expression: sync_large_objects
       In an equation for ‘testcase’: testcase = sync_large_objects
-    • Relevant bindings include
-        testcase :: m (Field (Way (GHC6'8 minor) n t p) a b)
-          (bound at T4174.hs:45:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T4254b.hs b/testsuite/tests/indexed-types/should_fail/T4254b.hs
new file mode 100644
index 0000000000..ffd117bc4c
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4254b.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies, FunctionalDependencies, RankNTypes, MultiParamTypeClasses #-}
+module T4254b where
+
+class FD a b | a -> b where
+  op :: a -> b;
+  op = undefined
+
+instance FD Int Bool
+
+fails :: forall a b. (a~Int,FD a b) => a -> Bool
+fails  = op
+-- Could fail: no proof that b~Bool
+-- But can also succeed; it's not a *wanted* constraint
diff --git a/testsuite/tests/indexed-types/should_fail/T4254b.stderr b/testsuite/tests/indexed-types/should_fail/T4254b.stderr
new file mode 100644
index 0000000000..d45d0ccdaf
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4254b.stderr
@@ -0,0 +1,20 @@
+
+T4254b.hs:10:10: error:
+    • Couldn't match type ‘b’ with ‘Bool’
+        arising from a functional dependency between constraints:
+          ‘FD Int Bool’
+            arising from a type ambiguity check for
+            the type signature for ‘fails’ at T4254b.hs:10:10-48
+          ‘FD Int b’
+            arising from the type signature for:
+                           fails :: forall a b.
+                                    (a ~ Int, FD a b) =>
+                                    a -> Bool at T4254b.hs:10:10-48
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          fails :: forall a b. (a ~ Int, FD a b) => a -> Bool
+        at T4254b.hs:10:10-48
+    • In the ambiguity check for ‘fails’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      In the type signature:
+        fails :: forall a b. (a ~ Int, FD a b) => a -> Bool
diff --git a/testsuite/tests/indexed-types/should_fail/T7729.stderr b/testsuite/tests/indexed-types/should_fail/T7729.stderr
index baf93df666..8973e8690e 100644
--- a/testsuite/tests/indexed-types/should_fail/T7729.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7729.stderr
@@ -4,7 +4,6 @@ T7729.hs:36:14: error:
                      with: t0 (BasePrimMonad m)
       Expected: t0 (BasePrimMonad m) a -> Rand m a
         Actual: BasePrimMonad (Rand m) a -> Rand m a
-      The type variable ‘t0’ is ambiguous
     • In the first argument of ‘(.)’, namely ‘liftPrim’
       In the expression: liftPrim . lift
       In an equation for ‘liftPrim’: liftPrim = liftPrim . lift
diff --git a/testsuite/tests/indexed-types/should_fail/T7729a.stderr b/testsuite/tests/indexed-types/should_fail/T7729a.stderr
index 60be4271ed..34ef48e179 100644
--- a/testsuite/tests/indexed-types/should_fail/T7729a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7729a.stderr
@@ -1,10 +1,9 @@
 
 T7729a.hs:36:26: error:
     • Couldn't match type: BasePrimMonad m
-                     with: t0 (BasePrimMonad m)
+                     with: t0 m0
       Expected: BasePrimMonad (Rand m) a
-        Actual: t0 (BasePrimMonad m) a
-      The type variable ‘t0’ is ambiguous
+        Actual: t0 m0 a
     • In the first argument of ‘liftPrim’, namely ‘(lift x)’
       In the expression: liftPrim (lift x)
       In an equation for ‘liftPrim’: liftPrim x = liftPrim (lift x)
diff --git a/testsuite/tests/indexed-types/should_fail/T8227.hs b/testsuite/tests/indexed-types/should_fail/T8227.hs
index 05d8222ff4..86bea833e2 100644
--- a/testsuite/tests/indexed-types/should_fail/T8227.hs
+++ b/testsuite/tests/indexed-types/should_fail/T8227.hs
@@ -1,12 +1,19 @@
 {-# LANGUAGE TypeFamilies #-}
 module T8227
-  ( 
+  (
     absoluteToParam
   ) where
 
 import Data.Kind (Type)
 import T8227a
 
+{-
+type family V a :: Type
+
+type instance V Double    = Double
+type instance V (a -> b)   = V b
+-}
+
 type family Scalar a :: Type
 type instance Scalar (a -> v) = a -> Scalar v
 
@@ -41,3 +48,19 @@ fuv0 ~ fuv1 -> fuv1
 -}
 
 
+{-
+Once upon a time, we reported errors with
+     Couldn't match expected type: Scalar (V a)
+                  with actual type: Scalar (V (Scalar (V a)))
+                                    -> Scalar (V (Scalar (V a)))
+Now, it's
+     Couldn't match type: Scalar (V a)
+                     with: t0 -> t0
+      Expected: Scalar (V a)
+        Actual: Scalar (V (t0 -> t0)) -> Scalar (V (t0 -> t0))
+The old message is a bit better. But the only way we can get to the old
+message is to allow a wanted to rewrite a wanted. This is a bad idea
+in general, so we accept the error message regression. The new message
+isn't wrong, and perhaps in some ways its simplicity is actually an
+improvement over the previous one.
+-}
diff --git a/testsuite/tests/indexed-types/should_fail/T8227.stderr b/testsuite/tests/indexed-types/should_fail/T8227.stderr
index 0c8cef576d..e821356430 100644
--- a/testsuite/tests/indexed-types/should_fail/T8227.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T8227.stderr
@@ -1,27 +1,23 @@
 
-T8227.hs:17:27: error:
-    • Couldn't match expected type: Scalar (V a)
-                  with actual type: Scalar (V (Scalar (V a)))
-                                    -> Scalar (V (Scalar (V a)))
+T8227.hs:24:27: error:
+    • Couldn't match type: Scalar (V a)
+                     with: t0 -> t0
+      Expected: Scalar (V a)
+        Actual: Scalar (V (t0 -> t0)) -> Scalar (V (t0 -> t0))
     • In the expression: arcLengthToParam eps eps
       In an equation for ‘absoluteToParam’:
           absoluteToParam eps seg = arcLengthToParam eps eps
     • Relevant bindings include
-        seg :: a (bound at T8227.hs:17:21)
-        eps :: Scalar (V a) (bound at T8227.hs:17:17)
+        seg :: a (bound at T8227.hs:24:21)
+        eps :: Scalar (V a) (bound at T8227.hs:24:17)
         absoluteToParam :: Scalar (V a) -> a -> Scalar (V a)
-          (bound at T8227.hs:17:1)
+          (bound at T8227.hs:24:1)
 
-T8227.hs:17:44: error:
-    • Couldn't match expected type: Scalar (V (Scalar (V a)))
-                  with actual type: Scalar (V a)
-      NB: ‘Scalar’ is a non-injective type family
-    • In the first argument of ‘arcLengthToParam’, namely ‘eps’
+T8227.hs:24:48: error:
+    • Couldn't match type ‘t0’ with ‘Scalar (V t0)’
+        arising from a type equality Scalar (V a) ~ t0 -> t0
+      The type variable ‘t0’ is ambiguous
+    • In the second argument of ‘arcLengthToParam’, namely ‘eps’
       In the expression: arcLengthToParam eps eps
       In an equation for ‘absoluteToParam’:
           absoluteToParam eps seg = arcLengthToParam eps eps
-    • Relevant bindings include
-        seg :: a (bound at T8227.hs:17:21)
-        eps :: Scalar (V a) (bound at T8227.hs:17:17)
-        absoluteToParam :: Scalar (V a) -> a -> Scalar (V a)
-          (bound at T8227.hs:17:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T8518.hs b/testsuite/tests/indexed-types/should_fail/T8518.hs
index 666ddd09ad..428e691a1d 100644
--- a/testsuite/tests/indexed-types/should_fail/T8518.hs
+++ b/testsuite/tests/indexed-types/should_fail/T8518.hs
@@ -13,5 +13,6 @@ class Continuation c where
 callCont :: Continuation c => c -> (Z c) -> (B c) -> Maybe (F c)
 callCont c z b = rpt (4 :: Int) c z b
     where
+      --rpt :: Int -> c -> Z c -> B c -> F c
         rpt 0 c' z' b' = fromJust (fst <$> (continue c' z' b'))
-        rpt i c' z' b' = let c'' = fromJust (snd <$> (continue c' z' b')) in rpt (i-1) c''
+        rpt i c' z' b' = let c'' = fromJust (snd <$> (continue c' z' b')) in rpt (i-1) c'' -- z'' b''
diff --git a/testsuite/tests/indexed-types/should_fail/T8518.stderr b/testsuite/tests/indexed-types/should_fail/T8518.stderr
index b16ee1ef91..044991ff5b 100644
--- a/testsuite/tests/indexed-types/should_fail/T8518.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T8518.stderr
@@ -1,6 +1,6 @@
 
 T8518.hs:14:18: error:
-    • Couldn't match expected type: Z c -> B c -> Maybe (F c)
+    • Couldn't match expected type: Z c -> B c -> t0
                   with actual type: F c
     • The function ‘rpt’ is applied to four value arguments,
         but its type ‘Int -> c -> F c’ has only two
@@ -17,7 +17,7 @@ T8518.hs:14:18: error:
         c :: c (bound at T8518.hs:14:10)
         callCont :: c -> Z c -> B c -> Maybe (F c) (bound at T8518.hs:14:1)
 
-T8518.hs:16:9: error:
+T8518.hs:17:9: error:
     • Couldn't match type: F t2
                      with: Z t2 -> B t2 -> F t2
       Expected: t1 -> t2 -> F t2
@@ -29,4 +29,4 @@ T8518.hs:16:9: error:
                 rpt 0 c' z' b' = fromJust (fst <$> (continue c' z' b'))
                 rpt i c' z' b' = let ... in rpt (i - 1) c''
     • Relevant bindings include
-        rpt :: t1 -> t2 -> F t2 (bound at T8518.hs:16:9)
+        rpt :: t1 -> t2 -> F t2 (bound at T8518.hs:17:9)
diff --git a/testsuite/tests/indexed-types/should_fail/T9662.stderr b/testsuite/tests/indexed-types/should_fail/T9662.stderr
index e2f7597b93..9584311636 100644
--- a/testsuite/tests/indexed-types/should_fail/T9662.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9662.stderr
@@ -1,13 +1,13 @@
 
 T9662.hs:49:8: error:
-    • Couldn't match type ‘n’ with ‘Int’
+    • Couldn't match type ‘k’ with ‘Int’
       Expected: Exp (((sh :. k) :. m) :. n)
                 -> Exp (((sh :. m) :. n) :. k)
         Actual: Exp
                   (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int))
                 -> Exp
                      (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int))
-      ‘n’ is a rigid type variable bound by
+      ‘k’ is a rigid type variable bound by
         the type signature for:
           test :: forall sh k m n.
                   Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index dd87053e5a..c5321fc455 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -58,9 +58,9 @@ test('T3330a', normal, compile_fail, [''])
 test('T3330b', normal, compile_fail, [''])
 test('T3330c', normal, compile_fail, [''])
 test('T4179', normal, compile_fail, [''])
-test('T4254', normal, compile, [''])
+test('T4254b', normal, compile_fail, [''])
 test('T2239', normal, compile, [''])
-test('T3440', normal, compile_fail, [''])
+test('T3440', expect_broken(19974), compile_fail, [''])
 test('T4485', normal, compile_fail, [''])
 test('T4174', normal, compile_fail, [''])
 test('DerivUnsatFam', normal, compile_fail, [''])
diff --git a/testsuite/tests/linters/notes.stdout b/testsuite/tests/linters/notes.stdout
index 8493d1ea4c..8e4ad38ac8 100644
--- a/testsuite/tests/linters/notes.stdout
+++ b/testsuite/tests/linters/notes.stdout
@@ -107,7 +107,6 @@ ref    compiler/GHC/Tc/Utils/Env.hs:1141:0:     Note [Generating fresh names for
 ref    compiler/GHC/Tc/Utils/Env.hs:1192:7:     Note [Placeholder PatSyn kinds]
 ref    compiler/GHC/Tc/Utils/TcMType.hs:793:7:     Note [Kind checking for GADTs]
 ref    compiler/GHC/Tc/Utils/TcType.hs:529:7:     Note [TyVars and TcTyVars]
-ref    compiler/GHC/Tc/Utils/Unify.hs:1489:7:     Note [Unification preconditions, (TYVAR-TV)]
 ref    compiler/GHC/ThToHs.hs:1738:11:     Note [Adding parens for splices]
 ref    compiler/GHC/ThToHs.hs:1749:3:     Note [Adding parens for splices]
 ref    compiler/GHC/Types/Basic.hs:586:17:     Note [Safe Haskell isSafeOverlap]
diff --git a/testsuite/tests/partial-sigs/should_compile/InstanceGivenOverlap3.hs b/testsuite/tests/partial-sigs/should_compile/InstanceGivenOverlap3.hs
new file mode 100644
index 0000000000..be4cd92ed9
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/InstanceGivenOverlap3.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE PartialTypeSignatures, FlexibleContexts #-}
+
+module InstanceGivenOverlap3 where
+
+f :: Eq [a] => a -> _
+f x = x
diff --git a/testsuite/tests/partial-sigs/should_compile/T10403.stderr b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
index fd38a126c2..38f562a516 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10403.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
@@ -15,17 +15,34 @@ T10403.hs:16:12: warning: [-Wpartial-type-signatures (in -Wdefault)]
 
 T10403.hs:20:7: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’
-        standing for ‘(a1 -> a2) -> B t0 a1 -> H (B t0)’
-      Where: ‘t0’ is an ambiguous type variable
+        standing for ‘(a1 -> a2) -> f0 a1 -> H f0’
+      Where: ‘f0’ is an ambiguous type variable
              ‘a2’, ‘a1’ are rigid type variables bound by
-               the inferred type of h2 :: (a1 -> a2) -> B t0 a1 -> H (B t0)
+               the inferred type of h2 :: (a1 -> a2) -> f0 a1 -> H f0
                at T10403.hs:23:1-41
     • In the type signature: h2 :: _
 
+T10403.hs:23:15: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Ambiguous type variable ‘f0’ arising from a use of ‘fmap’
+      prevents the constraint ‘(Functor f0)’ from being solved.
+      Relevant bindings include
+        b :: f0 a1 (bound at T10403.hs:23:6)
+        h2 :: (a1 -> a2) -> f0 a1 -> H f0 (bound at T10403.hs:23:1)
+      Probable fix: use a type annotation to specify what ‘f0’ should be.
+      Potentially matching instances:
+        instance Functor IO -- Defined in ‘GHC.Base’
+        instance Functor (B t) -- Defined at T10403.hs:11:10
+        ...plus 8 others
+        ...plus one instance involving out-of-scope types
+        (use -fprint-potential-instances to see them all)
+    • In the second argument of ‘(.)’, namely ‘fmap (const ())’
+      In the expression: (H . fmap (const ())) (fmap f b)
+      In an equation for ‘h2’: h2 f b = (H . fmap (const ())) (fmap f b)
+
 T10403.hs:29:8: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Couldn't match type ‘t0’ with ‘t’
+    • Couldn't match type ‘f0’ with ‘B t’
       Expected: H (B t)
-        Actual: H (B t0)
+        Actual: H f0
     • because type variable ‘t’ would escape its scope
     This (rigid, skolem) type variable is bound by
       the type signature for:
diff --git a/testsuite/tests/partial-sigs/should_compile/all.T b/testsuite/tests/partial-sigs/should_compile/all.T
index e38358f88a..bb7c58a576 100644
--- a/testsuite/tests/partial-sigs/should_compile/all.T
+++ b/testsuite/tests/partial-sigs/should_compile/all.T
@@ -102,3 +102,4 @@ test('T16762d', normal, compile, [''])
 test('T14658', normal, compile, [''])
 test('T18646', normal, compile, [''])
 test('T20921', normal, compile, [''])
+test('InstanceGivenOverlap3', expect_broken(20076), compile, [''])
diff --git a/testsuite/tests/partial-sigs/should_fail/NamedWildcardsNotInMonotype.stderr b/testsuite/tests/partial-sigs/should_fail/NamedWildcardsNotInMonotype.stderr
index 423fe1b040..69128accaf 100644
--- a/testsuite/tests/partial-sigs/should_fail/NamedWildcardsNotInMonotype.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/NamedWildcardsNotInMonotype.stderr
@@ -6,6 +6,12 @@ NamedWildcardsNotInMonotype.hs:5:1: error:
                    forall {a} {w}. (Show a, Eq w, Eq a) => a -> a -> String
         at NamedWildcardsNotInMonotype.hs:5:1-33
       The type variable ‘w0’ is ambiguous
+      Potentially matching instances:
+        instance Eq Ordering -- Defined in ‘GHC.Classes’
+        instance Eq () -- Defined in ‘GHC.Classes’
+        ...plus 22 others
+        ...plus four instances involving out-of-scope types
+        (use -fprint-potential-instances to see them all)
     • In the ambiguity check for the inferred type for ‘foo’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       When checking the inferred type
diff --git a/testsuite/tests/partial-sigs/should_fail/T10999.stderr b/testsuite/tests/partial-sigs/should_fail/T10999.stderr
index d6fe29c811..4942fb9f8a 100644
--- a/testsuite/tests/partial-sigs/should_fail/T10999.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T10999.stderr
@@ -17,10 +17,10 @@ T10999.hs:5:17: error:
       In the type signature: f :: _ => () -> _
 
 T10999.hs:8:28: error:
-    • Ambiguous type variable ‘b0’ arising from a use of ‘f’
-      prevents the constraint ‘(Ord b0)’ from being solved.
-      Relevant bindings include g :: [b0] (bound at T10999.hs:8:1)
-      Probable fix: use a type annotation to specify what ‘b0’ should be.
+    • Ambiguous type variable ‘b1’ arising from a use of ‘f’
+      prevents the constraint ‘(Ord b1)’ from being solved.
+      Relevant bindings include g :: [b1] (bound at T10999.hs:8:1)
+      Probable fix: use a type annotation to specify what ‘b1’ should be.
       Potentially matching instances:
         instance Ord a => Ord (Set.Set a) -- Defined in ‘Data.Set.Internal’
         instance Ord Ordering -- Defined in ‘GHC.Classes’
diff --git a/testsuite/tests/partial-sigs/should_fail/T14584.stderr b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
index 9d0247f22b..7a47f25967 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14584.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
@@ -1,20 +1,9 @@
 
-T14584.hs:56:41: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Could not deduce (SingI a) arising from a use of ‘sing’
-      from the context: (Action act, Monoid a, Good m)
-        bound by the instance declaration at T14584.hs:54:10-89
-    • In the second argument of ‘fromSing’, namely
-        ‘(sing @m @a :: Sing _)’
-      In the fourth argument of ‘act’, namely
-        ‘(fromSing @m (sing @m @a :: Sing _))’
-      In the expression:
-        act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
-
 T14584.hs:56:50: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Could not deduce (m ~ *)
-      from the context: (Action act, Monoid a, Good m)
+    • Could not deduce (m1 ~ *)
+      from the context: (Action act, Monoid a, Good m1)
         bound by the instance declaration at T14584.hs:54:10-89
-      ‘m’ is a rigid type variable bound by
+      ‘m1’ is a rigid type variable bound by
         the instance declaration
         at T14584.hs:54:10-89
     • In the type ‘a’
@@ -24,8 +13,9 @@ T14584.hs:56:50: warning: [-Wdeferred-type-errors (in -Wdefault)]
         ‘(fromSing @m (sing @m @a :: Sing _))’
 
 T14584.hs:56:60: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘a :: m’
-      Where: ‘a’, ‘m’ are rigid type variables bound by
+    • Found type wildcard ‘_’ standing for ‘a0 :: m’
+      Where: ‘a0’ is an ambiguous type variable
+             ‘m’ is a rigid type variable bound by
                the instance declaration
                at T14584.hs:54:10-89
     • In the first argument of ‘Sing’, namely ‘_’
diff --git a/testsuite/tests/partial-sigs/should_fail/T14584a.stderr b/testsuite/tests/partial-sigs/should_fail/T14584a.stderr
index c3e957b9dd..febc57797d 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14584a.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14584a.stderr
@@ -1,10 +1,4 @@
 
-T14584a.hs:12:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Couldn't match expected type ‘()’ with actual type ‘m -> m’
-    • Probable cause: ‘id @m :: _’ is applied to too few arguments
-      In the expression: id @m :: _
-      In an equation for ‘f’: f = id @m :: _
-
 T14584a.hs:12:9: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Expected a type, but ‘m’ has kind ‘k’
       ‘k’ is a rigid type variable bound by
@@ -16,11 +10,7 @@ T14584a.hs:12:9: warning: [-Wdeferred-type-errors (in -Wdefault)]
       In an equation for ‘f’: f = id @m :: _
 
 T14584a.hs:12:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘m -> m’
-      Where: ‘m’, ‘k’ are rigid type variables bound by
-               the type signature for:
-                 f :: forall {k} (m :: k). ()
-               at T14584a.hs:11:1-17
+    • Found type wildcard ‘_’ standing for ‘()’
     • In an expression type signature: _
       In the expression: id @m :: _
       In an equation for ‘f’: f = id @m :: _
@@ -36,11 +26,3 @@ T14584a.hs:15:17: warning: [-Wdeferred-type-errors (in -Wdefault)]
       In the expression: id @m
       In an equation for ‘h’: h = id @m
     • Relevant bindings include h :: m -> m (bound at T14584a.hs:15:9)
-
-T14584a.hs:16:8: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Couldn't match expected type ‘()’ with actual type ‘m -> m’
-    • Probable cause: ‘h’ is applied to too few arguments
-      In the expression: h
-      In the expression: let h = id @m in h
-      In an equation for ‘g’: g = let h = id @m in h
-    • Relevant bindings include h :: m -> m (bound at T14584a.hs:15:9)
diff --git a/testsuite/tests/polykinds/T14172.stderr b/testsuite/tests/polykinds/T14172.stderr
index 2ad319592c..b4eb6302d0 100644
--- a/testsuite/tests/polykinds/T14172.stderr
+++ b/testsuite/tests/polykinds/T14172.stderr
@@ -11,9 +11,11 @@ T14172.hs:7:46: error:
       In the type ‘(a -> f b) -> g a -> f (h _)’
 
 T14172.hs:8:19: error:
-    • Couldn't match type ‘h’ with ‘Compose f'0 g'0’
-        arising from a use of ‘_Wrapping’
-      ‘h’ is a rigid type variable bound by
+    • Couldn't match type ‘a’ with ‘g'1 a'0’
+      Expected: (f'0 a -> f (f'0 b)) -> g a -> f (h a')
+        Actual: (Unwrapped (Compose f'0 g'1 a'0) -> f (Unwrapped (h a')))
+                -> Compose f'0 g'1 a'0 -> f (h a')
+      ‘a’ is a rigid type variable bound by
         the inferred type of
           traverseCompose :: (a -> f b) -> g a -> f (h a')
         at T14172.hs:7:1-47
diff --git a/testsuite/tests/polykinds/T9017.stderr b/testsuite/tests/polykinds/T9017.stderr
index 2070ea667e..ca6a4b564d 100644
--- a/testsuite/tests/polykinds/T9017.stderr
+++ b/testsuite/tests/polykinds/T9017.stderr
@@ -1,12 +1,12 @@
 
 T9017.hs:8:7: error:
-    • Couldn't match kind ‘k1’ with ‘*’
+    • Couldn't match kind ‘k2’ with ‘*’
       When matching types
         a0 :: * -> * -> *
         a :: k1 -> k2 -> *
       Expected: a b (m b)
         Actual: a0 b0 (m0 b0)
-      ‘k1’ is a rigid type variable bound by
+      ‘k2’ is a rigid type variable bound by
         the type signature for:
           foo :: forall {k1} {k2} (a :: k1 -> k2 -> *) (b :: k1)
                         (m :: k1 -> k2).
diff --git a/testsuite/tests/quantified-constraints/T21006.stderr b/testsuite/tests/quantified-constraints/T21006.stderr
index aa5c5ef9a2..6be755e4b0 100644
--- a/testsuite/tests/quantified-constraints/T21006.stderr
+++ b/testsuite/tests/quantified-constraints/T21006.stderr
@@ -1,7 +1,7 @@
 
 T21006.hs:14:10: error:
-    • Couldn't match kind ‘Constraint’ with ‘*’
-      When matching types
-        b :: *
-        c :: Constraint
+    • Could not deduce c
+        arising from the superclasses of an instance declaration
+      from the context: (Determines b, Determines c)
+        bound by a quantified context at T21006.hs:14:10-15
     • In the instance declaration for ‘OpCode’
diff --git a/testsuite/tests/quotes/TH_localname.stderr b/testsuite/tests/quotes/TH_localname.stderr
index 246781a336..09cfae4b6e 100644
--- a/testsuite/tests/quotes/TH_localname.stderr
+++ b/testsuite/tests/quotes/TH_localname.stderr
@@ -1,25 +1,29 @@
 
 TH_localname.hs:3:11: error:
-    • Ambiguous type variable ‘m0’ arising from a quotation bracket
-      prevents the constraint ‘(Language.Haskell.TH.Syntax.Quote
-                                  m0)’ from being solved.
+    • Ambiguous type variable ‘t0’ arising from a use of ‘Language.Haskell.TH.Syntax.lift’
+      prevents the constraint ‘(Language.Haskell.TH.Syntax.Lift
+                                  t0)’ from being solved.
       Relevant bindings include
+        y :: t0 (bound at TH_localname.hs:3:6)
         x :: t0 -> m0 Language.Haskell.TH.Syntax.Exp
           (bound at TH_localname.hs:3:1)
-      Probable fix: use a type annotation to specify what ‘m0’ should be.
-      Potentially matching instance:
-        instance Language.Haskell.TH.Syntax.Quote IO
+      Probable fix: use a type annotation to specify what ‘t0’ should be.
+      Potentially matching instances:
+        instance (Language.Haskell.TH.Syntax.Lift a,
+                  Language.Haskell.TH.Syntax.Lift b) =>
+                 Language.Haskell.TH.Syntax.Lift (Either a b)
           -- Defined in ‘Language.Haskell.TH.Syntax’
-        ...plus one instance involving out-of-scope types
+        instance Language.Haskell.TH.Syntax.Lift a =>
+                 Language.Haskell.TH.Syntax.Lift (Maybe a)
+          -- Defined in ‘Language.Haskell.TH.Syntax’
+        ...plus 15 others
+        ...plus 12 instances involving out-of-scope types
         (use -fprint-potential-instances to see them all)
-    • In the expression:
+    • In the expression: Language.Haskell.TH.Syntax.lift y
+      In the expression:
         [| y |]
         pending(rn) [<y, Language.Haskell.TH.Syntax.lift y>]
       In the expression:
         \ y
           -> [| y |]
              pending(rn) [<y, Language.Haskell.TH.Syntax.lift y>]
-      In an equation for ‘x’:
-          x = \ y
-                -> [| y |]
-                   pending(rn) [<y, Language.Haskell.TH.Syntax.lift y>]
diff --git a/testsuite/tests/tcplugins/ArgsPlugin.hs b/testsuite/tests/tcplugins/ArgsPlugin.hs
index 19e99bedd0..cb193db05b 100644
--- a/testsuite/tests/tcplugins/ArgsPlugin.hs
+++ b/testsuite/tests/tcplugins/ArgsPlugin.hs
@@ -56,9 +56,9 @@ plugin = mkPlugin solver don'tRewrite
 -- Solve "MyClass Integer" with a class dictionary that depends on
 -- a plugin argument.
 solver :: [String]
-       -> PluginDefs -> EvBindsVar -> [Ct] -> [Ct] -> [Ct]
+       -> PluginDefs -> EvBindsVar -> [Ct] -> [Ct]
        -> TcPluginM TcPluginSolveResult
-solver args defs _ev _gs _ds ws = do
+solver args defs _ev _gs ws = do
   let
     argsVal :: Integer
     argsVal = case args of
diff --git a/testsuite/tests/tcplugins/Common.hs b/testsuite/tests/tcplugins/Common.hs
index 3ccc9a4a1b..f2f425381d 100644
--- a/testsuite/tests/tcplugins/Common.hs
+++ b/testsuite/tests/tcplugins/Common.hs
@@ -89,7 +89,7 @@ lookupDefs = do
   add                           <- tcLookupTyCon   =<< lookupOrig defs ( mkTcOcc   "Add"      )
   pure ( PluginDefs { .. } )
 
-mkPlugin :: ( [String] -> PluginDefs -> EvBindsVar -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult )
+mkPlugin :: ( [String] -> PluginDefs -> EvBindsVar -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult )
          -> ( [String] -> PluginDefs -> UniqFM TyCon TcPluginRewriter )
          -> Plugin
 mkPlugin solve rewrite =
@@ -98,7 +98,7 @@ mkPlugin solve rewrite =
     , pluginRecompile = purePlugin
     }
 
-mkTcPlugin :: ( PluginDefs -> EvBindsVar -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult )
+mkTcPlugin :: ( PluginDefs -> EvBindsVar -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult )
            -> ( PluginDefs -> UniqFM TyCon TcPluginRewriter )
            -> TcPlugin
 mkTcPlugin solve rewrite =
@@ -109,8 +109,8 @@ mkTcPlugin solve rewrite =
     , tcPluginStop    = \ _ -> pure ()
     }
 
-don'tSolve :: [String] -> s -> EvBindsVar -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult
-don'tSolve _ _ _ _ _ _ = pure $ TcPluginOk [] []
+don'tSolve :: [String] -> s -> EvBindsVar -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult
+don'tSolve _ _ _ _ _ = pure $ TcPluginOk [] []
 
 don'tRewrite :: [String] -> s -> UniqFM TyCon TcPluginRewriter
 don'tRewrite _ _ = emptyUFM
diff --git a/testsuite/tests/tcplugins/EmitWantedPlugin.hs b/testsuite/tests/tcplugins/EmitWantedPlugin.hs
index d5175dc13e..744c76623b 100644
--- a/testsuite/tests/tcplugins/EmitWantedPlugin.hs
+++ b/testsuite/tests/tcplugins/EmitWantedPlugin.hs
@@ -54,9 +54,9 @@ plugin = mkPlugin solver don'tRewrite
 -- emits a new Wanted equality @ty ~ ()@, and solves the
 -- @MyClass ty@ constraint using it.
 solver :: [String]
-       -> PluginDefs -> EvBindsVar -> [Ct] -> [Ct] -> [Ct]
+       -> PluginDefs -> EvBindsVar -> [Ct] -> [Ct]
        -> TcPluginM TcPluginSolveResult
-solver args defs _ev _gs _ds ws = do
+solver args defs _ev _gs ws = do
   (solved, new) <- unzip . catMaybes <$> traverse ( solveCt defs ) ws
   pure $ TcPluginOk solved new
 
diff --git a/testsuite/tests/tcplugins/NullaryPlugin.hs b/testsuite/tests/tcplugins/NullaryPlugin.hs
index 060c1aa2f2..742054fcda 100644
--- a/testsuite/tests/tcplugins/NullaryPlugin.hs
+++ b/testsuite/tests/tcplugins/NullaryPlugin.hs
@@ -42,9 +42,9 @@ plugin = mkPlugin solver don'tRewrite
 
 -- Solve "Nullary".
 solver :: [String]
-       -> PluginDefs -> EvBindsVar -> [Ct] -> [Ct] -> [Ct]
+       -> PluginDefs -> EvBindsVar -> [Ct] -> [Ct]
        -> TcPluginM TcPluginSolveResult
-solver _args defs _ev _gs _ds ws = do
+solver _args defs _ev _gs ws = do
   solved <- catMaybes <$> traverse ( solveCt defs ) ws
   pure $ TcPluginOk solved []
 
diff --git a/testsuite/tests/tcplugins/RewritePerfPlugin.hs b/testsuite/tests/tcplugins/RewritePerfPlugin.hs
index 036d89129c..b2fab46eb5 100644
--- a/testsuite/tests/tcplugins/RewritePerfPlugin.hs
+++ b/testsuite/tests/tcplugins/RewritePerfPlugin.hs
@@ -84,7 +84,7 @@ rewritingPlugin :: TcPlugin
 rewritingPlugin =
   TcPlugin
     { tcPluginInit    = lookupDefs
-    , tcPluginSolve   = \ _ _ _ _ _ -> pure $ TcPluginOk [] []
+    , tcPluginSolve   = \ _ _ _ _ -> pure $ TcPluginOk [] []
     , tcPluginRewrite = rewriter
     , tcPluginStop    = \ _ -> pure ()
     }
diff --git a/testsuite/tests/tcplugins/TyFamPlugin.hs b/testsuite/tests/tcplugins/TyFamPlugin.hs
index 1ae0390df0..c7d5d75d42 100644
--- a/testsuite/tests/tcplugins/TyFamPlugin.hs
+++ b/testsuite/tests/tcplugins/TyFamPlugin.hs
@@ -60,9 +60,9 @@ plugin :: Plugin
 plugin = mkPlugin solver don'tRewrite
 
 solver :: [String]
-       -> PluginDefs -> EvBindsVar -> [Ct] -> [Ct] -> [Ct]
+       -> PluginDefs -> EvBindsVar -> [Ct] -> [Ct]
        -> TcPluginM TcPluginSolveResult
-solver _args defs _ev _gs _ds ws = do
+solver _args defs _ev _gs ws = do
   solved <- catMaybes <$> traverse ( solveCt defs ) ws
   pure $ TcPluginOk solved []
 
diff --git a/testsuite/tests/typecheck/no_skolem_info/T19752.stderr b/testsuite/tests/typecheck/no_skolem_info/T19752.stderr
index 9f0bc741da..702522c059 100644
--- a/testsuite/tests/typecheck/no_skolem_info/T19752.stderr
+++ b/testsuite/tests/typecheck/no_skolem_info/T19752.stderr
@@ -5,8 +5,6 @@ T19752.hs:12:10: error:
         bound by the type signature for:
                    f :: forall b. (F b ~ a) => a
         at T19752.hs:12:10-23
-      Expected: forall b. (F b ~ a) => a
-        Actual: forall b. (F b ~ a) => a
       ‘a’ is a rigid type variable bound by
         the type signature for:
           g :: forall a. a
diff --git a/testsuite/tests/typecheck/should_compile/FloatFDs.hs b/testsuite/tests/typecheck/should_compile/FloatFDs.hs
new file mode 100644
index 0000000000..d7d0e7f5e8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/FloatFDs.hs
@@ -0,0 +1,181 @@
+-- This is the original inspiration for #18398
+
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Text.Parsec.Expr
+-- Copyright   :  (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
+-- License     :  BSD-style (see the LICENSE file)
+--
+-- Maintainer  :  derek.a.elkins@gmail.com
+-- Stability   :  provisional
+-- Portability :  non-portable
+--
+-- A helper module to parse \"expressions\".
+-- Builds a parser given a table of operators and associativities.
+--
+-----------------------------------------------------------------------------
+
+module Text.Parsec.Expr
+    ( Assoc(..), Operator(..), OperatorTable
+    , buildExpressionParser
+    ) where
+
+import Data.Typeable ( Typeable )
+
+import Text.Parsec.Prim
+import Text.Parsec.Combinator
+
+-----------------------------------------------------------
+-- Assoc and OperatorTable
+-----------------------------------------------------------
+
+-- |  This data type specifies the associativity of operators: left, right
+-- or none.
+
+data Assoc                = AssocNone
+                          | AssocLeft
+                          | AssocRight
+   deriving ( Typeable )
+
+-- | This data type specifies operators that work on values of type @a@.
+-- An operator is either binary infix or unary prefix or postfix. A
+-- binary operator has also an associated associativity.
+
+data Operator s u m a   = Infix (ParsecT s u m (a -> a -> a)) Assoc
+                        | Prefix (ParsecT s u m (a -> a))
+                        | Postfix (ParsecT s u m (a -> a))
+#if MIN_VERSION_base(4,7,0)
+    deriving ( Typeable )
+#endif
+
+-- | An @OperatorTable s u m a@ is a list of @Operator s u m a@
+-- lists. The list is ordered in descending
+-- precedence. All operators in one list have the same precedence (but
+-- may have a different associativity).
+
+type OperatorTable s u m a = [[Operator s u m a]]
+
+-----------------------------------------------------------
+-- Convert an OperatorTable and basic term parser into
+-- a full fledged expression parser
+-----------------------------------------------------------
+
+-- | @buildExpressionParser table term@ builds an expression parser for
+-- terms @term@ with operators from @table@, taking the associativity
+-- and precedence specified in @table@ into account. Prefix and postfix
+-- operators of the same precedence can only occur once (i.e. @--2@ is
+-- not allowed if @-@ is prefix negate). Prefix and postfix operators
+-- of the same precedence associate to the left (i.e. if @++@ is
+-- postfix increment, than @-2++@ equals @-1@, not @-3@).
+--
+-- The @buildExpressionParser@ takes care of all the complexity
+-- involved in building expression parser. Here is an example of an
+-- expression parser that handles prefix signs, postfix increment and
+-- basic arithmetic.
+--
+-- >  expr    = buildExpressionParser table term
+-- >          <?> "expression"
+-- >
+-- >  term    =  parens expr
+-- >          <|> natural
+-- >          <?> "simple expression"
+-- >
+-- >  table   = [ [prefix "-" negate, prefix "+" id ]
+-- >            , [postfix "++" (+1)]
+-- >            , [binary "*" (*) AssocLeft, binary "/" (div) AssocLeft ]
+-- >            , [binary "+" (+) AssocLeft, binary "-" (-)   AssocLeft ]
+-- >            ]
+-- >
+-- >  binary  name fun assoc = Infix (do{ reservedOp name; return fun }) assoc
+-- >  prefix  name fun       = Prefix (do{ reservedOp name; return fun })
+-- >  postfix name fun       = Postfix (do{ reservedOp name; return fun })
+
+buildExpressionParser :: (Stream s m t)
+                      => OperatorTable s u m a
+                      -> ParsecT s u m a
+                      -> ParsecT s u m a
+{-# INLINABLE buildExpressionParser #-}
+buildExpressionParser operators simpleExpr
+    = foldl (makeParser) simpleExpr operators
+    where
+--      makeParser :: Stream s m t => ParsecT s u m a -> [Operator s u m a] -> ParsecT s u m a
+--      uncommenting this avoids the original problem, but we want to compile even
+--      without offering this hint
+      makeParser term ops
+        = let (rassoc,lassoc,nassoc
+               ,prefix,postfix)      = foldr splitOp ([],[],[],[],[]) ops
+
+              rassocOp   = choice rassoc
+              lassocOp   = choice lassoc
+              nassocOp   = choice nassoc
+              prefixOp   = choice prefix  <?> ""
+              postfixOp  = choice postfix <?> ""
+
+              ambiguous assoc op= try $
+                                  do{ _ <- op; fail ("ambiguous use of a " ++ assoc
+                                                     ++ " associative operator")
+                                    }
+
+              ambiguousRight    = ambiguous "right" rassocOp
+              ambiguousLeft     = ambiguous "left" lassocOp
+              ambiguousNon      = ambiguous "non" nassocOp
+
+              termP      = do{ pre  <- prefixP
+                             ; x    <- term
+                             ; post <- postfixP
+                             ; return (post (pre x))
+                             }
+
+              postfixP   = postfixOp <|> return id
+
+              prefixP    = prefixOp <|> return id
+
+              rassocP x  = do{ f <- rassocOp
+                             ; y  <- do{ z <- termP; rassocP1 z }
+                             ; return (f x y)
+                             }
+                           <|> ambiguousLeft
+                           <|> ambiguousNon
+                           -- <|> return x
+
+              rassocP1 x = rassocP x  <|> return x
+
+              lassocP x  = do{ f <- lassocOp
+                             ; y <- termP
+                             ; lassocP1 (f x y)
+                             }
+                           <|> ambiguousRight
+                           <|> ambiguousNon
+                           -- <|> return x
+
+              lassocP1 x = lassocP x <|> return x
+
+              nassocP x  = do{ f <- nassocOp
+                             ; y <- termP
+                             ;    ambiguousRight
+                              <|> ambiguousLeft
+                              <|> ambiguousNon
+                              <|> return (f x y)
+                             }
+                           -- <|> return x
+
+           in  do{ x <- termP
+                 ; rassocP x <|> lassocP  x <|> nassocP x <|> return x
+                   <?> "operator"
+                 }
+
+
+      splitOp (Infix op assoc) (rassoc,lassoc,nassoc,prefix,postfix)
+        = case assoc of
+            AssocNone  -> (rassoc,lassoc,op:nassoc,prefix,postfix)
+            AssocLeft  -> (rassoc,op:lassoc,nassoc,prefix,postfix)
+            AssocRight -> (op:rassoc,lassoc,nassoc,prefix,postfix)
+
+      splitOp (Prefix op) (rassoc,lassoc,nassoc,prefix,postfix)
+        = (rassoc,lassoc,nassoc,op:prefix,postfix)
+
+      splitOp (Postfix op) (rassoc,lassoc,nassoc,prefix,postfix)
+        = (rassoc,lassoc,nassoc,prefix,op:postfix)
diff --git a/testsuite/tests/typecheck/should_compile/FunDepOrigin1.hs b/testsuite/tests/typecheck/should_compile/FunDepOrigin1.hs
new file mode 100644
index 0000000000..39d90bb531
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/FunDepOrigin1.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts #-}
+
+module FunDepOrigin1 where
+
+class C a b | a -> b where
+  op :: a -> b -> b
+
+foo :: C Bool (Maybe a) => x -> Maybe a
+foo _ = op True Nothing
+
+bar :: C Bool [a] => x -> [a]
+bar _ = op False []
diff --git a/testsuite/tests/typecheck/should_compile/ImplicitParamFDs.hs b/testsuite/tests/typecheck/should_compile/ImplicitParamFDs.hs
new file mode 100644
index 0000000000..6ab7144803
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/ImplicitParamFDs.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE ImplicitParams #-}
+
+module ImplicitParamFDs where
+
+import Data.Char
+
+bar :: (?x::Bool) => Bool
+bar = ?x
+
+foo :: (?x::Int) => Bool
+foo = let ?x = True in bar
+
+quux :: (?x :: Char) => (Int, Bool)
+quux = (ord ?x, let ?x = True in ?x)
+
+flub :: (?x :: Int) => (Int, Integer)
+flub = (?x, let ?x = 5 in ?x)
diff --git a/testsuite/tests/typecheck/should_compile/T11462_Plugin.hs b/testsuite/tests/typecheck/should_compile/T11462_Plugin.hs
index fc6b3348fa..2c31225702 100644
--- a/testsuite/tests/typecheck/should_compile/T11462_Plugin.hs
+++ b/testsuite/tests/typecheck/should_compile/T11462_Plugin.hs
@@ -10,7 +10,7 @@ plugin = defaultPlugin { tcPlugin = Just . thePlugin }
 thePlugin :: [CommandLineOption] -> TcPlugin
 thePlugin opts = TcPlugin
   { tcPluginInit    = return ()
-  , tcPluginSolve   = \_ _ _ _ _ -> return $ TcPluginOk [] []
+  , tcPluginSolve   = \_ _ _ _ -> return $ TcPluginOk [] []
   , tcPluginRewrite = \_ -> emptyUFM
   , tcPluginStop    = \_ -> return ()
   }
diff --git a/testsuite/tests/typecheck/should_compile/T11525_Plugin.hs b/testsuite/tests/typecheck/should_compile/T11525_Plugin.hs
index 5aedad2a6b..e68ddbc0dc 100644
--- a/testsuite/tests/typecheck/should_compile/T11525_Plugin.hs
+++ b/testsuite/tests/typecheck/should_compile/T11525_Plugin.hs
@@ -10,7 +10,7 @@ plugin = defaultPlugin { tcPlugin = Just . thePlugin }
 thePlugin :: [CommandLineOption] -> TcPlugin
 thePlugin opts = TcPlugin
   { tcPluginInit    = return ()
-  , tcPluginSolve   = \_ _ _ _ _ -> return $ TcPluginOk [] []
+  , tcPluginSolve   = \_ _ _ _ -> return $ TcPluginOk [] []
   , tcPluginRewrite = \_ -> emptyUFM
   , tcPluginStop    = \_ -> return ()
   }
diff --git a/testsuite/tests/typecheck/should_compile/T13651.stderr b/testsuite/tests/typecheck/should_compile/T13651.stderr
index 72ed83da20..a25eedcbbc 100644
--- a/testsuite/tests/typecheck/should_compile/T13651.stderr
+++ b/testsuite/tests/typecheck/should_compile/T13651.stderr
@@ -1,6 +1,6 @@
 
 T13651.hs:12:8: error:
-    • Could not deduce (F cr (Bar h (Foo u)) ~ Bar h (Bar r u))
+    • Could not deduce (cs ~ Bar (Foo h) (Foo s))
       from the context: (F cr cu ~ Bar h (Bar r u),
                          F cu cs ~ Bar (Foo h) (Bar u s))
         bound by the type signature for:
@@ -8,12 +8,12 @@ T13651.hs:12:8: error:
                           (F cr cu ~ Bar h (Bar r u), F cu cs ~ Bar (Foo h) (Bar u s)) =>
                           Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> Foo (cr -> cs)
         at T13651.hs:(12,8)-(14,65)
-      Expected: forall cr cu h r u cs s.
-                (F cr cu ~ Bar h (Bar r u), F cu cs ~ Bar (Foo h) (Bar u s)) =>
-                Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> Foo (cr -> cs)
-        Actual: forall cr cu h r u cs s.
-                (F cr cu ~ Bar h (Bar r u), F cu cs ~ Bar (Foo h) (Bar u s)) =>
-                Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> Foo (cr -> cs)
+      ‘cs’ is a rigid type variable bound by
+        the type signature for:
+          foo :: forall cr cu h r u cs s.
+                 (F cr cu ~ Bar h (Bar r u), F cu cs ~ Bar (Foo h) (Bar u s)) =>
+                 Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> Foo (cr -> cs)
+        at T13651.hs:(12,8)-(14,65)
     • In the ambiguity check for ‘foo’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       In the type signature:
diff --git a/testsuite/tests/typecheck/should_compile/T18406b.hs b/testsuite/tests/typecheck/should_compile/T18406b.hs
new file mode 100644
index 0000000000..cf65684eee
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T18406b.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE ScopedTypeVariables, MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts #-}
+
+module Bug where
+
+class C a b | a -> b where
+  op :: a -> a
+
+foo :: forall a b. C a b => a -> b -> a
+foo x y = blah x
+  where
+    -- GHC should infer
+    -- blah :: a -> a
+    -- and not
+    -- blah :: forall b0. C a b0 => a -> a
+    blah z = [x,z] `seq` op z
diff --git a/testsuite/tests/typecheck/should_compile/T18406b.stderr b/testsuite/tests/typecheck/should_compile/T18406b.stderr
new file mode 100644
index 0000000000..4f7a47ea0e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T18406b.stderr
@@ -0,0 +1,54 @@
+TYPE SIGNATURES
+  foo :: forall a b. C a b => a -> b -> a
+  op :: forall a b. C a b => a -> a
+TYPE CONSTRUCTORS
+  class C{2} :: * -> * -> Constraint
+COERCION AXIOMS
+  axiom Bug.N:C :: forall a b. C a b = a -> a
+Dependent modules: []
+Dependent packages: [base-4.16.0.0]
+
+==================== Typechecker ====================
+Bug.$tcC
+  = GHC.Types.TyCon
+      12754692886077552850##64 18375870125396612007##64 Bug.$trModule
+      (GHC.Types.TrNameS "C"#) 0# $krep
+Bug.$tc'C:C
+  = GHC.Types.TyCon
+      302756782745842909##64 14248103394115774781##64 Bug.$trModule
+      (GHC.Types.TrNameS "'C:C"#) 2# $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepVar 0
+$krep [InlPrag=[~]] = GHC.Types.KindRepVar 1
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun GHC.Types.krep$* $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun GHC.Types.krep$* $krep
+$krep [InlPrag=[~]]
+  = GHC.Types.KindRepTyConApp
+      GHC.Types.$tcConstraint [] @GHC.Types.KindRep
+$krep [InlPrag=[~]]
+  = GHC.Types.KindRepTyConApp
+      Bug.$tcC
+      ((:) @GHC.Types.KindRep
+         $krep ((:) @GHC.Types.KindRep $krep [] @GHC.Types.KindRep))
+Bug.$trModule
+  = GHC.Types.Module
+      (GHC.Types.TrNameS "main"#) (GHC.Types.TrNameS "Bug"#)
+AbsBinds [] []
+  {Exports: [foo <= foo
+               wrap: <>]
+   Exported types: foo :: forall a b. C a b => a -> b -> a
+                   [LclId]
+   Binds: foo x y
+            = blah x
+            where
+                AbsBinds [] []
+                  {Exports: [blah <= blah
+                               wrap: <>]
+                   Exported types: blah :: a -> a
+                                   [LclId]
+                   Binds: blah z = [x, z] `seq` op z
+                   Evidence: [EvBinds{[W] $dC = $dC}]}
+   Evidence: [EvBinds{}]}
+
+
diff --git a/testsuite/tests/typecheck/should_compile/T18529.hs b/testsuite/tests/typecheck/should_compile/T18529.hs
new file mode 100644
index 0000000000..9f5238c363
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T18529.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, AllowAmbiguousTypes #-}
+
+module Bug where
+
+class C a b where
+  op :: a -> b -> ()
+
+-- GHC should infer
+-- foo :: (C a b0, Num b0) => a -> ()
+-- This might actually be callable, if we have e.g. instance b ~ Bool => C Int b
+foo x = op x 3
diff --git a/testsuite/tests/typecheck/should_compile/T18529.stderr b/testsuite/tests/typecheck/should_compile/T18529.stderr
new file mode 100644
index 0000000000..a0273795d7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T18529.stderr
@@ -0,0 +1,49 @@
+TYPE SIGNATURES
+  foo :: forall {a} {b}. (C a b, Num b) => a -> ()
+  op :: forall a b. C a b => a -> b -> ()
+TYPE CONSTRUCTORS
+  class C{2} :: * -> * -> Constraint
+COERCION AXIOMS
+  axiom Bug.N:C :: forall a b. C a b = a -> b -> ()
+Dependent modules: []
+Dependent packages: [base-4.16.0.0]
+
+==================== Typechecker ====================
+Bug.$tcC
+  = GHC.Types.TyCon
+      12754692886077552850##64 18375870125396612007##64 Bug.$trModule
+      (GHC.Types.TrNameS "C"#) 0# $krep
+Bug.$tc'C:C
+  = GHC.Types.TyCon
+      302756782745842909##64 14248103394115774781##64 Bug.$trModule
+      (GHC.Types.TrNameS "'C:C"#) 2# $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepVar 0
+$krep [InlPrag=[~]] = GHC.Types.KindRepVar 1
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun GHC.Types.krep$* $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun GHC.Types.krep$* $krep
+$krep [InlPrag=[~]]
+  = GHC.Types.KindRepTyConApp
+      GHC.Types.$tcConstraint [] @GHC.Types.KindRep
+$krep [InlPrag=[~]]
+  = GHC.Types.KindRepTyConApp GHC.Tuple.$tc() [] @GHC.Types.KindRep
+$krep [InlPrag=[~]]
+  = GHC.Types.KindRepTyConApp
+      Bug.$tcC
+      ((:) @GHC.Types.KindRep
+         $krep ((:) @GHC.Types.KindRep $krep [] @GHC.Types.KindRep))
+Bug.$trModule
+  = GHC.Types.Module
+      (GHC.Types.TrNameS "main"#) (GHC.Types.TrNameS "Bug"#)
+AbsBinds [a, b] [$dC, $dNum]
+  {Exports: [foo <= foo
+               wrap: <>]
+   Exported types: foo :: forall {a} {b}. (C a b, Num b) => a -> ()
+                   [LclId]
+   Binds: foo x = op @a @b $dC x 3
+   Evidence: [EvBinds{[W] $dC = $dC
+                      [W] $dNum = $dNum}]}
+
+
diff --git a/testsuite/tests/typecheck/should_compile/T18851d.hs b/testsuite/tests/typecheck/should_compile/T18851d.hs
new file mode 100644
index 0000000000..95ca539628
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T18851d.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE DataKinds, TypeApplications, GADTs #-}
+
+module T18851d where
+
+import GHC.TypeNats
+
+data VSucc n where
+  F :: VSucc (1 + n)
+
+foo :: VSucc n -> VSucc n -> VSucc n
+foo (F @n1) F = F @n1
diff --git a/testsuite/tests/typecheck/should_compile/T19665.hs b/testsuite/tests/typecheck/should_compile/T19665.hs
index a6ba719718..ed1282faaa 100644
--- a/testsuite/tests/typecheck/should_compile/T19665.hs
+++ b/testsuite/tests/typecheck/should_compile/T19665.hs
@@ -1,8 +1,7 @@
 {-# LANGUAGE ScopedTypeVariables, TypeApplications, TypeFamilies,
              RoleAnnotations, FlexibleContexts, AllowAmbiguousTypes #-}
 
--- See Note [Deriveds do rewrite Deriveds] in GHC.Tc.Types.Constraint
--- for commentary.
+-- See #19665 for commentary.
 
 module T19665 where
 
diff --git a/testsuite/tests/typecheck/should_compile/T20584b.hs b/testsuite/tests/typecheck/should_compile/T20584b.hs
index a3e3287265..10e419066d 100644
--- a/testsuite/tests/typecheck/should_compile/T20584b.hs
+++ b/testsuite/tests/typecheck/should_compile/T20584b.hs
@@ -22,3 +22,4 @@ secs k
                | t >= 1e2  = printf "%.1f %s" t u
                | t >= 1e1  = printf "%.2f %s" t u
                | otherwise = printf "%.3f %s" t u
+
diff --git a/testsuite/tests/typecheck/should_compile/T20668.hs b/testsuite/tests/typecheck/should_compile/T20668.hs
new file mode 100644
index 0000000000..bb76a324c9
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T20668.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeFamilies, NoMonoLocalBinds #-}
+  -- The NoMonoLocalBinds is needed because of #21023
+  -- If you are here after #21023 is fixed, consider removing the NoMonoLocalBinds.
+
+module T20668 where
+
+type family F a
+
+inject :: a -> F a
+inject = undefined
+
+x = [5]
+
+f y = [inject y, x]
diff --git a/testsuite/tests/typecheck/should_compile/T20922.hs b/testsuite/tests/typecheck/should_compile/T20922.hs
new file mode 100644
index 0000000000..915f6fe6ff
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T20922.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeApplications       #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
+module PatternsBug where
+
+import Data.Kind
+  ( Type )
+import Data.Proxy
+  ( Proxy(..) )
+import Data.Type.Equality
+  ( (:~:)(Refl) )
+import Unsafe.Coerce
+  ( unsafeCoerce )
+
+passGetterIndex
+  :: forall (js :: [Type]) (jss :: [[Type]]) (s :: Type) (as :: [Type])
+  . SSameLength js as -> HList js -> Viewers (js ': jss) s as -> Viewers jss s as
+passGetterIndex (SSameSucc ( same1 :: SSameLength t_js t_as ) ) js views =
+  case ( js, views ) of
+    ( (k :: j) :> (ks :: HList t_js), ConsViewer same2 (_ :: Proxy is) (_ :: Proxy iss) _ getters ) ->
+      case same2 of
+        ( sameSucc@(SSameSucc (same3 :: SSameLength t_is jss) ) ) ->
+          case sameSucc of
+            ( _ :: SSameLength (i ': t_is) (js ': jss) )
+              | Refl <- ( unsafeCoerce Refl :: ZipCons t_is (Tail iss) :~: jss )
+              , Refl <- ( unsafeCoerce Refl :: ( t_js ': MapTail jss ) :~: iss )
+              , Refl <- ( unsafeCoerce Refl :: i :~: j )
+          --    , Proxy :: Proxy bss <- Proxy @(Tail iss)
+              -> ConsViewer same3 (Proxy @t_is) (Proxy @(Tail iss)) Proxy
+          --      -> ConsViewer same3 (Proxy @t_is) (Proxy @bss) Proxy
+                ( passGetterIndex @t_js @(MapTail jss) @s @t_as same1 ks getters )
+
+data Viewers (iss :: [[Type]]) (s :: Type) (as :: [Type]) where
+  -- NilViewer ...
+  ConsViewer :: forall (is :: [Type]) (s :: Type) (a :: Type) (iss :: [[Type]]) (as :: [Type])
+             .  SSameLength is (ZipCons is iss)
+             -> Proxy is
+             -> Proxy iss
+             -> Proxy a
+             -> Viewers iss s as
+             -> Viewers (ZipCons is iss) s (a ': as)
+
+data SSameLength (is :: [k]) (js :: [l]) where
+  SSameZero :: SSameLength '[] '[]
+  SSameSucc :: SSameLength is js -> SSameLength (i ': is) (j ': js)
+
+infixr 3 :>
+data HList (as :: [Type]) where
+  HNil :: HList '[]
+  (:>) :: a -> HList as -> HList (a ': as)
+
+type family ListVariadic (as :: [Type]) (b :: Type) = (r :: Type) | r -> as b where
+
+type family ZipCons (as :: [k]) (bss :: [[k]]) = (r :: [[k]]) | r -> as bss where
+  ZipCons '[] '[] = '[]
+  ZipCons (a ': as) (bs ': bss) = (a ': bs) ': ZipCons as bss
+
+type family Tail (x :: [k]) :: [k] where
+  Tail (_ ': xs) = xs
+
+type family MapTail (x :: [[k]]) :: [[k]] where
+  MapTail '[]         = '[]
+  MapTail (xs ': xss) = Tail xs ': MapTail xss
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 39878e3ce6..1b1cb1ec5a 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -168,7 +168,6 @@ test('tc164', normal, compile, [''])
 test('tc165', normal, compile, [''])
 test('tc166', normal, compile, [''])
 test('tc167', normal, compile, [''])
-test('tc168', normal, compile_fail, [''])
 test('tc169', normal, compile, [''])
 
 test('tc170', [extra_files(['Tc170_Aux.hs'])], makefile_test, [])
@@ -237,7 +236,10 @@ test('tc227', normal, compile, [''])
 test('tc228', normal, compile, [''])
 test('tc229', normal, compile, [''])
 test('tc230', normal, compile, [''])
-test('tc231', normalise_version('base','ghc-prim'), compile, [''])
+
+test('tc231', normalise_version('base','ghc-prim'), compile_fail, [''])
+# Could go either way (see comments in the test itself)
+
 test('tc232', normal, compile, [''])
 test('tc233', normal, compile, [''])
 test('tc234', normal, compile, [''])
@@ -258,9 +260,6 @@ test('tc246', normal, compile, [''])
 test('tc247', normal, compile, [''])
 test('tc248', normal, compile, [''])
 
-test('FD1', normal, compile_fail, [''])
-test('FD2', normal, compile_fail, [''])
-test('FD3', normal, compile_fail, [''])
 test('FD4', normal, compile, [''])
 
 test('faxen', normal, compile, [''])
@@ -588,6 +587,7 @@ test('T13848', normal, compile, [''])
 test('T13871', normal, compile, [''])
 test('T13879', normal, compile, [''])
 test('T13881', normal, compile, [''])
+test('T18851d', normal, compile, [''])
 test('T13915a', expect_broken(15245), multimod_compile, ['T13915a', '-v0'])
 test('T13915b', expect_broken(15245), compile, [''])
 test('T13984', normal, compile, [''])
@@ -679,6 +679,7 @@ test('T15549b', normal, compile, [''])
 test('T16188', normal, compile, [''])
 test('T16204a', normal, compile, [''])
 test('T16204b', normal, compile, [''])
+test('T20668', normal, compile, [''])
 test('T16225', normal, compile, [''])
 test('T13951', normal, compile, [''])
 test('T16312', normal, compile, ['-O'])
@@ -716,7 +717,7 @@ test('T19186', normal, compile, [''])
 test('T17021a', normal, compile, [''])
 test('T17723', [], makefile_test, [])
 test('T17772', normal, compile, [''])
-test('T19665', expect_broken(19665), compile, [''])
+test('T19665', normal, compile, [''])
 test('T18005', normal, compile, [''])
 test('T18023', normal, compile, [''])
 test('T18036', normal, compile, [''])
@@ -739,6 +740,7 @@ test('T18118', normal, multimod_compile, ['T18118', '-v0'])
 test('T18412', normal, compile, [''])
 test('T18470', normal, compile, [''])
 test('T18308', normal, compile, [''])
+test('T20922', normal, compile, [''])
 test('T18323', normal, compile, [''])
 test('T19677', normal, compile, [''])
 test('T18585', normal, compile, [''])
@@ -754,7 +756,7 @@ test('T17812', normal, compile, [''])
 test('T17186', normal, compile, [''])
 test('CbvOverlap', normal, compile, [''])
 test('InstanceGivenOverlap', normal, compile, [''])
-test('InstanceGivenOverlap2', normal, compile_fail, [''])
+test('InstanceGivenOverlap2', expect_broken(20076), compile_fail, [''])
 test('T19044', normal, compile, [''])
 test('T19052', normal, compile, [''])
 test('LocalGivenEqs', normal, compile, [''])
@@ -811,3 +813,8 @@ test('T20946', normal, compile, [''])
 test('T20996', normal, compile, [''])
 test('T20732', normal, compile, [''])
 test('T21010', [extra_files(['T21010A.hs', 'T21010B.hs'])], multimod_compile, ['T21010.hs', '-v0'])
+test('FunDepOrigin1', normal, compile, [''])
+test('FloatFDs', normal, compile, [''])
+test('ImplicitParamFDs', normal, compile, [''])
+test('T18406b', normal, compile, ['-ddump-tc -fprint-explicit-foralls -dsuppress-uniques -fprint-typechecker-elaboration'])
+test('T18529', normal, compile, ['-ddump-tc -fprint-explicit-foralls -dsuppress-uniques -fprint-typechecker-elaboration'])
diff --git a/testsuite/tests/typecheck/should_compile/tc231.hs b/testsuite/tests/typecheck/should_compile/tc231.hs
index 9e91be3a6a..8a655e1c0e 100644
--- a/testsuite/tests/typecheck/should_compile/tc231.hs
+++ b/testsuite/tests/typecheck/should_compile/tc231.hs
@@ -5,12 +5,16 @@
 -- See #1456
 
 -- The key thing here is that foo should get the type
---     foo :: forall b s t1. (Zork s (Z [Char]) b)
---         => Q s (Z [Char]) t1 -> ST s ()
+--     foo :: forall s b chain. (Zork s (Z [Char]) b)
+--         => Q s (Z [Char]) chain -> ST s ()
 
 -- Note the quantification over 'b', which was previously
 -- omitted; see Note [Important subtlety in oclose] in GHC.Tc.Instance.FunDeps
+-- (Note removed in ecddaca17dccbe1d0b56220d838fce8bc4b97884, but you can
+-- find it in the history)
 
+-- June 2021: marking this test as should_fail again.
+-- See https://gitlab.haskell.org/ghc/ghc/-/issues/20064
 
 module ShouldCompile where
 
@@ -18,13 +22,13 @@ import GHC.ST
 
 data Q s a chain = Node s a chain
 
-data Z a  = Z  a
+data Z a = Z a
 
-s :: Q t (Z [Char]) t1 -> Q t (Z [Char]) t1
+s :: Q s (Z [Char]) chain -> Q s (Z [Char]) chain
 s = undefined
 
 class  Zork s a b | a -> b where
-  huh :: Q s a chain ->  ST s ()
+  huh :: Q s a chain -> ST s ()
 
+--foo :: Zork s (Z [Char]) b => Q s (Z [Char]) chain -> ST s ()
 foo b = huh (s b)
-
diff --git a/testsuite/tests/typecheck/should_compile/tc231.stderr b/testsuite/tests/typecheck/should_compile/tc231.stderr
index 16ed21fdd4..9eb532bc05 100644
--- a/testsuite/tests/typecheck/should_compile/tc231.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc231.stderr
@@ -1,18 +1,6 @@
-TYPE SIGNATURES
-  foo ::
-    forall {s} {b} {chain}.
-    Zork s (Z [Char]) b =>
-    Q s (Z [Char]) chain -> ST s ()
-  huh :: forall s a b chain. Zork s a b => Q s a chain -> ST s ()
-  s :: forall t t1. Q t (Z [Char]) t1 -> Q t (Z [Char]) t1
-TYPE CONSTRUCTORS
-  data type Q{3} :: * -> * -> * -> *
-  data type Z{1} :: * -> *
-  class Zork{3} :: * -> * -> * -> Constraint
-COERCION AXIOMS
-  axiom N:Zork :: Zork s a b = forall chain. Q s a chain -> ST s ()
-DATA CONSTRUCTORS
-  Z :: forall a. a -> Z a
-  Node :: forall s a chain. s -> a -> chain -> Q s a chain
-Dependent modules: []
-Dependent packages: [base-4.16.0.0]
+
+tc231.hs:34:9: error:
+    • No instance for (Zork s (Z [Char]) b0)
+        arising from a use of ‘huh’
+    • In the expression: huh (s b)
+      In an equation for ‘foo’: foo b = huh (s b)
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_compile/FD1.hs b/testsuite/tests/typecheck/should_fail/FD1.hs
index ef458e1ff5..39c45bfdb4 100644
--- a/testsuite/tests/typecheck/should_compile/FD1.hs
+++ b/testsuite/tests/typecheck/should_fail/FD1.hs
@@ -14,4 +14,3 @@ instance E a a
 
 plus :: (E a (Int -> Int)) => Int -> a
 plus x y = x + y
-
diff --git a/testsuite/tests/typecheck/should_compile/FD1.stderr b/testsuite/tests/typecheck/should_fail/FD1.stderr
index 64a01c43e1..64a01c43e1 100644
--- a/testsuite/tests/typecheck/should_compile/FD1.stderr
+++ b/testsuite/tests/typecheck/should_fail/FD1.stderr
diff --git a/testsuite/tests/typecheck/should_compile/FD2.hs b/testsuite/tests/typecheck/should_fail/FD2.hs
index f8732c846d..f8732c846d 100644
--- a/testsuite/tests/typecheck/should_compile/FD2.hs
+++ b/testsuite/tests/typecheck/should_fail/FD2.hs
diff --git a/testsuite/tests/typecheck/should_compile/FD2.stderr b/testsuite/tests/typecheck/should_fail/FD2.stderr
index a5462aa94e..a5462aa94e 100644
--- a/testsuite/tests/typecheck/should_compile/FD2.stderr
+++ b/testsuite/tests/typecheck/should_fail/FD2.stderr
diff --git a/testsuite/tests/typecheck/should_compile/FD3.hs b/testsuite/tests/typecheck/should_fail/FD3.hs
index 475e379c10..475e379c10 100644
--- a/testsuite/tests/typecheck/should_compile/FD3.hs
+++ b/testsuite/tests/typecheck/should_fail/FD3.hs
diff --git a/testsuite/tests/typecheck/should_compile/FD3.stderr b/testsuite/tests/typecheck/should_fail/FD3.stderr
index d7ac728b6c..d7ac728b6c 100644
--- a/testsuite/tests/typecheck/should_compile/FD3.stderr
+++ b/testsuite/tests/typecheck/should_fail/FD3.stderr
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_compile/tc168.hs b/testsuite/tests/typecheck/should_fail/tc168.hs
index caa2651d6b..48c765bdbf 100644
--- a/testsuite/tests/typecheck/should_compile/tc168.hs
+++ b/testsuite/tests/typecheck/should_fail/tc168.hs
@@ -10,7 +10,7 @@
 -- signature   g :: C a (b,c) => a -> b
 -- would fail
 
-module ShouldCompile where
+module ShouldFail where
 
 class C a b where { op :: a -> b }
 
diff --git a/testsuite/tests/typecheck/should_compile/tc168.stderr b/testsuite/tests/typecheck/should_fail/tc168.stderr
index 082cf3d96d..082cf3d96d 100644
--- a/testsuite/tests/typecheck/should_compile/tc168.stderr
+++ b/testsuite/tests/typecheck/should_fail/tc168.stderr
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)
diff --git a/testsuite/tests/typecheck/should_run/T3731.hs b/testsuite/tests/typecheck/should_run/T3731.hs
index 3024629eca..430434dfcb 100644
--- a/testsuite/tests/typecheck/should_run/T3731.hs
+++ b/testsuite/tests/typecheck/should_run/T3731.hs
@@ -8,6 +8,9 @@
 
 module Main (main) where
 
+-- June 2021: no longer compiles.
+-- See T3731_simple for a simpler test case which explains the situation.
+
 import Data.Typeable
 
 class Sat a where
diff --git a/testsuite/tests/typecheck/should_run/T3731.stderr b/testsuite/tests/typecheck/should_run/T3731.stderr
new file mode 100644
index 0000000000..fabf1af91d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T3731.stderr
@@ -0,0 +1,23 @@
+
+T3731.hs:4:15: warning: [-Wdeprecated-flags (in -Wdefault)]
+    -XOverlappingInstances is deprecated: instead use per-instance pragmas OVERLAPPING/OVERLAPPABLE/OVERLAPS
+
+T3731.hs:122:32: error:
+    • Could not deduce (Default a)
+        arising from a superclass required to satisfy ‘Data DefaultD a’,
+        arising from a use of ‘dataTypeOf’
+      from the context: Data DefaultD a
+        bound by the type signature for:
+                   defaultDefaultValue :: forall a. Data DefaultD a => a
+        at T3731.hs:119:1-43
+      Possible fix:
+        add (Default a) to the context of
+          the type signature for:
+            defaultDefaultValue :: forall a. Data DefaultD a => a
+    • In the second argument of ‘($)’, namely
+        ‘dataTypeOf defaultProxy res’
+      In the expression: datarep $ dataTypeOf defaultProxy res
+      In the expression:
+        case datarep $ dataTypeOf defaultProxy res of
+          AlgRep (c : _) -> fromConstrB defaultProxy (defaultValueD dict) c
+          AlgRep [] -> error "defaultDefaultValue: Bad DataRep"
diff --git a/testsuite/tests/typecheck/should_run/T3731_simple.hs b/testsuite/tests/typecheck/should_run/T3731_simple.hs
new file mode 100644
index 0000000000..c1f6758ebd
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T3731_simple.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE
+  FlexibleInstances,
+  UndecidableInstances
+#-}
+
+module Bug where
+
+class Default a
+class Sat a
+
+instance Default a => Sat a
+
+class Sat a => Data a where
+  dataTypeOf :: a -> a
+
+defaultDefaultValue :: Data a => a
+defaultDefaultValue = res
+    where
+      res = dataTypeOf res
+
+-- GHC does not infer the principal type for res,
+-- inferring (Default a, Data a) => a instead of Data a => a.
+-- See Note [Inferring principal types] in Ghc.Tc.Solver
+--
+-- This used to be fine, as "Default a" was a Derived constraint
+-- that could be dropped. Without Deriveds, we instead get a
+-- Wanted constraint, which can't be dropped.
+-- This means that this program no longer compiles.
+-- (Note that a type signature on "res" allows the program to
+-- compile again.)
diff --git a/testsuite/tests/typecheck/should_run/T3731_simple.stderr b/testsuite/tests/typecheck/should_run/T3731_simple.stderr
new file mode 100644
index 0000000000..912f019c02
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T3731_simple.stderr
@@ -0,0 +1,16 @@
+
+T3731_simple.hs:19:13: error:
+    • Could not deduce (Default a)
+        arising from a superclass required to satisfy ‘Data a’,
+        arising from a use of ‘dataTypeOf’
+      from the context: Data a
+        bound by the type signature for:
+                   defaultDefaultValue :: forall a. Data a => a
+        at T3731_simple.hs:16:1-34
+    • In the expression: dataTypeOf res
+      In an equation for ‘res’: res = dataTypeOf res
+      In an equation for ‘defaultDefaultValue’:
+          defaultDefaultValue
+            = res
+            where
+                res = dataTypeOf res
diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T
index a34fb61747..a465999b58 100755
--- a/testsuite/tests/typecheck/should_run/all.T
+++ b/testsuite/tests/typecheck/should_run/all.T
@@ -81,8 +81,13 @@ test('T16646', normal, compile_and_run, [''])
 # Support files for T1735 are in directory T1735_Help/
 test('T1735', normal, multimod_compile_and_run, ['T1735',''])
 
-test('T3731', normal, compile_and_run, [''])
+# The following two tests no longer compile
+# See Note [Inferring principal types] in Ghc.Tc.Solver
+test('T3731', normal, compile_fail, [''])
+test('T3731_simple', normal, compile_fail, [''])
+
 test('T3731-short', normal, compile_and_run, [''])
+
 test('T3500a', normal, compile_and_run, [''])
 test('T3500b', normal, compile_and_run, [''])
 test('T4809', normal, compile_and_run, [''])
author	Richard Eisenberg <rae@richarde.dev>	2022-02-18 23:29:52 +0100
committer	Marge Bot <ben+marge-bot@smart-cactus.org>	2022-02-23 08:16:07 -0500
commit	a599abbad939820c666ced00ae9eb33706a4f360 (patch)
tree	7b3811972a50da9e81018056cdcdeef158bc22e3 /testsuite/tests
parent	558c7d554b9724abfaa2bcc1f42050e67b36a988 (diff)
download	haskell-a599abbad939820c666ced00ae9eb33706a4f360.tar.gz