Use local instances with least superclass depth

See new Note [Use only the best local instance] in
GHC.Tc.Solver.Interact.

This commit also refactors the InstSC/OtherSC mechanism
slightly.

Close #20582.

9 files changed, 187 insertions, 82 deletions

diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index 7177f7347f..6a6ccecf20 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -1028,11 +1028,11 @@ tryReporter ctxt (str, keep_me,  suppress_after, reporter) cts
 
 pprArising :: CtOrigin -> SDoc
 -- Used for the main, top-level error message
--- We've done special processing for TypeEq, KindEq, Given
-pprArising (TypeEqOrigin {}) = empty
-pprArising (KindEqOrigin {}) = empty
-pprArising (GivenOrigin {})  = empty
-pprArising orig              = pprCtOrigin orig
+-- We've done special processing for TypeEq, KindEq, givens
+pprArising (TypeEqOrigin {})         = empty
+pprArising (KindEqOrigin {})         = empty
+pprArising orig | isGivenOrigin orig = empty
+                | otherwise          = pprCtOrigin orig
 
 -- Add the "arising from..." part to a message about bunch of dicts
 addArising :: CtOrigin -> SDoc -> SDoc
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index 5a504211f0..0ec6532105 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -586,23 +586,23 @@ mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc })
                -- get down to a base predicate, we'll include its size.
                -- #10335
 
-       | GivenOrigin skol_info <- ctLocOrigin loc
          -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
-         -- for explantation of InstSC and Note [Replacement vs keeping] in
-         -- GHC.Tc.Solver.Interact for why we need OtherSC and depths
-       = let new_skol_info = case skol_info of
+         -- for explantation of InstSCOrigin and Note [Replacement vs keeping] in
+         -- GHC.Tc.Solver.Interact for why we need OtherSCOrigin and depths
+       | otherwise
+       = loc { ctl_origin = new_orig }
+       where
+         new_orig = case ctLocOrigin loc of
             -- these cases are when we have something that's already a superclass constraint
-               InstSC  sc_depth n  -> InstSC  (sc_depth + 1) (n `max` size)
-               OtherSC sc_depth si -> OtherSC (sc_depth + 1) si
+           InstSCOrigin  sc_depth n  -> InstSCOrigin  (sc_depth + 1) (n `max` size)
+           OtherSCOrigin sc_depth si -> OtherSCOrigin (sc_depth + 1) si
 
             -- these cases do not already have a superclass constraint: depth starts at 1
-               InstSkol -> InstSC 1 size
-               _        -> OtherSC 1 skol_info
-         in
-         loc { ctl_origin = GivenOrigin new_skol_info }
+           GivenOrigin InstSkol      -> InstSCOrigin  1 size
+           GivenOrigin other_skol    -> OtherSCOrigin 1 other_skol
 
-       | otherwise  -- Probably doesn't happen, since this function
-       = loc        -- is only used for Givens, but does no harm
+           other_orig                -> pprPanic "Given constraint without given origin" $
+                                        ppr evar $$ ppr other_orig
 
 mk_strict_superclasses rec_clss ev tvs theta cls tys
   | all noFreeVarsOfType tys
diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs
index 0ab5f5facb..53b6097ec7 100644
--- a/compiler/GHC/Tc/Solver/InertSet.hs
+++ b/compiler/GHC/Tc/Solver/InertSet.hs
@@ -1649,7 +1649,7 @@ mightEqualLater (IS { inert_cycle_breakers = cbvs })
 prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
 -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
 prohibitedSuperClassSolve from_loc solve_loc
-  | GivenOrigin (InstSC _ given_size) <- ctLocOrigin from_loc
+  | InstSCOrigin _ given_size <- ctLocOrigin from_loc
   , ScOrigin wanted_size <- ctLocOrigin solve_loc
   = given_size >= wanted_size
   | otherwise
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index a1bd9f7d0b..a088637e46 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -491,7 +491,7 @@ solveOneFromTheOther ev_i ev_w
 
   -- After this, neither ev_i or ev_w are Derived
   | CtWanted { ctev_loc = loc_w } <- ev_w
-  , prohibitedSuperClassSolve (ctEvLoc ev_i) loc_w
+  , prohibitedSuperClassSolve loc_i loc_w
   = -- inert must be Given
     do { traceTcS "prohibitedClassSolve1" (ppr ev_i $$ ppr ev_w)
        ; return KeepWork }
@@ -539,31 +539,28 @@ solveOneFromTheOther ev_i ev_w
      different_level_strategy  -- Both Given
        | isIPLikePred pred = if lvl_w > lvl_i then KeepWork  else KeepInert
        | otherwise         = if lvl_w > lvl_i then KeepInert else KeepWork
-       -- See Note [Replacement vs keeping] (the different-level bullet)
+       -- See Note [Replacement vs keeping] part (1)
        -- For the isIPLikePred case see Note [Shadowing of Implicit Parameters]
 
      same_level_strategy -- Both Given
-       = case (un_given (ctLocOrigin loc_i), un_given (ctLocOrigin loc_w)) of
-              -- case 2(b) from Note [Replacement vs keeping]
-           (InstSC _depth_i size_i, InstSC _depth_w size_w) | size_w < size_i -> KeepWork
-                                                            | otherwise       -> KeepInert
+       = case (ctLocOrigin loc_i, ctLocOrigin loc_w) of
+              -- case 2(a) from Note [Replacement vs keeping]
+           (InstSCOrigin _depth_i size_i, InstSCOrigin _depth_w size_w)
+             | size_w < size_i -> KeepWork
+             | otherwise       -> KeepInert
 
               -- case 2(c) from Note [Replacement vs keeping]
-           (InstSC depth_i _, OtherSC depth_w _)  -> choose_shallower depth_i depth_w
-           (OtherSC depth_i _, InstSC depth_w _)  -> choose_shallower depth_i depth_w
-           (OtherSC depth_i _, OtherSC depth_w _) -> choose_shallower depth_i depth_w
+           (InstSCOrigin depth_i _, OtherSCOrigin depth_w _)  -> choose_shallower depth_i depth_w
+           (OtherSCOrigin depth_i _, InstSCOrigin depth_w _)  -> choose_shallower depth_i depth_w
+           (OtherSCOrigin depth_i _, OtherSCOrigin depth_w _) -> choose_shallower depth_i depth_w
 
-              -- case 2(a) from Note [Replacement vs keeping]
-           (InstSC {}, _)                         -> KeepWork
-           (OtherSC {}, _)                        -> KeepWork
+              -- case 2(b) from Note [Replacement vs keeping]
+           (InstSCOrigin {}, _)                         -> KeepWork
+           (OtherSCOrigin {}, _)                        -> KeepWork
 
              -- case 2(d) from Note [Replacement vs keeping]
            _                                      -> KeepInert
 
-     un_given (GivenOrigin skol_info) = skol_info
-     un_given orig = pprPanic "Given without GivenOrigin in solveOneFromTheOther" $
-                     vcat [ppr ev_i, ppr ev_w, ppr orig]
-
      choose_shallower depth_i depth_w | depth_w < depth_i = KeepWork
                                       | otherwise         = KeepInert
        -- favor KeepInert in the equals case, according to 2(d) from the Note
@@ -592,7 +589,10 @@ solveOneFromTheOther.
 
   2) Constraints coming from the same level (i.e. same implication)
 
-       (a) Prefer constraints that are not superclass selections. Example:
+       (a) If both are InstSCOrigin, choose the one with the smallest TypeSize,
+           according to Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance.
+
+       (b) Prefer constraints that are not superclass selections. Example:
 
              f :: (Eq a, Ord a) => a -> Bool
              f x = x == x
@@ -605,20 +605,18 @@ solveOneFromTheOther.
            Getting this wrong was #20602. See also
            Note [Tracking redundant constraints] in GHC.Tc.Solver.
 
-       (b) If both are InstSC, choose the one with the smallest TypeSize,
-           according to Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance.
-
-       (c) If both are superclass selections (but not both InstSC), choose the one
+       (c) If both are superclass selections (but not both InstSCOrigin), choose the one
            with the shallower superclass-selection depth, in the hope of identifying
            more correct redundant constraints. This is really a generalization of
-           point (a).
+           point (b), because the superclass depth of a non-superclass
+           constraint is 0.
 
        (d) Finally, when there is still a choice, use KeepInert rather than
            KeepWork, for two reasons:
              - to avoid unnecessary munging of the inert set.
              - to cut off superclass loops; see Note [Superclass loops] in GHC.Tc.Solver.Canonical
 
-Doing the depth-check for implicit parameters, rather than making the work item
+Doing the level-check for implicit parameters, rather than making the work item
 always override, is important.  Consider
 
     data T a where { T1 :: (?x::Int) => T Int; T2 :: T a }
@@ -634,7 +632,7 @@ Now consider these steps
   - process a~Int, kicking out (?x::a)
   - process (?x::Int), the inner given, adding to inert set
   - process (?x::a), the outer given, overriding the inner given
-Wrong!  The depth-check ensures that the inner implicit parameter wins.
+Wrong!  The level-check ensures that the inner implicit parameter wins.
 (Actually I think that the order in which the work-list is processed means
 that this chain of events won't happen, but that's very fragile.)
 
@@ -2455,35 +2453,57 @@ matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult
 matchLocalInst pred loc
   = do { inerts@(IS { inert_cans = ics }) <- getTcSInerts
        ; case match_local_inst inerts (inert_insts ics) of
-           ([], False) -> do { traceTcS "No local instance for" (ppr pred)
-                             ; return NoInstance }
-           ([(dfun_ev, inst_tys)], unifs)
-             | not unifs
+           ([], Nothing) -> do { traceTcS "No local instance for" (ppr pred)
+                               ; return NoInstance }
+
+             -- See Note [Use only the best local instance] about
+             -- superclass depths
+           (matches, unifs)
+             | [(dfun_ev, inst_tys)] <- best_matches
+             , maybe True (> min_sc_depth) unifs
              -> do { let dfun_id = ctEvEvId dfun_ev
                    ; (tys, theta) <- instDFunType dfun_id inst_tys
                    ; let result = OneInst { cir_new_theta = theta
                                           , cir_mk_ev     = evDFunApp dfun_id tys
                                           , cir_what      = LocalInstance }
-                   ; traceTcS "Local inst found:" (ppr result)
+                   ; traceTcS "Best local inst found:" (ppr result)
+                   ; traceTcS "All local insts:" (ppr matches)
                    ; return result }
-           _ -> do { traceTcS "Multiple local instances for" (ppr pred)
-                   ; return NotSure }}
+
+             | otherwise
+             -> do { traceTcS "Multiple local instances for" (ppr pred)
+                   ; return NotSure }
+
+             where
+               extract_depth = sc_depth . ctEvLoc . fst
+               min_sc_depth = minimum (map extract_depth matches)
+               best_matches = filter ((== min_sc_depth) . extract_depth) matches }
   where
     pred_tv_set = tyCoVarsOfType pred
 
+    sc_depth :: CtLoc -> Int
+    sc_depth ctloc = case ctLocOrigin ctloc of
+      InstSCOrigin depth _  -> depth
+      OtherSCOrigin depth _ -> depth
+      _                     -> 0
+
+    -- See Note [Use only the best local instance] about superclass depths
     match_local_inst :: InertSet
                      -> [QCInst]
                      -> ( [(CtEvidence, [DFunInstType])]
-                        , Bool )      -- True <=> Some unify but do not match
+                        , Maybe Int )   -- Nothing ==> no unifying local insts
+                                        -- Just n ==> unifying local insts, with
+                                        --            minimum superclass depth
+                                        --            of n
     match_local_inst _inerts []
-      = ([], False)
+      = ([], Nothing)
     match_local_inst inerts (qci@(QCI { qci_tvs = qtvs, qci_pred = qpred
-                               , qci_ev = ev })
+                               , qci_ev = qev })
                              : qcis)
       | let in_scope = mkInScopeSet (qtv_set `unionVarSet` pred_tv_set)
       , Just tv_subst <- ruleMatchTyKiX qtv_set (mkRnEnv2 in_scope)
                                         emptyTvSubstEnv qpred pred
-      , let match = (ev, map (lookupVarEnv tv_subst) qtvs)
+      , let match = (qev, map (lookupVarEnv tv_subst) qtvs)
       = (match:matches, unif)
 
       | otherwise
@@ -2491,8 +2511,52 @@ matchLocalInst pred loc
                   (ppr qci $$ ppr pred)
             -- ASSERT: unification relies on the
             -- quantified variables being fresh
-        (matches, unif || this_unif)
+        (matches, unif `combine` this_unif)
       where
+        qloc = ctEvLoc qev
         qtv_set = mkVarSet qtvs
-        this_unif = mightEqualLater inerts qpred (ctEvLoc ev) pred loc
+        this_unif
+          | mightEqualLater inerts qpred qloc pred loc = Just (sc_depth qloc)
+          | otherwise = Nothing
         (matches, unif) = match_local_inst inerts qcis
+
+        combine Nothing  Nothing    = Nothing
+        combine (Just n) Nothing    = Just n
+        combine Nothing  (Just n)   = Just n
+        combine (Just n1) (Just n2) = Just (n1 `min` n2)
+
+{- Note [Use only the best local instance]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (#20582) the ambiguity check for
+  (forall a. Ord (m a), forall a. Semigroup a => Eq (m a)) => m Int
+
+Because of eager expansion of given superclasses, we get
+  [G] forall a. Ord (m a)
+  [G] forall a. Eq (m a)
+  [G] forall a. Semigroup a => Eq (m a)
+
+  [W] forall a. Ord (m a)
+  [W] forall a. Semigroup a => Eq (m a)
+
+The first wanted is solved straightforwardly. But the second wanted
+matches *two* local instances. Our general rule around multiple local
+instances is that we refuse to commit to any of them. However, that
+means that our type fails the ambiguity check. That's bad: the type
+is perfectly fine. (This actually came up in the wild, in the streamly
+library.)
+
+The solution is to prefer local instances with fewer superclass selections.
+So, matchLocalInst is careful to whittle down the matches only to the
+ones with the shallowest superclass depth, and also to worry about unifying
+local instances that are at that depth (or less).
+
+By preferring these shallower local instances, we can use the last given
+listed above and pass the ambiguity check.
+
+The instance-depth mechanism uses the same superclass depth
+information as described in Note [Replacement vs keeping], 2a.
+
+Test case: typecheck/should_compile/T20582.
+
+-}
+
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index 26e1689e59..98fb149c27 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -1601,9 +1601,9 @@ Answer:
     GivenOrigin InstSkol.
 
   * When we make a superclass selection from InstSkol we use
-    a SkolemInfo of (InstSC size), where 'size' is the size of
-    the constraint whose superclass we are taking.  A similarly
-    when taking the superclass of an InstSC.  This is implemented
+    a CtOrigin of (InstSCOrigin size), where 'size' is the size of
+    the constraint whose superclass we are taking.  And similarly
+    when taking the superclass of an InstSCOrigin.  This is implemented
     in GHC.Tc.Solver.Canonical.mk_strict_superclasses (in the
     mk_given_loc helper function).
 
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index 7953336a6b..a2229342d8 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -220,21 +220,6 @@ data SkolemInfo
 
   | InstSkol            -- Bound at an instance decl
 
-  -- | A "given" constraint obtained by superclass selection.
-  | InstSC Int          -- ^ The number of superclass selections necessary to
-                        -- get this constraint; see Note [Replacement vs keeping] in
-                        -- GHC.Tc.Solver.Interact
-           TypeSize     -- ^ If @(C ty1 .. tyn)@ is the largest class from
-                        --    which we made a superclass selection in the chain,
-                        --    then @TypeSize = sizeTypes [ty1, .., tyn]@
-                        -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
-
-  -- | A "given" constraint obtained by superclass selection, but not from an instance context.
-  -- Needed for Note [Replacement vs keeping] in GHC.Tc.Solver.Interact.
-  | OtherSC Int    -- ^ The number of superclass selections necessary to
-                   -- get this constraint
-            SkolemInfo   -- ^ Where the sub-class constraint arose from
-
   | FamInstSkol         -- Bound at a family instance decl
   | PatSkol             -- An existential type variable bound by a pattern for
       ConLike           -- a data constructor with an existential type.
@@ -284,8 +269,6 @@ pprSkolInfo (IPSkol ips)      = text "the implicit-parameter binding" <> plural
                                  <+> pprWithCommas ppr ips
 pprSkolInfo (DerivSkol pred)  = text "the deriving clause for" <+> quotes (ppr pred)
 pprSkolInfo InstSkol          = text "the instance declaration"
-pprSkolInfo (InstSC _ n)      = text "the instance declaration" <> whenPprDebug (parens (ppr n))
-pprSkolInfo (OtherSC _ si)    = pprSkolInfo si  -- superclass constraints don't bind skolems
 pprSkolInfo FamInstSkol       = text "a family instance declaration"
 pprSkolInfo BracketSkol       = text "a Template Haskell bracket"
 pprSkolInfo (RuleSkol name)   = text "the RULE" <+> pprRuleName name
@@ -376,9 +359,44 @@ in the right place.  So we proceed as follows:
 -}
 
 data CtOrigin
-  = GivenOrigin SkolemInfo
+  = -- | A given constraint from a user-written type signature. The
+    -- 'SkolemInfo' inside gives more information.
+    GivenOrigin SkolemInfo
+
+  -- The following are other origins for given constraints that cannot produce
+  -- new skolems -- hence no SkolemInfo.
+
+  -- | 'InstSCOrigin' is used for a Given constraint obtained by superclass selection
+  -- from the context of an instance declaration.  E.g.
+  --       instance @(Foo a, Bar a) => C [a]@ where ...
+  -- When typechecking the instance decl itself, including producing evidence
+  -- for the superclasses of @C@, the superclasses of @(Foo a)@ and @(Bar a)@ will
+  -- have 'InstSCOrigin' origin.
+  | InstSCOrigin ScDepth      -- ^ The number of superclass selections necessary to
+                              -- get this constraint; see Note [Replacement vs keeping]
+                              -- and Note [Use only the best local instance], both in
+                              -- GHC.Tc.Solver.Interact
+                 TypeSize     -- ^ If @(C ty1 .. tyn)@ is the largest class from
+                              --    which we made a superclass selection in the chain,
+                              --    then @TypeSize = sizeTypes [ty1, .., tyn]@
+                              -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
+
+  -- | 'OtherSCOrigin' is used for a Given constraint obtained by superclass
+  -- selection from a constraint /other than/ the context of an instance
+  -- declaration. (For the latter we use 'InstSCOrigin'.)  E.g.
+  --      f :: Foo a => blah
+  --      f = e
+  -- When typechecking body of 'f', the superclasses of the Given (Foo a)
+  -- will have 'OtherSCOrigin'.
+  -- Needed for Note [Replacement vs keeping] and
+  -- Note [Use only the best local instance], both in GHC.Tc.Solver.Interact.
+  | OtherSCOrigin ScDepth -- ^ The number of superclass selections necessary to
+                          -- get this constraint
+                  SkolemInfo   -- ^ Where the sub-class constraint arose from
+                               -- (used only for printing)
 
   -- All the others are for *wanted* constraints
+
   | OccurrenceOf Name              -- Occurrence of an overloaded identifier
   | OccurrenceOfRecSel RdrName     -- Occurrence of a record selector
   | AppOrigin                      -- An application of some kind
@@ -422,10 +440,12 @@ data CtOrigin
   | RecordUpdOrigin
   | ViewPatOrigin
 
-  | ScOrigin TypeSize   -- Typechecking superclasses of an instance declaration
-                        -- If the instance head is C ty1 .. tyn
-                        --    then TypeSize = sizeTypes [ty1, .., tyn]
-                        -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
+  -- | 'ScOrigin' is used only for the Wanted constraints for the
+  -- superclasses of an instance declaration.
+  -- If the instance head is @C ty1 .. tyn@
+  --    then @TypeSize = sizeTypes [ty1, .., tyn]@
+  -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
+  | ScOrigin TypeSize
 
   | DerivClauseOrigin   -- Typechecking a deriving clause (as opposed to
                         -- standalone deriving).
@@ -497,6 +517,11 @@ data CtOrigin
             -- We record it here for access in 'GHC.Tc.Errors.mkFRRErr'.
       !FRROrigin
 
+-- | The number of superclass selections needed to get this Given.
+-- If @d :: C ty@   has @ScDepth=2@, then the evidence @d@ will look
+-- like @sc_sel (sc_sel dg)@, where @dg@ is a Given.
+type ScDepth = Int
+
 -- An origin is visible if the place where the constraint arises is manifest
 -- in user code. Currently, all origins are visible except for invisible
 -- TypeEqOrigins. This is used when choosing which error of
@@ -514,6 +539,8 @@ toInvisibleOrigin orig                   = orig
 
 isGivenOrigin :: CtOrigin -> Bool
 isGivenOrigin (GivenOrigin {})              = True
+isGivenOrigin (InstSCOrigin {})             = True
+isGivenOrigin (OtherSCOrigin {})            = True
 isGivenOrigin (FunDepOrigin1 _ o1 _ _ o2 _) = isGivenOrigin o1 && isGivenOrigin o2
 isGivenOrigin (FunDepOrigin2 _ o1 _ _)      = isGivenOrigin o1
 isGivenOrigin (CycleBreakerOrigin o)        = isGivenOrigin o
@@ -591,7 +618,9 @@ lGRHSCtOrigin _ = Shouldn'tHappenOrigin "multi-way GRHS"
 pprCtOrigin :: CtOrigin -> SDoc
 -- "arising from ..."
 -- Not an instance of Outputable because of the "arising from" prefix
-pprCtOrigin (GivenOrigin sk) = ctoHerald <+> ppr sk
+pprCtOrigin (GivenOrigin sk)     = ctoHerald <+> ppr sk
+pprCtOrigin (InstSCOrigin {})    = ctoHerald <+> pprSkolInfo InstSkol   -- keep output in sync
+pprCtOrigin (OtherSCOrigin _ si) = ctoHerald <+> pprSkolInfo si
 
 pprCtOrigin (SpecPragOrigin ctxt)
   = case ctxt of
@@ -717,6 +746,8 @@ pprCtO BracketOrigin         = text "a quotation bracket"
 -- get here via callStackOriginFS, when doing ambiguity checks
 -- A bit silly, but no great harm
 pprCtO (GivenOrigin {})             = text "a given constraint"
+pprCtO (InstSCOrigin {})            = text "the superclass of an instance constraint"
+pprCtO (OtherSCOrigin {})           = text "the superclass of a given constraint"
 pprCtO (SpecPragOrigin {})          = text "a SPECIALISE pragma"
 pprCtO (FunDepOrigin1 {})           = text "a functional dependency"
 pprCtO (FunDepOrigin2 {})           = text "a functional dependency"
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 65c5d3a50e..56facd6970 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -2428,7 +2428,6 @@ zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
                                      ; return (InferSkol ntys') }
   where
     do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
-zonkSkolemInfo (OtherSC depth si) = OtherSC depth <$> zonkSkolemInfo si
 zonkSkolemInfo skol_info = return skol_info
 
 {-
@@ -2567,6 +2566,10 @@ zonkTidyOrigin env (GivenOrigin skol_info)
   = do { skol_info1 <- zonkSkolemInfo skol_info
        ; let skol_info2 = tidySkolemInfo env skol_info1
        ; return (env, GivenOrigin skol_info2) }
+zonkTidyOrigin env (OtherSCOrigin sc_depth skol_info)
+  = do { skol_info1 <- zonkSkolemInfo skol_info
+       ; let skol_info2 = tidySkolemInfo env skol_info1
+       ; return (env, OtherSCOrigin sc_depth skol_info2) }
 zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual   = act
                                       , uo_expected = exp })
   = do { (env1, act') <- zonkTidyTcType env  act
diff --git a/testsuite/tests/typecheck/should_compile/T20582.hs b/testsuite/tests/typecheck/should_compile/T20582.hs
new file mode 100644
index 0000000000..9b49787be6
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T20582.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+
+module T20582 where
+
+f :: (forall a. Ord (m a), forall a. Semigroup a => Eq (m a)) => m Int
+f = f
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 9fbf11b641..d5faf615b4 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -573,6 +573,7 @@ test('T13490', normal, compile, [''])
 test('T13474', normal, compile, [''])
 test('T13524', normal, compile, [''])
 test('T20602', normal, compile, [''])
+test('T20582', normal, compile, [''])
 test('T13509', normal, compile, [''])
 test('T13526', normal, compile, [''])
 test('T13594', normal, compile_fail, [''])