Re-engineer Given flatten-skolems

The big change here is to fix an outright bug in flattening of Givens,
albeit one that is very hard to exhibit.  Suppose we have the constraint
    forall a. (a ~ F b) => ..., (forall c. ....(F b)...) ...

Then
 - we'll flatten the (F) b to a fsk, say  (F b ~ fsk1)
 - we'll rewrite the (F b) inside the inner implication to 'fsk1'
 - when we leave the outer constraint we are suppose to unflatten;
   but that fsk1 will still be there
 - if we re-simplify the entire outer implication, we'll re-flatten
   the Given (F b) to, say, (F b ~ fsk2)
Now we have two fsks standing for the same thing, and that is very
wrong.

Solution: make fsks behave more like fmvs:
 - A flatten-skolem is now a MetaTyVar, whose MetaInfo is FlatSkolTv
 - We "fill in" that meta-tyvar when leaving the implication
 - The old FlatSkol form of TcTyVarDetails is gone completely
 - We track the flatten-skolems for the current implication in
   a new field of InertSet, inert_fsks.

See Note [The flattening story] in TcFlatten.

In doing this I found various other things to fix:

* I removed the zonkSimples from TcFlatten.unflattenWanteds; it wasn't
  needed.   But I added one in TcSimplify.floatEqualities, which does
  the zonk precisely when it is needed.

* Trac #13674 showed up a case where we had
     - an insoluble Given,   e.g.  a ~ [a]
     - the same insoluble Wanted   a ~ [a]
  We don't use the Given to rewwrite the Wanted (obviously), but
  we therefore ended up reporting
      Can't deduce (a ~ [a]) from (a ~ [a])
  which is silly.

  Conclusion: when reporting errors, make the occurs check "win"
  See Note [Occurs check wins] in TcErrors

26 files changed, 321 insertions, 187 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 5dddd5da0c..77bf63d98e 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1538,7 +1538,7 @@ Suppose we have  [G] Num (F [a])
 then we flatten to
      [G] Num fsk
      [G] F [a] ~ fsk
-where fsk is a flatten-skolem (FlatSkol). Suppose we have
+where fsk is a flatten-skolem (FlatSkolTv). Suppose we have
       type instance F [a] = a
 then we'll reduce the second constraint to
      [G] a ~ fsk
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index eacdbb682f..c9e07fc43d 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -1466,7 +1466,7 @@ mkEqErr1 ctxt ct   -- Wanted or derived;
                NomEq  -> empty
                ReprEq -> mkCoercibleExplanation rdr_env fam_envs ty1 ty2
        ; dflags <- getDynFlags
-       ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct))
+       ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct) $$ ppr keep_going)
        ; let report = mconcat [important wanted_msg, important coercible_msg,
                                relevant_bindings binds_msg]
        ; if keep_going
@@ -1604,15 +1604,21 @@ reportEqErr ctxt report ct oriented ty1 ty2
   where misMatch = important $ misMatchOrCND ctxt ct oriented ty1 ty2
         eqInfo = important $ mkEqInfoMsg ct ty1 ty2
 
-mkTyVarEqErr :: DynFlags -> ReportErrCtxt -> Report -> Ct
+mkTyVarEqErr, mkTyVarEqErr'
+  :: DynFlags -> ReportErrCtxt -> Report -> Ct
              -> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg
 -- tv1 and ty2 are already tidied
 mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
-  | isUserSkolem ctxt tv1   -- ty2 won't be a meta-tyvar, or else the thing would
+  = do { traceTc "mkTyVarEqErr" (ppr ct $$ ppr tv1 $$ ppr ty2)
+       ; mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 }
+
+mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2
+  | not insoluble_occurs_check   -- See Note [Occurs check wins]
+  , isUserSkolem ctxt tv1   -- ty2 won't be a meta-tyvar, or else the thing would
                             -- be oriented the other way round;
                             -- see TcCanonical.canEqTyVarTyVar
-  || isSigTyVar tv1 && not (isTyVarTy ty2)
-  || ctEqRel ct == ReprEq && not insoluble_occurs_check
+    || isSigTyVar tv1 && not (isTyVarTy ty2)
+    || ctEqRel ct == ReprEq
      -- the cases below don't really apply to ReprEq (except occurs check)
   = mkErrorMsgFromCt ctxt ct $ mconcat
         [ important $ misMatchOrCND ctxt ct oriented ty1 ty2
@@ -1827,7 +1833,6 @@ extraTyVarInfo ctxt tv
   = ASSERT2( isTyVar tv, ppr tv )
     case tcTyVarDetails tv of
           SkolemTv {}   -> pprSkol implics tv
-          FlatSkol {}   -> pp_tv <+> text "is a flattening type variable"
           RuntimeUnk {} -> pp_tv <+> text "is an interactive-debugger skolem"
           MetaTv {}     -> empty
   where
@@ -2016,7 +2021,22 @@ mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
 
 mkExpectedActualMsg _ _ _ _ _ = panic "mkExpectedAcutalMsg"
 
-{-
+{- Note [Insoluble occurs check wins]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider [G] a ~ [a],  [W] a ~ [a] (Trac #13674).  The Given is insoluble
+so we don't use it for rewriting.  The Wanted is also insoluble, and
+we don't solve it from the Given.  It's very confusing to say
+    Cannot solve a ~ [a] from given constraints a ~ [a]
+
+And indeed even thinking about the Givens is silly; [W] a ~ [a] is
+just as insoluble as Int ~ Bool.
+
+Conclusion: if there's an insoluble occurs check (isInsolubleOccursCheck)
+then report it first.
+
+(NB: there are potentially-soluble ones, like (a ~ F a b), and we don't
+wnat to be as draconian with them.)
+
 Note [Expanding type synonyms to make types similar]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index dc211c61e4..650cbd8219 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -4,7 +4,7 @@ module TcFlatten(
    FlattenMode(..),
    flatten, flattenManyNom,
 
-   unflatten,
+   unflattenWanteds
  ) where
 
 #include "HsVersions.h"
@@ -36,31 +36,50 @@ import Control.Arrow ( first )
 Note [The flattening story]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 * A CFunEqCan is either of form
-     [G] <F xis> : F xis ~ fsk   -- fsk is a FlatSkol
-     [W]       x : F xis ~ fmv   -- fmv is a unification variable,
-                                 -- but untouchable,
-                                 -- with MetaInfo = FlatMetaTv
+     [G] <F xis> : F xis ~ fsk   -- fsk is a FlatSkolTv
+     [W]       x : F xis ~ fmv   -- fmv is a FlatMetaTv
   where
      x is the witness variable
-     fsk/fmv is a flatten skolem
      xis are function-free
-  CFunEqCans are always [Wanted], or [Given], never [Derived]
+     fsk/fmv is a flatten skolem;
+        it is always untouchable (level 0)
 
-  fmv untouchable just means that in a CTyVarEq, say,
-       fmv ~ Int
-  we do NOT unify fmv.
+* CFunEqCans can have any flavour: [G], [W], [WD] or [D]
 
 * KEY INSIGHTS:
 
    - A given flatten-skolem, fsk, is known a-priori to be equal to
-     F xis (the LHS), with <F xis> evidence
+     F xis (the LHS), with <F xis> evidence.  The fsk is still a
+     unification variable, but it is "owned" by its CFunEqCan, and
+     is filled in (unflattened) only by unflattenGivens.
 
    - A unification flatten-skolem, fmv, stands for the as-yet-unknown
-     type to which (F xis) will eventually reduce
+     type to which (F xis) will eventually reduce.  It is filled in
+     only by dischargeFmv.
 
-* Inert set invariant: if F xis1 ~ fsk1, F xis2 ~ fsk2
-                       then xis1 /= xis2
-  i.e. at most one CFunEqCan with a particular LHS
+   - All fsk/fmv variables are "untouchable".  To make it simple to test,
+     we simply give them TcLevel=0.  This means that in a CTyVarEq, say,
+       fmv ~ Int
+     we NEVER unify fmv.
+
+   - A unification flatten-skolems, fmv, ONLY gets unified when either
+       a) The CFunEqCan takes a step, using an axiom
+       b) By unflattenWanteds
+    They are never unified in any other form of equality.
+    For example [W] ffmv ~ Int  is stuck; it does not unify with fmv.
+
+* We *never* substitute in the RHS (i.e. the fsk/fmv) of a CFunEqCan.
+  That would destroy the invariant about the shape of a CFunEqCan,
+  and it would risk wanted/wanted interactions. The only way we
+  learn information about fsk is when the CFunEqCan takes a step.
+
+  However we *do* substitute in the LHS of a CFunEqCan (else it
+  would never get to fire!)
+
+* Unflattening:
+   - We unflatten Givens when leaving their scope (see unflattenGivens)
+   - We unflatten Wanteds at the end of each attempt to simplify the
+     wanteds; see unflattenWanteds, called from solveSimpleWanteds.
 
 * Each canonical [G], [W], or [WD] CFunEqCan x : F xis ~ fsk/fmv
   has its own distinct evidence variable x and flatten-skolem fsk/fmv.
@@ -70,7 +89,11 @@ Note [The flattening story]
   In contrast a [D] CFunEqCan shares its fmv with its partner [W],
   but does not "own" it.  If we reduce a [D] F Int ~ fmv, where
   say type instance F Int = ty, then we don't discharge fmv := ty.
-  Rather we simply generate [D] fmv ~ ty
+  Rather we simply generate [D] fmv ~ ty (in TcInteract.reduce_top_fun_eq)
+
+* Inert set invariant: if F xis1 ~ fsk1, F xis2 ~ fsk2
+                       then xis1 /= xis2
+  i.e. at most one CFunEqCan with a particular LHS
 
 * Function applications can occur in the RHS of a CTyEqCan.  No reason
   not allow this, and it reduces the amount of flattening that must occur.
@@ -104,20 +127,6 @@ Note [The flattening story]
     - Add new wanted to flat cache
     - Discharge x = F cos ; x2
 
-* Unification flatten-skolems, fmv, ONLY get unified when either
-    a) The CFunEqCan takes a step, using an axiom
-    b) During un-flattening
-  They are never unified in any other form of equality.
-  For example [W] ffmv ~ Int  is stuck; it does not unify with fmv.
-
-* We *never* substitute in the RHS (i.e. the fsk/fmv) of a CFunEqCan.
-  That would destroy the invariant about the shape of a CFunEqCan,
-  and it would risk wanted/wanted interactions. The only way we
-  learn information about fsk is when the CFunEqCan takes a step.
-
-  However we *do* substitute in the LHS of a CFunEqCan (else it
-  would never get to fire!)
-
 * [Interacting rule]
     (inert)     [W] x1 : F tys ~ fmv1
     (work item) [W] x2 : F tys ~ fmv2
@@ -1476,8 +1485,8 @@ flattens to
 We must solve both!
 -}
 
-unflatten :: Cts -> Cts -> TcS Cts
-unflatten tv_eqs funeqs
+unflattenWanteds :: Cts -> Cts -> TcS Cts
+unflattenWanteds tv_eqs funeqs
  = do { tclvl    <- getTcLevel
 
       ; traceTcS "Unflattening" $ braces $
@@ -1506,10 +1515,7 @@ unflatten tv_eqs funeqs
       ; let all_flat = tv_eqs `andCts` funeqs
       ; traceTcS "Unflattening done" $ braces (pprCts all_flat)
 
-          -- Step 5: zonk the result
-          -- Motivation: makes them nice and ready for the next step
-          --             (see TcInteract.solveSimpleWanteds)
-      ; zonkSimples all_flat }
+      ; return all_flat }
   where
     ----------------
     unflatten_funeq :: Ct -> Cts -> TcS Cts
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index 1b9fed98b6..b75d59be67 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -1557,7 +1557,6 @@ zonkTyVarOcc env@(ZonkEnv zonk_unbound_tyvar tv_env _) tv
   = case tcTyVarDetails tv of
          SkolemTv {}    -> lookup_in_env
          RuntimeUnk {}  -> lookup_in_env
-         FlatSkol ty    -> zonkTcTypeToType env ty
          MetaTv { mtv_ref = ref }
            -> do { cts <- readMutVar ref
                  ; case cts of
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 4368fcbb1b..83dc10cae4 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -160,6 +160,7 @@ solveSimpleGivens givens
 solveSimpleWanteds :: Cts -> TcS WantedConstraints
 -- NB: 'simples' may contain /derived/ equalities, floated
 --     out from a nested implication. So don't discard deriveds!
+-- The result is not necessarily zonked
 solveSimpleWanteds simples
   = do { traceTcS "solveSimpleWanteds {" (ppr simples)
        ; dflags <- getDynFlags
@@ -199,12 +200,13 @@ solveSimpleWanteds simples
 solve_simple_wanteds :: WantedConstraints -> TcS (Int, WantedConstraints)
 -- Try solving these constraints
 -- Affects the unification state (of course) but not the inert set
+-- The result is not necessarily zonked
 solve_simple_wanteds (WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
   = nestTcS $
     do { solveSimples simples1
        ; (implics2, tv_eqs, fun_eqs, insols2, others) <- getUnsolvedInerts
        ; (unif_count, unflattened_eqs) <- reportUnifications $
-                                          unflatten tv_eqs fun_eqs
+                                          unflattenWanteds tv_eqs fun_eqs
             -- See Note [Unflatten after solving the simple wanteds]
        ; return ( unif_count
                 , WC { wc_simple = others `andCts` unflattened_eqs
@@ -2241,6 +2243,13 @@ Other notes:
      - natural numbers
      - Typeable
 
+* Flatten-skolems: we do not treat a flatten-skolem as unifiable
+  for this purpose.
+  E.g.   f :: Eq (F a) => [a] -> [a]
+         f xs = ....(xs==xs).....
+  Here we get [W] Eq [a], and we don't want to refrain from solving
+  it because of the given (Eq (F a)) constraint!
+
 * The given-overlap problem is arguably not easy to appear in practice
   due to our aggressive prioritization of equality solving over other
   constraints, but it is possible. I've added a test case in
@@ -2274,7 +2283,7 @@ Other notes:
   in point.
 
 All of this is disgustingly delicate, so to discourage people from writing
-simplifiable class givens, we warn about signatures that contain them;#
+simplifiable class givens, we warn about signatures that contain them;
 see TcValidity Note [Simplifiable given constraints].
 -}
 
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 1ae90661a8..d26b25758e 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -550,8 +550,13 @@ instSkolTyCoVarX mk_tcv subst tycovar
 newFskTyVar :: TcType -> TcM TcTyVar
 newFskTyVar fam_ty
   = do { uniq <- newUnique
-       ; let name = mkSysTvName uniq (fsLit "fsk")
-       ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
+       ; ref  <- newMutVar Flexi
+       ; let details = MetaTv { mtv_info  = FlatSkolTv
+                              , mtv_ref   = ref
+                              , mtv_tclvl = fmvTcLevel }
+             name = mkMetaTyVarName uniq (fsLit "fsk")
+       ; return (mkTcTyVar name (typeKind fam_ty) details) }
+
 {-
 Note [Kind substitution when instantiating]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -593,10 +598,9 @@ newFmvTyVar :: TcType -> TcM TcTyVar
 newFmvTyVar fam_ty
   = do { uniq <- newUnique
        ; ref  <- newMutVar Flexi
-       ; cur_lvl <- getTcLevel
        ; let details = MetaTv { mtv_info  = FlatMetaTv
                               , mtv_ref   = ref
-                              , mtv_tclvl = fmvTcLevel cur_lvl }
+                              , mtv_tclvl = fmvTcLevel }
              name = mkMetaTyVarName uniq (fsLit "s")
        ; return (mkTcTyVar name (typeKind fam_ty) details) }
 
@@ -707,7 +711,7 @@ writeMetaTyVarRef tyvar ref ty
     tv_lvl = tcTyVarLevel tyvar
     ty_lvl = tcTypeLevel ty
 
-    level_check_ok = isFmvTyVar tyvar
+    level_check_ok = isFlattenTyVar tyvar
                   || not (ty_lvl `strictlyDeeperThan` tv_lvl)
     level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty
 
@@ -768,6 +772,7 @@ newAnonMetaTyVar meta_info kind
               s = case meta_info of
                         TauTv       -> fsLit "t"
                         FlatMetaTv  -> fsLit "fmv"
+                        FlatSkolTv  -> fsLit "fsk"
                         SigTv       -> fsLit "a"
         ; details <- newMetaDetails meta_info
         ; return (mkTcTyVar name kind details) }
@@ -998,7 +1003,7 @@ zonkQuantifiedTyVar tv
 
       MetaTv {} -> skolemiseUnboundMetaTyVar tv
 
-      _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
+      _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- RuntimeUnk
 
 defaultTyVar :: Bool      -- True <=> please default this kind variable to *
              -> TcTyVar   -- If it's a MetaTyVar then it is unbound
@@ -1490,7 +1495,6 @@ zonkTcTyVar tv
   = case tcTyVarDetails tv of
       SkolemTv {}   -> zonk_kind_and_return
       RuntimeUnk {} -> zonk_kind_and_return
-      FlatSkol ty   -> zonkTcType ty
       MetaTv { mtv_ref = ref }
          -> do { cts <- readMutVar ref
                ; case cts of
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index e5e9eb2245..e018d5d7b6 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -1589,8 +1589,8 @@ data Ct
         --    *never* over-saturated (because if so
         --    we should have decomposed)
 
-      cc_fsk    :: TcTyVar  -- [Given]  always a FlatSkol skolem
-                            -- [Wanted] always a FlatMetaTv unification variable
+      cc_fsk    :: TcTyVar  -- [Given]  always a FlatSkolTv
+                            -- [Wanted] always a FlatMetaTv
         -- See Note [The flattening story] in TcFlatten
     }
 
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index f7153f8d2a..434553dec1 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -52,7 +52,7 @@ module TcSMonad (
     getNoGivenEqs, setInertCans,
     getInertEqs, getInertCans, getInertGivens,
     getInertInsols,
-    emptyInert, getTcSInerts, setTcSInerts,
+    getTcSInerts, setTcSInerts,
     matchableGivens, prohibitedSuperClassSolve,
     getUnsolvedInerts,
     removeInertCts, getPendingScDicts,
@@ -383,6 +383,16 @@ data InertSet
               -- Canonical Given, Wanted, Derived
               -- Sometimes called "the inert set"
 
+       , inert_fsks :: [(TcTyVar, TcType)]
+              -- A list of (fsk, ty) pairs; we add one element when we flatten
+              -- a function application in a Given constraint, creating
+              -- a new fsk in newFlattenSkolem.  When leaving a nested scope,
+              -- unflattenGivens unifies fsk := ty
+              --
+              -- We could also get this info from inert_funeqs, filtered by
+              -- level, but it seems simpler and more direct to capture the
+              -- fsk as we generate them.
+
        , inert_flat_cache :: ExactFunEqMap (TcCoercion, TcType, CtFlavour)
               -- See Note [Type family equations]
               -- If    F tys :-> (co, rhs, flav),
@@ -421,6 +431,7 @@ emptyInert
                          , inert_irreds   = emptyCts
                          , inert_insols   = emptyCts }
        , inert_flat_cache    = emptyExactFunEqs
+       , inert_fsks          = []
        , inert_solved_dicts  = emptyDictMap }
 
 
@@ -1814,24 +1825,21 @@ getNoGivenEqs :: TcLevel          -- TcLevel of this implication
 -- See Note [When does an implication have given equalities?]
 getNoGivenEqs tclvl skol_tvs
   = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds
-                    , inert_funeqs = funeqs
                     , inert_insols = insols })
               <- getInertCans
-       ; let local_fsks = foldFunEqs add_fsk funeqs emptyVarSet
-
-             has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False
+       ; let has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False
                                       (iirreds `unionBags` insols)
-                          || anyDVarEnv (eqs_given_here local_fsks) ieqs
+                          || anyDVarEnv eqs_given_here ieqs
 
        ; traceTcS "getNoGivenEqs" (vcat [ ppr has_given_eqs, ppr inerts
                                         , ppr insols])
        ; return (not has_given_eqs, insols) }
   where
-    eqs_given_here :: VarSet -> EqualCtList -> Bool
-    eqs_given_here local_fsks [CTyEqCan { cc_tyvar = tv, cc_ev = ev }]
+    eqs_given_here :: EqualCtList -> Bool
+    eqs_given_here [CTyEqCan { cc_tyvar = tv, cc_ev = ev }]
                               -- Givens are always a sigleton
-      = not (skolem_bound_here local_fsks tv) && ev_given_here ev
-    eqs_given_here _ _ = False
+      = not (skolem_bound_here tv) && ev_given_here ev
+    eqs_given_here _ = False
 
     ev_given_here :: CtEvidence -> Bool
     -- True for a Given bound by the curent implication,
@@ -1840,16 +1848,10 @@ getNoGivenEqs tclvl skol_tvs
       =  isGiven ev
       && tclvl == ctLocLevel (ctEvLoc ev)
 
-    add_fsk :: Ct -> VarSet -> VarSet
-    add_fsk ct fsks | CFunEqCan { cc_fsk = tv, cc_ev = ev } <- ct
-                    , isGiven ev = extendVarSet fsks tv
-                    | otherwise  = fsks
-
     skol_tv_set = mkVarSet skol_tvs
-    skolem_bound_here local_fsks tv -- See Note [Let-bound skolems]
+    skolem_bound_here tv -- See Note [Let-bound skolems]
       = case tcTyVarDetails tv of
           SkolemTv {} -> tv `elemVarSet` skol_tv_set
-          FlatSkol {} -> not (tv `elemVarSet` local_fsks)
           _           -> False
 
 -- | Returns Given constraints that might,
@@ -1889,9 +1891,11 @@ matchableGivens loc_w pred (IS { inert_cans = inert_cans })
     -- bindable when unifying with givens. That ensures that we
     -- conservatively assume that a meta tyvar might get unified with
     -- something that matches the 'given', until demonstrated
-    -- otherwise.
-    bind_meta_tv tv | isMetaTyVar tv = BindMe
-                    | otherwise      = Skolem
+    -- otherwise.  More info in Note [Instance and Given overlap]
+    -- in TcInteract
+    bind_meta_tv tv | isMetaTyVar tv
+                    , not (isFskTyVar tv) = BindMe
+                    | otherwise           = Skolem
 
 prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
 -- See Note [Solving superclass constraints] in TcInstDcls
@@ -2413,6 +2417,8 @@ runTcSWithEvBinds ev_binds_var tcs
        ; when (count > 0) $
          csTraceTcM $ return (text "Constraint solver steps =" <+> int count)
 
+       ; unflattenGivens inert_var
+
 #if defined(DEBUG)
        ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
        ; checkForCyclicBinds ev_binds
@@ -2420,6 +2426,7 @@ runTcSWithEvBinds ev_binds_var tcs
 
        ; return res }
 
+----------------------------
 #if defined(DEBUG)
 checkForCyclicBinds :: EvBindMap -> TcM ()
 checkForCyclicBinds ev_binds_map
@@ -2447,6 +2454,7 @@ checkForCyclicBinds ev_binds_map
             -- Note [Deterministic SCC] in Digraph.
 #endif
 
+----------------------------
 setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a
 setEvBindsTcS ref (TcS thing_inside)
  = TcS $ \ env -> thing_inside (env { tcs_ev_binds = ref })
@@ -2460,8 +2468,9 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside)
                    , tcs_count         = count
                    } ->
     do { inerts <- TcM.readTcRef old_inert_var
-       ; let nest_inert = inerts { inert_flat_cache = emptyExactFunEqs }
-                                     -- See Note [Do not inherit the flat cache]
+       ; let nest_inert = emptyInert { inert_cans         = inert_cans inerts
+                                     , inert_solved_dicts = inert_solved_dicts inerts }
+                          -- See Note [Do not inherit the flat cache]
        ; new_inert_var <- TcM.newTcRef nest_inert
        ; new_wl_var    <- TcM.newTcRef emptyWorkList
        ; let nest_env = TcSEnv { tcs_ev_binds      = ref
@@ -2472,6 +2481,8 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside)
        ; res <- TcM.setTcLevel inner_tclvl $
                 thing_inside nest_env
 
+       ; unflattenGivens new_inert_var
+
 #if defined(DEBUG)
        -- Perform a check that the thing_inside did not cause cycles
        ; ev_binds <- TcM.getTcEvBindsMap ref
@@ -2627,15 +2638,6 @@ unifyTyVar tv ty
        ; TcM.writeMetaTyVar tv ty
        ; TcM.updTcRef (tcs_unified env) (+1) }
 
-unflattenFmv :: TcTyVar -> TcType -> TcS ()
--- Fill a flatten-meta-var, simply by unifying it.
--- This does NOT count as a unification in tcs_unified.
-unflattenFmv tv ty
-  = ASSERT2( isMetaTyVar tv, ppr tv )
-    TcS $ \ _ ->
-    do { TcM.traceTc "unflattenFmv" (ppr tv <+> text ":=" <+> ppr ty)
-       ; TcM.writeMetaTyVar tv ty }
-
 reportUnifications :: TcS a -> TcS (Int, a)
 reportUnifications (TcS thing_inside)
   = TcS $ \ env ->
@@ -2790,8 +2792,12 @@ which will result in two Deriveds to end up in the insoluble set:
   wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
 -}
 
--- Flatten skolems
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- *********************************************************************
+*                                                                      *
+*                Flatten skolems                                       *
+*                                                                      *
+********************************************************************* -}
+
 newFlattenSkolem :: CtFlavour -> CtLoc
                  -> TyCon -> [TcType]                    -- F xis
                  -> TcS (CtEvidence, Coercion, TcTyVar)  -- [G/WD] x:: F xis ~ fsk
@@ -2806,9 +2812,14 @@ newFlattenSkolem flav loc tc xis
     new_skolem
       | Given <- flav
       = do { fsk <- wrapTcS (TcM.newFskTyVar fam_ty)
-           ; let co = mkNomReflCo fam_ty
-           ; ev  <- newGivenEvVar loc (mkPrimEqPred fam_ty (mkTyVarTy fsk),
-                                       EvCoercion co)
+
+           -- Extend the inert_fsks list, for use by unflattenGivens
+           ; updInertTcS $ \is -> is { inert_fsks = (fsk, fam_ty) : inert_fsks is }
+
+           -- Construct the Refl evidence
+           ; let pred = mkPrimEqPred fam_ty (mkTyVarTy fsk)
+                 co   = mkNomReflCo fam_ty
+           ; ev  <- newGivenEvVar loc (pred, EvCoercion co)
            ; return (ev, co, fsk) }
 
       | otherwise  -- Generate a [WD] for both Wanted and Derived
@@ -2817,6 +2828,25 @@ newFlattenSkolem flav loc tc xis
            ; (ev, hole_co) <- newWantedEq loc Nominal fam_ty (mkTyVarTy fmv)
            ; return (ev, hole_co, fmv) }
 
+----------------------------
+unflattenGivens :: IORef InertSet -> TcM ()
+-- Unflatten all the fsks created by flattening types in Given
+-- constraints We must be sure to do this, else we end up with
+-- flatten-skolems buried in any residual Wanteds
+--
+-- NB: this is the /only/ way that a fsk (MetaDetails = FlatSkolTv)
+--     is filled in. Nothing else does so.
+--
+-- It's here (rather than in TcFlatten) becuause the Right Places
+-- to call it are in runTcSWithEvBinds/nestImplicTcS, where it
+-- is nicely paired with the creation an empty inert_fsks list.
+unflattenGivens inert_var
+ = do { inerts <- TcM.readTcRef inert_var
+       ; mapM_ flatten_one (inert_fsks inerts) }
+  where
+    flatten_one (fsk, ty) = TcM.writeMetaTyVar fsk ty
+
+----------------------------
 extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS ()
 extendFlatCache tc xi_args stuff@(_, ty, fl)
   | isGivenOrWDeriv fl  -- Maintain the invariant that inert_flat_cache
@@ -2832,6 +2862,33 @@ extendFlatCache tc xi_args stuff@(_, ty, fl)
   | otherwise
   = return ()
 
+----------------------------
+unflattenFmv :: TcTyVar -> TcType -> TcS ()
+-- Fill a flatten-meta-var, simply by unifying it.
+-- This does NOT count as a unification in tcs_unified.
+unflattenFmv tv ty
+  = ASSERT2( isMetaTyVar tv, ppr tv )
+    TcS $ \ _ ->
+    do { TcM.traceTc "unflattenFmv" (ppr tv <+> text ":=" <+> ppr ty)
+       ; TcM.writeMetaTyVar tv ty }
+
+----------------------------
+demoteUnfilledFmv :: TcTyVar -> TcS ()
+-- If a flatten-meta-var is still un-filled,
+-- turn it into an ordinary meta-var
+demoteUnfilledFmv fmv
+  = wrapTcS $ do { is_filled <- TcM.isFilledMetaTyVar fmv
+                 ; unless is_filled $
+                   do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv)
+                      ; TcM.writeMetaTyVar fmv tv_ty } }
+
+
+{- *********************************************************************
+*                                                                      *
+*                Instantaiation etc
+*                                                                      *
+********************************************************************* -}
+
 -- Instantiations
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -2845,15 +2902,6 @@ newFlexiTcSTy knd = wrapTcS (TcM.newFlexiTyVarTy knd)
 cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
 cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)
 
-demoteUnfilledFmv :: TcTyVar -> TcS ()
--- If a flatten-meta-var is still un-filled,
--- turn it into an ordinary meta-var
-demoteUnfilledFmv fmv
-  = wrapTcS $ do { is_filled <- TcM.isFilledMetaTyVar fmv
-                 ; unless is_filled $
-                   do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv)
-                      ; TcM.writeMetaTyVar fmv tv_ty } }
-
 instFlexi :: [TKVar] -> TcS TCvSubst
 instFlexi = instFlexiX emptyTCvSubst
 
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 557d40de1e..a611198253 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -615,8 +615,8 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
                         psig_givens = mkGivens loc psig_theta_vars
                   ; _ <- solveSimpleGivens psig_givens
                          -- See Note [Add signature contexts as givens]
-                  ; solveWanteds wanteds }
-       ; wanted_transformed_incl_derivs <- TcM.zonkWC wanted_transformed_incl_derivs
+                  ; wanteds' <- solveWanteds wanteds
+                  ; TcS.zonkWC wanteds' }
 
        -- Find quant_pred_candidates, the predicates that
        -- we'll consider quantifying over
@@ -1953,20 +1953,29 @@ floatEqualities skols no_given_eqs
                 wanteds@(WC { wc_simple = simples })
   | not no_given_eqs  -- There are some given equalities, so don't float
   = return (emptyBag, wanteds)   -- Note [Float Equalities out of Implications]
+
   | otherwise
-  = do { outer_tclvl <- TcS.getTcLevel
+  = do { -- First zonk: the inert set (from whence they came) are is fully
+         -- zonked, but unflattening may have filled in unification
+         -- variables, and we /must/ see them.  Otherwise we may float
+         -- constraints that mention the skolems!
+         simples <- TcS.zonkSimples simples
+
+       -- Now we can pick the ones to float
+       ; let (float_eqs, remaining_simples) = partitionBag (usefulToFloat skol_set) simples
+             skol_set = mkVarSet skols
+
+       -- Promote any unification variables mentioned in the floated equalities
+       -- See Note [Promoting unification variables]
+       ; outer_tclvl <- TcS.getTcLevel
        ; mapM_ (promoteTyVarTcS outer_tclvl)
                (tyCoVarsOfCtsList float_eqs)
-           -- See Note [Promoting unification variables]
 
        ; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols
                                           , text "Simples =" <+> ppr simples
                                           , text "Floated eqs =" <+> ppr float_eqs])
        ; return ( float_eqs
                 , wanteds { wc_simple = remaining_simples } ) }
-  where
-    skol_set = mkVarSet skols
-    (float_eqs, remaining_simples) = partitionBag (usefulToFloat skol_set) simples
 
 usefulToFloat :: VarSet -> Ct -> Bool
 usefulToFloat skol_set ct   -- The constraint is un-flattened and de-canonicalised
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index bd72981511..e22dfc3822 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -496,10 +496,6 @@ data TcTyVarDetails
                   --          when looking up instances
                   -- See Note [Binding when looking up instances] in InstEnv
 
-  | FlatSkol      -- A flatten-skolem.  It stands for the TcType, and zonking
-       TcType     -- will replace it by that type.
-                  -- See Note [The flattening story] in TcFlatten
-
   | RuntimeUnk    -- Stands for an as-yet-unknown type in the GHCi
                   -- interactive context
 
@@ -523,21 +519,26 @@ data MetaInfo
                    -- never contains any ForAlls.
 
    | SigTv         -- A variant of TauTv, except that it should not be
-                   -- unified with a type, only with a type variable
+                   --   unified with a type, only with a type variable
                    -- See Note [Signature skolems]
 
    | FlatMetaTv    -- A flatten meta-tyvar
                    -- It is a meta-tyvar, but it is always untouchable, with level 0
                    -- See Note [The flattening story] in TcFlatten
 
+   | FlatSkolTv    -- A flatten skolem tyvar
+                   -- Just like FlatMetaTv, but is comletely "owned" by
+                   --   its Given CFunEqCan.
+                   -- It is filled in /only/ by unflattenGivens
+                   -- See Note [The flattening story] in TcFlatten
+
 instance Outputable MetaDetails where
   ppr Flexi         = text "Flexi"
   ppr (Indirect ty) = text "Indirect" <+> ppr ty
 
 pprTcTyVarDetails :: TcTyVarDetails -> SDoc
 -- For debugging
-pprTcTyVarDetails (RuntimeUnk {})  = text "rt"
-pprTcTyVarDetails (FlatSkol {})    = text "fsk"
+pprTcTyVarDetails (RuntimeUnk {})      = text "rt"
 pprTcTyVarDetails (SkolemTv lvl True)  = text "ssk" <> colon <> ppr lvl
 pprTcTyVarDetails (SkolemTv lvl False) = text "sk"  <> colon <> ppr lvl
 pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
@@ -546,7 +547,8 @@ pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
     pp_info = case info of
                 TauTv      -> text "tau"
                 SigTv      -> text "sig"
-                FlatMetaTv -> text "fuv"
+                FlatMetaTv -> text "fmv"
+                FlatSkolTv -> text "fsk"
 
 
 {- *********************************************************************
@@ -715,7 +717,7 @@ Note [TcLevel assignment]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 We arrange the TcLevels like this
 
-   0   Level for flatten meta-vars
+   0   Level for all flatten meta-vars
    1   Top level
    2   First-level implication constraints
    3   Second-level implication constraints
@@ -727,9 +729,9 @@ The flatten meta-vars are all at level 0, just to make them untouchable.
 maxTcLevel :: TcLevel -> TcLevel -> TcLevel
 maxTcLevel (TcLevel a) (TcLevel b) = TcLevel (a `max` b)
 
-fmvTcLevel :: TcLevel -> TcLevel
+fmvTcLevel :: TcLevel
 -- See Note [TcLevel assignment]
-fmvTcLevel _ = TcLevel 0
+fmvTcLevel = TcLevel 0
 
 topTcLevel :: TcLevel
 -- See Note [TcLevel assignment]
@@ -763,7 +765,6 @@ tcTyVarLevel tv
     case tcTyVarDetails tv of
           MetaTv { mtv_tclvl = tv_lvl } -> tv_lvl
           SkolemTv tv_lvl _             -> tv_lvl
-          FlatSkol ty                   -> tcTypeLevel ty
           RuntimeUnk                    -> topTcLevel
 
 tcTypeLevel :: TcType -> TcLevel
@@ -1167,20 +1168,15 @@ isFmvTyVar tv
         MetaTv { mtv_info = FlatMetaTv } -> True
         _                                -> False
 
--- | True of both given and wanted flatten-skolems (fak and usk)
-isFlattenTyVar tv
+isFskTyVar tv
   = ASSERT2( tcIsTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of
-        FlatSkol {}                      -> True
-        MetaTv { mtv_info = FlatMetaTv } -> True
+        MetaTv { mtv_info = FlatSkolTv } -> True
         _                                -> False
 
--- | True of FlatSkol skolems only
-isFskTyVar tv
-  = ASSERT2( tcIsTcTyVar tv, ppr tv )
-    case tcTyVarDetails tv of
-        FlatSkol {} -> True
-        _           -> False
+-- | True of both given and wanted flatten-skolems (fak and usk)
+isFlattenTyVar tv
+  = isFmvTyVar tv || isFskTyVar tv
 
 isSkolemTyVar tv
   = ASSERT2( tcIsTcTyVar tv, ppr tv )
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index e103d20f0d..3f1d77a8f7 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -1603,7 +1603,6 @@ canSolveByUnification tclvl tv xi
                                         SigTv -> True
                                         _     -> False
                        SkolemTv {} -> True
-                       FlatSkol {} -> False
                        RuntimeUnk  -> True
 
 {- Note [Fmv Orientation Invariant]
diff --git a/testsuite/tests/deriving/should_fail/T7148.stderr b/testsuite/tests/deriving/should_fail/T7148.stderr
index f8e5055b12..ee42cc91f1 100644
--- a/testsuite/tests/deriving/should_fail/T7148.stderr
+++ b/testsuite/tests/deriving/should_fail/T7148.stderr
@@ -1,18 +1,14 @@
 
 T7148.hs:27:40: error:
-    • Couldn't match type ‘b’ with ‘Tagged a b’
+    • Occurs check: cannot construct the infinite type: b ~ Tagged a b
         arising from the coercion of the method ‘iso2’
           from type ‘forall b1. SameType b1 () -> SameType b1 b’
             to type ‘forall b1. SameType b1 () -> SameType b1 (Tagged a b)’
-      ‘b’ is a rigid type variable bound by
-        the deriving clause for ‘IsoUnit (Tagged a b)’ at T7148.hs:27:40-46
     • When deriving the instance for (IsoUnit (Tagged a b))
 
 T7148.hs:27:40: error:
-    • Couldn't match type ‘b’ with ‘Tagged a b’
+    • Occurs check: cannot construct the infinite type: b ~ Tagged a b
         arising from the coercion of the method ‘iso1’
           from type ‘forall b1. SameType () b1 -> SameType b b1’
             to type ‘forall b1. SameType () b1 -> SameType (Tagged a b) b1’
-      ‘b’ is a rigid type variable bound by
-        the deriving clause for ‘IsoUnit (Tagged a b)’ at T7148.hs:27:40-46
     • When deriving the instance for (IsoUnit (Tagged a b))
diff --git a/testsuite/tests/gadt/T3169.stderr b/testsuite/tests/gadt/T3169.stderr
index 4bc39a731b..d0f650b9ab 100644
--- a/testsuite/tests/gadt/T3169.stderr
+++ b/testsuite/tests/gadt/T3169.stderr
@@ -1,10 +1,6 @@
 
 T3169.hs:13:22: error:
-    • Couldn't match type ‘elt’ with ‘Map b elt’
-      ‘elt’ is a rigid type variable bound by
-        the type signature for:
-          lookup :: forall elt. (a, b) -> Map (a, b) elt -> Maybe elt
-        at T3169.hs:12:3-8
+    • Occurs check: cannot construct the infinite type: elt ~ Map b elt
       Expected type: Map a (Map b elt)
         Actual type: Map (a, b) elt
     • In the second argument of ‘lookup’, namely ‘m’
diff --git a/testsuite/tests/gadt/T7558.stderr b/testsuite/tests/gadt/T7558.stderr
index ff90037ff6..568f64fcee 100644
--- a/testsuite/tests/gadt/T7558.stderr
+++ b/testsuite/tests/gadt/T7558.stderr
@@ -1,10 +1,6 @@
 
 T7558.hs:8:4: error:
-    • Couldn't match type ‘a’ with ‘Maybe a’
-      ‘a’ is a rigid type variable bound by
-        the type signature for:
-          f :: forall a. T a a -> Bool
-        at T7558.hs:7:1-18
+    • Occurs check: cannot construct the infinite type: a ~ Maybe a
       Inaccessible code in
         a pattern with constructor:
           MkT :: forall a b. a ~ Maybe b => a -> Maybe b -> T a b,
diff --git a/testsuite/tests/indexed-types/should_fail/T13674.hs b/testsuite/tests/indexed-types/should_fail/T13674.hs
new file mode 100644
index 0000000000..4d9a81d8a5
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T13674.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+module T13674 where
+
+import Data.Proxy
+import GHC.Exts (Constraint)
+import GHC.TypeLits
+import Unsafe.Coerce (unsafeCoerce)
+
+data Dict :: Constraint -> * where
+  Dict :: a => Dict a
+
+infixr 9 :-
+newtype a :- b = Sub (a => Dict b)
+
+-- | Given that @a :- b@, derive something that needs a context @b@, using the context @a@
+(\\) :: a => (b => r) -> (a :- b) -> r
+r \\ Sub Dict = r
+
+newtype Magic n = Magic (KnownNat n => Dict (KnownNat n))
+
+magic :: forall n m o. (Integer -> Integer -> Integer) -> (KnownNat n, KnownNat m) :- KnownNat o
+magic f = Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy :: Proxy n) `f` natVal (Proxy :: Proxy m))
+
+type family Lcm :: Nat -> Nat -> Nat where
+
+axiom :: forall a b. Dict (a ~ b)
+axiom = unsafeCoerce (Dict :: Dict (a ~ a))
+
+lcmNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)
+lcmNat = magic lcm
+
+lcmIsIdempotent :: forall n. Dict (n ~ Lcm n n)
+lcmIsIdempotent = axiom
+
+newtype GF (n :: Nat) = GF Integer
+
+x :: GF 5
+x = GF 3
+
+y :: GF 5
+y = GF 4
+
+foo :: (KnownNat m, KnownNat n) => GF m -> GF n -> GF (Lcm m n)
+foo m@(GF x) n@(GF y) = GF $ (x*y) `mod` (lcm (natVal m) (natVal n))
+
+bar :: (KnownNat m)  => GF m -> GF m -> GF m
+bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
diff --git a/testsuite/tests/indexed-types/should_fail/T13674.stderr b/testsuite/tests/indexed-types/should_fail/T13674.stderr
new file mode 100644
index 0000000000..53a7cb705c
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T13674.stderr
@@ -0,0 +1,28 @@
+
+T13674.hs:56:21: error:
+    • Occurs check: cannot construct the infinite type: m ~ Lcm m m
+      Expected type: GF m
+        Actual type: GF (Lcm m m)
+    • In the first argument of ‘(-)’, namely ‘foo x y’
+      In the expression:
+        foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
+      In an equation for ‘bar’:
+          bar (x :: GF m) y
+            = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
+    • Relevant bindings include
+        y :: GF m (bound at T13674.hs:56:17)
+        x :: GF m (bound at T13674.hs:56:6)
+        bar :: GF m -> GF m -> GF m (bound at T13674.hs:56:1)
+
+T13674.hs:56:31: error:
+    • Occurs check: cannot construct the infinite type: m ~ Lcm m m
+      Expected type: GF m
+        Actual type: GF (Lcm m m)
+    • In the first argument of ‘(\\)’, namely ‘foo y x’
+      In the first argument of ‘(\\)’, namely ‘foo y x \\ lcmNat @m @m’
+      In the second argument of ‘(-)’, namely
+        ‘foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)’
+    • Relevant bindings include
+        y :: GF m (bound at T13674.hs:56:17)
+        x :: GF m (bound at T13674.hs:56:6)
+        bar :: GF m -> GF m -> GF m (bound at T13674.hs:56:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T4272.stderr b/testsuite/tests/indexed-types/should_fail/T4272.stderr
index f60711a758..f0c5ab57f0 100644
--- a/testsuite/tests/indexed-types/should_fail/T4272.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4272.stderr
@@ -1,10 +1,7 @@
 
 T4272.hs:15:26: error:
-    • Couldn't match type ‘a’ with ‘TermFamily a a’
-      ‘a’ is a rigid type variable bound by
-        the type signature for:
-          laws :: forall a b. TermLike a => TermFamily a a -> b
-        at T4272.hs:14:1-53
+    • Occurs check: cannot construct the infinite type:
+        a ~ TermFamily a a
       Expected type: TermFamily a (TermFamily a a)
         Actual type: TermFamily a a
     • In the first argument of ‘terms’, namely
diff --git a/testsuite/tests/indexed-types/should_fail/T9662.stderr b/testsuite/tests/indexed-types/should_fail/T9662.stderr
index 3cdc60a18c..54b05665a3 100644
--- a/testsuite/tests/indexed-types/should_fail/T9662.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9662.stderr
@@ -1,7 +1,7 @@
 
 T9662.hs:47:8: error:
-    • Couldn't match type ‘m’ with ‘Int’
-      ‘m’ is a rigid type variable bound by
+    • Couldn't match type ‘k’ with ‘Int’
+      ‘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 9cad8e1734..24abd30cf0 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -133,3 +133,4 @@ test('T12867', normal, compile_fail, [''])
 test('T7102', [ expect_broken(7102) ], ghci_script, ['T7102.script'])
 test('T7102a', normal, ghci_script, ['T7102a.script'])
 test('T13271', normal, compile_fail, [''])
+test('T13674', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_compile/FD3.stderr b/testsuite/tests/typecheck/should_compile/FD3.stderr
index d7ac728b6c..85728da0a6 100644
--- a/testsuite/tests/typecheck/should_compile/FD3.stderr
+++ b/testsuite/tests/typecheck/should_compile/FD3.stderr
@@ -1,13 +1,9 @@
 
 FD3.hs:15:15: error:
-    • Couldn't match type ‘a’ with ‘(String, a)’
+    • Occurs check: cannot construct the infinite type: a ~ (String, a)
         arising from a functional dependency between:
           constraint ‘MkA (String, a) a’ arising from a use of ‘mkA’
           instance ‘MkA a1 a1’ at FD3.hs:12:10-16
-      ‘a’ is a rigid type variable bound by
-        the type signature for:
-          translate :: forall a. (String, a) -> A a
-        at FD3.hs:14:1-31
     • In the expression: mkA a
       In an equation for ‘translate’: translate a = mkA a
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_compile/T9834.stderr b/testsuite/tests/typecheck/should_compile/T9834.stderr
index 303b1defe6..01b003fa3a 100644
--- a/testsuite/tests/typecheck/should_compile/T9834.stderr
+++ b/testsuite/tests/typecheck/should_compile/T9834.stderr
@@ -1,8 +1,6 @@
 
 T9834.hs:23:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Couldn't match type ‘p’ with ‘(->) (p a0)’
-      ‘p’ is a rigid type variable bound by
-        the class declaration for ‘ApplicativeFix’ at T9834.hs:21:39
+    • Occurs check: cannot construct the infinite type: p ~ (->) (p a0)
       Expected type: (forall (q :: * -> *).
                       Applicative q =>
                       Comp p q a -> Comp p q a)
diff --git a/testsuite/tests/typecheck/should_fail/mc19.stderr b/testsuite/tests/typecheck/should_fail/mc19.stderr
index cffb7f61c5..1b9682e6c8 100644
--- a/testsuite/tests/typecheck/should_fail/mc19.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc19.stderr
@@ -1,10 +1,6 @@
 
 mc19.hs:10:31: error:
-    • Couldn't match type ‘a’ with ‘[a]’
-      ‘a’ is a rigid type variable bound by
-        a type expected by the context:
-          forall a. [a] -> [a]
-        at mc19.hs:10:10-35
+    • Occurs check: cannot construct the infinite type: a ~ [a]
       Expected type: [a] -> [a]
         Actual type: [a] -> [[a]]
     • In the expression: inits
diff --git a/testsuite/tests/typecheck/should_fail/mc21.stderr b/testsuite/tests/typecheck/should_fail/mc21.stderr
index 9cffcfb492..014628f94a 100644
--- a/testsuite/tests/typecheck/should_fail/mc21.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc21.stderr
@@ -1,10 +1,6 @@
 
 mc21.hs:12:26: error:
-    • Couldn't match type ‘a’ with ‘[a]’
-      ‘a’ is a rigid type variable bound by
-        a type expected by the context:
-          forall a. [a] -> [[a]]
-        at mc21.hs:(11,9)-(12,31)
+    • Occurs check: cannot construct the infinite type: a ~ [a]
       Expected type: [a] -> [[a]]
         Actual type: [[a]] -> [[a]]
     • In the expression: take 5
diff --git a/testsuite/tests/typecheck/should_fail/mc22.stderr b/testsuite/tests/typecheck/should_fail/mc22.stderr
index ec82baf620..40a754a9c5 100644
--- a/testsuite/tests/typecheck/should_fail/mc22.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc22.stderr
@@ -1,10 +1,6 @@
 
 mc22.hs:10:26: error:
-    • Couldn't match type ‘a’ with ‘t a’
-      ‘a’ is a rigid type variable bound by
-        a type expected by the context:
-          forall a. [a] -> [t a]
-        at mc22.hs:(9,9)-(10,31)
+    • Occurs check: cannot construct the infinite type: a ~ t a
       Expected type: [a] -> [t a]
         Actual type: [t a] -> [t a]
     • In the expression: take 5
diff --git a/testsuite/tests/typecheck/should_fail/tcfail191.stderr b/testsuite/tests/typecheck/should_fail/tcfail191.stderr
index 8eb11f9c62..125c2d8393 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail191.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail191.stderr
@@ -1,10 +1,6 @@
 
 tcfail191.hs:11:26: error:
-    • Couldn't match type ‘a’ with ‘[a]’
-      ‘a’ is a rigid type variable bound by
-        a type expected by the context:
-          forall a. [a] -> [[a]]
-        at tcfail191.hs:(10,9)-(11,31)
+    • Occurs check: cannot construct the infinite type: a ~ [a]
       Expected type: [a] -> [[a]]
         Actual type: [[a]] -> [[a]]
     • In the expression: take 5
diff --git a/testsuite/tests/typecheck/should_fail/tcfail193.stderr b/testsuite/tests/typecheck/should_fail/tcfail193.stderr
index 6259dfc2a2..028e2f0232 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail193.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail193.stderr
@@ -1,10 +1,6 @@
 
 tcfail193.hs:10:31: error:
-    • Couldn't match type ‘a’ with ‘[a]’
-      ‘a’ is a rigid type variable bound by
-        a type expected by the context:
-          forall a. [a] -> [a]
-        at tcfail193.hs:10:10-35
+    • Occurs check: cannot construct the infinite type: a ~ [a]
       Expected type: [a] -> [a]
         Actual type: [a] -> [[a]]
     • In the expression: inits