module GHC.Tc.Solver.Default(
   tryDefaulting, tryUnsatisfiableGivens,
   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( mkNomReflCo, isReflCo )
import GHC.Core.Unify    ( tcMatchTyKis )
import GHC.Core.Predicate
import GHC.Core.Type
import GHC.Core.TyCon    ( TyCon )

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          ( intersect )
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].
-}


tryDefaulting :: WantedConstraints -> TcS WantedConstraints
-- This is the function that pulls all the defaulting strategies together
tryDefaulting :: WantedConstraints -> TcS WantedConstraints
tryDefaulting WantedConstraints
wc
 = do { dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
      ; traceTcS "tryDefaulting:before" (ppr wc)
      ; wc1 <- tryTyVarDefaulting dflags wc
      ; wc2 <- tryConstraintDefaulting wc1
      ; wc3 <- tryTypeClassDefaulting wc2
      ; wc4 <- tryUnsatisfiableGivens wc3
      ; traceTcS "tryDefaulting:after" (ppr wc4)
      ; return wc4 }

solveAgainIf :: Bool -> WantedConstraints -> TcS WantedConstraints
-- If the Bool is true, solve the wanted constraints again
-- See Note [Must simplify after defaulting]
solveAgainIf :: Bool -> WantedConstraints -> TcS WantedConstraints
solveAgainIf Bool
False WantedConstraints
wc = WantedConstraints -> TcS WantedConstraints
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return WantedConstraints
wc
solveAgainIf Bool
True  WantedConstraints
wc = TcS WantedConstraints -> TcS WantedConstraints
forall a. TcS a -> TcS a
nestTcS (WantedConstraints -> TcS WantedConstraints
solveWanteds WantedConstraints
wc)


{- ******************************************************************************
*                                                                               *
                        tryTyVarDefaulting
*                                                                               *
****************************************************************************** -}

tryTyVarDefaulting  :: DynFlags -> WantedConstraints -> TcS WantedConstraints
tryTyVarDefaulting :: DynFlags -> WantedConstraints -> TcS WantedConstraints
tryTyVarDefaulting DynFlags
dflags WantedConstraints
wc
  | WantedConstraints -> Bool
isEmptyWC WantedConstraints
wc
  = WantedConstraints -> TcS WantedConstraints
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return WantedConstraints
wc
  | WantedConstraints -> Bool
insolubleWC WantedConstraints
wc
  , GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_PrintExplicitRuntimeReps DynFlags
dflags -- See Note [Defaulting insolubles]
  = WantedConstraints -> TcS WantedConstraints
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return WantedConstraints
wc
  | Bool
otherwise
  = do { -- Need to zonk first, as the WantedConstraints are not yet zonked.
       ; free_tvs <- [TcTyVar] -> TcS [TcTyVar]
TcS.zonkTyCoVarsAndFVList (WantedConstraints -> [TcTyVar]
tyCoVarsOfWCList WantedConstraints
wc)
       ; let defaultable_tvs = (TcTyVar -> Bool) -> [TcTyVar] -> [TcTyVar]
forall a. (a -> Bool) -> [a] -> [a]
filter TcTyVar -> Bool
can_default [TcTyVar]
free_tvs
             can_default TcTyVar
tv
               =   TcTyVar -> Bool
isTyVar TcTyVar
tv
                   -- Weed out coercion variables.

                Bool -> Bool -> Bool
&& TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
                   -- Weed out runtime-skolems in GHCi, which we definitely
                   -- shouldn't try to default.

                Bool -> Bool -> Bool
&& Bool -> Bool
not (TcTyVar
tv TcTyVar -> VarSet -> Bool
`elemVarSet` WantedConstraints -> VarSet
nonDefaultableTyVarsOfWC WantedConstraints
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 :: Bool
noUnification  = Bool
False
didUnification :: Bool
didUnification = Bool
True

-- | Like 'defaultTyVar', but in the TcS monad.
defaultTyVarTcS :: TcTyVar -> TcS UnificationDone
defaultTyVarTcS :: TcTyVar -> TcS Bool
defaultTyVarTcS TcTyVar
the_tv
  | TcTyVar -> Bool
isTyVarTyVar TcTyVar
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
  = Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
noUnification
  | TcTyVar -> Bool
isRuntimeRepVar TcTyVar
the_tv
  = do { String -> SDoc -> TcS ()
traceTcS String
"defaultTyVarTcS RuntimeRep" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
the_tv)
       ; TcTyVar -> TcType -> TcS ()
unifyTyVar TcTyVar
the_tv TcType
liftedRepTy
       ; Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
didUnification }
  | TcTyVar -> Bool
isLevityVar TcTyVar
the_tv
  = do { String -> SDoc -> TcS ()
traceTcS String
"defaultTyVarTcS Levity" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
the_tv)
       ; TcTyVar -> TcType -> TcS ()
unifyTyVar TcTyVar
the_tv TcType
liftedDataConTy
       ; Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
didUnification }
  | TcTyVar -> Bool
isMultiplicityVar TcTyVar
the_tv
  = do { String -> SDoc -> TcS ()
traceTcS String
"defaultTyVarTcS Multiplicity" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
the_tv)
       ; TcTyVar -> TcType -> TcS ()
unifyTyVar TcTyVar
the_tv TcType
ManyTy
       ; Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
didUnification }
  | Bool
otherwise
  = Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
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 :: WantedConstraints -> TcS WantedConstraints
tryUnsatisfiableGivens WantedConstraints
wc =
  do { (final_wc, did_work) <- (StateT Bool TcS WantedConstraints
-> Bool -> TcS (WantedConstraints, Bool)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
`runStateT` Bool
False) (StateT Bool TcS WantedConstraints
 -> TcS (WantedConstraints, Bool))
-> StateT Bool TcS WantedConstraints
-> TcS (WantedConstraints, Bool)
forall a b. (a -> b) -> a -> b
$ WantedConstraints -> StateT Bool TcS WantedConstraints
go_wc WantedConstraints
wc
     ; solveAgainIf did_work final_wc }
  where
    go_wc :: WantedConstraints -> StateT Bool TcS WantedConstraints
go_wc (WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
wtds, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
impls, wc_errors :: WantedConstraints -> Bag DelayedError
wc_errors = Bag DelayedError
errs })
      = do impls' <- (Implication -> StateT Bool TcS (Maybe Implication))
-> Bag Implication -> StateT Bool TcS (Bag Implication)
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> Bag a -> m (Bag b)
mapMaybeBagM Implication -> StateT Bool TcS (Maybe Implication)
go_impl Bag Implication
impls
           return $ WC { wc_simple = wtds, wc_impl = impls', wc_errors = errs }
    go_impl :: Implication -> StateT Bool TcS (Maybe Implication)
go_impl Implication
impl
      | ImplicStatus -> Bool
isSolvedStatus (Implication -> ImplicStatus
ic_status Implication
impl)
      = Maybe Implication -> StateT Bool TcS (Maybe Implication)
forall a. a -> StateT Bool TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Implication -> StateT Bool TcS (Maybe Implication))
-> Maybe Implication -> StateT Bool TcS (Maybe Implication)
forall a b. (a -> b) -> a -> b
$ Implication -> Maybe Implication
forall a. a -> Maybe a
Just Implication
impl
      -- Is there a Given with type "Unsatisfiable msg"?
      -- If so, use it to solve all other Wanteds.
      | (TcTyVar, TcType)
unsat_given:[(TcTyVar, TcType)]
_ <- (TcTyVar -> Maybe (TcTyVar, TcType))
-> [TcTyVar] -> [(TcTyVar, TcType)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TcTyVar -> Maybe (TcTyVar, TcType)
unsatisfiableEv_maybe (Implication -> [TcTyVar]
ic_given Implication
impl)
      = do { Bool -> StateT Bool TcS ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put Bool
True
           ; TcS (Maybe Implication) -> StateT Bool TcS (Maybe Implication)
forall (m :: * -> *) a. Monad m => m a -> StateT Bool m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TcS (Maybe Implication) -> StateT Bool TcS (Maybe Implication))
-> TcS (Maybe Implication) -> StateT Bool TcS (Maybe Implication)
forall a b. (a -> b) -> a -> b
$ (TcTyVar, TcType) -> Implication -> TcS (Maybe Implication)
solveImplicationUsingUnsatGiven (TcTyVar, TcType)
unsat_given Implication
impl }
      -- Otherwise, recurse.
      | Bool
otherwise
      = do { wcs' <- WantedConstraints -> StateT Bool TcS WantedConstraints
go_wc (Implication -> WantedConstraints
ic_wanted Implication
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 :: TcTyVar -> Maybe (TcTyVar, TcType)
unsatisfiableEv_maybe TcTyVar
v = (TcTyVar
v,) (TcType -> (TcTyVar, TcType))
-> Maybe TcType -> Maybe (TcTyVar, TcType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcType -> Maybe TcType
isUnsatisfiableCt_maybe (TcTyVar -> TcType
idType TcTyVar
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 (Maybe Implication)
solveImplicationUsingUnsatGiven :: (TcTyVar, TcType) -> Implication -> TcS (Maybe Implication)
solveImplicationUsingUnsatGiven
  unsat_given :: (TcTyVar, TcType)
unsat_given@(TcTyVar
given_ev,TcType
_)
  impl :: Implication
impl@(Implic { ic_wanted :: Implication -> WantedConstraints
ic_wanted = WantedConstraints
wtd, ic_tclvl :: Implication -> TcLevel
ic_tclvl = TcLevel
tclvl, ic_binds :: Implication -> EvBindsVar
ic_binds = EvBindsVar
ev_binds_var, ic_need_inner :: Implication -> VarSet
ic_need_inner = VarSet
inner })
  | EvBindsVar -> Bool
isCoEvBindsVar EvBindsVar
ev_binds_var
  -- We can't use Unsatisfiable evidence in kinds.
  -- See Note [Coercion evidence only] in GHC.Tc.Types.Evidence.
  = Maybe Implication -> TcS (Maybe Implication)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Implication -> TcS (Maybe Implication))
-> Maybe Implication -> TcS (Maybe Implication)
forall a b. (a -> b) -> a -> b
$ Implication -> Maybe Implication
forall a. a -> Maybe a
Just Implication
impl
  | Bool
otherwise
  = do { wcs <- EvBindsVar
-> TcLevel -> TcS WantedConstraints -> TcS WantedConstraints
forall a. EvBindsVar -> TcLevel -> TcS a -> TcS a
nestImplicTcS EvBindsVar
ev_binds_var TcLevel
tclvl (TcS WantedConstraints -> TcS WantedConstraints)
-> TcS WantedConstraints -> TcS WantedConstraints
forall a b. (a -> b) -> a -> b
$ WantedConstraints -> TcS WantedConstraints
go_wc WantedConstraints
wtd
       ; setImplicationStatus $
         impl { ic_wanted = wcs
              , ic_need_inner = inner `extendVarSet` given_ev } }
  where
    go_wc :: WantedConstraints -> TcS WantedConstraints
    go_wc :: WantedConstraints -> TcS WantedConstraints
go_wc wc :: WantedConstraints
wc@(WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
wtds, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
impls })
      = do { (Ct -> TcS ()) -> Cts -> TcS ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> Bag a -> m ()
mapBagM_ Ct -> TcS ()
go_simple Cts
wtds
           ; impls <- (Implication -> TcS (Maybe Implication))
-> Bag Implication -> TcS (Bag Implication)
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> Bag a -> m (Bag b)
mapMaybeBagM ((TcTyVar, TcType) -> Implication -> TcS (Maybe Implication)
solveImplicationUsingUnsatGiven (TcTyVar, TcType)
unsat_given) Bag Implication
impls
           ; return $ wc { wc_simple = emptyBag, wc_impl = impls } }
    go_simple :: Ct -> TcS ()
    go_simple :: Ct -> TcS ()
go_simple Ct
ct = case Ct -> CtEvidence
ctEvidence Ct
ct of
      CtWanted { ctev_pred :: CtEvidence -> TcType
ctev_pred = TcType
pty, ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dst }
        -> do { ev_expr <- (TcTyVar, TcType) -> TcType -> TcS EvExpr
unsatisfiableEvExpr (TcTyVar, TcType)
unsat_given TcType
pty
              ; setWantedEvTerm dst EvNonCanonical $ EvExpr ev_expr }
      CtEvidence
_ -> () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
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 :: (TcTyVar, TcType) -> TcType -> TcS EvExpr
unsatisfiableEvExpr (TcTyVar
unsat_ev, TcType
given_msg) TcType
wtd_ty
  = do { mod <- TcS Module
forall (m :: * -> *). HasModule m => m Module
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 = HasDebugCallStack =>
FunTyFlag -> TcType -> TcType -> TcType -> TcType
FunTyFlag -> TcType -> TcType -> TcType -> TcType
mkFunTy FunTyFlag
visArgConstraintLike TcType
ManyTy TcType
unboxedUnitTy TcType
wtd_ty
             mkDictBox = case TcType -> BoxingInfo (ZonkAny 0)
forall b. TcType -> BoxingInfo b
boxingDataCon TcType
fun_ty of
               BI_Box { bi_data_con :: forall b. BoxingInfo b -> DataCon
bi_data_con = DataCon
mkDictBox } -> DataCon
mkDictBox
               BoxingInfo (ZonkAny 0)
_ -> String -> SDoc -> DataCon
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"unsatisfiableEvExpr: no DictBox!" (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
wtd_ty)
             dictBox = DataCon -> TyCon
dataConTyCon DataCon
mkDictBox
       ; ev_bndr <- mkSysLocalM (fsLit "ct") ManyTy fun_ty
             -- Dict ((##) -=> wtd_ty)
       ; let scrut_ty = TyCon -> [TcType] -> TcType
mkTyConApp TyCon
dictBox [TcType
fun_ty]
             -- unsatisfiable @{LiftedRep} @given_msg @(Dict ((##) -=> wtd_ty)) unsat_ev
             scrut =
               EvExpr -> [EvExpr] -> EvExpr
mkCoreApps (TcTyVar -> EvExpr
forall b. TcTyVar -> Expr b
Var TcTyVar
unsatisfiable_id)
                 [ TcType -> EvExpr
forall b. TcType -> Expr b
Type TcType
liftedRepTy
                 , TcType -> EvExpr
forall b. TcType -> Expr b
Type TcType
given_msg
                 , TcType -> EvExpr
forall b. TcType -> Expr b
Type TcType
scrut_ty
                 , TcTyVar -> EvExpr
forall b. TcTyVar -> Expr b
Var TcTyVar
unsat_ev ]
             -- case scrut of { MkDictBox @((##) -=> wtd_ty)) ct -> ct (# #) }
             ev_expr =
               EvExpr -> Scaled TcType -> TcType -> [CoreAlt] -> EvExpr
mkWildCase EvExpr
scrut (TcType -> Scaled TcType
forall a. a -> Scaled a
unrestricted (TcType -> Scaled TcType) -> TcType -> Scaled TcType
forall a b. (a -> b) -> a -> b
$ TcType
scrut_ty) TcType
wtd_ty
               [ AltCon -> [TcTyVar] -> EvExpr -> CoreAlt
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
mkDictBox) [TcTyVar
ev_bndr] (EvExpr -> CoreAlt) -> EvExpr -> CoreAlt
forall a b. (a -> b) -> a -> b
$
                   EvExpr -> [EvExpr] -> EvExpr
mkCoreApps (TcTyVar -> EvExpr
forall b. TcTyVar -> Expr b
Var TcTyVar
ev_bndr) [EvExpr
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 :: WantedConstraints -> TcS WantedConstraints
tryConstraintDefaulting WantedConstraints
wc
  | WantedConstraints -> Bool
isEmptyWC WantedConstraints
wc
  = WantedConstraints -> TcS WantedConstraints
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return WantedConstraints
wc
  | Bool
otherwise
  = do { (n_unifs, better_wc) <- TcS WantedConstraints -> TcS (Int, WantedConstraints)
forall a. TcS a -> TcS (Int, a)
reportUnifications (WantedConstraints -> TcS WantedConstraints
go_wc WantedConstraints
wc)
         -- We may have done unifications; so solve again
       ; solveAgainIf (n_unifs > 0) better_wc }
  where
    go_wc :: WantedConstraints -> TcS WantedConstraints
    go_wc :: WantedConstraints -> TcS WantedConstraints
go_wc wc :: WantedConstraints
wc@(WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implics })
      = do { mb_simples <- (Ct -> TcS (Maybe Ct)) -> Cts -> TcS Cts
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> Bag a -> m (Bag b)
mapMaybeBagM Ct -> TcS (Maybe Ct)
go_simple Cts
simples
           ; mb_implics <- mapMaybeBagM go_implic implics
           ; return (wc { wc_simple = mb_simples, wc_impl   = mb_implics }) }

    go_simple :: Ct -> TcS (Maybe Ct)
    go_simple :: Ct -> TcS (Maybe Ct)
go_simple Ct
ct = do { solved <- CtDefaultingStrategy
tryCtDefaultingStrategy Ct
ct
                      ; if solved then return Nothing
                                  else return (Just ct) }

    go_implic :: Implication -> TcS (Maybe Implication)
    -- The Maybe is because solving the CallStack constraint
    -- may well allow us to discard the implication entirely
    go_implic :: Implication -> TcS (Maybe Implication)
go_implic Implication
implic
      | ImplicStatus -> Bool
isSolvedStatus (Implication -> ImplicStatus
ic_status Implication
implic)
      = Maybe Implication -> TcS (Maybe Implication)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Implication -> Maybe Implication
forall a. a -> Maybe a
Just Implication
implic)  -- Nothing to solve inside here
      | Bool
otherwise
      = do { wanteds <- EvBindsVar -> TcS WantedConstraints -> TcS WantedConstraints
forall a. EvBindsVar -> TcS a -> TcS a
setEvBindsTcS (Implication -> EvBindsVar
ic_binds Implication
implic) (TcS WantedConstraints -> TcS WantedConstraints)
-> TcS WantedConstraints -> TcS WantedConstraints
forall a b. (a -> b) -> a -> b
$
                        -- defaultCallStack sets a binding, so
                        -- we must set the correct binding group
                        WantedConstraints -> TcS WantedConstraints
go_wc (Implication -> WantedConstraints
ic_wanted Implication
implic)
           ; setImplicationStatus (implic { ic_wanted = wanteds }) }

tryCtDefaultingStrategy :: CtDefaultingStrategy
-- The composition of all the CtDefaultingStrategies we want
tryCtDefaultingStrategy :: CtDefaultingStrategy
tryCtDefaultingStrategy
  = (CtDefaultingStrategy
 -> CtDefaultingStrategy -> CtDefaultingStrategy)
-> [CtDefaultingStrategy] -> CtDefaultingStrategy
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 CtDefaultingStrategy
-> CtDefaultingStrategy -> CtDefaultingStrategy
combineStrategies
    [ CtDefaultingStrategy
defaultCallStack
    , CtDefaultingStrategy
defaultExceptionContext
    , CtDefaultingStrategy
defaultEquality ]

-- | Default @ExceptionContext@ constraints to @emptyExceptionContext@.
defaultExceptionContext :: CtDefaultingStrategy
defaultExceptionContext :: CtDefaultingStrategy
defaultExceptionContext Ct
ct
  | ClassPred Class
cls [TcType]
tys <- TcType -> Pred
classifyPredType (Ct -> TcType
ctPred Ct
ct)
  , Maybe FastString -> Bool
forall a. Maybe a -> Bool
isJust (Class -> [TcType] -> Maybe FastString
isExceptionContextPred Class
cls [TcType]
tys)
  = do { TcRnMessage -> TcS ()
warnTcS (TcRnMessage -> TcS ()) -> TcRnMessage -> TcS ()
forall a b. (a -> b) -> a -> b
$ CtLoc -> TcRnMessage
TcRnDefaultedExceptionContext (Ct -> CtLoc
ctLoc Ct
ct)
       ; empty_ec_id <- Name -> TcS TcTyVar
forall (m :: * -> *). MonadThings m => Name -> m TcTyVar
lookupId Name
emptyExceptionContextName
       ; let ev = Ct -> CtEvidence
ctEvidence Ct
ct
             ev_tm = EvExpr -> TcCoercion -> EvTerm
mkEvCast (TcTyVar -> EvExpr
forall b. TcTyVar -> Expr b
Var TcTyVar
empty_ec_id) (TcType -> TcCoercion
wrapIP (CtEvidence -> TcType
ctEvPred CtEvidence
ev))
       ; setEvBindIfWanted ev EvCanonical ev_tm
         -- EvCanonical: see Note [CallStack and ExecptionContext hack]
         --              in GHC.Tc.Solver.Dict
       ; return True }
  | Bool
otherwise
  = Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- | Default any remaining @CallStack@ constraints to empty @CallStack@s.
-- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
defaultCallStack :: CtDefaultingStrategy
defaultCallStack :: CtDefaultingStrategy
defaultCallStack Ct
ct
  | ClassPred Class
cls [TcType]
tys <- TcType -> Pred
classifyPredType (Ct -> TcType
ctPred Ct
ct)
  , Maybe FastString -> Bool
forall a. Maybe a -> Bool
isJust (Class -> [TcType] -> Maybe FastString
isCallStackPred Class
cls [TcType]
tys)
  = do { CtEvidence -> EvCallStack -> TcS ()
solveCallStack (Ct -> CtEvidence
ctEvidence Ct
ct) EvCallStack
EvCsEmpty
       ; Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True }
  | Bool
otherwise
  = Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

defaultEquality :: CtDefaultingStrategy
-- See Note [Defaulting equalities]
defaultEquality :: CtDefaultingStrategy
defaultEquality Ct
ct
  | EqPred EqRel
NomEq TcType
ty1 TcType
ty2 <- TcType -> Pred
classifyPredType (Ct -> TcType
ctPred Ct
ct)
  = do { -- Remember: `ct` may not be zonked;
         -- see (DE3) in Note [Defaulting equalities]
         z_ty1 <- TcType -> TcS TcType
TcS.zonkTcType TcType
ty1
       ; z_ty2 <- TcS.zonkTcType ty2

       -- 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 TcTyVar
z_tv1, Maybe TcTyVar
_) -> TcTyVar -> TcType -> TcS Bool
try_default_tv TcTyVar
z_tv1 TcType
z_ty2
           (Maybe TcTyVar
_, Just TcTyVar
z_tv2) -> TcTyVar -> TcType -> TcS Bool
try_default_tv TcTyVar
z_tv2 TcType
z_ty1
           (Maybe TcTyVar, Maybe TcTyVar)
_               -> Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False }
  | Bool
otherwise
  = Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

  where
    try_default_tv :: TcTyVar -> TcType -> TcS Bool
try_default_tv TcTyVar
lhs_tv TcType
rhs_ty
      | MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
info, mtv_tclvl :: TcTyVarDetails -> TcLevel
mtv_tclvl = TcLevel
lvl } <- TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
lhs_tv
      , TcTyVar -> TcType
tyVarKind TcTyVar
lhs_tv HasDebugCallStack => TcType -> TcType -> Bool
TcType -> TcType -> Bool
`tcEqType` HasDebugCallStack => TcType -> TcType
TcType -> TcType
typeKind TcType
rhs_ty
      , MetaInfo -> TcType -> Bool
checkTopShape MetaInfo
info TcType
rhs_ty
      -- Do not test for touchability of lhs_tv; that is the whole point!
      -- See (DE2) in Note [Defaulting equalities]
      = do { String -> SDoc -> TcS ()
traceTcS String
"defaultEquality 1" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
lhs_tv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
rhs_ty)

           -- checkTyEqRhs: check that we can in fact unify lhs_tv := rhs_ty
           -- See Note [Defaulting equalities]
           --   LC_Promote: promote deeper unification variables (DE4)
           --   LC_Promote True: ...including under type families (DE5)
           ; let flags :: TyEqFlags ()
                 flags :: TyEqFlags ()
flags = TEF { tef_foralls :: Bool
tef_foralls  = Bool
False
                             , tef_fam_app :: TyEqFamApp ()
tef_fam_app  = TyEqFamApp ()
forall a. TyEqFamApp a
TEFA_Recurse
                             , tef_lhs :: CanEqLHS
tef_lhs      = TcTyVar -> CanEqLHS
TyVarLHS TcTyVar
lhs_tv
                             , tef_unifying :: AreUnifying
tef_unifying = MetaInfo -> TcLevel -> LevelCheck -> AreUnifying
Unifying MetaInfo
info TcLevel
lvl (Bool -> LevelCheck
LC_Promote Bool
True)
                             , tef_occurs :: CheckTyEqProblem
tef_occurs   = CheckTyEqProblem
cteInsolubleOccurs }
           ; res :: PuResult () Reduction <- TcM (PuResult () Reduction) -> TcS (PuResult () Reduction)
forall a. TcM a -> TcS a
wrapTcS (TyEqFlags () -> TcType -> TcM (PuResult () Reduction)
forall a. TyEqFlags a -> TcType -> TcM (PuResult a Reduction)
checkTyEqRhs TyEqFlags ()
flags TcType
rhs_ty)

           ; case res of
               PuFail {}   -> String -> TcS Bool
cant_default_tv String
"checkTyEqRhs"
               PuOK Bag ()
_ Reduction
redn -> Bool -> SDoc -> TcS Bool -> TcS Bool
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TcCoercion -> Bool
isReflCo (Reduction -> TcCoercion
reductionCoercion Reduction
redn)) (Reduction -> SDoc
forall a. Outputable a => a -> SDoc
ppr Reduction
redn) (TcS Bool -> TcS Bool) -> TcS Bool -> TcS Bool
forall a b. (a -> b) -> a -> b
$
                               -- With TEFA_Recurse we never get any reductions
                              TcS Bool
default_tv }
      | Bool
otherwise
      = String -> TcS Bool
cant_default_tv String
"fall through"

      where
        cant_default_tv :: String -> TcS Bool
cant_default_tv String
msg
          = do { String -> SDoc -> TcS ()
traceTcS (String
"defaultEquality fails: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg) (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
                 [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
lhs_tv SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'~' SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+>  TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
rhs_ty
                      , TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TcTyVar -> TcType
tyVarKind TcTyVar
lhs_tv)
                      , TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HasDebugCallStack => TcType -> TcType
TcType -> TcType
typeKind TcType
rhs_ty) ]
               ; Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False }

        -- All tests passed: do the unification
        default_tv :: TcS Bool
default_tv
          = do { String -> SDoc -> TcS ()
traceTcS String
"defaultEquality success:" (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
rhs_ty)
               ; TcTyVar -> TcType -> TcS ()
unifyTyVar TcTyVar
lhs_tv TcType
rhs_ty  -- NB: unifyTyVar adds to the
                                           -- TcS unification counter
               ; CtEvidence -> CanonicalEvidence -> EvTerm -> TcS ()
setEvBindIfWanted (Ct -> CtEvidence
ctEvidence Ct
ct) CanonicalEvidence
EvCanonical (EvTerm -> TcS ()) -> EvTerm -> TcS ()
forall a b. (a -> b) -> a -> b
$
                 TcCoercion -> EvTerm
evCoercion (TcType -> TcCoercion
mkNomReflCo TcType
rhs_ty)
               ; Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True }

combineStrategies :: CtDefaultingStrategy -> CtDefaultingStrategy -> CtDefaultingStrategy
combineStrategies :: CtDefaultingStrategy
-> CtDefaultingStrategy -> CtDefaultingStrategy
combineStrategies CtDefaultingStrategy
default1 CtDefaultingStrategy
default2 Ct
ct
  = do { solved <- CtDefaultingStrategy
default1 Ct
ct
       ; case solved of
           Bool
True  -> Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True  -- default1 solved it!
           Bool
False -> CtDefaultingStrategy
default2 Ct
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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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.  So the new plan is this:

  * For the Wanted constraint
        [W] alpha ~ ty
    if the only reason for not unifying is untouchability, then during
    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.  We can lift it by saying that the innermost
  given equality is at top level.

(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.

(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`.

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.


*********************************************************************************
*                                                                               *
*                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.

Type-class defaulting is guided by the `DefaultEnv`: see Note [Named default declarations]
in GHC.Tc.Gen.Default

The entry point for defaulting the unsolved constraints is `applyDefaultingRules`,
which depends on `disambigGroup`, which in turn depends on workhorse
`disambigProposalSequences`. The latter is also used by defaulting plugins through
`disambigMultiGroup` (see Note [Defaulting plugins] below).

The algorithm works as follows. Let S be the complete set of unsolved
constraints, and initialize Sx to an empty set of constraints. For every type
variable `v` that is free in S:

1. Define Cv = { Ci v | Ci v ∈ S }, the subset of S consisting of all constraints in S of
   form (Ci v), where Ci is a single-parameter type class.  (We do no defaulting for
   multi-parameter type classes.)

2. Define Dv, by extending Cv with the superclasses of every Ci in Cv

3. Define Ev, by filtering Dv to contain only classes with a default declaration.

4. For each Ci in Ev, if Ci has a non-empty default list in the `DefaultEnv`, find the first
   type T in the default list for Ci for which, for every (Ci v) in Cv, the constraint (Ci T)
  is soluble.

5. If there is precisely one type T in the resulting type set, resolve the ambiguity by adding
   a constraint (v~ Ti) constraint to a set Sx; otherwise report a static error.

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 :: WantedConstraints -> TcS WantedConstraints
tryTypeClassDefaulting WantedConstraints
wc
  | WantedConstraints -> Bool
isEmptyWC WantedConstraints
wc Bool -> Bool -> Bool
|| WantedConstraints -> Bool
insolubleWC WantedConstraints
wc -- See Note [Defaulting insolubles]
  = WantedConstraints -> TcS WantedConstraints
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return WantedConstraints
wc
  | Bool
otherwise  -- See Note [When to do type-class defaulting]
  = do { something_happened <- WantedConstraints -> TcS Bool
applyDefaultingRules WantedConstraints
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 :: WantedConstraints -> TcS Bool
applyDefaultingRules WantedConstraints
wanteds
  | WantedConstraints -> Bool
isEmptyWC WantedConstraints
wanteds
  = Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  | Bool
otherwise
  = do { (default_env, extended_rules) <- TcS (DefaultEnv, Bool)
getDefaultInfo
       ; wanteds                       <- TcS.zonkWC wanteds

       ; tcg_env <- TcS.getGblEnv
       ; let plugins = TcGblEnv -> [FillDefaulting]
tcg_defaulting_plugins TcGblEnv
tcg_env
             default_tys = DefaultEnv -> [ClassDefaults]
defaultList DefaultEnv
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 = ([ClassDefaults], Bool) -> WantedConstraints -> [(TcTyVar, [Ct])]
findDefaultableGroups ([ClassDefaults]
default_tys, Bool
extended_rules) WantedConstraints
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 :: WantedConstraints
-> FillDefaulting -> TcS (WantedConstraints, Bool)
run_defaulting_plugin WantedConstraints
wanteds FillDefaulting
p
          = do { groups <- TcPluginM [DefaultingProposal] -> TcS [DefaultingProposal]
forall a. TcPluginM a -> TcS a
runTcPluginTcS (FillDefaulting
p WantedConstraints
wanteds)
               ; defaultedGroups <-
                    filterM (\DefaultingProposal
g -> WantedConstraints -> [Ct] -> ProposalSequence -> TcS Bool
disambigMultiGroup
                                   WantedConstraints
wanteds
                                   (DefaultingProposal -> [Ct]
deProposalCts DefaultingProposal
g)
                                   ([Proposal] -> ProposalSequence
ProposalSequence ([(TcTyVar, TcType)] -> Proposal
Proposal ([(TcTyVar, TcType)] -> Proposal)
-> [[(TcTyVar, TcType)]] -> [Proposal]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DefaultingProposal -> [[(TcTyVar, TcType)]]
deProposals DefaultingProposal
g)))
                    groups
               ; traceTcS "defaultingPlugin " $ ppr defaultedGroups
               ; case defaultedGroups of
                 [] -> (WantedConstraints, Bool) -> TcS (WantedConstraints, Bool)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (WantedConstraints
wanteds, Bool
False)
                 [DefaultingProposal]
_  -> 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' <- WantedConstraints -> TcS WantedConstraints
TcS.zonkWC WantedConstraints
wanteds
                     return (wanteds', True) }

findDefaultableGroups
    :: ( [ClassDefaults]
       , Bool )            -- extended default rules
    -> WantedConstraints   -- Unsolved
    -> [(TyVar, [Ct])]
findDefaultableGroups :: ([ClassDefaults], Bool) -> WantedConstraints -> [(TcTyVar, [Ct])]
findDefaultableGroups ([ClassDefaults]
default_tys, Bool
extended_defaults) WantedConstraints
wanteds
  | [ClassDefaults] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ClassDefaults]
default_tys
  = []
  | Bool
otherwise
  = [ (TcTyVar
tv, ((Ct, Class, TcTyVar) -> Ct) -> [(Ct, Class, TcTyVar)] -> [Ct]
forall a b. (a -> b) -> [a] -> [b]
map (Ct, Class, TcTyVar) -> Ct
forall a b c. (a, b, c) -> a
fstOf3 [(Ct, Class, TcTyVar)]
group)
    | group' :: NonEmpty (Ct, Class, TcTyVar)
group'@((Ct
_,Class
_,TcTyVar
tv) :| [(Ct, Class, TcTyVar)]
_) <- [NonEmpty (Ct, Class, TcTyVar)]
unary_groups
    , let group :: [(Ct, Class, TcTyVar)]
group = NonEmpty (Ct, Class, TcTyVar) -> [(Ct, Class, TcTyVar)]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty (Ct, Class, TcTyVar)
group'
    , TcTyVar -> Bool
defaultable_tyvar TcTyVar
tv
    , [TyCon] -> Bool
defaultable_classes (((Ct, Class, TcTyVar) -> TyCon)
-> [(Ct, Class, TcTyVar)] -> [TyCon]
forall a b. (a -> b) -> [a] -> [b]
map (Class -> TyCon
classTyCon (Class -> TyCon)
-> ((Ct, Class, TcTyVar) -> Class) -> (Ct, Class, TcTyVar) -> TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ct, Class, TcTyVar) -> Class
forall a b c. (a, b, c) -> b
sndOf3) [(Ct, Class, TcTyVar)]
group) ]
  where
    simples :: Cts
simples  = Bool -> WantedConstraints -> Cts
approximateWC Bool
True WantedConstraints
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

    ([(Ct, Class, TcTyVar)]
unaries, [Ct]
non_unaries) = (Ct -> Either (Ct, Class, TcTyVar) Ct)
-> [Ct] -> ([(Ct, Class, TcTyVar)], [Ct])
forall a b c. (a -> Either b c) -> [a] -> ([b], [c])
partitionWith Ct -> Either (Ct, Class, TcTyVar) Ct
find_unary (Cts -> [Ct]
forall a. Bag a -> [a]
bagToList Cts
simples)
    unary_groups :: [NonEmpty (Ct, Class, TcTyVar)]
unary_groups           = ((Ct, Class, TcTyVar) -> (Ct, Class, TcTyVar) -> Ordering)
-> [(Ct, Class, TcTyVar)] -> [NonEmpty (Ct, Class, TcTyVar)]
forall a. (a -> a -> Ordering) -> [a] -> [NonEmpty a]
equivClasses (Ct, Class, TcTyVar) -> (Ct, Class, TcTyVar) -> Ordering
forall {a} {a} {b} {a} {b}.
Ord a =>
(a, b, a) -> (a, b, a) -> Ordering
cmp_tv [(Ct, Class, TcTyVar)]
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 * (a:*))   (#8931)
    -- step (1) in Note [How type-class constraints are defaulted]
    find_unary :: Ct -> Either (Ct, Class, TyVar) Ct
    find_unary :: Ct -> Either (Ct, Class, TcTyVar) Ct
find_unary Ct
cc
        | Just (Class
cls,[TcType]
tys)   <- TcType -> Maybe (Class, [TcType])
getClassPredTys_maybe (Ct -> TcType
ctPred Ct
cc)
        , [TcType
ty] <- TyCon -> [TcType] -> [TcType]
filterOutInvisibleTypes (Class -> TyCon
classTyCon Class
cls) [TcType]
tys
              -- Ignore invisible arguments for this purpose
        , Just TcTyVar
tv <- TcType -> Maybe TcTyVar
getTyVar_maybe TcType
ty
        , TcTyVar -> Bool
isMetaTyVar TcTyVar
tv  -- We might have runtime-skolems in GHCi, and
                          -- we definitely don't want to try to assign to those!
        = (Ct, Class, TcTyVar) -> Either (Ct, Class, TcTyVar) Ct
forall a b. a -> Either a b
Left (Ct
cc, Class
cls, TcTyVar
tv)
    find_unary Ct
cc = Ct -> Either (Ct, Class, TcTyVar) Ct
forall a b. b -> Either a b
Right Ct
cc  -- Non unary or non dictionary

    bad_tvs :: TcTyCoVarSet  -- TyVars mentioned by non-unaries
    bad_tvs :: VarSet
bad_tvs = (Ct -> VarSet) -> [Ct] -> VarSet
forall a. (a -> VarSet) -> [a] -> VarSet
mapUnionVarSet Ct -> VarSet
tyCoVarsOfCt [Ct]
non_unaries

    cmp_tv :: (a, b, a) -> (a, b, a) -> Ordering
cmp_tv (a
_,b
_,a
tv1) (a
_,b
_,a
tv2) = a
tv1 a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
tv2

    defaultable_tyvar :: TcTyVar -> Bool
    defaultable_tyvar :: TcTyVar -> Bool
defaultable_tyvar TcTyVar
tv
        = let b1 :: Bool
b1 = TcTyVar -> Bool
isTyConableTyVar TcTyVar
tv  -- Note [Avoiding spurious errors]
              b2 :: Bool
b2 = Bool -> Bool
not (TcTyVar
tv TcTyVar -> VarSet -> Bool
`elemVarSet` VarSet
bad_tvs)
          in Bool
b1 Bool -> Bool -> Bool
&& (Bool
b2 Bool -> Bool -> Bool
|| Bool
extended_defaults) -- Note [Multi-parameter defaults]

    -- Determines if any of the given type class constructors is in default_tys
    -- step (3) in Note [How type-class constraints are defaulted]
    defaultable_classes :: [TyCon] -> Bool
    defaultable_classes :: [TyCon] -> Bool
defaultable_classes [TyCon]
clss = Bool -> Bool
not (Bool -> Bool) -> ([TyCon] -> Bool) -> [TyCon] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TyCon] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([TyCon] -> Bool) -> ([TyCon] -> [TyCon]) -> [TyCon] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TyCon] -> [TyCon] -> [TyCon]
forall a. Eq a => [a] -> [a] -> [a]
intersect [TyCon]
clss ([TyCon] -> Bool) -> [TyCon] -> Bool
forall a b. (a -> b) -> a -> b
$ (ClassDefaults -> TyCon) -> [ClassDefaults] -> [TyCon]
forall a b. (a -> b) -> [a] -> [b]
map ClassDefaults -> TyCon
cd_class [ClassDefaults]
default_tys

------------------------------

-- | 'Proposal's to be tried in sequence until the first one that succeeds
newtype ProposalSequence = ProposalSequence{ProposalSequence -> [Proposal]
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 -> SDoc
ppr (ProposalSequence [Proposal]
proposals) = [Proposal] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Proposal]
proposals
instance Outputable Proposal where
  ppr :: Proposal -> SDoc
ppr (Proposal [(TcTyVar, TcType)]
assignments) = [(TcTyVar, TcType)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(TcTyVar, TcType)]
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 :: WantedConstraints -> [ClassDefaults] -> (TcTyVar, [Ct]) -> TcS Bool
disambigGroup WantedConstraints
orig_wanteds [ClassDefaults]
default_ctys (TcTyVar
tv, [Ct]
wanteds)
  = WantedConstraints
-> [Ct]
-> [ProposalSequence]
-> (NonEmpty ([TcTyVar], Subst) -> Bool)
-> TcS Bool
disambigProposalSequences WantedConstraints
orig_wanteds [Ct]
wanteds [ProposalSequence]
proposalSequences NonEmpty ([TcTyVar], Subst) -> Bool
allConsistent
  where
    proposalSequences :: [ProposalSequence]
proposalSequences = [ [Proposal] -> ProposalSequence
ProposalSequence [[(TcTyVar, TcType)] -> Proposal
Proposal [(TcTyVar
tv, TcType
ty)] | TcType
ty <- [TcType]
tys]
                        | ClassDefaults{cd_types :: ClassDefaults -> [TcType]
cd_types = [TcType]
tys} <- [ClassDefaults]
defaultses ]
    allConsistent :: NonEmpty ([TcTyVar], Subst) -> Bool
allConsistent (([TcTyVar]
_, Subst
sub) :| [([TcTyVar], Subst)]
subs) = (([TcTyVar], Subst) -> Bool) -> [([TcTyVar], Subst)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TcTyVar -> Subst -> Subst -> Bool
eqSubAt TcTyVar
tv Subst
sub (Subst -> Bool)
-> (([TcTyVar], Subst) -> Subst) -> ([TcTyVar], Subst) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([TcTyVar], Subst) -> Subst
forall a b. (a, b) -> b
snd) [([TcTyVar], Subst)]
subs
    defaultses :: [ClassDefaults]
defaultses =
      [ ClassDefaults
defaults | defaults :: ClassDefaults
defaults@ClassDefaults{cd_class :: ClassDefaults -> TyCon
cd_class = TyCon
cls} <- [ClassDefaults]
default_ctys
                 , (Ct -> Bool) -> [Ct] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TyCon -> Ct -> Bool
isDictForClass TyCon
cls) [Ct]
wanteds ]
    isDictForClass :: TyCon -> Ct -> Bool
isDictForClass TyCon
clcon Ct
ct = ((Class, [TcType]) -> Bool) -> Maybe (Class, [TcType]) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((TyCon
clcon TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
==) (TyCon -> Bool)
-> ((Class, [TcType]) -> TyCon) -> (Class, [TcType]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Class -> TyCon
classTyCon (Class -> TyCon)
-> ((Class, [TcType]) -> Class) -> (Class, [TcType]) -> TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Class, [TcType]) -> Class
forall a b. (a, b) -> a
fst) (TcType -> Maybe (Class, [TcType])
getClassPredTys_maybe (TcType -> Maybe (Class, [TcType]))
-> TcType -> Maybe (Class, [TcType])
forall a b. (a -> b) -> a -> b
$ Ct -> TcType
ctPred Ct
ct)
    eqSubAt :: TcTyVar -> Subst -> Subst -> Bool
    eqSubAt :: TcTyVar -> Subst -> Subst -> Bool
eqSubAt TcTyVar
tvar Subst
s1 Subst
s2 = Maybe Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or (Maybe Bool -> Bool) -> Maybe Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (TcType -> TcType -> Bool)
-> Maybe TcType -> Maybe TcType -> Maybe Bool
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 HasDebugCallStack => TcType -> TcType -> Bool
TcType -> TcType -> Bool
tcEqType (Subst -> TcTyVar -> Maybe TcType
lookupTyVar Subst
s1 TcTyVar
tvar) (Subst -> TcTyVar -> Maybe TcType
lookupTyVar Subst
s2 TcTyVar
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 :: WantedConstraints -> [Ct] -> ProposalSequence -> TcS Bool
disambigMultiGroup WantedConstraints
orig_wanteds [Ct]
wanteds ProposalSequence
proposalSequence
  = WantedConstraints
-> [Ct]
-> [ProposalSequence]
-> (NonEmpty ([TcTyVar], Subst) -> Bool)
-> TcS Bool
disambigProposalSequences WantedConstraints
orig_wanteds [Ct]
wanteds [ProposalSequence
proposalSequence] (Bool -> NonEmpty ([TcTyVar], Subst) -> Bool
forall a b. a -> b -> a
const Bool
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 :: WantedConstraints
-> [Ct]
-> [ProposalSequence]
-> (NonEmpty ([TcTyVar], Subst) -> Bool)
-> TcS Bool
disambigProposalSequences WantedConstraints
orig_wanteds [Ct]
wanteds [ProposalSequence]
proposalSequences NonEmpty ([TcTyVar], Subst) -> Bool
allConsistent
  = do { (ProposalSequence -> TcS ()) -> [ProposalSequence] -> TcS ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ ((Proposal -> TcS ()) -> [Proposal] -> TcS ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Proposal -> TcS ()
reportInvalidDefaultedTyVars ([Proposal] -> TcS ())
-> (ProposalSequence -> [Proposal]) -> ProposalSequence -> TcS ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProposalSequence -> [Proposal]
getProposalSequence) [ProposalSequence]
proposalSequences
       ; fake_ev_binds_var <- TcS EvBindsVar
TcS.newTcEvBinds
       ; tclvl             <- TcS.getTcLevel
       -- Step (4) 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 (5) in Note [How type-class constraints are defaulted]
       ; case successes of
           success :: ([TcTyVar], Subst)
success@([TcTyVar]
tvs, Subst
subst) : [([TcTyVar], Subst)]
rest
             | NonEmpty ([TcTyVar], Subst) -> Bool
allConsistent (([TcTyVar], Subst)
success ([TcTyVar], Subst)
-> [([TcTyVar], Subst)] -> NonEmpty ([TcTyVar], Subst)
forall a. a -> [a] -> NonEmpty a
:| [([TcTyVar], Subst)]
rest)
             -> do { [TcTyVar] -> Subst -> TcS ()
applyDefaultSubst [TcTyVar]
tvs Subst
subst
                   ; let warn :: TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) ()
warn TcTyVar
tv = (TcType -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> Maybe TcType -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Ct] -> TcTyVar -> TcType -> IOEnv (Env TcGblEnv TcLclEnv) ()
warnDefaulting [Ct]
wanteds TcTyVar
tv) (Subst -> TcTyVar -> Maybe TcType
lookupTyVar Subst
subst TcTyVar
tv)
                   ; IOEnv (Env TcGblEnv TcLclEnv) () -> TcS ()
forall a. TcM a -> TcS a
wrapWarnTcS (IOEnv (Env TcGblEnv TcLclEnv) () -> TcS ())
-> IOEnv (Env TcGblEnv TcLclEnv) () -> TcS ()
forall a b. (a -> b) -> a -> b
$ (TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> [TcTyVar] -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) ()
warn [TcTyVar]
tvs
                   ; String -> SDoc -> TcS ()
traceTcS String
"disambigProposalSequences succeeded }" ([ProposalSequence] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [ProposalSequence]
proposalSequences)
                   ; Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True }
           [([TcTyVar], Subst)]
_ ->
             do { String -> SDoc -> TcS ()
traceTcS String
"disambigProposalSequences failed }" ([ProposalSequence] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [ProposalSequence]
proposalSequences)
                ; Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False } }
  where
    reportInvalidDefaultedTyVars :: Proposal -> TcS ()
    firstSuccess :: ProposalSequence -> TcS (Maybe ([TcTyVar], Subst))
    firstSuccess :: ProposalSequence -> TcS (Maybe ([TcTyVar], Subst))
firstSuccess (ProposalSequence [Proposal]
proposals)
      = First ([TcTyVar], Subst) -> Maybe ([TcTyVar], Subst)
forall a. First a -> Maybe a
getFirst (First ([TcTyVar], Subst) -> Maybe ([TcTyVar], Subst))
-> TcS (First ([TcTyVar], Subst)) -> TcS (Maybe ([TcTyVar], Subst))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Proposal -> TcS (First ([TcTyVar], Subst)))
-> [Proposal] -> TcS (First ([TcTyVar], Subst))
forall (m :: * -> *) (t :: * -> *) b a.
(Applicative m, Foldable t, Monoid b) =>
(a -> m b) -> t a -> m b
foldMapM ((Maybe ([TcTyVar], Subst) -> First ([TcTyVar], Subst))
-> TcS (Maybe ([TcTyVar], Subst)) -> TcS (First ([TcTyVar], Subst))
forall a b. (a -> b) -> TcS a -> TcS b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe ([TcTyVar], Subst) -> First ([TcTyVar], Subst)
forall a. Maybe a -> First a
First (TcS (Maybe ([TcTyVar], Subst)) -> TcS (First ([TcTyVar], Subst)))
-> (Proposal -> TcS (Maybe ([TcTyVar], Subst)))
-> Proposal
-> TcS (First ([TcTyVar], Subst))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Ct] -> Proposal -> TcS (Maybe ([TcTyVar], Subst))
tryDefaultGroup [Ct]
wanteds) [Proposal]
proposals
    reportInvalidDefaultedTyVars :: Proposal -> TcS ()
reportInvalidDefaultedTyVars proposal :: Proposal
proposal@(Proposal [(TcTyVar, TcType)]
assignments)
      = do { let tvs :: [TcTyVar]
tvs = (TcTyVar, TcType) -> TcTyVar
forall a b. (a, b) -> a
fst ((TcTyVar, TcType) -> TcTyVar) -> [(TcTyVar, TcType)] -> [TcTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TcTyVar, TcType)]
assignments
             ; invalid_tvs <- (TcTyVar -> TcS Bool) -> [TcTyVar] -> TcS [TcTyVar]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterOutM TcTyVar -> TcS Bool
TcS.isUnfilledMetaTyVar [TcTyVar]
tvs
             ; traverse_ (errInvalidDefaultedTyVar orig_wanteds proposal) (nonEmpty invalid_tvs) }

applyDefaultSubst :: [TcTyVar] -> Subst -> TcS ()
applyDefaultSubst :: [TcTyVar] -> Subst -> TcS ()
applyDefaultSubst [TcTyVar]
tvs Subst
subst =
  do { deep_tvs <- (TcTyVar -> TcS Bool) -> [TcTyVar] -> TcS [TcTyVar]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM TcTyVar -> TcS Bool
TcS.isUnfilledMetaTyVar ([TcTyVar] -> TcS [TcTyVar]) -> [TcTyVar] -> TcS [TcTyVar]
forall a b. (a -> b) -> a -> b
$ VarSet -> [TcTyVar]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet (VarSet -> [TcTyVar]) -> VarSet -> [TcTyVar]
forall a b. (a -> b) -> a -> b
$ VarSet -> VarSet
closeOverKinds ([TcTyVar] -> VarSet
mkVarSet [TcTyVar]
tvs)
     ; forM_ deep_tvs $ \ TcTyVar
tv -> (TcType -> TcS ()) -> Maybe TcType -> TcS ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TcTyVar -> TcType -> TcS ()
unifyTyVar TcTyVar
tv) (VarEnv TcType -> TcTyVar -> Maybe TcType
forall a. VarEnv a -> TcTyVar -> Maybe a
lookupVarEnv (Subst -> VarEnv TcType
getTvSubstEnv Subst
subst) TcTyVar
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 :: [Ct] -> Proposal -> TcS (Maybe ([TcTyVar], Subst))
tryDefaultGroup [Ct]
wanteds (Proposal [(TcTyVar, TcType)]
assignments)
          | let ([TcTyVar]
tvs, [TcType]
default_tys) = [(TcTyVar, TcType)] -> ([TcTyVar], [TcType])
forall a b. [(a, b)] -> ([a], [b])
unzip [(TcTyVar, TcType)]
assignments
          , Just Subst
subst <- [TcType] -> [TcType] -> Maybe Subst
tcMatchTyKis ([TcTyVar] -> [TcType]
mkTyVarTys [TcTyVar]
tvs) [TcType]
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 TcLclEnv
TcS.getLclEnv
               ; tc_lvl <- TcS.getTcLevel
               ; let loc = TcLevel -> SkolemInfoAnon -> CtLocEnv -> CtLoc
mkGivenLoc TcLevel
tc_lvl (SkolemInfo -> SkolemInfoAnon
getSkolemInfo SkolemInfo
HasDebugCallStack => SkolemInfo
unkSkol) (TcLclEnv -> CtLocEnv
mkCtLocEnv TcLclEnv
lcl_env)
               -- Equality constraints are possible due to type defaulting plugins
               ; wanted_evs <- sequence [ newWantedNC loc rewriters pred'
                                        | wanted <- wanteds
                                        , CtWanted { ctev_pred = pred
                                                   , ctev_rewriters = rewriters }
                                            <- return (ctEvidence wanted)
                                        , let pred' = HasDebugCallStack => Subst -> TcType -> TcType
Subst -> TcType -> TcType
substTy Subst
subst TcType
pred ]
               ; residual_wc <- solveSimpleWanteds $ listToBag $ map mkNonCanonical wanted_evs
               ; return $ if isEmptyWC residual_wc then Just (tvs, subst) else Nothing }

          | Bool
otherwise
          = Maybe ([TcTyVar], Subst) -> TcS (Maybe ([TcTyVar], Subst))
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([TcTyVar], Subst)
forall a. Maybe a
Nothing

errInvalidDefaultedTyVar :: WantedConstraints -> Proposal -> NonEmpty TcTyVar -> TcS ()
errInvalidDefaultedTyVar :: WantedConstraints -> Proposal -> NonEmpty TcTyVar -> TcS ()
errInvalidDefaultedTyVar WantedConstraints
wanteds (Proposal [(TcTyVar, TcType)]
assignments) NonEmpty TcTyVar
problematic_tvs
  = TcRnMessage -> TcS ()
forall a. TcRnMessage -> TcS a
failTcS (TcRnMessage -> TcS ()) -> TcRnMessage -> TcS ()
forall a b. (a -> b) -> a -> b
$ [Ct] -> [(TcTyVar, TcType)] -> NonEmpty TcTyVar -> TcRnMessage
TcRnInvalidDefaultedTyVar [Ct]
tidy_wanteds [(TcTyVar, TcType)]
tidy_assignments NonEmpty TcTyVar
tidy_problems
  where
    proposal_tvs :: [TcTyVar]
proposal_tvs = ((TcTyVar, TcType) -> [TcTyVar])
-> [(TcTyVar, TcType)] -> [TcTyVar]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(TcTyVar
tv, TcType
ty) -> TcTyVar
tv TcTyVar -> [TcTyVar] -> [TcTyVar]
forall a. a -> [a] -> [a]
: TcType -> [TcTyVar]
tyCoVarsOfTypeList TcType
ty) [(TcTyVar, TcType)]
assignments
    tidy_env :: TidyEnv
tidy_env = TidyEnv -> [TcTyVar] -> TidyEnv
tidyFreeTyCoVars TidyEnv
emptyTidyEnv ([TcTyVar] -> TidyEnv) -> [TcTyVar] -> TidyEnv
forall a b. (a -> b) -> a -> b
$ [TcTyVar]
proposal_tvs [TcTyVar] -> [TcTyVar] -> [TcTyVar]
forall a. [a] -> [a] -> [a]
++ NonEmpty TcTyVar -> [TcTyVar]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty TcTyVar
problematic_tvs
    tidy_wanteds :: [Ct]
tidy_wanteds = (Ct -> Ct) -> [Ct] -> [Ct]
forall a b. (a -> b) -> [a] -> [b]
map (TidyEnv -> Ct -> Ct
tidyCt TidyEnv
tidy_env) ([Ct] -> [Ct]) -> [Ct] -> [Ct]
forall a b. (a -> b) -> a -> b
$ WantedConstraints -> [Ct]
flattenWC WantedConstraints
wanteds
    tidy_assignments :: [(TcTyVar, TcType)]
tidy_assignments = [(TidyEnv -> TcTyVar -> TcTyVar
tidyTyCoVarOcc TidyEnv
tidy_env TcTyVar
tv, TidyEnv -> TcType -> TcType
tidyType TidyEnv
tidy_env TcType
ty) | (TcTyVar
tv, TcType
ty) <- [(TcTyVar, TcType)]
assignments]
    tidy_problems :: NonEmpty TcTyVar
tidy_problems = (TcTyVar -> TcTyVar) -> NonEmpty TcTyVar -> NonEmpty TcTyVar
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TidyEnv -> TcTyVar -> TcTyVar
tidyTyCoVarOcc TidyEnv
tidy_env) NonEmpty TcTyVar
problematic_tvs

    flattenWC :: WantedConstraints -> [Ct]
    flattenWC :: WantedConstraints -> [Ct]
flattenWC (WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
cts, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
impls })
      = Cts -> [Ct]
ctsElts Cts
cts [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ (Implication -> [Ct]) -> Bag Implication -> [Ct]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (WantedConstraints -> [Ct]
flattenWC (WantedConstraints -> [Ct])
-> (Implication -> WantedConstraints) -> Implication -> [Ct]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Implication -> WantedConstraints
ic_wanted) Bag Implication
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 :: Bool -> Class -> Bool
isInteractiveClass Bool
ovl_strings Class
cls
    = Bool -> Class -> Bool
isNumClass Bool
ovl_strings Class
cls Bool -> Bool -> Bool
|| (Class -> Unique
classKey Class
cls Unique -> [Unique] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Unique]
interactiveClassKeys)

    -- isNumClass adds IsString to the standard numeric classes,
    -- when -XOverloadedStrings is enabled
isNumClass :: Bool   -- -XOverloadedStrings?
           -> Class -> Bool
isNumClass :: Bool -> Class -> Bool
isNumClass Bool
ovl_strings Class
cls
  = Class -> Bool
isNumericClass Class
cls Bool -> Bool -> Bool
|| (Bool
ovl_strings Bool -> Bool -> Bool
&& (Class
cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
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).
-}