content: {-# LANGUAGE DuplicateRecordFields #-}
  {-# LANGUAGE MultiWayIf #-}
  
  module GHC.Tc.Solver.Default(
     tryDefaulting, tryDefaultingForAmbiguityCheck,
     isInteractiveClass, isNumClass
     ) where
  
  import GHC.Prelude
  
  import GHC.Tc.Errors
  import GHC.Tc.Errors.Types
  import GHC.Tc.Types.Evidence
  import GHC.Tc.Solver.Solve   ( solveSimpleWanteds, setImplicationStatus )
  import GHC.Tc.Solver.Dict    ( solveCallStack )
  import GHC.Tc.Utils.Unify
  import GHC.Tc.Utils.TcMType as TcM
  import GHC.Tc.Utils.Monad   as TcM
  import GHC.Tc.Zonk.TcType     as TcM
  import GHC.Tc.Solver.Solve( solveWanteds )
  import GHC.Tc.Solver.Monad  as TcS
  import GHC.Tc.Types.Constraint
  import GHC.Tc.Types.CtLoc( mkGivenLoc )
  import GHC.Tc.Types.Origin
  import GHC.Tc.Utils.TcType
  
  import GHC.Core.Class
  import GHC.Core.Reduction( Reduction, reductionCoercion )
  import GHC.Core
  import GHC.Core.DataCon
  import GHC.Core.Make
  import GHC.Core.Coercion( isReflCo, mkReflCo, mkSubCo, hasCoercionHole )
  import GHC.Core.Unify    ( tcMatchTyKis )
  import GHC.Core.Predicate
  import GHC.Core.Type
  import GHC.Core.TyCo.Tidy
  
  import GHC.Types.DefaultEnv ( ClassDefaults (..), defaultList )
  import GHC.Types.Unique.Set
  import GHC.Types.Id
  
  import GHC.Builtin.Utils
  import GHC.Builtin.Names
  import GHC.Builtin.Types
  
  import GHC.Types.TyThing ( MonadThings(lookupId) )
  import GHC.Types.Var
  import GHC.Types.Var.Env
  import GHC.Types.Var.Set
  import GHC.Types.Id.Make  ( unboxedUnitExpr )
  
  import GHC.Driver.DynFlags
  import GHC.Unit.Module ( getModule )
  
  import GHC.Utils.Misc
  import GHC.Utils.Panic
  import GHC.Utils.Outputable
  
  import GHC.Data.FastString
  import GHC.Data.List.SetOps
  import GHC.Data.Bag
  
  import Control.Monad
  import Control.Monad.Trans.Class        ( lift )
  import Control.Monad.Trans.State.Strict ( StateT(runStateT), put )
  import Data.Foldable      ( toList, traverse_ )
  import Data.List.NonEmpty ( NonEmpty(..), nonEmpty )
  import qualified Data.List.NonEmpty as NE
  import GHC.Data.Maybe     ( isJust, mapMaybe, catMaybes )
  import Data.Monoid     ( First(..) )
  
  
  {- Note [Top-level Defaulting Plan]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  We have considered two design choices for where/when to apply defaulting.
     (i) Do it in SimplCheck mode only /whenever/ you try to solve some
         simple constraints, maybe deep inside the context of implications.
         This used to be the case in GHC 7.4.1.
     (ii) Do it in a tight loop at simplifyTop, once all other constraints have
          finished. This is the current story.
  
  Option (i) had many disadvantages:
     a) Firstly, it was deep inside the actual solver.
     b) Secondly, it was dependent on the context (Infer a type signature,
        or Check a type signature, or Interactive) since we did not want
        to always start defaulting when inferring (though there is an exception to
        this, see Note [Default while Inferring]).
     c) It plainly did not work. Consider typecheck/should_compile/DfltProb2.hs:
            f :: Int -> Bool
            f x = const True (\y -> let w :: a -> a
                                        w a = const a (y+1)
                                    in w y)
        We will get an implication constraint (for beta the type of y):
                 [untch=beta] forall a. 0 => Num beta
        which we really cannot default /while solving/ the implication, since beta is
        untouchable.
  
  Instead our new defaulting story is to pull defaulting out of the solver loop and
  go with option (ii), implemented at SimplifyTop. Namely:
       - First, have a go at solving the residual constraint of the whole
         program
       - Try to approximate it with a simple constraint
       - Figure out derived defaulting equations for that simple constraint
       - Go round the loop again if you did manage to get some equations
  
  Now, that has to do with class defaulting. However there exists type variable /kind/
  defaulting. Again this is done at the top-level and the plan is:
       - At the top-level, once you had a go at solving the constraint, do
         figure out /all/ the touchable unification variables of the wanted constraints.
       - Apply defaulting to their kinds
  
  More details in Note [DefaultTyVar].
  
  Note [Limited defaulting in the ambiguity check]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  When simplifying constraints for the ambiguity check, we don't want full
  defaulting.  E.g. #11947 was an example:
     f :: Num a => Int -> Int
  This is ambiguous of course, but we don't want to default the (Num
  alpha) constraint to (Num Int)!  Doing so gives a defaulting warning,
  but no error.
  
  But we still do
  
  * tryConstraintDefaulting.  Example in T10009 where we have this type signature
      f :: (UnF (F b) ~ b) => F b -> ()
    We finish up with an equality that is a member of it's
      [W] hole{co_aF0} {rewriters: {co_aF0}}:: b_aES[tau:1] ~# b_aEP[sk:1]
    It is not unified because of (REWRITERS) in Note [Unification preconditions]
    in GHC.Tc.Utils.Unify
  
    (`tryConstraintDefaulting` defaults call-stack and exception constraint
    as well as equalities; but in the case of the ambiguity check we will
    only see equality constraints.  Does not seem worth making a version
    of `tryConstraintDefaulting` that looks only for equalities.)
  
  * tryUnsatisfiableGivens: see Wrinkle [Ambiguity] under point (C) of
    Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors.
  -}
  
  
  tryDefaulting :: WantedConstraints -> TcS WantedConstraints
  -- This is the function that pulls all the defaulting strategies together
  tryDefaulting wc
   = do { dflags <- getDynFlags
        ; traceTcS "tryDefaulting {" (ppr wc)
        ; wc1 <- tryTyVarDefaulting dflags wc
        ; wc2 <- tryConstraintDefaulting wc1
        ; wc3 <- tryTypeClassDefaulting wc2
        ; wc4 <- tryUnsatisfiableGivens wc3
        ; traceTcS "tryDefaulting }" (ppr wc4)
        ; return wc4 }
  
  tryDefaultingForAmbiguityCheck  :: WantedConstraints -> TcS WantedConstraints
  -- See Note [Limited defaulting in the ambiguity check]
  tryDefaultingForAmbiguityCheck wc
   = do { traceTcS "tryDefaulting for ambiguity {" (ppr wc)
        ; wc1 <- tryConstraintDefaulting wc
        ; wc2 <- tryUnsatisfiableGivens wc1
        ; traceTcS "tryDefaulting }" (ppr wc2)
        ; return wc2 }
  
  solveAgainIf :: Bool -> WantedConstraints -> TcS WantedConstraints
  -- If the Bool is true, solve the wanted constraints again
  -- See Note [Must simplify after defaulting]
  solveAgainIf False wc = return wc
  solveAgainIf True  wc = nestTcS (solveWanteds wc)
  
  
  {- ******************************************************************************
  *                                                                               *
                          tryTyVarDefaulting
  *                                                                               *
  ****************************************************************************** -}
  
  tryTyVarDefaulting  :: DynFlags -> WantedConstraints -> TcS WantedConstraints
  tryTyVarDefaulting dflags wc
    | isEmptyWC wc
    = return wc
    | insolubleWC wc
    , gopt Opt_PrintExplicitRuntimeReps dflags -- See Note [Defaulting insolubles]
    = return wc
    | otherwise
    = do { -- Need to zonk first, as the WantedConstraints are not yet zonked.
         ; free_tvs <- TcS.zonkTyCoVarsAndFVList (tyCoVarsOfWCList wc)
         ; let defaultable_tvs = filter can_default free_tvs
               can_default tv
                 =   isTyVar tv
                     -- Weed out coercion variables.
  
                  && isMetaTyVar tv
                     -- Weed out runtime-skolems in GHCi, which we definitely
                     -- shouldn't try to default.
  
                  && not (tv `elemVarSet` nonDefaultableTyVarsOfWC wc)
                     -- Weed out variables for which defaulting would be unhelpful,
                     -- e.g. alpha appearing in [W] alpha[conc] ~# rr[sk].
  
         ; unification_s <- mapM defaultTyVarTcS defaultable_tvs -- Has unification side effects
         ; solveAgainIf (or unification_s) wc }
               -- solveAgainIf: see Note [Must simplify after defaulting]
  
  type UnificationDone = Bool
  
  noUnification, didUnification :: UnificationDone
  noUnification  = False
  didUnification = True
  
  -- | Like 'defaultTyVar', but in the TcS monad.
  defaultTyVarTcS :: TcTyVar -> TcS UnificationDone
  defaultTyVarTcS the_tv
    | isTyVarTyVar the_tv
      -- TyVarTvs should only be unified with a tyvar
      -- never with a type; c.f. GHC.Tc.Utils.TcMType.defaultTyVar
      -- and Note [Inferring kinds for type declarations] in GHC.Tc.TyCl
    = return noUnification
    | isRuntimeRepVar the_tv
    = do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv)
         ; unifyTyVar the_tv liftedRepTy
         ; return didUnification }
    | isLevityVar the_tv
    = do { traceTcS "defaultTyVarTcS Levity" (ppr the_tv)
         ; unifyTyVar the_tv liftedDataConTy
         ; return didUnification }
    | isMultiplicityVar the_tv
    = do { traceTcS "defaultTyVarTcS Multiplicity" (ppr the_tv)
         ; unifyTyVar the_tv ManyTy
         ; return didUnification }
    | otherwise
    = return noUnification  -- the common case
  
  
  {- ******************************************************************************
  *                                                                               *
                          tryUnsatisfiableGivens
  *                                                                               *
  ****************************************************************************** -}
  
  -- | If an implication contains a Given of the form @Unsatisfiable msg@,
  -- use it to solve all Wanteds within the implication.
  -- See point (C) in Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors.
  --
  -- This does a complete walk over the implication tree.
  tryUnsatisfiableGivens :: WantedConstraints -> TcS WantedConstraints
  tryUnsatisfiableGivens wc =
    do { (final_wc, did_work) <- (`runStateT` False) $ go_wc wc
       ; solveAgainIf did_work final_wc }
    where
      go_wc (WC { wc_simple = wtds, wc_impl = impls, wc_errors = errs })
        = do impls' <- mapBagM go_impl impls
             return $ WC { wc_simple = wtds, wc_impl = impls', wc_errors = errs }
      go_impl impl
        | isSolvedStatus (ic_status impl)
        = return impl
        -- Is there a Given with type "Unsatisfiable msg"?
        -- If so, use it to solve all other Wanteds.
        | unsat_given:_ <- mapMaybe unsatisfiableEv_maybe (ic_given impl)
        = do { put True
             ; lift $ solveImplicationUsingUnsatGiven unsat_given impl }
        -- Otherwise, recurse.
        | otherwise
        = do { wcs' <- go_wc (ic_wanted impl)
             ; lift $ setImplicationStatus $ impl { ic_wanted = wcs' } }
  
  -- | Is this evidence variable the evidence for an 'Unsatisfiable' constraint?
  --
  -- If so, return the variable itself together with the error message type.
  unsatisfiableEv_maybe :: EvVar -> Maybe (EvVar, Type)
  unsatisfiableEv_maybe v = (v,) <$> isUnsatisfiableCt_maybe (idType v)
  
  -- | We have an implication with an 'Unsatisfiable' Given; use that Given to
  -- solve all the other Wanted constraints, including those nested within
  -- deeper implications.
  solveImplicationUsingUnsatGiven :: (EvVar, Type) -> Implication -> TcS Implication
  solveImplicationUsingUnsatGiven
    unsat_given@(given_ev,_)
    impl@(Implic { ic_wanted = wtd, ic_tclvl = tclvl, ic_binds = ev_binds_var
                 , ic_need_implic = inner })
    | isCoEvBindsVar ev_binds_var
    -- We can't use Unsatisfiable evidence in kinds.
    -- See Note [Coercion evidence only] in GHC.Tc.Types.Evidence.
    = return impl
    | otherwise
    = do { wcs <- nestImplicTcS ev_binds_var tclvl $ go_wc wtd
         ; setImplicationStatus $
           impl { ic_wanted = wcs
                , ic_need_implic = inner `extendEvNeedSet` given_ev } }
                  -- Record that the Given is needed; I'm not certain why
    where
      go_wc :: WantedConstraints -> TcS WantedConstraints
      go_wc wc@(WC { wc_simple = wtds, wc_impl = impls })
        = do { mapBagM_ go_simple wtds
             ; impls <- mapBagM (solveImplicationUsingUnsatGiven unsat_given) impls
             ; return $ wc { wc_simple = emptyBag, wc_impl = impls } }
      go_simple :: Ct -> TcS ()
      go_simple ct = case ctEvidence ct of
        CtWanted (WantedCt { ctev_pred = pty, ctev_dest = dest })
          -> do { ev_expr <- unsatisfiableEvExpr unsat_given pty
                ; setWantedEvTerm dest EvNonCanonical $ EvExpr ev_expr }
        _ -> return ()
  
  -- | Create an evidence expression for an arbitrary constraint using
  -- evidence for an "Unsatisfiable" Given.
  --
  -- See Note [Evidence terms from Unsatisfiable Givens]
  unsatisfiableEvExpr :: (EvVar, ErrorMsgType) -> PredType -> TcS EvExpr
  unsatisfiableEvExpr (unsat_ev, given_msg) wtd_ty
    = do { mod <- getModule
           -- If we're typechecking GHC.TypeError, return a bogus expression;
           -- it's only used for the ambiguity check, which throws the evidence away anyway.
           -- This avoids problems with circularity; where we are trying to look
           -- up the "unsatisfiable" Id while we are in the middle of typechecking it.
         ; if mod == gHC_INTERNAL_TYPEERROR then return (Var unsat_ev) else
      do { unsatisfiable_id <- tcLookupId unsatisfiableIdName
  
           -- See Note [Evidence terms from Unsatisfiable Givens]
           -- for a description of what evidence term we are constructing here.
  
         ; let -- (##) -=> wtd_ty
               fun_ty = mkFunTy visArgConstraintLike ManyTy unboxedUnitTy wtd_ty
               mkDictBox = case boxingDataCon fun_ty of
                 BI_Box { bi_data_con = mkDictBox } -> mkDictBox
                 _ -> pprPanic "unsatisfiableEvExpr: no DictBox!" (ppr wtd_ty)
               dictBox = dataConTyCon mkDictBox
         ; ev_bndr <- mkSysLocalM (fsLit "ct") ManyTy fun_ty
               -- Dict ((##) -=> wtd_ty)
         ; let scrut_ty = mkTyConApp dictBox [fun_ty]
               -- unsatisfiable @{LiftedRep} @given_msg @(Dict ((##) -=> wtd_ty)) unsat_ev
               scrut =
                 mkCoreApps (Var unsatisfiable_id)
                   [ Type liftedRepTy
                   , Type given_msg
                   , Type scrut_ty
                   , Var unsat_ev ]
               -- case scrut of { MkDictBox @((##) -=> wtd_ty)) ct -> ct (# #) }
               ev_expr =
                 mkWildCase scrut (unrestricted $ scrut_ty) wtd_ty
                 [ Alt (DataAlt mkDictBox) [ev_bndr] $
                     mkCoreApps (Var ev_bndr) [unboxedUnitExpr]
                 ]
          ; return ev_expr } }
  
  {- Note [Evidence terms from Unsatisfiable Givens]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  An Unsatisfiable Given constraint, of the form [G] Unsatisfiable msg, should be
  able to solve ANY Wanted constraint whatsoever.
  
  Recall that we have
  
    unsatisfiable :: forall {rep} (msg :: ErrorMessage) (a :: TYPE rep)
                  .  Unsatisfiable msg => a
  
  We want to use this function, together with the evidence
  [G] unsat_ev :: Unsatisfiable msg, to solve any other constraint [W] wtd_ty.
  
  We could naively think that a valid evidence term for the Wanted might be:
  
    wanted_ev = unsatisfiable @{rep} @msg @wtd_ty unsat_ev
  
  Unfortunately, this is a kind error: "wtd_ty :: CONSTRAINT rep", but
  "unsatisfiable" expects the third type argument to be of kind "TYPE rep".
  
  Instead, we use a boxing data constructor to box the constraint into a type.
  In the end, we construct the following evidence for the implication:
  
    [G] unsat_ev :: Unsatisfiable msg
      ==>
        [W] wtd_ev :: wtd_ty
  
    wtd_ev =
      case unsatisfiable @{LiftedRep} @msg @(Dict ((##) -=> wtd_ty)) unsat_ev of
        MkDictBox ct -> ct (# #)
  
  Note that we play the same trick with the function arrow -=> that we did
  in order to define "unsatisfiable" in terms of "unsatisfiableLifted", as described
  in Note [The Unsatisfiable representation-polymorphism trick] in base:GHC.TypeError.
  This allows us to indirectly box constraints with different representations
  (such as primitive equality constraints).
  -}
  
  
  {- ******************************************************************************
  *                                                                               *
                          tryConstraintDefaulting
  *                                                                               *
  ****************************************************************************** -}
  
  -- | A 'TcS' action which can may solve a `Ct`
  type CtDefaultingStrategy = Ct -> TcS Bool
    -- True <=> I solved the constraint
  
  tryConstraintDefaulting :: WantedConstraints -> TcS WantedConstraints
  -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
  tryConstraintDefaulting wc
    | isEmptyWC wc
    = return wc
    | otherwise
    = do { (n_unifs, better_wc) <- reportUnifications (go_wc wc)
           -- We may have done unifications; so solve again
         ; solveAgainIf (n_unifs > 0) better_wc }
    where
      go_wc :: WantedConstraints -> TcS WantedConstraints
      go_wc wc@(WC { wc_simple = simples, wc_impl = implics })
        = do { simples' <- mapMaybeBagM go_simple simples
             ; implics' <- mapBagM go_implic implics
             ; return (wc { wc_simple = simples', wc_impl = implics' }) }
  
      go_simple :: Ct -> TcS (Maybe Ct)
      go_simple ct = do { solved <- tryCtDefaultingStrategy ct
                        ; if solved then return Nothing
                                    else return (Just ct) }
  
      go_implic :: Implication -> TcS Implication
      -- The Maybe is because solving the CallStack constraint
      -- may well allow us to discard the implication entirely
      go_implic implic
        | isSolvedStatus (ic_status implic)
        = return implic  -- Nothing to solve inside here
        | otherwise
        = do { wanteds <- setEvBindsTcS (ic_binds implic) $
                          -- defaultCallStack sets a binding, so
                          -- we must set the correct binding group
                          go_wc (ic_wanted implic)
             ; setImplicationStatus (implic { ic_wanted = wanteds }) }
  
  tryCtDefaultingStrategy :: CtDefaultingStrategy
  -- The composition of all the CtDefaultingStrategies we want
  tryCtDefaultingStrategy
    = foldr1 combineStrategies
      ( defaultCallStack :|
        defaultExceptionContext :
        defaultEquality :
        [] )
  
  -- | Default @ExceptionContext@ constraints to @emptyExceptionContext@.
  defaultExceptionContext :: CtDefaultingStrategy
  defaultExceptionContext ct
    | ClassPred cls tys <- classifyPredType (ctPred ct)
    , isJust (isExceptionContextPred cls tys)
    = do { warnTcS $ TcRnDefaultedExceptionContext (ctLoc ct)
         ; empty_ec_id <- lookupId emptyExceptionContextName
         ; let ev = ctEvidence ct
               ev_tm = EvExpr (evWrapIPE (ctEvPred ev) (Var empty_ec_id))
         ; setEvBindIfWanted ev EvCanonical ev_tm
           -- EvCanonical: see Note [CallStack and ExceptionContext hack]
           --              in GHC.Tc.Solver.Dict
         ; return True }
    | otherwise
    = return False
  
  -- | Default any remaining @CallStack@ constraints to empty @CallStack@s.
  -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
  defaultCallStack :: CtDefaultingStrategy
  defaultCallStack ct
    | ClassPred cls tys <- classifyPredType (ctPred ct)
    , isJust (isCallStackPred cls tys)
    = do { solveCallStack (ctEvidence ct) EvCsEmpty
         ; return True }
    | otherwise
    = return False
  
  defaultEquality :: CtDefaultingStrategy
  -- See Note [Defaulting equalities]
  defaultEquality ct
    | EqPred eq_rel ty1 ty2 <- classifyPredType (ctPred ct)
    = do { -- Remember: `ct` may not be zonked;
           -- see (DE3) in Note [Defaulting equalities]
           z_ty1 <- TcS.zonkTcType ty1
         ; z_ty2 <- TcS.zonkTcType ty2
         ; case eq_rel of
            { NomEq ->
         -- Now see if either LHS or RHS is a bare type variable
         -- You might think the type variable will only be on the LHS
         -- but with a type function we might get   F t1 ~ alpha
           case (getTyVar_maybe z_ty1, getTyVar_maybe z_ty2) of
             (Just z_tv1, _) -> try_default_tv z_tv1 z_ty2
             (_, Just z_tv2) -> try_default_tv z_tv2 z_ty1
             _               -> return False ;
  
            ; ReprEq
                -- See Note [Defaulting representational equalities]
                | CIrredCan (IrredCt { ir_reason }) <- ct
                , isInsolubleReason ir_reason
                -- Don't do this for definitely insoluble representational
                -- equalities such as Int ~R# Bool.
                -> return False
                | otherwise
                ->
         do { traceTcS "defaultEquality ReprEq {" $ vcat
                [ text "ct:" <+> ppr ct
                , text "z_ty1:" <+> ppr z_ty1
                , text "z_ty2:" <+> ppr z_ty2
                ]
              -- Promote this representational equality to a nominal equality.
              --
              -- This handles cases such as @IO alpha[tau] ~R# IO Int@
              -- by defaulting @alpha := Int@, which is useful in practice
              -- (see Note [Defaulting representational equalities]).
            ; (co, new_eqs, _unifs) <-
                wrapUnifierX (ctEvidence ct) Nominal $
                -- NB: nominal equality!
                  \ uenv -> uType uenv z_ty1 z_ty2
              -- Only accept this solution if no new equalities are produced
              -- by the unifier.
              --
              -- See Note [Defaulting representational equalities].
            ; if null new_eqs
              then do { setEvBindIfWanted (ctEvidence ct) EvCanonical $
                         (evCoercion $ mkSubCo co)
                      ; return True }
              else return False
            } } }
    | otherwise
    = return False
  
    where
      try_default_tv lhs_tv rhs_ty
        | MetaTv { mtv_info = info } <- tcTyVarDetails lhs_tv
        , tyVarKind lhs_tv `tcEqType` typeKind rhs_ty
        , checkTopShape info rhs_ty
        , not (hasCoercionHole rhs_ty) -- See (DE6) in Note [Defaulting equalities]
        -- Do not test for touchability of lhs_tv; that is the whole point!
        -- See (DE2) in Note [Defaulting equalities]
        = do { traceTcS "defaultEquality 1" (ppr lhs_tv $$ ppr rhs_ty)
  
             -- checkTyEqRhs: check that we can in fact unify lhs_tv := rhs_ty
             -- See Note [Defaulting equalities]
             ; let flags :: TyEqFlags TcM ()
                   flags = defaulting_TEFTask lhs_tv
  
             ; res :: PuResult () Reduction <- wrapTcS (checkTyEqRhs flags rhs_ty)
  
             ; case res of
                 PuFail {}   -> cant_default_tv "checkTyEqRhs"
                 PuOK _ redn -> assertPpr (isReflCo (reductionCoercion redn)) (ppr redn) $
                                 -- With TEFA_Recurse we never get any reductions
                                default_tv }
        | otherwise
        = cant_default_tv "fall through"
  
        where
          cant_default_tv msg
            = do { traceTcS ("defaultEquality fails: " ++ msg) $
                   vcat [ ppr lhs_tv <+> char '~' <+>  ppr rhs_ty
                        , ppr (tyVarKind lhs_tv)
                        , ppr (typeKind rhs_ty) ]
                 ; return False }
  
          -- All tests passed: do the unification
          default_tv
            = do { traceTcS "defaultEquality success:" (ppr rhs_ty)
                 ; unifyTyVar lhs_tv rhs_ty  -- NB: unifyTyVar adds to the
                                             -- TcS unification counter
                 ; setEvBindIfWanted (ctEvidence ct) EvCanonical $
                   evCoercion (mkReflCo Nominal rhs_ty)
                 ; return True
                 }
  
  
  combineStrategies :: CtDefaultingStrategy -> CtDefaultingStrategy -> CtDefaultingStrategy
  combineStrategies default1 default2 ct
    = do { solved <- default1 ct
         ; case solved of
             True  -> return True  -- default1 solved it!
             False -> default2 ct  -- default1 failed, try default2
         }
  
  
  {- Note [When to do type-class defaulting]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  In GHC 7.6 and 7.8.2, we did type-class defaulting only if insolubleWC
  was false, on the grounds that defaulting can't help solve insoluble
  constraints.  But if we *don't* do defaulting we may report a whole
  lot of errors that would be solved by defaulting; these errors are
  quite spurious because fixing the single insoluble error means that
  defaulting happens again, which makes all the other errors go away.
  This is jolly confusing: #9033.
  
  So it seems better to always do type-class defaulting.
  
  However, always doing defaulting does mean that we'll do it in
  situations like this (#5934):
     run :: (forall s. GenST s) -> Int
     run = fromInteger 0
  We don't unify the return type of fromInteger with the given function
  type, because the latter involves foralls.  So we're left with
      (Num alpha, alpha ~ (forall s. GenST s) -> Int)
  Now we do defaulting, get alpha := Integer, and report that we can't
  match Integer with (forall s. GenST s) -> Int.  That's not totally
  stupid, but perhaps a little strange.
  
  Another potential alternative would be to suppress *all* non-insoluble
  errors if there are *any* insoluble errors, anywhere, but that seems
  too drastic.
  
  Note [Defaulting equalities]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  In top-level defaulting (as per Note [Top-level Defaulting Plan]), it makes
  sense to try to default equality constraints, in addition to e.g. typeclass
  defaulting: this doesn't threaten principal types (see DE1 below), but
  allows GHC to accept strictly more programs.
  
  This Note explains defaulting nominal equalities; see also
  Note [Defaulting representational equalities] which describes
  the defaulting of representational equalities.
  
  Consider
  
    f :: forall a. (forall t. (F t ~ Int) => a -> Int) -> Int
  
    g :: Int
    g = f id
  
  We'll typecheck
  
    id :: forall t. (F t ~ Int) => alpha[1] -> Int
  
  where the `alpha[1]` comes from instantiating `f`. So we'll end up
  with the implication constraint
  
     forall[2] t. (F t ~ Int) => alpha[1] ~ Int
  
  and that can't be solved because `alpha` is untouchable under the
  equality (F t ~ Int).
  
  This is tiresome, and gave rise to user complaints: #25125 and #25029.
  Moreover, in this case there is no good reason not to unify alpha:=Int.
  Doing so solves the constraint, and since `alpha` is not otherwise
  constrained, it does no harm.
  
  In conclusion, for a Wanted equality constraint [W] lhs ~ rhs, if the only
  reason for not unifying is that either lhs or rhs is an untouchable metavariable
  then, in top-level defaulting, go ahead and unify.
  
  In top-level defaulting, we already do several other somewhat-ad-hoc,
  but terribly convenient, unifications. This is just one more.
  
  Wrinkles:
  
  (DE1) Note carefully that this does not threaten principal types.
    The original worry about unifying untouchable type variables was this:
  
       data T a where
         T1 :: T Bool
       f x = case x of T1 -> True
  
    Should we infer f :: T a -> Bool, or f :: T a -> a.  Both are valid, but
    neither is more general than the other.
  
  (DE2) We still can't unify if there is a skolem-escape check, or an occurs check,
    or it it'd mean unifying a TyVarTv with a non-tyvar.  It's only the
    "untouchability test" that we lift.
  
  (DE3) The contraint we are looking at may not be fully zonked; for example,
    an earlier defaulting might have affected it. So we zonk-on-the fly in
    `defaultEquality`.
  
  (DE4) Promotion. Suppose we see  alpha[2] := Maybe beta[4].  We want to promote
    beta[4] to level 2 and unify alpha[2] := Maybe beta'[2].  This is done by
    checkTyEqRhs called in defaultEquality.
  
  (DE5) Promotion. Suppose we see  alpha[2] := F beta[4], where F is a type
    family. Then we still want to promote beta to beta'[2], and unify. This is
    unusual: more commonly, we don't promote unification variables under a
    type family.  But here we want to.  (This mattered in #25251.)
  
    Hence the Bool flag on LC_Promote, and its use in `tef_unifying` in
    `defaultEquality`.
  
  (DE6) /Don't/ unify if the RHS has a free coercion hole in it.  That means
    that there is an as-yet-unsolved equality constraint (whose evidence
    will fill that hole); unifying can lead to very confusing type errors.
    e.g.    [W] co1 :: IntRep ~ LiftedRep
            [W] co2 {rewritten by co1} :: alpha ~ t2 |> (TYPE co1)
    Unifying alpha := (t1 |> TYPE co1) is a Bad Idea.
  
    Note that we /do/ unify even if the constraint has a non-empty rewriter
    set, which has prevented unification up to now; see
    Note [Unify only if the rewriter set is empty] in GHC.Tc.Solver.Equality.
    In obscure situations a constraint can end up in its own rewriter set, but
    without a coercion hole being in the RHS.
  
    See #10009, and Note [Limited defaulting in the ambiguity check].
  
  
  Note [Must simplify after defaulting]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  We may have a deeply buried constraint
      (t:*) ~ (a:Open)
  which we couldn't solve because of the kind incompatibility, and 'a' is free.
  Then when we default 'a' we can solve the constraint.  And we want to do
  that before starting in on type classes.  We MUST do it before reporting
  errors, because it isn't an error!  #7967 was due to this.
  
  Note [Defaulting representational equalities]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Suppose we end up with [W] alpha ~#R Int, with no other constraints on alpha.
  Then it makes sense to simply unify alpha := Int -- the alternative is to
  reject the program due to an ambiguous metavariable alpha, so it makes sense
  to unify and accept instead.
  
  This is particularly convenient for users of `coerce`, as it lessens the
  amount of type annotations required (see #21003). Consider for example:
  
    -- 'foldMap' defined using 'traverse'
    foldMapUsingTraverse :: forall t m a. (Traversable t, Monoid m) => (a -> m) -> t a -> m
    foldMapUsingTraverse = coerce $ traverse @t @(Const m)
  
    -- 'traverse_' defined using 'foldMap'
    traverse_UsingFoldMap :: forall f t a. (Foldable t, Applicative f) => (a -> f ()) -> t a -> f ()
    traverse_UsingFoldMap = coerce $ foldMap @t @(Ap f ())
  
  Typechecking these functions results in unsolved Wanted constraints of the form
  [W] alpha[tau] ~R# some_ty; accepting such programs by unifying
  alpha := some_ty avoids the need for users to specify tiresome additional
  type annotations, such as:
  
      foldMapUsingTraverse = coerce $ traverse @t @(Const m) @a
      traverse_UsingFoldMap = coerce $ foldMap @t @(Ap f ()) @a
  
  Consider also the following example:
  
    -- 'sequence_', but for two nested 'Foldable' structures
    sequenceNested_ :: forall f1 f2. (Foldable f1, Foldable f2) => f1 (f2 (IO ())) -> IO ()
    sequenceNested_ = coerce $ sequence_ @( Compose f1 f2 )
  
  Here, we end up with [W] mu[tau] beta[tau] ~#R IO (), and it similarly makes
  sense to default mu := IO, beta := (). This avoids requiring the
  user to provide additional type applications:
  
      sequenceNested_ = coerce $ sequence_ @( Compose f1 f2 ) @IO @()
  
  The plan for defaulting a representational equality, say [W] ty1 ~R# ty2,
  is thus as follows:
  
    1. attempt to unify ty1 ~# ty2 (at nominal role)
    2. a. if this succeeds without deferring any constraints, accept this solution
       b. otherwise, keep the original constraint.
  
  (2b) ensures that we don't degrade all error messages by always turning unsolved
  representational equalities into nominal ones; we only want to default a
  representational equality when we can fully solve it.
  
  Note that this does not threaten principle types. Recall that the original worry
  (as per Note [Do not unify representational equalities]) was that we might have
  
      [W] alpha ~R# Int
      [W] alpha ~ Age
  
  in which case unifying alpha := Int would be wrong, as the correct solution is
  alpha := Age. This worry doesn't concern us in top-level defaulting, because
  defaulting takes place after generalisation; it is fully monomorphic.
  
  *********************************************************************************
  *                                                                               *
  *                Type-class defaulting
  *                                                                               *
  *********************************************************************************
  
  Note [How type-class constraints are defaulted]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Type-class defaulting deals with the situation where we have unsolved
  constraints like (Num alpha), where `alpha` is a unification variable.  We want
  to pick a default for `alpha`, such as `alpha := Int` to resolve the ambiguity.
  
  The function 'tryTypeClassDefaulting' implements type-class defaulting. The
  algorithm for defaulting depends on whether certain extensions are enabled,
  such as -XOverloadedStrings or -XExtendedDefaultRules. To explain this, let us
  define the following:
  
    Unary typeclass:
      a typeclass with a single visible type argument.
  
      Examples:
  
        Num :: Type -> Constraint
        Eq :: Type -> Constraint
        Foldable :: (Type -> Type) -> Constraint
        Typeable :: forall k. k -> Constraint   -- NB: also has an /invisible/ argument
  
      Non-examples:
  
        Nullary :: Constraint
        Binary :: Type -> Type -> Constraint
        Binary2 :: forall k -> k -> Constraint  -- Two visible arguments
  
    Defaultable class
      a typeclass which has at least one in-scope default declaration
  
      This includes the two different categories of default declarations:
  
        - Haskell 98 default declarations such as 'default (Integer, Float)'.
  
          - `Num` is always defaultable; either the user says 'default( Integer, Float )'
            or (absent such a declaration) the system fills in a fallback default declaration.
            See Section 4.3.4 in https://www.haskell.org/onlinereport/haskell2010/haskellch4.html
  
          - With `OverloadedStrings`, the class `IsString` is defaultable
          - With `ExtendedDefaultRules`, the classes `Show`, `Eq`, `Ord`, `Foldable` and `Traversable`
            are defaultable
  
        - Named default declarations, which apply to the named class, e.g.
          'default Cls(X, Y)' applies precisely to 'Cls'.
          Note that these may be locally defined, or they may be imported.
  
    Standard class:
      a class defined in the Prelude or the standard library, as defined
      by the Haskell 98 report (section 4.3.4)
  
      These are defined in GHC.Builtin.Names.standardClassKeys.
  
  The rules for defaulting a collection 'S' of unsolved constraints are as follows:
  
    1. For each metavariable 'v' appearing in 'S', define
  
         U_v = { C v | C v ∈ U, C is a unary typeclass }
  
       We then process each 'U_v' in turn, in order to find a defaulting
       assignment 'v := ty' that solves all of 'U_v'.
  
    2. Unless -XExtendedDefaultRules is in effect, give up if 'v' appears:
  
        - in any constraint that isn't a unary class constraint
        - in a class constraint which is non-standard and does not have
          a default declaration in scope.
  
    3. Compute candidate assignments: for each unary typeclass 'C' in 'U_v' which
       has a default declaration in scope, find the first type 'ty' in the list
       of in-scope default types for 'C' for which all of 'U_v' is soluble.
  
    4. If there is precisely one type candidate type assignment 'ty' that allows
       all of 'U_v' to be solved, we default 'v := ty'. Otherwise, do nothing
       ('v' remains ambiguous).
  
  Note [Defaulting plugins]
  ~~~~~~~~~~~~~~~~~~~~~~~~~
  Defaulting plugins enable extending or overriding the defaulting
  behaviour. In `applyDefaultingRules`, before the built-in defaulting
  mechanism runs, the loaded defaulting plugins are passed the
  `WantedConstraints` and get a chance to propose defaulting assignments
  based on them.
  
  Proposals are represented as `[DefaultingProposal]` with each proposal
  consisting of a type variable to fill-in, the list of defaulting types to
  try in order, and a set of constraints to check at each try. This is
  the same representation (albeit in a nicely packaged-up data type) as
  the candidates generated by the built-in defaulting mechanism, so the
  actual trying of proposals is done by the same `disambigGroup` function.
  
  Wrinkle (DP1): The role of `WantedConstraints`
  
    Plugins are passed `WantedConstraints` that can perhaps be
    progressed on by defaulting. But a defaulting plugin is not a solver
    plugin, its job is to provide defaulting proposals, i.e. mappings of
    type variable to types. How do plugins know which type variables
    they are supposed to default?
  
    The `WantedConstraints` passed to the defaulting plugin are zonked
    beforehand to ensure all remaining metavariables are unfilled. Thus,
    the `WantedConstraints` serve a dual purpose: they are both the
    constraints of the given context that can act as hints to the
    defaulting, as well as the containers of the type variables under
    consideration for defaulting.
  
  Wrinkle (DP2): Interactions between defaulting mechanisms
  
    In the general case, we have multiple defaulting plugins loaded and
    there is also the built-in defaulting mechanism. In this case, we
    have to be careful to keep the `WantedConstraints` passed to the
    plugins up-to-date by zonking between successful defaulting
    rounds. Otherwise, two plugins might come up with a defaulting
    proposal for the same metavariable; if the first one is accepted by
    `disambigGroup` (thus the meta gets filled), the second proposal
    becomes invalid (see #23821 for an example).
  
  Note [Defaulting insolubles]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  If a set of wanteds is insoluble, we have no hope of accepting the
  program. Yet we do not stop constraint solving, etc., because we may
  simplify the wanteds to produce better error messages. So, once
  we have an insoluble constraint, everything we do is just about producing
  helpful error messages.
  
  Should we default in this case or not? Let's look at an example (tcfail004):
  
    (f,g) = (1,2,3)
  
  With defaulting, we get a conflict between (a0,b0) and (Integer,Integer,Integer).
  Without defaulting, we get a conflict between (a0,b0) and (a1,b1,c1). I (Richard)
  find the latter more helpful. Several other test cases (e.g. tcfail005) suggest
  similarly. So: we should not do class defaulting with insolubles.
  
  On the other hand, RuntimeRep-defaulting is different. Witness tcfail078:
  
    f :: Integer i => i
    f =               0
  
  Without RuntimeRep-defaulting, we GHC suggests that Integer should have kind
  TYPE r0 -> Constraint and then complains that r0 is actually untouchable
  (presumably, because it can't be sure if `Integer i` entails an equality).
  If we default, we are told of a clash between (* -> Constraint) and Constraint.
  The latter seems far better, suggesting we *should* do RuntimeRep-defaulting
  even on insolubles.
  
  But, evidently, not always. Witness UnliftedNewtypesInfinite:
  
    newtype Foo = FooC (# Int#, Foo #)
  
  This should fail with an occurs-check error on the kind of Foo (with -XUnliftedNewtypes).
  If we default RuntimeRep-vars, we get
  
    Expecting a lifted type, but ‘(# Int#, Foo #)’ is unlifted
  
  which is just plain wrong.
  
  Another situation in which we don't want to default involves concrete metavariables.
  
  In equalities such as   alpha[conc] ~# rr[sk]  ,  alpha[conc] ~# RR beta[tau]
  for a type family RR (all at kind RuntimeRep), we would prefer to report a
  representation-polymorphism error rather than default alpha and get error:
  
    Could not unify `rr` with `Lifted` / Could not unify `RR b0` with `Lifted`
  
  which is very confusing. For this reason, we weed out the concrete
  metavariables participating in such equalities in nonDefaultableTyVarsOfWC.
  Just looking at insolublity is not enough, as `alpha[conc] ~# RR beta[tau]` could
  become soluble after defaulting beta (see also #21430).
  
  Conclusion: we should do RuntimeRep-defaulting on insolubles only when the
  user does not want to hear about RuntimeRep stuff -- that is, when
  -fprint-explicit-runtime-reps is not set.
  However, we must still take care not to default concrete type variables
  participating in an equality with a non-concrete type, as seen in the
  last example above.
  
  -}
  
  tryTypeClassDefaulting :: WantedConstraints -> TcS WantedConstraints
  tryTypeClassDefaulting wc
    | isEmptyWC wc || insolubleWC wc -- See Note [Defaulting insolubles]
    = return wc
    | otherwise  -- See Note [When to do type-class defaulting]
    = do { something_happened <- applyDefaultingRules wc
                                 -- See Note [Top-level Defaulting Plan]
         ; solveAgainIf something_happened wc }
  
  applyDefaultingRules :: WantedConstraints -> TcS Bool
  -- True <=> I did some defaulting, by unifying a meta-tyvar
  -- Input WantedConstraints are not necessarily zonked
  -- See Note [How type-class constraints are defaulted]
  
  applyDefaultingRules wanteds
    | isEmptyWC wanteds
    = return False
    | otherwise
    = do { (default_env, extended_rules) <- getDefaultInfo
         ; wanteds                       <- TcS.zonkWC wanteds
  
         ; tcg_env <- TcS.getGblEnv
         ; let plugins = tcg_defaulting_plugins tcg_env
               default_tys = defaultList default_env
               -- see Note [Named default declarations] in GHC.Tc.Gen.Default
  
         -- Run any defaulting plugins
         -- See Note [Defaulting plugins] for an overview
         ; (wanteds, plugin_defaulted) <- if null plugins then return (wanteds, []) else
             do {
               ; traceTcS "defaultingPlugins {" (ppr wanteds)
               ; (wanteds, defaultedGroups) <- mapAccumLM run_defaulting_plugin wanteds plugins
               ; traceTcS "defaultingPlugins }" (ppr defaultedGroups)
               ; return (wanteds, defaultedGroups)
               }
  
         ; let groups = findDefaultableGroups (default_tys, extended_rules) wanteds
  
         ; traceTcS "applyDefaultingRules {" $
                    vcat [ text "wanteds =" <+> ppr wanteds
                         , text "groups  =" <+> ppr groups
                         , text "info    =" <+> ppr (default_tys, extended_rules) ]
  
         ; something_happeneds <- mapM (disambigGroup wanteds default_tys) groups
  
         ; traceTcS "applyDefaultingRules }" (ppr something_happeneds)
  
         ; return $ or something_happeneds || or plugin_defaulted }
  
      where
        run_defaulting_plugin wanteds p
            = do { groups <- runTcPluginTcS (p wanteds)
                 ; defaultedGroups <-
                      filterM (\g -> disambigMultiGroup
                                     wanteds
                                     (deProposalCts g)
                                     (ProposalSequence (Proposal <$> deProposals g)))
                      groups
                 ; traceTcS "defaultingPlugin " $ ppr defaultedGroups
                 ; case defaultedGroups of
                   [] -> return (wanteds, False)
                   _  -> do
                       -- If a defaulting plugin solves any tyvars, some of the wanteds
                       -- will have filled-in metavars by now (see wrinkle DP2 of
                       -- Note [Defaulting plugins]). So we re-zonk to make sure later
                       -- defaulting doesn't try to solve the same metavars.
                       wanteds' <- TcS.zonkWC wanteds
                       return (wanteds', True) }
  
  findDefaultableGroups
      :: ( [ClassDefaults]
         , Bool )            -- extended default rules
      -> WantedConstraints   -- Unsolved
      -> [(TyVar, [Ct])]
  findDefaultableGroups (default_tys, extended_defaults) wanteds
    | null default_tys
    = []
    | otherwise
    = [ (tv, map fstOf3 group)
      | group'@((_,_,tv) :| _) <- unary_groups
      , let group = toList group'
      , defaultable_tyvar tv
      , defaultable_classes (map sndOf3 group) ]
    where
      simples  = approximateWC True wanteds
        -- True: for the purpose of defaulting we don't care
        --       about shape or enclosing equalities
        -- See (W3) in Note [ApproximateWC] in GHC.Tc.Types.Constraint
  
      (unaries, non_unaries) = partitionWith find_unary (bagToList simples)
      unary_groups           = equivClasses cmp_tv unaries
  
      unary_groups :: [NonEmpty (Ct, Class, TcTyVar)] -- (C tv) constraints
      unaries      :: [(Ct, Class, TcTyVar)]          -- (C tv) constraints
      non_unaries  :: [Ct]                            -- and *other* constraints
  
      -- Finds unary type-class constraints
      -- But take account of polykinded classes like Typeable,
      -- which may look like (Typeable Type (a:Type))   (#8931)
      -- See step (1) in Note [How type-class constraints are defaulted]
      find_unary :: Ct -> Either (Ct, Class, TyVar) Ct
      find_unary cc
          | Just (cls,tys)   <- getClassPredTys_maybe (ctPred cc)
          , [ty] <- filterOutInvisibleTypes (classTyCon cls) tys
                -- Ignore invisible arguments for this purpose
          , Just tv <- getTyVar_maybe ty
          , isMetaTyVar tv  -- We might have runtime-skolems in GHCi, and
                            -- we definitely don't want to try to assign to those!
          = Left (cc, cls, tv)
      find_unary cc = Right cc  -- Non unary or non dictionary
  
      nonunary_tvs :: TcTyCoVarSet  -- TyVars mentioned by non-unaries
      nonunary_tvs = mapUnionVarSet tyCoVarsOfCt non_unaries
  
      cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
  
      defaultable_tyvar :: TcTyVar -> Bool
      defaultable_tyvar tv
          = let b1 = isTyConableTyVar tv  -- Note [Avoiding spurious errors]
                b2 = not (tv `elemVarSet` nonunary_tvs)
            in b1 && (b2 || extended_defaults) -- Note [Multi-parameter defaults]
  
      -- Determines whether the collection of class constraints permits defaulting.
      -- See step (2) in Note [How type-class constraints are defaulted]
      defaultable_classes :: [Class] -> Bool
      defaultable_classes clss =
        -- One of the classes has a default declaration in scope
        -- (this includes 'Num', and e.g. 'IsString' with -XOverloadedStrings)
        any (`elementOfUniqSet` classes_with_defaults) clss
          &&
        -- AND, either:
        --  - ExtendedDefaultRules is in effect, or
        --  - all the classes are standard or have a default declaration in scope
        (extended_defaults || all is_std_or_has_default clss)
      is_std_or_has_default :: Class -> Bool
      is_std_or_has_default cls =
        (getUnique cls `elem` standardClassKeys)
          ||
        (cls `elementOfUniqSet` classes_with_defaults)
  
      -- All classes with a default declaration in scope; either:
      --
      --  - a named default declaration such as 'default C(Double, Bool)', or
      --  - a Haskell 98 default declaration such as 'default(Int, Float)',
      --    which adds defaults for Num, for IsString with OverloadedStrings,
      --    and for Foldable/Traversable/... with ExtendedDefaultRules
      classes_with_defaults = mkUniqSet $ map cd_class default_tys
  
  ------------------------------
  
  -- | 'Proposal's to be tried in sequence until the first one that succeeds
  newtype ProposalSequence = ProposalSequence{getProposalSequence :: [Proposal]}
  
  -- | An atomic set of proposed type assignments to try applying all at once
  newtype Proposal = Proposal [(TcTyVar, Type)]
  
  instance Outputable ProposalSequence where
    ppr (ProposalSequence proposals) = ppr proposals
  instance Outputable Proposal where
    ppr (Proposal assignments) = ppr assignments
  
  disambigGroup :: WantedConstraints -- ^ Original constraints, for diagnostic purposes
                -> [ClassDefaults]   -- ^ The default classes and types
                -> (TcTyVar, [Ct])   -- ^ All constraints sharing same type variable
                -> TcS Bool   -- True <=> something happened, reflected in ty_binds
  disambigGroup orig_wanteds default_ctys (tv, wanteds)
    = disambigProposalSequences orig_wanteds wanteds proposalSequences allConsistent
    where
      proposalSequences = [ ProposalSequence [Proposal [(tv, ty)] | ty <- tys]
                          | ClassDefaults{cd_types = tys} <- defaultses ]
      allConsistent ((_, sub) :| subs) = all (eqSubAt tv sub . snd) subs
      defaultses =
        [ defaults | defaults@ClassDefaults{cd_class = cls} <- default_ctys
                   , any (isDictForClass (className cls)) wanteds ]
      isDictForClass clcon ct = any ((clcon ==) . className . fst) (getClassPredTys_maybe $ ctPred ct)
      eqSubAt :: TcTyVar -> Subst -> Subst -> Bool
      eqSubAt tvar s1 s2 = or $ liftA2 tcEqType (lookupTyVar s1 tvar) (lookupTyVar s2 tvar)
  
  -- See Note [How type-class constraints are defaulted]
  disambigMultiGroup :: WantedConstraints    -- ^ Original constraints, for diagnostic purposes
                     -> [Ct]                 -- ^ check these are solved by defaulting
                     -> ProposalSequence     -- ^ defaulting type assignments to try
                     -> TcS Bool   -- True <=> something happened, reflected in ty_binds
  disambigMultiGroup orig_wanteds wanteds proposalSequence
    = disambigProposalSequences orig_wanteds wanteds [proposalSequence] (const True)
  
  disambigProposalSequences :: WantedConstraints   -- ^ Original constraints, for diagnostic purposes
                            -> [Ct]                -- ^ Check these are solved by defaulting
                            -> [ProposalSequence]  -- ^ The sequences of assignment proposals
                            -> (NonEmpty ([TcTyVar], Subst) -> Bool)
                                                   -- ^ Predicate for successful assignments
                            -> TcS Bool   -- True <=> something happened, reflected in ty_binds
  disambigProposalSequences orig_wanteds wanteds proposalSequences allConsistent
    = do { traverse_ (traverse_ reportInvalidDefaultedTyVars . getProposalSequence) proposalSequences
         ; fake_ev_binds_var <- TcS.newTcEvBinds
         ; tclvl             <- TcS.getTcLevel
         -- Step (3) in Note [How type-class constraints are defaulted]
         ; successes <- fmap catMaybes $
                        nestImplicTcS fake_ev_binds_var (pushTcLevel tclvl) $
                        mapM firstSuccess proposalSequences
         ; traceTcS "disambigProposalSequences {" (vcat [ ppr wanteds
                                                        , ppr proposalSequences
                                                        , ppr successes ])
         -- Step (4) in Note [How type-class constraints are defaulted]
         ; case successes of
             success@(tvs, subst) : rest
               | allConsistent (success :| rest)
               -> do { applyDefaultSubst tvs subst
                     ; let warn tv = mapM_ (warnDefaulting wanteds tv) (lookupTyVar subst tv)
                     ; wrapWarnTcS $ mapM_ warn tvs
                     ; traceTcS "disambigProposalSequences succeeded }" (ppr proposalSequences)
                     ; return True }
             _ ->
               do { traceTcS "disambigProposalSequences failed }" (ppr proposalSequences)
                  ; return False } }
    where
      reportInvalidDefaultedTyVars :: Proposal -> TcS ()
      firstSuccess :: ProposalSequence -> TcS (Maybe ([TcTyVar], Subst))
      firstSuccess (ProposalSequence proposals)
        = getFirst <$> foldMapM (fmap First . tryDefaultGroup wanteds) proposals
      reportInvalidDefaultedTyVars proposal@(Proposal assignments)
        = do { let tvs = fst <$> assignments
               ; invalid_tvs <- filterOutM TcS.isUnfilledMetaTyVar tvs
               ; traverse_ (errInvalidDefaultedTyVar orig_wanteds proposal) (nonEmpty invalid_tvs) }
  
  applyDefaultSubst :: [TcTyVar] -> Subst -> TcS ()
  applyDefaultSubst tvs subst =
    do { deep_tvs <- filterM TcS.isUnfilledMetaTyVar $ nonDetEltsUniqSet $ closeOverKinds (mkVarSet tvs)
       ; forM_ deep_tvs $ \ tv -> mapM_ (unifyTyVar tv) (lookupVarEnv (getTvSubstEnv subst) tv)
       }
  
  tryDefaultGroup :: [Ct]       -- ^ check these are solved by defaulting
                  -> Proposal   -- ^ defaulting type assignments to try
                  -> TcS (Maybe ([TcTyVar], Subst))  -- ^ successful substitutions, *not* reflected in ty_binds
  tryDefaultGroup wanteds (Proposal assignments)
            | let (tvs, default_tys) = unzip assignments
            , Just subst <- tcMatchTyKis (mkTyVarTys tvs) default_tys
              -- Make sure the kinds match too; hence this call to tcMatchTyKi
              -- E.g. suppose the only constraint was (Typeable k (a::k))
              -- With the addition of polykinded defaulting we also want to reject
              -- ill-kinded defaulting attempts like (Eq []) or (Foldable Int) here.
            = do { lcl_env <- TcS.getLclEnv
                 ; tc_lvl <- TcS.getTcLevel
                 ; let loc = mkGivenLoc tc_lvl (getSkolemInfo unkSkol) (mkCtLocEnv lcl_env)
                       new_wtd_ct :: WantedCtEvidence -> TcS Ct
                       new_wtd_ct (WantedCt { ctev_pred = wtd_pred, ctev_rewriters = rws }) =
                         mkNonCanonical . CtWanted <$>
                           -- NB: equality constraints are possible,
                           -- due to type defaulting plugins
                           newWantedNC loc rws (substTy subst wtd_pred)
                 ; new_wanteds <- sequence [ new_wtd_ct wtd
                                           | CtWanted wtd <- map ctEvidence wanteds
                                           ]
                 ; residual <- solveSimpleWanteds (listToBag new_wanteds)
                 ; return $ if isEmptyWC residual then Just (tvs, subst) else Nothing }
  
            | otherwise
            = return Nothing
  
  errInvalidDefaultedTyVar :: WantedConstraints -> Proposal -> NonEmpty TcTyVar -> TcS ()
  errInvalidDefaultedTyVar wanteds (Proposal assignments) problematic_tvs
    = failTcS $ TcRnInvalidDefaultedTyVar tidy_wanteds tidy_assignments tidy_problems
    where
      proposal_tvs = concatMap (\(tv, ty) -> tv : tyCoVarsOfTypeList ty) assignments
      tidy_env = tidyFreeTyCoVars emptyTidyEnv $ proposal_tvs ++ NE.toList problematic_tvs
      tidy_wanteds = map (tidyCt tidy_env) $ flattenWC wanteds
      tidy_assignments = [(tidyTyCoVarOcc tidy_env tv, tidyType tidy_env ty) | (tv, ty) <- assignments]
      tidy_problems = fmap (tidyTyCoVarOcc tidy_env) problematic_tvs
  
      flattenWC :: WantedConstraints -> [Ct]
      flattenWC (WC { wc_simple = cts, wc_impl = impls })
        = ctsElts cts ++ concatMap (flattenWC . ic_wanted) impls
  
  -- In interactive mode, or with -XExtendedDefaultRules,
  -- we default Show a to Show () to avoid gratuitous errors on "show []"
  isInteractiveClass :: Bool   -- -XOverloadedStrings?
                     -> Class -> Bool
  isInteractiveClass ovl_strings cls
      = isNumClass ovl_strings cls || (classKey cls `elem` interactiveClassKeys)
  
      -- isNumClass adds IsString to the standard numeric classes,
      -- when -XOverloadedStrings is enabled
  isNumClass :: Bool   -- -XOverloadedStrings?
             -> Class -> Bool
  isNumClass ovl_strings cls
    = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
  
  
  {-
  Note [Avoiding spurious errors]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  When doing the unification for defaulting, we check for skolem
  type variables, and simply don't default them.  For example:
     f = (*)      -- Monomorphic
     g :: Num a => a -> a
     g x = f x x
  Here, we get a complaint when checking the type signature for g,
  that g isn't polymorphic enough; but then we get another one when
  dealing with the (Num a) context arising from f's definition;
  we try to unify a with Int (to default it), but find that it's
  already been unified with the rigid variable from g's type sig.
  
  Note [Multi-parameter defaults]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  With -XExtendedDefaultRules, we default only based on single-variable
  constraints, but do not exclude from defaulting any type variables which also
  appear in multi-variable constraints. This means that the following will
  default properly:
  
     default (Integer, Double)
  
     class A b (c :: Symbol) where
        a :: b -> Proxy c
  
     instance A Integer c where a _ = Proxy
  
     main = print (a 5 :: Proxy "5")
  
  Note that if we change the above instance ("instance A Integer") to
  "instance A Double", we get an error:
  
     No instance for (A Integer "5")
  
  This is because the first defaulted type (Integer) has successfully satisfied
  its single-parameter constraints (in this case Num).
  -}
  