{-# 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). -}