growThetaTyVars,
simplifyAmbiguityCheck,
simplifyDefault,
- simplifyTop, simplifyInteractive, solveEqualities,
+ simplifyTop, simplifyTopImplic, captureTopConstraints,
+ simplifyInteractive,
+ solveEqualities, solveLocalEqualities,
simplifyWantedsTcM,
tcCheckSatisfiability,
+ simpl_top,
+
+ promoteTyVar,
+ promoteTyVarSet,
+
-- For Rules we need these
- solveWanteds, runTcSDeriveds
+ solveWanteds, solveWantedsAndDrop,
+ approximateWC, runTcSDeriveds
) where
#include "HsVersions.h"
+import GhcPrelude
+
import Bag
import Class ( Class, classKey, classTyCon )
import DynFlags ( WarningFlag ( Opt_WarnMonomorphism )
, WarnReason ( Reason )
, DynFlags( solverIterations ) )
+import Id ( idType )
import Inst
import ListSetOps
-import Maybes
import Name
import Outputable
import PrelInfo
import TcErrors
import TcEvidence
import TcInteract
-import TcCanonical ( makeSuperClasses )
+import TcCanonical ( makeSuperClasses, solveCallStack )
import TcMType as TcM
import TcRnMonad as TcM
import TcSMonad as TcS
import TcType
import TrieMap () -- DV: for now
import Type
-import TysWiredIn ( ptrRepLiftedTy )
-import Unify ( tcMatchTy )
+import TysWiredIn ( liftedRepTy )
+import Unify ( tcMatchTyKi )
import Util
import Var
import VarSet
-import UniqFM
+import UniqSet
import BasicTypes ( IntWithInf, intGtLimit )
import ErrUtils ( emptyMessages )
import qualified GHC.LanguageExtensions as LangExt
-import Control.Monad ( when, unless )
-import Data.List ( partition )
+import Control.Monad
+import Data.Foldable ( toList )
+import Data.List ( partition )
+import Data.List.NonEmpty ( NonEmpty(..) )
+import Maybes ( isJust )
{-
*********************************************************************************
*********************************************************************************
-}
+captureTopConstraints :: TcM a -> TcM (a, WantedConstraints)
+-- (captureTopConstraints m) runs m, and returns the type constraints it
+-- generates plus the constraints produced by static forms inside.
+-- If it fails with an exception, it reports any insolubles
+-- (out of scope variables) before doing so
+captureTopConstraints thing_inside
+ = do { static_wc_var <- TcM.newTcRef emptyWC ;
+ ; (mb_res, lie) <- TcM.updGblEnv (\env -> env { tcg_static_wc = static_wc_var } ) $
+ TcM.tryCaptureConstraints thing_inside
+ ; stWC <- TcM.readTcRef static_wc_var
+
+ -- See TcRnMonad Note [Constraints and errors]
+ -- If the thing_inside threw an exception, but generated some insoluble
+ -- constraints, report the latter before propagating the exception
+ -- Otherwise they will be lost altogether
+ ; case mb_res of
+ Right res -> return (res, lie `andWC` stWC)
+ Left {} -> do { _ <- reportUnsolved lie; failM } }
+ -- This call to reportUnsolved is the reason
+ -- this function is here instead of TcRnMonad
+
+simplifyTopImplic :: Bag Implication -> TcM ()
+simplifyTopImplic implics
+ = do { empty_binds <- simplifyTop (mkImplicWC implics)
+
+ -- Since all the inputs are implications the returned bindings will be empty
+ ; MASSERT2( isEmptyBag empty_binds, ppr empty_binds )
+
+ ; return () }
+
simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
-- Simplify top-level constraints
-- Usually these will be implications,
; TcM.writeTcRef errs_var emptyMessages
; warnAllUnsolved $ WC { wc_simple = unsafe_ol
- , wc_insol = emptyCts
, wc_impl = emptyBag }
; whyUnsafe <- fst <$> TcM.readTcRef errs_var
; return (evBindMapBinds binds1 `unionBags` binds2) }
+-- | Type-check a thing that emits only equality constraints, solving any
+-- constraints we can and re-emitting constraints that we can't. The thing_inside
+-- should generally bump the TcLevel to make sure that this run of the solver
+-- doesn't affect anything lying around.
+solveLocalEqualities :: TcM a -> TcM a
+solveLocalEqualities thing_inside
+ = do { traceTc "solveLocalEqualities {" empty
+
+ ; (result, wanted) <- captureConstraints thing_inside
+
+ ; traceTc "solveLocalEqualities: running solver {" (ppr wanted)
+ ; reduced_wanted <- runTcSEqualities (solveWanteds wanted)
+ ; traceTc "solveLocalEqualities: running solver }" (ppr reduced_wanted)
+
+ ; emitConstraints reduced_wanted
+
+ ; traceTc "solveLocalEqualities end }" empty
+ ; return result }
+
-- | Type-check a thing that emits only equality constraints, then
-- solve those constraints. Fails outright if there is trouble.
+-- Use this if you're not going to get another crack at solving
+-- (because, e.g., you're checking a datatype declaration)
solveEqualities :: TcM a -> TcM a
solveEqualities thing_inside
= checkNoErrs $ -- See Note [Fail fast on kind errors]
do { (result, wanted) <- captureConstraints thing_inside
; traceTc "solveEqualities {" $ text "wanted = " <+> ppr wanted
; final_wc <- runTcSEqualities $ simpl_top wanted
+ -- NB: Use simpl_top here so that we potentially default RuntimeRep
+ -- vars to LiftedRep. This is needed to avoid #14991.
; traceTc "End solveEqualities }" empty
; traceTc "reportAllUnsolved {" empty
; traceTc "reportAllUnsolved }" empty
; return result }
+-- | Simplify top-level constraints, but without reporting any unsolved
+-- constraints nor unsafe overlapping.
simpl_top :: WantedConstraints -> TcS WantedConstraints
-- See Note [Top-level Defaulting Plan]
simpl_top wanteds
-- zonkTyCoVarsAndFV: the wc_first_go is not yet zonked
-- filter isMetaTyVar: we might have runtime-skolems in GHCi,
-- and we definitely don't want to try to assign to those!
- -- the isTyVar needs to weed out coercion variables
+ -- The isTyVar is needed to weed out coercion variables
; defaulted <- mapM defaultTyVarTcS meta_tvs -- Has unification side effects
; if or defaulted
-- See Note [Overview of implicit CallStacks] in TcEvidence
defaultCallStacks wanteds
= do simples <- handle_simples (wc_simple wanteds)
- implics <- mapBagM handle_implic (wc_impl wanteds)
- return (wanteds { wc_simple = simples, wc_impl = implics })
+ mb_implics <- mapBagM handle_implic (wc_impl wanteds)
+ return (wanteds { wc_simple = simples
+ , wc_impl = catBagMaybes mb_implics })
where
handle_simples simples
= catBagMaybes <$> mapBagM defaultCallStack simples
+ handle_implic :: Implication -> TcS (Maybe Implication)
+ -- The Maybe is because solving the CallStack constraint
+ -- may well allow us to discard the implication entirely
handle_implic implic
+ | isSolvedStatus (ic_status implic)
+ = return (Just implic)
+ | otherwise
= do { wanteds <- setEvBindsTcS (ic_binds implic) $
-- defaultCallStack sets a binding, so
-- we must set the correct binding group
defaultCallStacks (ic_wanted implic)
- ; return (implic { ic_wanted = wanteds }) }
+ ; setImplicationStatus (implic { ic_wanted = wanteds }) }
defaultCallStack ct
- | Just _ <- isCallStackPred (ctPred ct)
- = do { solveCallStack (cc_ev ct) EvCsEmpty
+ | ClassPred cls tys <- classifyPredType (ctPred ct)
+ , Just {} <- isCallStackPred cls tys
+ = do { solveCallStack (ctEvidence ct) EvCsEmpty
; return Nothing }
defaultCallStack ct
-- inaccessible code
; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
; traceTc "reportUnsolved(ambig) {" empty
- ; tc_lvl <- TcM.getTcLevel
- ; unless (allow_ambiguous && not (insolubleWC tc_lvl final_wc))
+ ; unless (allow_ambiguous && not (insolubleWC final_wc))
(discardResult (reportUnsolved final_wc))
; traceTc "reportUnsolved(ambig) }" empty
-> TcM () -- Succeeds if the constraint is soluble
simplifyDefault theta
= do { traceTc "simplifyDefault" empty
- ; loc <- getCtLocM DefaultOrigin Nothing
- ; let wanted = [ CtDerived { ctev_pred = pred
- , ctev_loc = loc }
- | pred <- theta ]
- ; unsolved <- runTcSDeriveds (solveWanteds (mkSimpleWC wanted))
+ ; wanteds <- newWanteds DefaultOrigin theta
+ ; unsolved <- runTcSDeriveds (solveWantedsAndDrop (mkSimpleWC wanteds))
; traceTc "reportUnsolved {" empty
; reportAllUnsolved unsolved
; traceTc "reportUnsolved }" empty
do { traceTcS "checkSatisfiability {" (ppr given_ids)
; let given_cts = mkGivens given_loc (bagToList given_ids)
-- See Note [Superclasses and satisfiability]
- ; insols <- solveSimpleGivens given_cts
+ ; solveSimpleGivens given_cts
+ ; insols <- getInertInsols
; insols <- try_harder insols
; traceTcS "checkSatisfiability }" (ppr insols)
; return (isEmptyBag insols) }
| not (isEmptyBag insols) -- We've found that it's definitely unsatisfiable
= return insols -- Hurrah -- stop now.
| otherwise
- = do { pending_given <- getPendingScDicts
+ = do { pending_given <- getPendingGivenScs
; new_given <- makeSuperClasses pending_given
- ; solveSimpleGivens new_given }
+ ; solveSimpleGivens new_given
+ ; getInertInsols }
{- Note [Superclasses and satisfiability]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-> WantedConstraints
-> TcM ([TcTyVar], -- Quantify over these type variables
[EvVar], -- ... and these constraints (fully zonked)
- TcEvBinds) -- ... binding these evidence variables
+ TcEvBinds, -- ... binding these evidence variables
+ WantedConstraints, -- Redidual as-yet-unsolved constraints
+ Bool) -- True <=> the residual constraints are insoluble
+
simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
| isEmptyWC wanteds
= do { gbl_tvs <- tcGetGlobalTyCoVars
; dep_vars <- zonkTcTypesAndSplitDepVars (map snd name_taus)
- ; qtkvs <- quantifyZonkedTyVars gbl_tvs dep_vars
+ ; qtkvs <- quantifyTyVars gbl_tvs dep_vars
; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
- ; return (qtkvs, [], emptyTcEvBinds) }
+ ; return (qtkvs, [], emptyTcEvBinds, emptyWC, False) }
| otherwise
= do { traceTc "simplifyInfer {" $ vcat
-- bindings, so we can't just revert to the input
-- constraint.
- ; tc_lcl_env <- TcM.getLclEnv
+ ; tc_env <- TcM.getEnv
; ev_binds_var <- TcM.newTcEvBinds
; psig_theta_vars <- mapM TcM.newEvVar psig_theta
; wanted_transformed_incl_derivs
<- setTcLevel rhs_tclvl $
- runTcSWithEvBinds False (Just ev_binds_var) $
- do { let loc = mkGivenLoc rhs_tclvl UnkSkol tc_lcl_env
+ runTcSWithEvBinds ev_binds_var $
+ do { let loc = mkGivenLoc rhs_tclvl UnkSkol $
+ env_lcl tc_env
psig_givens = mkGivens loc psig_theta_vars
; _ <- solveSimpleGivens psig_givens
-- See Note [Add signature contexts as givens]
; solveWanteds wanteds }
- ; wanted_transformed_incl_derivs <- TcM.zonkWC wanted_transformed_incl_derivs
-- Find quant_pred_candidates, the predicates that
-- we'll consider quantifying over
-- the psig_theta; it's just the extra bit
-- NB2: We do not do any defaulting when inferring a type, this can lead
-- to less polymorphic types, see Note [Default while Inferring]
-
- ; let wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
- ; quant_pred_candidates -- Fully zonked
- <- if insolubleWC rhs_tclvl wanted_transformed_incl_derivs
- then return [] -- See Note [Quantification with errors]
- -- NB: must include derived errors in this test,
- -- hence "incl_derivs"
-
- else do { let quant_cand = approximateWC wanted_transformed
- meta_tvs = filter isMetaTyVar $
- tyCoVarsOfCtsList quant_cand
-
- ; gbl_tvs <- tcGetGlobalTyCoVars
- -- Miminise quant_cand. We are not interested in any evidence
- -- produced, because we are going to simplify wanted_transformed
- -- again later. All we want here are the predicates over which to
- -- quantify.
- --
- -- If any meta-tyvar unifications take place (unlikely),
- -- we'll pick that up later.
-
- -- See Note [Promote _and_ default when inferring]
- ; let def_tyvar tv
- = when (not $ tv `elemVarSet` gbl_tvs) $
- defaultTyVar tv
- ; mapM_ def_tyvar meta_tvs
- ; mapM_ (promoteTyVar rhs_tclvl) meta_tvs
-
- ; WC { wc_simple = simples }
- <- setTcLevel rhs_tclvl $
- runTcSDeriveds $
- solveSimpleWanteds $
- mapBag toDerivedCt quant_cand
- -- NB: we don't want evidence,
- -- so use Derived constraints
-
- ; simples <- TcM.zonkSimples simples
-
- ; return [ ctEvPred ev | ct <- bagToList simples
- , let ev = ctEvidence ct ] }
-
- -- NB: quant_pred_candidates is already fully zonked
+ ; wanted_transformed_incl_derivs <- TcM.zonkWC wanted_transformed_incl_derivs
+ ; let definite_error = insolubleWC wanted_transformed_incl_derivs
+ -- See Note [Quantification with errors]
+ -- NB: must include derived errors in this test,
+ -- hence "incl_derivs"
+ wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
+ quant_pred_candidates
+ | definite_error = []
+ | otherwise = ctsPreds (approximateWC False wanted_transformed)
-- Decide what type variables and constraints to quantify
+ -- NB: quant_pred_candidates is already fully zonked
-- NB: bound_theta are constraints we want to quantify over,
- -- /apart from/ the psig_theta, which we always quantify over
- ; (qtvs, bound_theta) <- decideQuantification infer_mode name_taus psig_theta
+ -- including the psig_theta, which we always quantify over
+ -- NB: bound_theta are fully zonked
+ ; (qtvs, bound_theta, co_vars) <- decideQuantification infer_mode rhs_tclvl
+ name_taus partial_sigs
quant_pred_candidates
-
- -- Promote any type variables that are free in the inferred type
- -- of the function:
- -- f :: forall qtvs. bound_theta => zonked_tau
- -- These variables now become free in the envt, and hence will show
- -- up whenever 'f' is called. They may currently at rhs_tclvl, but
- -- they had better be unifiable at the outer_tclvl!
- -- Example: envt mentions alpha[1]
- -- tau_ty = beta[2] -> beta[2]
- -- consraints = alpha ~ [beta]
- -- we don't quantify over beta (since it is fixed by envt)
- -- so we must promote it! The inferred type is just
- -- f :: beta -> beta
- ; zonked_taus <- mapM (TcM.zonkTcType . snd) name_taus
- -- decideQuantification turned some meta tyvars into
- -- quantified skolems, so we have to zonk again
-
- ; let phi_tkvs = tyCoVarsOfTypes bound_theta -- Already zonked
- `unionVarSet` tyCoVarsOfTypes zonked_taus
- promote_tkvs = closeOverKinds phi_tkvs `delVarSetList` qtvs
-
- ; MASSERT2( closeOverKinds promote_tkvs `subVarSet` promote_tkvs
- , ppr phi_tkvs $$
- ppr (closeOverKinds phi_tkvs) $$
- ppr promote_tkvs $$
- ppr (closeOverKinds promote_tkvs) )
- -- we really don't want a type to be promoted when its kind isn't!
-
- -- promoteTyVar ignores coercion variables
- ; outer_tclvl <- TcM.getTcLevel
- ; mapM_ (promoteTyVar outer_tclvl) (nonDetEltsUFM promote_tkvs)
- -- It's OK to use nonDetEltsUFM here because promoteTyVar is
- -- commutative
-
- -- Emit an implication constraint for the
- -- remaining constraints from the RHS
- -- extra_qtvs: see Note [Quantification and partial signatures]
; bound_theta_vars <- mapM TcM.newEvVar bound_theta
- ; psig_theta_vars <- mapM zonkId psig_theta_vars
- ; all_qtvs <- add_psig_tvs qtvs
- [ tv | sig <- partial_sigs
- , (_,tv) <- sig_inst_skols sig ]
-
- ; let full_theta = psig_theta ++ bound_theta
- full_theta_vars = psig_theta_vars ++ bound_theta_vars
- skol_info = InferSkol [ (name, mkSigmaTy [] full_theta ty)
- | (name, ty) <- name_taus ]
- -- Don't add the quantified variables here, because
- -- they are also bound in ic_skols and we want them
- -- to be tidied uniformly
-
- implic = Implic { ic_tclvl = rhs_tclvl
- , ic_skols = all_qtvs
- , ic_no_eqs = False
- , ic_given = full_theta_vars
- , ic_wanted = wanted_transformed
- , ic_status = IC_Unsolved
- , ic_binds = Just ev_binds_var
- , ic_info = skol_info
- , ic_env = tc_lcl_env }
- ; emitImplication implic
+
+ -- We must produce bindings for the psig_theta_vars, because we may have
+ -- used them in evidence bindings constructed by solveWanteds earlier
+ -- Easiest way to do this is to emit them as new Wanteds (Trac #14643)
+ ; ct_loc <- getCtLocM AnnOrigin Nothing
+ ; let psig_wanted = [ CtWanted { ctev_pred = idType psig_theta_var
+ , ctev_dest = EvVarDest psig_theta_var
+ , ctev_nosh = WDeriv
+ , ctev_loc = ct_loc }
+ | psig_theta_var <- psig_theta_vars ]
+
+ -- Now construct the residual constraint
+ ; residual_wanted <- mkResidualConstraints rhs_tclvl tc_env ev_binds_var
+ name_taus co_vars qtvs bound_theta_vars
+ (wanted_transformed `andWC` mkSimpleWC psig_wanted)
-- All done!
; traceTc "} simplifyInfer/produced residual implication for quantification" $
vcat [ text "quant_pred_candidates =" <+> ppr quant_pred_candidates
- , text "promote_tvs=" <+> ppr promote_tkvs
, text "psig_theta =" <+> ppr psig_theta
, text "bound_theta =" <+> ppr bound_theta
- , text "full_theta =" <+> ppr full_theta
- , text "qtvs =" <+> ppr qtvs
- , text "implic =" <+> ppr implic ]
+ , text "qtvs =" <+> ppr qtvs
+ , text "definite_error =" <+> ppr definite_error ]
+
+ ; return ( qtvs, bound_theta_vars, TcEvBinds ev_binds_var
+ , residual_wanted, definite_error ) }
+ -- NB: bound_theta_vars must be fully zonked
+
+
+--------------------
+mkResidualConstraints :: TcLevel -> Env TcGblEnv TcLclEnv -> EvBindsVar
+ -> [(Name, TcTauType)]
+ -> VarSet -> [TcTyVar] -> [EvVar]
+ -> WantedConstraints -> TcM WantedConstraints
+-- Emit the remaining constraints from the RHS.
+-- See Note [Emitting the residual implication in simplifyInfer]
+mkResidualConstraints rhs_tclvl tc_env ev_binds_var
+ name_taus co_vars qtvs full_theta_vars wanteds
+ | isEmptyWC wanteds
+ = return wanteds
+
+ | otherwise
+ = do { wanted_simple <- TcM.zonkSimples (wc_simple wanteds)
+ ; let (outer_simple, inner_simple) = partitionBag is_mono wanted_simple
+ is_mono ct = isWantedCt ct && ctEvId ct `elemVarSet` co_vars
+
+ ; _ <- promoteTyVarSet (tyCoVarsOfCts outer_simple)
- ; return ( qtvs, full_theta_vars, TcEvBinds ev_binds_var ) }
+ ; let inner_wanted = wanteds { wc_simple = inner_simple }
+ ; return (WC { wc_simple = outer_simple
+ , wc_impl = mk_implic inner_wanted })}
where
- add_psig_tvs qtvs [] = return qtvs
- add_psig_tvs qtvs (tv:tvs)
- = do { tv <- zonkTcTyVarToTyVar tv
- ; if tv `elem` qtvs
- then add_psig_tvs qtvs tvs
- else do { mb_tv <- zonkQuantifiedTyVar False tv
- ; case mb_tv of
- Nothing -> add_psig_tvs qtvs tvs
- Just tv -> add_psig_tvs (tv:qtvs) tvs } }
-
-{- Note [Add signature contexts as givens]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ mk_implic inner_wanted
+ | isEmptyWC inner_wanted
+ = emptyBag
+ | otherwise
+ = unitBag (implicationPrototype { ic_tclvl = rhs_tclvl
+ , ic_skols = qtvs
+ , ic_telescope = Nothing
+ , ic_given = full_theta_vars
+ , ic_wanted = inner_wanted
+ , ic_binds = ev_binds_var
+ , ic_no_eqs = False
+ , ic_info = skol_info
+ , ic_env = tc_env })
+
+ full_theta = map idType full_theta_vars
+ skol_info = InferSkol [ (name, mkSigmaTy [] full_theta ty)
+ | (name, ty) <- name_taus ]
+ -- Don't add the quantified variables here, because
+ -- they are also bound in ic_skols and we want them
+ -- to be tidied uniformly
+
+--------------------
+ctsPreds :: Cts -> [PredType]
+ctsPreds cts = [ ctEvPred ev | ct <- bagToList cts
+ , let ev = ctEvidence ct ]
+
+{- Note [Emitting the residual implication in simplifyInfer]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ f = e
+where f's type is inferred to be something like (a, Proxy k (Int |> co))
+and we have an as-yet-unsolved, or perhaps insoluble, constraint
+ [W] co :: Type ~ k
+We can't form types like (forall co. blah), so we can't generalise over
+the coercion variable, and hence we can't generalise over things free in
+its kind, in the case 'k'. But we can still generalise over 'a'. So
+we'll generalise to
+ f :: forall a. (a, Proxy k (Int |> co))
+Now we do NOT want to form the residual implication constraint
+ forall a. [W] co :: Type ~ k
+because then co's eventual binding (which will be a value binding if we
+use -fdefer-type-errors) won't scope over the entire binding for 'f' (whose
+type mentions 'co'). Instead, just as we don't generalise over 'co', we
+should not bury its constraint inside the implication. Instead, we must
+put it outside.
+
+That is the reason for the partitionBag in emitResidualConstraints,
+which takes the CoVars free in the inferred type, and pulls their
+constraints out. (NB: this set of CoVars should be closed-over-kinds.)
+
+All rather subtle; see Trac #14584.
+
+Note [Add signature contexts as givens]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this (Trac #11016):
f2 :: (?x :: Int) => _
f2 = ?x
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If the monomorphism restriction does not apply, then we quantify as follows:
- * Take the global tyvars, and "grow" them using the equality constraints
- E.g. if x:alpha is in the environment, and alpha ~ [beta] (which can
+* Step 1. Take the global tyvars, and "grow" them using the equality
+ constraints
+ E.g. if x:alpha is in the environment, and alpha ~ [beta] (which can
happen because alpha is untouchable here) then do not quantify over
beta, because alpha fixes beta, and beta is effectively free in
the environment too
- These are the mono_tvs
- * Take the free vars of the tau-type (zonked_tau_tvs) and "grow" them
- using all the constraints. These are tau_tvs_plus
+ We also account for the monomorphism restriction; if it applies,
+ add the free vars of all the constraints.
+
+ Result is mono_tvs; we will not quantify over these.
+
+* Step 2. Default any non-mono tyvars (i.e ones that are definitely
+ not going to become further constrained), and re-simplify the
+ candidate constraints.
- * Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being
+ Motivation for re-simplification (Trac #7857): imagine we have a
+ constraint (C (a->b)), where 'a :: TYPE l1' and 'b :: TYPE l2' are
+ not free in the envt, and instance forall (a::*) (b::*). (C a) => C
+ (a -> b) The instance doesn't match while l1,l2 are polymorphic, but
+ it will match when we default them to LiftedRep.
+
+ This is all very tiresome.
+
+* Step 3: decide which variables to quantify over, as follows:
+
+ - Take the free vars of the tau-type (zonked_tau_tvs) and "grow"
+ them using all the constraints. These are tau_tvs_plus
+
+ - Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being
careful to close over kinds, and to skolemise the quantified tyvars.
(This actually unifies each quantifies meta-tyvar with a fresh skolem.)
- Result is qtvs.
- * Filter the constraints using pickQuantifiablePreds and the qtvs.
- We have to zonk the constraints first, so they "see" the freshly
- created skolems.
+ Result is qtvs.
-If the MR does apply, mono_tvs includes all the constrained tyvars --
-including all covars -- and the quantified constraints are empty/insoluble.
+* Step 4: Filter the constraints using pickQuantifiablePreds and the
+ qtvs. We have to zonk the constraints first, so they "see" the
+ freshly created skolems.
-}
decideQuantification
:: InferMode
+ -> TcLevel
-> [(Name, TcTauType)] -- Variables to be generalised
- -> [PredType] -- All annotated constraints from signatures
- -> [PredType] -- Candidate theta
+ -> [TcIdSigInst] -- Partial type signatures (if any)
+ -> [PredType] -- Candidate theta; already zonked
-> TcM ( [TcTyVar] -- Quantify over these (skolems)
- , [PredType] ) -- and this context (fully zonked)
+ , [PredType] -- and this context (fully zonked)
+ , VarSet)
-- See Note [Deciding quantification]
-decideQuantification infer_mode name_taus psig_theta candidates
- = do { gbl_tvs <- tcGetGlobalTyCoVars
- ; zonked_taus <- mapM TcM.zonkTcType (psig_theta ++ taus)
- -- psig_theta: see Note [Quantification and partial signatures]
- ; ovl_strings <- xoptM LangExt.OverloadedStrings
- ; let DV {dv_kvs = zkvs, dv_tvs = ztvs} = splitDepVarsOfTypes zonked_taus
- (gbl_cand, quant_cand) -- gbl_cand = do not quantify me
- = case infer_mode of -- quant_cand = try to quantify me
- ApplyMR -> (candidates, [])
- NoRestrictions -> ([], candidates)
- EagerDefaulting -> partition is_interactive_ct candidates
- where
- is_interactive_ct ct
- | Just (cls, _) <- getClassPredTys_maybe ct
- = isInteractiveClass ovl_strings cls
- | otherwise
- = False
-
- eq_constraints = filter isEqPred quant_cand
- constrained_tvs = tyCoVarsOfTypes gbl_cand
- mono_tvs = growThetaTyVars eq_constraints $
- gbl_tvs `unionVarSet` constrained_tvs
- tau_tvs_plus = growThetaTyVarsDSet quant_cand ztvs
- dvs_plus = DV { dv_kvs = zkvs, dv_tvs = tau_tvs_plus }
-
- ; qtvs <- quantifyZonkedTyVars mono_tvs dvs_plus
- -- We don't grow the kvs, as there's no real need to. Recall
- -- that quantifyTyVars uses the separation between kvs and tvs
- -- only for defaulting, and we don't want (ever) to default a tv
- -- to *. So, don't grow the kvs.
-
- ; quant_cand <- TcM.zonkTcTypes quant_cand
- -- quantifyTyVars turned some meta tyvars into
- -- quantified skolems, so we have to zonk again
-
- ; let qtv_set = mkVarSet qtvs
- theta = pickQuantifiablePreds qtv_set quant_cand
- min_theta = mkMinimalBySCs theta
- -- See Note [Minimize by Superclasses]
+decideQuantification infer_mode rhs_tclvl name_taus psigs candidates
+ = do { -- Step 1: find the mono_tvs
+ ; (mono_tvs, candidates, co_vars) <- decideMonoTyVars infer_mode
+ name_taus psigs candidates
+
+ -- Step 2: default any non-mono tyvars, and re-simplify
+ -- This step may do some unification, but result candidates is zonked
+ ; candidates <- defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
+
+ -- Step 3: decide which kind/type variables to quantify over
+ ; qtvs <- decideQuantifiedTyVars mono_tvs name_taus psigs candidates
+
+ -- Step 4: choose which of the remaining candidate
+ -- predicates to actually quantify over
+ -- NB: decideQuantifiedTyVars turned some meta tyvars
+ -- into quantified skolems, so we have to zonk again
+ ; candidates <- TcM.zonkTcTypes candidates
+ ; psig_theta <- TcM.zonkTcTypes (concatMap sig_inst_theta psigs)
+ ; let quantifiable_candidates
+ = pickQuantifiablePreds (mkVarSet qtvs) candidates
+ -- NB: do /not/ run pickQuantifiablePreds over psig_theta,
+ -- because we always want to quantify over psig_theta, and not
+ -- drop any of them; e.g. CallStack constraints. c.f Trac #14658
+
+ theta = mkMinimalBySCs id $ -- See Note [Minimize by Superclasses]
+ (psig_theta ++ quantifiable_candidates)
+
+ ; traceTc "decideQuantification"
+ (vcat [ text "infer_mode:" <+> ppr infer_mode
+ , text "candidates:" <+> ppr candidates
+ , text "psig_theta:" <+> ppr psig_theta
+ , text "mono_tvs:" <+> ppr mono_tvs
+ , text "co_vars:" <+> ppr co_vars
+ , text "qtvs:" <+> ppr qtvs
+ , text "theta:" <+> ppr theta ])
+ ; return (qtvs, theta, co_vars) }
+
+------------------
+decideMonoTyVars :: InferMode
+ -> [(Name,TcType)]
+ -> [TcIdSigInst]
+ -> [PredType]
+ -> TcM (TcTyCoVarSet, [PredType], CoVarSet)
+-- Decide which tyvars and covars cannot be generalised:
+-- (a) Free in the environment
+-- (b) Mentioned in a constraint we can't generalise
+-- (c) Connected by an equality to (a) or (b)
+-- Also return CoVars that appear free in the final quatified types
+-- we can't quantify over these, and we must make sure they are in scope
+decideMonoTyVars infer_mode name_taus psigs candidates
+ = do { (no_quant, maybe_quant) <- pick infer_mode candidates
+
+ -- If possible, we quantify over partial-sig qtvs, so they are
+ -- not mono. Need to zonk them because they are meta-tyvar SigTvs
+ ; psig_qtvs <- mapM zonkTcTyVarToTyVar $
+ concatMap (map snd . sig_inst_skols) psigs
+
+ ; psig_theta <- mapM TcM.zonkTcType $
+ concatMap sig_inst_theta psigs
+
+ ; taus <- mapM (TcM.zonkTcType . snd) name_taus
+
+ ; mono_tvs0 <- tcGetGlobalTyCoVars
+ ; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta
+
+ co_vars = coVarsOfTypes (psig_tys ++ taus)
+ co_var_tvs = closeOverKinds co_vars
+ -- The co_var_tvs are tvs mentioned in the types of covars or
+ -- coercion holes. We can't quantify over these covars, so we
+ -- must include the variable in their types in the mono_tvs.
+ -- E.g. If we can't quantify over co :: k~Type, then we can't
+ -- quantify over k either! Hence closeOverKinds
+
+ mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs
+
+ eq_constraints = filter isEqPred candidates
+ mono_tvs2 = growThetaTyVars eq_constraints mono_tvs1
+
+ constrained_tvs = (growThetaTyVars eq_constraints
+ (tyCoVarsOfTypes no_quant)
+ `minusVarSet` mono_tvs2)
+ `delVarSetList` psig_qtvs
+ -- constrained_tvs: the tyvars that we are not going to
+ -- quantify solely because of the moonomorphism restriction
+ --
+ -- (`minusVarSet` mono_tvs1`): a type variable is only
+ -- "constrained" (so that the MR bites) if it is not
+ -- free in the environment (Trac #13785)
+ --
+ -- (`delVarSetList` psig_qtvs): if the user has explicitly
+ -- asked for quantification, then that request "wins"
+ -- over the MR. Note: do /not/ delete psig_qtvs from
+ -- mono_tvs1, because mono_tvs1 cannot under any circumstances
+ -- be quantified (Trac #14479); see
+ -- Note [Quantification and partial signatures], Wrinkle 3, 4
+
+ mono_tvs = mono_tvs2 `unionVarSet` constrained_tvs
-- Warn about the monomorphism restriction
; warn_mono <- woptM Opt_WarnMonomorphism
- ; let mr_bites | ApplyMR <- infer_mode
- = constrained_tvs `intersectsVarSet` tcDepVarSet dvs_plus
- | otherwise
- = False
- ; warnTc (Reason Opt_WarnMonomorphism) (warn_mono && mr_bites) $
- hang (text "The Monomorphism Restriction applies to the binding"
- <> plural bndrs <+> text "for" <+> pp_bndrs)
- 2 (text "Consider giving a type signature for"
- <+> if isSingleton bndrs then pp_bndrs
- else text "these binders")
+ ; when (case infer_mode of { ApplyMR -> warn_mono; _ -> False}) $
+ warnTc (Reason Opt_WarnMonomorphism)
+ (constrained_tvs `intersectsVarSet` tyCoVarsOfTypes taus)
+ mr_msg
+
+ ; traceTc "decideMonoTyVars" $ vcat
+ [ text "mono_tvs0 =" <+> ppr mono_tvs0
+ , text "mono_tvs1 =" <+> ppr mono_tvs1
+ , text "no_quant =" <+> ppr no_quant
+ , text "maybe_quant =" <+> ppr maybe_quant
+ , text "eq_constraints =" <+> ppr eq_constraints
+ , text "mono_tvs =" <+> ppr mono_tvs
+ , text "co_vars =" <+> ppr co_vars ]
+
+ ; return (mono_tvs, maybe_quant, co_vars) }
+ where
+ pick :: InferMode -> [PredType] -> TcM ([PredType], [PredType])
+ -- Split the candidates into ones we definitely
+ -- won't quantify, and ones that we might
+ pick NoRestrictions cand = return ([], cand)
+ pick ApplyMR cand = return (cand, [])
+ pick EagerDefaulting cand = do { os <- xoptM LangExt.OverloadedStrings
+ ; return (partition (is_int_ct os) cand) }
+
+ -- For EagerDefaulting, do not quantify over
+ -- over any interactive class constraint
+ is_int_ct ovl_strings pred
+ | Just (cls, _) <- getClassPredTys_maybe pred
+ = isInteractiveClass ovl_strings cls
+ | otherwise
+ = False
- ; traceTc "decideQuantification"
- (vcat [ text "infer_mode:" <+> ppr infer_mode
- , text "gbl_cand:" <+> ppr gbl_cand
- , text "quant_cand:" <+> ppr quant_cand
- , text "gbl_tvs:" <+> ppr gbl_tvs
- , text "mono_tvs:" <+> ppr mono_tvs
- , text "tau_tvs_plus:" <+> ppr tau_tvs_plus
- , text "qtvs:" <+> ppr qtvs
- , text "min_theta:" <+> ppr min_theta ])
- ; return (qtvs, min_theta) }
+ pp_bndrs = pprWithCommas (quotes . ppr . fst) name_taus
+ mr_msg =
+ hang (sep [ text "The Monomorphism Restriction applies to the binding"
+ <> plural name_taus
+ , text "for" <+> pp_bndrs ])
+ 2 (hsep [ text "Consider giving"
+ , text (if isSingleton name_taus then "it" else "them")
+ , text "a type signature"])
+
+-------------------
+defaultTyVarsAndSimplify :: TcLevel
+ -> TyCoVarSet
+ -> [PredType] -- Assumed zonked
+ -> TcM [PredType] -- Guaranteed zonked
+-- Default any tyvar free in the constraints,
+-- and re-simplify in case the defaulting allows further simplification
+defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
+ = do { -- Promote any tyvars that we cannot generalise
+ -- See Note [Promote momomorphic tyvars]
+ ; traceTc "decideMonoTyVars: promotion:" (ppr mono_tvs)
+ ; prom <- promoteTyVarSet mono_tvs
+
+ -- Default any kind/levity vars
+ ; let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
+ = candidateQTyVarsOfTypes candidates
+ ; poly_kinds <- xoptM LangExt.PolyKinds
+ ; default_kvs <- mapM (default_one poly_kinds True)
+ (dVarSetElems cand_kvs)
+ ; default_tvs <- mapM (default_one poly_kinds False)
+ (dVarSetElems (cand_tvs `minusDVarSet` cand_kvs))
+ ; let some_default = or default_kvs || or default_tvs
+
+ ; case () of
+ _ | some_default -> simplify_cand candidates
+ | prom -> mapM TcM.zonkTcType candidates
+ | otherwise -> return candidates
+ }
where
- pp_bndrs = pprWithCommas (quotes . ppr) bndrs
- (bndrs, taus) = unzip name_taus
+ default_one poly_kinds is_kind_var tv
+ | not (isMetaTyVar tv)
+ = return False
+ | tv `elemVarSet` mono_tvs
+ = return False
+ | otherwise
+ = defaultTyVar (not poly_kinds && is_kind_var) tv
+
+ simplify_cand candidates
+ = do { clone_wanteds <- newWanteds DefaultOrigin candidates
+ ; WC { wc_simple = simples } <- setTcLevel rhs_tclvl $
+ simplifyWantedsTcM clone_wanteds
+ -- Discard evidence; simples is fully zonked
+
+ ; let new_candidates = ctsPreds simples
+ ; traceTc "Simplified after defaulting" $
+ vcat [ text "Before:" <+> ppr candidates
+ , text "After:" <+> ppr new_candidates ]
+ ; return new_candidates }
+
+------------------
+decideQuantifiedTyVars
+ :: TyCoVarSet -- Monomorphic tyvars
+ -> [(Name,TcType)] -- Annotated theta and (name,tau) pairs
+ -> [TcIdSigInst] -- Partial signatures
+ -> [PredType] -- Candidates, zonked
+ -> TcM [TyVar]
+-- Fix what tyvars we are going to quantify over, and quantify them
+decideQuantifiedTyVars mono_tvs name_taus psigs candidates
+ = do { -- Why psig_tys? We try to quantify over everything free in here
+ -- See Note [Quantification and partial signatures]
+ -- Wrinkles 2 and 3
+ ; psig_tv_tys <- mapM TcM.zonkTcTyVar [ tv | sig <- psigs
+ , (_,tv) <- sig_inst_skols sig ]
+ ; psig_theta <- mapM TcM.zonkTcType [ pred | sig <- psigs
+ , pred <- sig_inst_theta sig ]
+ ; tau_tys <- mapM (TcM.zonkTcType . snd) name_taus
+ ; mono_tvs <- TcM.zonkTyCoVarsAndFV mono_tvs
+
+ ; let -- Try to quantify over variables free in these types
+ psig_tys = psig_tv_tys ++ psig_theta
+ seed_tys = psig_tys ++ tau_tys
+
+ -- Now "grow" those seeds to find ones reachable via 'candidates'
+ grown_tcvs = growThetaTyVars candidates (tyCoVarsOfTypes seed_tys)
+
+ -- Now we have to classify them into kind variables and type variables
+ -- (sigh) just for the benefit of -XNoPolyKinds; see quantifyTyVars
+ --
+ -- Keep the psig_tys first, so that candidateQTyVarsOfTypes produces
+ -- them in that order, so that the final qtvs quantifies in the same
+ -- order as the partial signatures do (Trac #13524)
+ ; let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
+ = candidateQTyVarsOfTypes $
+ psig_tys ++ candidates ++ tau_tys
+ pick = (`dVarSetIntersectVarSet` grown_tcvs)
+ dvs_plus = DV { dv_kvs = pick cand_kvs, dv_tvs = pick cand_tvs }
+
+ ; traceTc "decideQuantifiedTyVars" (vcat
+ [ text "seed_tys =" <+> ppr seed_tys
+ , text "seed_tcvs =" <+> ppr (tyCoVarsOfTypes seed_tys)
+ , text "grown_tcvs =" <+> ppr grown_tcvs])
+
+ ; quantifyTyVars mono_tvs dvs_plus }
------------------
-growThetaTyVars :: ThetaType -> TyCoVarSet -> TyVarSet
+growThetaTyVars :: ThetaType -> TyCoVarSet -> TyCoVarSet
-- See Note [Growing the tau-tvs using constraints]
--- NB: only returns tyvars, never covars
-growThetaTyVars theta tvs
- | null theta = tvs_only
- | otherwise = filterVarSet isTyVar $
- transCloVarSet mk_next seed_tvs
+growThetaTyVars theta tcvs
+ | null theta = tcvs
+ | otherwise = transCloVarSet mk_next seed_tcvs
where
- tvs_only = filterVarSet isTyVar tvs
- seed_tvs = tvs `unionVarSet` tyCoVarsOfTypes ips
+ seed_tcvs = tcvs `unionVarSet` tyCoVarsOfTypes ips
(ips, non_ips) = partition isIPPred theta
-- See Note [Inheriting implicit parameters] in TcType
mk_next :: VarSet -> VarSet -- Maps current set to newly-grown ones
mk_next so_far = foldr (grow_one so_far) emptyVarSet non_ips
- grow_one so_far pred tvs
- | pred_tvs `intersectsVarSet` so_far = tvs `unionVarSet` pred_tvs
- | otherwise = tvs
+ grow_one so_far pred tcvs
+ | pred_tcvs `intersectsVarSet` so_far = tcvs `unionVarSet` pred_tcvs
+ | otherwise = tcvs
where
- pred_tvs = tyCoVarsOfType pred
+ pred_tcvs = tyCoVarsOfType pred
-------------------
-growThetaTyVarsDSet :: ThetaType -> DTyCoVarSet -> DTyVarSet
--- See Note [Growing the tau-tvs using constraints]
--- NB: only returns tyvars, never covars
--- It takes a deterministic set of TyCoVars and returns a deterministic set
--- of TyVars.
--- The implementation mirrors growThetaTyVars, the only difference is that
--- it avoids unionDVarSet and uses more efficient extendDVarSetList.
-growThetaTyVarsDSet theta tvs
- | null theta = tvs_only
- | otherwise = filterDVarSet isTyVar $
- transCloDVarSet mk_next seed_tvs
- where
- tvs_only = filterDVarSet isTyVar tvs
- seed_tvs = tvs `extendDVarSetList` tyCoVarsOfTypesList ips
- (ips, non_ips) = partition isIPPred theta
- -- See Note [Inheriting implicit parameters] in TcType
- mk_next :: DVarSet -> DVarSet -- Maps current set to newly-grown ones
- mk_next so_far = foldr (grow_one so_far) emptyDVarSet non_ips
- grow_one so_far pred tvs
- | any (`elemDVarSet` so_far) pred_tvs = tvs `extendDVarSetList` pred_tvs
- | otherwise = tvs
- where
- pred_tvs = tyCoVarsOfTypeList pred
-
-{- Note [Quantification and partial signatures]
+{- Note [Promote momomorphic tyvars]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Promote any type variables that are free in the environment. Eg
+ f :: forall qtvs. bound_theta => zonked_tau
+The free vars of f's type become free in the envt, and hence will show
+up whenever 'f' is called. They may currently at rhs_tclvl, but they
+had better be unifiable at the outer_tclvl! Example: envt mentions
+alpha[1]
+ tau_ty = beta[2] -> beta[2]
+ constraints = alpha ~ [beta]
+we don't quantify over beta (since it is fixed by envt)
+so we must promote it! The inferred type is just
+ f :: beta -> beta
+
+NB: promoteTyVar ignores coercion variables
+
+Note [Quantification and partial signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When choosing type variables to quantify, the basic plan is to
quantify over all type variables that are
f x = ...
or
g :: (Eq _a) => _b -> _b
-In both cases we use plan InferGen, and hence call simplifyInfer.
-But those 'a' variables are skolems, and we should be sure to quantify
-over them, for two reasons
+In both cases we use plan InferGen, and hence call simplifyInfer. But
+those 'a' variables are skolems (actually SigTvs), and we should be
+sure to quantify over them. This leads to several wrinkles:
-* In the case of a type error
+* Wrinkle 1. In the case of a type error
f :: _ -> Maybe a
f x = True && x
The inferred type of 'f' is f :: Bool -> Bool, but there's a
left-over error of form (HoleCan (Maybe a ~ Bool)). The error-reporting
machine expects to find a binding site for the skolem 'a', so we
- add it to the ic_skols of the residual implication.
+ add it to the quantified tyvars.
- Note that we /only/ do this to the residual implication. We don't
- complicate the quantified type varialbes of 'f' for downstream code;
- it's just a device to make the error message generator know what to
- report.
-
-* Consider the partial type signature
+* Wrinkle 2. Consider the partial type signature
f :: (Eq _) => Int -> Int
f x = x
In normal cases that makes sense; e.g.
(thereby correctly triggering an ambiguity error later). If we don't
we'll end up with a strange open type
f :: Eq alpha => Int -> Int
- which isn't ambiguous but is still very wrong. That's why include
- psig_theta in the variables to quantify over, passed to
- decideQuantification.
+ which isn't ambiguous but is still very wrong.
+
+ Bottom line: Try to quantify over any variable free in psig_theta,
+ just like the tau-part of the type.
+
+* Wrinkle 3 (Trac #13482). Also consider
+ f :: forall a. _ => Int -> Int
+ f x = if (undefined :: a) == undefined then x else 0
+ Here we get an (Eq a) constraint, but it's not mentioned in the
+ psig_theta nor the type of 'f'. But we still want to quantify
+ over 'a' even if the monomorphism restriction is on.
+
+* Wrinkle 4 (Trac #14479)
+ foo :: Num a => a -> a
+ foo xxx = g xxx
+ where
+ g :: forall b. Num b => _ -> b
+ g y = xxx + y
+
+ In the signature for 'g', we cannot quantify over 'b' because it turns out to
+ get unified with 'a', which is free in g's environment. So we carefully
+ refrain from bogusly quantifying, in TcSimplify.decideMonoTyVars. We
+ report the error later, in TcBinds.chooseInferredQuantifiers.
Note [Quantifying over equality constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note [Quantification with errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we find that the RHS of the definition has some absolutely-insoluble
-constraints, we abandon all attempts to find a context to quantify
-over, and instead make the function fully-polymorphic in whatever
-type we have found. For two reasons
- a) Minimise downstream errors
- b) Avoid spurious errors from this function
-
-But NB that we must include *derived* errors in the check. Example:
+constraints (including especially "variable not in scope"), we
+
+* Abandon all attempts to find a context to quantify over,
+ and instead make the function fully-polymorphic in whatever
+ type we have found
+
+* Return a flag from simplifyInfer, indicating that we found an
+ insoluble constraint. This flag is used to suppress the ambiguity
+ check for the inferred type, which may well be bogus, and which
+ tends to obscure the real error. This fix feels a bit clunky,
+ but I failed to come up with anything better.
+
+Reasons:
+ - Avoid downstream errors
+ - Do not perform an ambiguity test on a bogus type, which might well
+ fail spuriously, thereby obfuscating the original insoluble error.
+ Trac #14000 is an example
+
+I tried an alternative approach: simply failM, after emitting the
+residual implication constraint; the exception will be caught in
+TcBinds.tcPolyBinds, which gives all the binders in the group the type
+(forall a. a). But that didn't work with -fdefer-type-errors, because
+the recovery from failM emits no code at all, so there is no function
+to run! But -fdefer-type-errors aspires to produce a runnable program.
+
+NB that we must include *derived* errors in the check for insolubles.
+Example:
(a::*) ~ Int#
We get an insoluble derived error *~#, and we don't want to discard
it before doing the isInsolubleWC test! (Trac #8262)
-- Postcondition: fully zonked and unflattened constraints
simplifyWantedsTcM wanted
= do { traceTc "simplifyWantedsTcM {" (ppr wanted)
- ; (result, _) <- runTcS (solveWantedsAndDrop $ mkSimpleWC wanted)
+ ; (result, _) <- runTcS (solveWantedsAndDrop (mkSimpleWC wanted))
; result <- TcM.zonkWC result
; traceTc "simplifyWantedsTcM }" (ppr result)
; return result }
solveWanteds :: WantedConstraints -> TcS WantedConstraints
-- so that the inert set doesn't mindlessly propagate.
-- NB: wc_simples may be wanted /or/ derived now
-solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
+solveWanteds wc@(WC { wc_simple = simples, wc_impl = implics })
= do { traceTcS "solveWanteds {" (ppr wc)
- -- Try the simple bit, including insolubles. Solving insolubles a
- -- second time round is a bit of a waste; but the code is simple
- -- and the program is wrong anyway, and we don't run the danger
- -- of adding Derived insolubles twice; see
- -- TcSMonad Note [Do not add duplicate derived insolubles]
; wc1 <- solveSimpleWanteds simples
- ; (no_new_scs, wc1) <- expandSuperClasses wc1
- ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
+ -- Any insoluble constraints are in 'simples' and so get rewritten
+ -- See Note [Rewrite insolubles] in TcSMonad
- ; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1)
+ ; (floated_eqs, implics2) <- solveNestedImplications $
+ implics `unionBags` wc_impl wc1
- ; dflags <- getDynFlags
- ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs no_new_scs
- (WC { wc_simple = simples1, wc_impl = implics2
- , wc_insol = insols `unionBags` insols1 })
+ ; dflags <- getDynFlags
+ ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs
+ (wc1 { wc_impl = implics2 })
- ; bb <- TcS.getTcEvBindsMap
+ ; ev_binds_var <- getTcEvBindsVar
+ ; bb <- TcS.getTcEvBindsMap ev_binds_var
; traceTcS "solveWanteds }" $
vcat [ text "final wc =" <+> ppr final_wc
, text "current evbinds =" <+> ppr (evBindMapBinds bb) ]
; return final_wc }
-simpl_loop :: Int -> IntWithInf -> Cts -> Bool
- -> WantedConstraints
- -> TcS WantedConstraints
-simpl_loop n limit floated_eqs no_new_scs
- wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
- | isEmptyBag floated_eqs && no_new_scs
- = return wc -- Done!
-
+simpl_loop :: Int -> IntWithInf -> Cts
+ -> WantedConstraints -> TcS WantedConstraints
+simpl_loop n limit floated_eqs wc@(WC { wc_simple = simples })
| n `intGtLimit` limit
= do { -- Add an error (not a warning) if we blow the limit,
-- Typically if we blow the limit we are going to report some other error
2 (vcat [ text "Unsolved:" <+> ppr wc
, ppUnless (isEmptyBag floated_eqs) $
text "Floated equalities:" <+> ppr floated_eqs
- , ppUnless no_new_scs $
- text "New superclasses found"
, text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit"
]))
; return wc }
+ | not (isEmptyBag floated_eqs)
+ = simplify_again n limit True (wc { wc_simple = floated_eqs `unionBags` simples })
+ -- Put floated_eqs first so they get solved first
+ -- NB: the floated_eqs may include /derived/ equalities
+ -- arising from fundeps inside an implication
+
+ | superClassesMightHelp wc
+ = -- We still have unsolved goals, and apparently no way to solve them,
+ -- so try expanding superclasses at this level, both Given and Wanted
+ do { pending_given <- getPendingGivenScs
+ ; let (pending_wanted, simples1) = getPendingWantedScs simples
+ ; if null pending_given && null pending_wanted
+ then return wc -- After all, superclasses did not help
+ else
+ do { new_given <- makeSuperClasses pending_given
+ ; new_wanted <- makeSuperClasses pending_wanted
+ ; solveSimpleGivens new_given -- Add the new Givens to the inert set
+ ; simplify_again n limit (null pending_given)
+ wc { wc_simple = simples1 `unionBags` listToBag new_wanted } } }
+
| otherwise
- = do { let n_floated = lengthBag floated_eqs
- ; csTraceTcS $
+ = return wc
+
+simplify_again :: Int -> IntWithInf -> Bool
+ -> WantedConstraints -> TcS WantedConstraints
+-- We have definitely decided to have another go at solving
+-- the wanted constraints (we have tried at least once already
+simplify_again n limit no_new_given_scs
+ wc@(WC { wc_simple = simples, wc_impl = implics })
+ = do { csTraceTcS $
text "simpl_loop iteration=" <> int n
- <+> (parens $ hsep [ text "no new scs =" <+> ppr no_new_scs <> comma
- , int n_floated <+> text "floated eqs" <> comma
+ <+> (parens $ hsep [ text "no new given superclasses =" <+> ppr no_new_given_scs <> comma
, int (lengthBag simples) <+> text "simples to solve" ])
+ ; traceTcS "simpl_loop: wc =" (ppr wc)
- -- solveSimples may make progress if either float_eqs hold
; (unifs1, wc1) <- reportUnifications $
- solveSimpleWanteds (floated_eqs `unionBags` simples)
- -- Put floated_eqs first so they get solved first
- -- NB: the floated_eqs may include /derived/ equalities
- -- arising from fundeps inside an implication
-
- ; (no_new_scs, wc1) <- expandSuperClasses wc1
- ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
+ solveSimpleWanteds $
+ simples
+ -- See Note [Cutting off simpl_loop]
-- We have already tried to solve the nested implications once
-- Try again only if we have unified some meta-variables
- -- (which is a bit like adding more givens
- -- See Note [Cutting off simpl_loop]
- ; (floated_eqs2, implics2) <- if unifs1 == 0 && isEmptyBag implics1
- then return (emptyBag, implics)
- else solveNestedImplications (implics `unionBags` implics1)
-
- ; simpl_loop (n+1) limit floated_eqs2 no_new_scs
- (WC { wc_simple = simples1, wc_impl = implics2
- , wc_insol = insols `unionBags` insols1 }) }
-
-expandSuperClasses :: WantedConstraints -> TcS (Bool, WantedConstraints)
--- If there are any unsolved wanteds, expand one step of superclasses for
--- unsolved wanteds or givens
--- See Note [The superclass story] in TcCanonical
-expandSuperClasses wc@(WC { wc_simple = unsolved, wc_insol = insols })
- | not (anyBag superClassesMightHelp unsolved)
- = return (True, wc)
- | otherwise
- = do { traceTcS "expandSuperClasses {" empty
- ; let (pending_wanted, unsolved') = mapAccumBagL get [] unsolved
- get acc ct = case isPendingScDict ct of
- Just ct' -> (ct':acc, ct')
- Nothing -> (acc, ct)
- ; pending_given <- getPendingScDicts
- ; if null pending_given && null pending_wanted
- then do { traceTcS "End expandSuperClasses no-op }" empty
- ; return (True, wc) }
- else
- do { new_given <- makeSuperClasses pending_given
- ; new_insols <- solveSimpleGivens new_given
- ; new_wanted <- makeSuperClasses pending_wanted
- ; traceTcS "End expandSuperClasses }"
- (vcat [ text "Given:" <+> ppr pending_given
- , text "Insols from given:" <+> ppr new_insols
- , text "Wanted:" <+> ppr new_wanted ])
- ; return (False, wc { wc_simple = unsolved' `unionBags` listToBag new_wanted
- , wc_insol = insols `unionBags` new_insols }) } }
+ -- (which is a bit like adding more givens), or we have some
+ -- new Given superclasses
+ ; let new_implics = wc_impl wc1
+ ; if unifs1 == 0 &&
+ no_new_given_scs &&
+ isEmptyBag new_implics
+
+ then -- Do not even try to solve the implications
+ simpl_loop (n+1) limit emptyBag (wc1 { wc_impl = implics })
+
+ else -- Try to solve the implications
+ do { (floated_eqs2, implics2) <- solveNestedImplications $
+ implics `unionBags` new_implics
+ ; simpl_loop (n+1) limit floated_eqs2 (wc1 { wc_impl = implics2 })
+ } }
solveNestedImplications :: Bag Implication
-> TcS (Cts, Bag Implication)
-- Precondition: The TcS monad contains an empty worklist and given-only inerts
-- which after trying to solve this implication we must restore to their original value
solveImplication imp@(Implic { ic_tclvl = tclvl
- , ic_binds = m_ev_binds
+ , ic_binds = ev_binds_var
, ic_skols = skols
, ic_given = given_ids
, ic_wanted = wanteds
, ic_info = info
- , ic_status = status
- , ic_env = env })
- | IC_Solved {} <- status
+ , ic_status = status })
+ | isSolvedStatus status
= return (emptyCts, Just imp) -- Do nothing
| otherwise -- Even for IC_Insoluble it is worth doing more work
= do { inerts <- getTcSInerts
; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts)
+ ; when debugIsOn check_tc_level
+
-- Solve the nested constraints
- ; ((no_given_eqs, given_insols, residual_wanted), used_tcvs)
- <- nestImplicTcS m_ev_binds (mkVarSet (skols ++ given_ids)) tclvl $
- do { let loc = mkGivenLoc tclvl info env
+ ; (no_given_eqs, given_insols, residual_wanted)
+ <- nestImplicTcS ev_binds_var tclvl $
+ do { let loc = mkGivenLoc tclvl info (implicLclEnv imp)
givens = mkGivens loc given_ids
- ; given_insols <- solveSimpleGivens givens
+ ; solveSimpleGivens givens
; residual_wanted <- solveWanteds wanteds
-- solveWanteds, *not* solveWantedsAndDrop, because
-- we want to retain derived equalities so we can float
-- them out in floatEqualities
- ; no_eqs <- getNoGivenEqs tclvl skols
+ ; (no_eqs, given_insols) <- getNoGivenEqs tclvl skols
-- Call getNoGivenEqs /after/ solveWanteds, because
-- solveWanteds can augment the givens, via expandSuperClasses,
-- to reveal given superclass equalities
; return (no_eqs, given_insols, residual_wanted) }
; (floated_eqs, residual_wanted)
- <- floatEqualities skols no_given_eqs residual_wanted
+ <- floatEqualities skols given_ids ev_binds_var
+ no_given_eqs residual_wanted
; traceTcS "solveImplication 2"
- (ppr given_insols $$ ppr residual_wanted $$ ppr used_tcvs)
+ (ppr given_insols $$ ppr residual_wanted)
; let final_wanted = residual_wanted `addInsols` given_insols
+ -- Don't lose track of the insoluble givens,
+ -- which signal unreachable code; put them in ic_wanted
; res_implic <- setImplicationStatus (imp { ic_no_eqs = no_given_eqs
, ic_wanted = final_wanted })
- used_tcvs
- ; evbinds <- TcS.getTcEvBindsMap
+ ; evbinds <- TcS.getTcEvBindsMap ev_binds_var
+ ; tcvs <- TcS.getTcEvTyCoVars ev_binds_var
; traceTcS "solveImplication end }" $ vcat
[ text "no_given_eqs =" <+> ppr no_given_eqs
, text "floated_eqs =" <+> ppr floated_eqs
, text "res_implic =" <+> ppr res_implic
- , text "implication evbinds = " <+> ppr (evBindMapBinds evbinds) ]
+ , text "implication evbinds =" <+> ppr (evBindMapBinds evbinds)
+ , text "implication tvcs =" <+> ppr tcvs ]
; return (floated_eqs, res_implic) }
+ where
+ -- TcLevels must be strictly increasing (see (ImplicInv) in
+ -- Note [TcLevel and untouchable type variables] in TcType),
+ -- and in fact I thinkthey should always increase one level at a time.
+ check_tc_level = do { cur_lvl <- TcS.getTcLevel
+ ; MASSERT2( tclvl == pushTcLevel cur_lvl
+ , text "Cur lvl =" <+> ppr cur_lvl $$
+ text "Imp lvl =" <+> ppr tclvl ) }
+
----------------------
-setImplicationStatus :: Implication -> TyCoVarSet -- needed variables
- -> TcS (Maybe Implication)
+setImplicationStatus :: Implication -> TcS (Maybe Implication)
-- Finalise the implication returned from solveImplication:
-- * Set the ic_status field
-- * Trim the ic_wanted field to remove Derived constraints
+-- Precondition: the ic_status field is not already IC_Solved
-- Return Nothing if we can discard the implication altogether
-setImplicationStatus implic@(Implic { ic_binds = m_ev_binds_var
- , ic_info = info
- , ic_tclvl = tc_lvl
- , ic_wanted = wc
- , ic_given = givens })
- used_tcvs
- | some_insoluble
- = return $ Just $
- implic { ic_status = IC_Insoluble
- , ic_wanted = wc { wc_simple = pruned_simples
- , wc_insol = pruned_insols } }
-
- | some_unsolved
- = return $ Just $
- implic { ic_status = IC_Unsolved
- , ic_wanted = wc { wc_simple = pruned_simples
- , wc_insol = pruned_insols } }
-
- | otherwise -- Everything is solved; look at the implications
+setImplicationStatus implic@(Implic { ic_status = status
+ , ic_info = info
+ , ic_wanted = wc
+ , ic_given = givens })
+ | ASSERT2( not (isSolvedStatus status ), ppr info )
+ -- Precondition: we only set the status if it is not already solved
+ not (isSolvedWC pruned_wc)
+ = do { traceTcS "setImplicationStatus(not-all-solved) {" (ppr implic)
+
+ ; implic <- neededEvVars implic
+
+ ; let new_status | insolubleWC pruned_wc = IC_Insoluble
+ | otherwise = IC_Unsolved
+ new_implic = implic { ic_status = new_status
+ , ic_wanted = pruned_wc }
+
+ ; traceTcS "setImplicationStatus(not-all-solved) }" (ppr new_implic)
+
+ ; return $ Just new_implic }
+
+ | otherwise -- Everything is solved
+ -- Set status to IC_Solved,
+ -- and compute the dead givens and outer needs
-- See Note [Tracking redundant constraints]
- = do { ev_binds <- case m_ev_binds_var of
- Just (EvBindsVar ref _) -> TcS.readTcRef ref
- Nothing -> return emptyEvBindMap
- ; let all_needs = neededEvVars ev_binds
- (used_tcvs `unionVarSet` implic_needs)
-
- dead_givens | warnRedundantGivens info
- = filterOut (`elemVarSet` all_needs) givens
- | otherwise = [] -- None to report
+ = do { traceTcS "setImplicationStatus(all-solved) {" (ppr implic)
+
+ ; implic@(Implic { ic_need_inner = need_inner
+ , ic_need_outer = need_outer }) <- neededEvVars implic
+
+ ; bad_telescope <- checkBadTelescope implic
- final_needs = all_needs `delVarSetList` givens
+ ; let dead_givens | warnRedundantGivens info
+ = filterOut (`elemVarSet` need_inner) givens
+ | otherwise = [] -- None to report
discard_entire_implication -- Can we discard the entire implication?
= null dead_givens -- No warning from this implication
- && isEmptyBag pruned_implics -- No live children
- && isEmptyVarSet final_needs -- No needed vars to pass up to parent
+ && not bad_telescope
+ && isEmptyWC pruned_wc -- No live children
+ && isEmptyVarSet need_outer -- No needed vars to pass up to parent
- final_status = IC_Solved { ics_need = final_needs
- , ics_dead = dead_givens }
+ final_status
+ | bad_telescope = IC_BadTelescope
+ | otherwise = IC_Solved { ics_dead = dead_givens }
final_implic = implic { ic_status = final_status
- , ic_wanted = wc { wc_simple = pruned_simples
- , wc_insol = pruned_insols
- , wc_impl = pruned_implics } }
- -- We can only prune the child implications (pruned_implics)
- -- in the IC_Solved status case, because only then we can
- -- accumulate their needed evidence variales into the
- -- IC_Solved final_status field of the parent implication.
+ , ic_wanted = pruned_wc }
+
+ ; traceTcS "setImplicationStatus(all-solved) }" $
+ vcat [ text "discard:" <+> ppr discard_entire_implication
+ , text "new_implic:" <+> ppr final_implic ]
; return $ if discard_entire_implication
then Nothing
else Just final_implic }
where
- WC { wc_simple = simples, wc_impl = implics, wc_insol = insols } = wc
-
- some_insoluble = insolubleWC tc_lvl wc
- some_unsolved = not (isEmptyBag simples && isEmptyBag insols)
- || isNothing mb_implic_needs
+ WC { wc_simple = simples, wc_impl = implics } = wc
pruned_simples = dropDerivedSimples simples
- pruned_insols = dropDerivedInsols insols
- pruned_implics = filterBag need_to_keep_implic implics
-
- mb_implic_needs :: Maybe VarSet
- -- Just vs => all implics are IC_Solved, with 'vs' needed
- -- Nothing => at least one implic is not IC_Solved
- mb_implic_needs = foldrBag add_implic (Just emptyVarSet) implics
- Just implic_needs = mb_implic_needs
-
- add_implic implic acc
- | Just vs_acc <- acc
- , IC_Solved { ics_need = vs } <- ic_status implic
- = Just (vs `unionVarSet` vs_acc)
- | otherwise = Nothing
-
- need_to_keep_implic ic
- | IC_Solved { ics_dead = [] } <- ic_status ic
- -- Fully solved, and no redundant givens to report
+ pruned_implics = filterBag keep_me implics
+ pruned_wc = WC { wc_simple = pruned_simples
+ , wc_impl = pruned_implics }
+
+ keep_me :: Implication -> Bool
+ keep_me ic
+ | IC_Solved { ics_dead = dead_givens } <- ic_status ic
+ -- Fully solved
+ , null dead_givens -- No redundant givens to report
, isEmptyBag (wc_impl (ic_wanted ic))
-- And no children that might have things to report
- = False
+ = False -- Tnen we don't need to keep it
| otherwise
- = True
+ = True -- Otherwise, keep it
+
+checkBadTelescope :: Implication -> TcS Bool
+-- True <=> the skolems form a bad telescope
+-- See Note [Keeping scoped variables in order: Explicit] in TcHsType
+checkBadTelescope (Implic { ic_telescope = m_telescope
+ , ic_skols = skols })
+ | isJust m_telescope
+ = do{ skols <- mapM TcS.zonkTcTyCoVarBndr skols
+ ; return (go emptyVarSet (reverse skols))}
+
+ | otherwise
+ = return False
+
+ where
+ go :: TyVarSet -- skolems that appear *later* than the current ones
+ -> [TcTyVar] -- ordered skolems, in reverse order
+ -> Bool -- True <=> there is an out-of-order skolem
+ go _ [] = False
+ go later_skols (one_skol : earlier_skols)
+ | tyCoVarsOfType (tyVarKind one_skol) `intersectsVarSet` later_skols
+ = True
+ | otherwise
+ = go (later_skols `extendVarSet` one_skol) earlier_skols
warnRedundantGivens :: SkolemInfo -> Bool
-warnRedundantGivens (SigSkol ctxt _)
+warnRedundantGivens (SigSkol ctxt _ _)
= case ctxt of
FunSigCtxt _ warn_redundant -> warn_redundant
ExprSigCtxt -> True
warnRedundantGivens (InstSkol {}) = True
warnRedundantGivens _ = False
-neededEvVars :: EvBindMap -> VarSet -> VarSet
+neededEvVars :: Implication -> TcS Implication
-- Find all the evidence variables that are "needed",
--- and then delete all those bound by the evidence bindings
--- See note [Tracking redundant constraints]
-neededEvVars ev_binds initial_seeds
- = needed `minusVarSet` bndrs
+-- and delete dead evidence bindings
+-- See Note [Tracking redundant constraints]
+-- See Note [Delete dead Given evidence bindings]
+--
+-- - Start from initial_seeds (from nested implications)
+--
+-- - Add free vars of RHS of all Wanted evidence bindings
+-- and coercion variables accumulated in tcvs (all Wanted)
+--
+-- - Generate 'needed', the needed set of EvVars, by doing transitive
+-- closure through Given bindings
+-- e.g. Needed {a,b}
+-- Given a = sc_sel a2
+-- Then a2 is needed too
+--
+-- - Prune out all Given bindings that are not needed
+--
+-- - From the 'needed' set, delete ev_bndrs, the binders of the
+-- evidence bindings, to give the final needed variables
+--
+neededEvVars implic@(Implic { ic_given = givens
+ , ic_binds = ev_binds_var
+ , ic_wanted = WC { wc_impl = implics }
+ , ic_need_inner = old_needs })
+ = do { ev_binds <- TcS.getTcEvBindsMap ev_binds_var
+ ; tcvs <- TcS.getTcEvTyCoVars ev_binds_var
+
+ ; let seeds1 = foldrBag add_implic_seeds old_needs implics
+ seeds2 = foldEvBindMap add_wanted seeds1 ev_binds
+ seeds3 = seeds2 `unionVarSet` tcvs
+ need_inner = findNeededEvVars ev_binds seeds3
+ live_ev_binds = filterEvBindMap (needed_ev_bind need_inner) ev_binds
+ need_outer = foldEvBindMap del_ev_bndr need_inner live_ev_binds
+ `delVarSetList` givens
+
+ ; TcS.setTcEvBindsMap ev_binds_var live_ev_binds
+ -- See Note [Delete dead Given evidence bindings]
+
+ ; traceTcS "neededEvVars" $
+ vcat [ text "old_needs:" <+> ppr old_needs
+ , text "seeds3:" <+> ppr seeds3
+ , text "ev_binds:" <+> ppr ev_binds
+ , text "live_ev_binds:" <+> ppr live_ev_binds ]
+
+ ; return (implic { ic_need_inner = need_inner
+ , ic_need_outer = need_outer }) }
where
- seeds = foldEvBindMap add_wanted initial_seeds ev_binds
- needed = transCloVarSet also_needs seeds
- bndrs = foldEvBindMap add_bndr emptyVarSet ev_binds
+ add_implic_seeds (Implic { ic_need_outer = needs, ic_given = givens }) acc
+ = (needs `delVarSetList` givens) `unionVarSet` acc
+
+ needed_ev_bind needed (EvBind { eb_lhs = ev_var
+ , eb_is_given = is_given })
+ | is_given = ev_var `elemVarSet` needed
+ | otherwise = True -- Keep all wanted bindings
+
+ del_ev_bndr :: EvBind -> VarSet -> VarSet
+ del_ev_bndr (EvBind { eb_lhs = v }) needs = delVarSet needs v
add_wanted :: EvBind -> VarSet -> VarSet
add_wanted (EvBind { eb_is_given = is_given, eb_rhs = rhs }) needs
| is_given = needs -- Add the rhs vars of the Wanted bindings only
| otherwise = evVarsOfTerm rhs `unionVarSet` needs
- also_needs :: VarSet -> VarSet
- also_needs needs
- = nonDetFoldUFM add emptyVarSet needs
- -- It's OK to use nonDetFoldUFM here because we immediately forget
- -- about the ordering by creating a set
- where
- add v needs
- | Just ev_bind <- lookupEvBind ev_binds v
- , EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind
- , is_given
- = evVarsOfTerm rhs `unionVarSet` needs
- | otherwise
- = needs
- add_bndr :: EvBind -> VarSet -> VarSet
- add_bndr (EvBind { eb_lhs = v }) vs = extendVarSet vs v
+{- Note [Delete dead Given evidence bindings]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+As a result of superclass expansion, we speculatively
+generate evidence bindings for Givens. E.g.
+ f :: (a ~ b) => a -> b -> Bool
+ f x y = ...
+We'll have
+ [G] d1 :: (a~b)
+and we'll specuatively generate the evidence binding
+ [G] d2 :: (a ~# b) = sc_sel d
+Now d2 is available for solving. But it may not be needed! Usually
+such dead superclass selections will eventually be dropped as dead
+code, but:
+
+ * It won't always be dropped (Trac #13032). In the case of an
+ unlifted-equality superclass like d2 above, we generate
+ case heq_sc d1 of d2 -> ...
+ and we can't (in general) drop that case exrpession in case
+ d1 is bottom. So it's technically unsound to have added it
+ in the first place.
+
+ * Simply generating all those extra superclasses can generate lots of
+ code that has to be zonked, only to be discarded later. Better not
+ to generate it in the first place.
+
+ Moreover, if we simplify this implication more than once
+ (e.g. because we can't solve it completely on the first iteration
+ of simpl_looop), we'll generate all the same bindings AGAIN!
+
+Easy solution: take advantage of the work we are doing to track dead
+(unused) Givens, and use it to prune the Given bindings too. This is
+all done by neededEvVars.
+
+This led to a remarkable 25% overall compiler allocation decrease in
+test T12227.
-{-
Note [Tracking redundant constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
With Opt_WarnRedundantConstraints, GHC can report which
----- How tracking works
+* The ic_need fields of an Implic records in-scope (given) evidence
+ variables bound by the context, that were needed to solve this
+ implication (so far). See the declaration of Implication.
+
* When the constraint solver finishes solving all the wanteds in
an implication, it sets its status to IC_Solved
- - The ics_dead field, of IC_Solved, records the subset of this implication's
- ic_given that are redundant (not needed).
-
- - The ics_need field of IC_Solved then records all the
- in-scope (given) evidence variables bound by the context, that
- were needed to solve this implication, including all its nested
- implications. (We remove the ic_given of this implication from
- the set, of course.)
+ - The ics_dead field, of IC_Solved, records the subset of this
+ implication's ic_given that are redundant (not needed).
* We compute which evidence variables are needed by an implication
in setImplicationStatus. A variable is needed if
a) it is free in the RHS of a Wanted EvBind,
b) it is free in the RHS of an EvBind whose LHS is needed,
c) it is in the ics_need of a nested implication.
- d) it is listed in the tcs_used_tcvs field of the nested TcSEnv
* We need to be careful not to discard an implication
prematurely, even one that is fully solved, because we might
exponentially many) iterations!
Conclusion: we should call solveNestedImplications only if we did
-some unifiction in solveSimpleWanteds; because that's the only way
-we'll get more Givens (a unificaiton is like adding a Given) to
+some unification in solveSimpleWanteds; because that's the only way
+we'll get more Givens (a unification is like adding a Given) to
allow the implication to make progress.
-}
-promoteTyVar :: TcLevel -> TcTyVar -> TcM ()
+promoteTyVar :: TcTyVar -> TcM Bool
-- When we float a constraint out of an implication we must restore
--- invariant (MetaTvInv) in Note [TcLevel and untouchable type variables] in TcType
+-- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in TcType
+-- Return True <=> we did some promotion
-- See Note [Promoting unification variables]
-promoteTyVar tclvl tv
- | isFloatedTouchableMetaTyVar tclvl tv
- = do { cloned_tv <- TcM.cloneMetaTyVar tv
- ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
- ; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv) }
- | otherwise
- = return ()
-
-promoteTyVarTcS :: TcLevel -> TcTyVar -> TcS ()
+promoteTyVar tv
+ = do { tclvl <- TcM.getTcLevel
+ ; if (isFloatedTouchableMetaTyVar tclvl tv)
+ then do { cloned_tv <- TcM.cloneMetaTyVar tv
+ ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
+ ; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv)
+ ; return True }
+ else return False }
+
+-- Returns whether or not *any* tyvar is defaulted
+promoteTyVarSet :: TcTyVarSet -> TcM Bool
+promoteTyVarSet tvs
+ = or <$> mapM promoteTyVar (nonDetEltsUniqSet tvs)
+ -- non-determinism is OK because order of promotion doesn't matter
+
+promoteTyVarTcS :: TcTyVar -> TcS ()
-- When we float a constraint out of an implication we must restore
--- invariant (MetaTvInv) in Note [TcLevel and untouchable type variables] in TcType
+-- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in TcType
-- See Note [Promoting unification variables]
-- We don't just call promoteTyVar because we want to use unifyTyVar,
-- not writeMetaTyVar
-promoteTyVarTcS tclvl tv
- | isFloatedTouchableMetaTyVar tclvl tv
- = do { cloned_tv <- TcS.cloneMetaTyVar tv
- ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
- ; unifyTyVar tv (mkTyVarTy rhs_tv) }
- | otherwise
- = return ()
-
--- | If the tyvar is a RuntimeRep var, set it to PtrRepLifted. Returns whether or
--- not this happened.
-defaultTyVar :: TcTyVar -> TcM ()
--- Precondition: MetaTyVars only
--- See Note [DefaultTyVar]
-defaultTyVar the_tv
- | isRuntimeRepVar the_tv
- = do { traceTc "defaultTyVar RuntimeRep" (ppr the_tv)
- ; writeMetaTyVar the_tv ptrRepLiftedTy }
-
- | otherwise = return () -- The common case
+promoteTyVarTcS tv
+ = do { tclvl <- TcS.getTcLevel
+ ; when (isFloatedTouchableMetaTyVar tclvl tv) $
+ do { cloned_tv <- TcS.cloneMetaTyVar tv
+ ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
+ ; unifyTyVar tv (mkTyVarTy rhs_tv) } }
-- | Like 'defaultTyVar', but in the TcS monad.
defaultTyVarTcS :: TcTyVar -> TcS Bool
defaultTyVarTcS the_tv
| isRuntimeRepVar the_tv
+ , not (isSigTyVar the_tv) -- SigTvs should only be unified with a tyvar
+ -- never with a type; c.f. TcMType.defaultTyVar
+ -- See Note [Kind generalisation and SigTvs]
= do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv)
- ; unifyTyVar the_tv ptrRepLiftedTy
+ ; unifyTyVar the_tv liftedRepTy
; return True }
| otherwise
= return False -- the common case
-approximateWC :: WantedConstraints -> Cts
+approximateWC :: Bool -> WantedConstraints -> Cts
-- Postcondition: Wanted or Derived Cts
-- See Note [ApproximateWC]
-approximateWC wc
+approximateWC float_past_equalities wc
= float_wc emptyVarSet wc
where
float_wc :: TcTyCoVarSet -> WantedConstraints -> Cts
float_wc trapping_tvs (WC { wc_simple = simples, wc_impl = implics })
- = filterBag is_floatable simples `unionBags`
- do_bag (float_implic new_trapping_tvs) implics
+ = filterBag (is_floatable trapping_tvs) simples `unionBags`
+ do_bag (float_implic trapping_tvs) implics
where
- is_floatable ct = tyCoVarsOfCt ct `disjointVarSet` new_trapping_tvs
- new_trapping_tvs = transCloVarSet grow trapping_tvs
-
- grow :: VarSet -> VarSet -- Maps current trapped tyvars to newly-trapped ones
- grow so_far = foldrBag (grow_one so_far) emptyVarSet simples
- grow_one so_far ct tvs
- | ct_tvs `intersectsVarSet` so_far = tvs `unionVarSet` ct_tvs
- | otherwise = tvs
- where
- ct_tvs = tyCoVarsOfCt ct
float_implic :: TcTyCoVarSet -> Implication -> Cts
float_implic trapping_tvs imp
- | ic_no_eqs imp -- No equalities, so float
+ | float_past_equalities || ic_no_eqs imp
= float_wc new_trapping_tvs (ic_wanted imp)
- | otherwise -- Don't float out of equalities
- = emptyCts -- See Note [ApproximateWC]
+ | otherwise -- Take care with equalities
+ = emptyCts -- See (1) under Note [ApproximateWC]
where
new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp
+
do_bag :: (a -> Bag c) -> Bag a -> Bag c
do_bag f = foldrBag (unionBags.f) emptyBag
-{-
-Note [ApproximateWC]
-~~~~~~~~~~~~~~~~~~~~
+ is_floatable skol_tvs ct
+ | isGivenCt ct = False
+ | isHoleCt ct = False
+ | insolubleEqCt ct = False
+ | otherwise = tyCoVarsOfCt ct `disjointVarSet` skol_tvs
+
+{- Note [ApproximateWC]
+~~~~~~~~~~~~~~~~~~~~~~~
approximateWC takes a constraint, typically arising from the RHS of a
let-binding whose type we are *inferring*, and extracts from it some
*simple* constraints that we might plausibly abstract over. Of course
The same function is used when doing type-class defaulting (see the call
to applyDefaultingRules) to extract constraints that that might be defaulted.
-There are two caveats:
+There is one caveat:
-1. We do *not* float anything out if the implication binds equality
- constraints, because that defeats the OutsideIn story. Consider
+1. When infering most-general types (in simplifyInfer), we do *not*
+ float anything out if the implication binds equality constraints,
+ because that defeats the OutsideIn story. Consider
data T a where
TInt :: T Int
MkT :: T a
float out of such implications, which meant it would happily infer
non-principal types.)
-2. We do not float out an inner constraint that shares a type variable
- (transitively) with one that is trapped by a skolem. Eg
- forall a. F a ~ beta, Integral beta
- We don't want to float out (Integral beta). Doing so would be bad
- when defaulting, because then we'll default beta:=Integer, and that
- makes the error message much worse; we'd get
- Can't solve F a ~ Integer
- rather than
- Can't solve Integral (F a)
-
- Moreover, floating out these "contaminated" constraints doesn't help
- when generalising either. If we generalise over (Integral b), we still
- can't solve the retained implication (forall a. F a ~ b). Indeed,
- arguably that too would be a harder error to understand.
+ HOWEVER (Trac #12797) in findDefaultableGroups we are not worried about
+ the most-general type; and we /do/ want to float out of equalities.
+ Hence the boolean flag to approximateWC.
+
+------ Historical note -----------
+There used to be a second caveat, driven by Trac #8155
+
+ 2. We do not float out an inner constraint that shares a type variable
+ (transitively) with one that is trapped by a skolem. Eg
+ forall a. F a ~ beta, Integral beta
+ We don't want to float out (Integral beta). Doing so would be bad
+ when defaulting, because then we'll default beta:=Integer, and that
+ makes the error message much worse; we'd get
+ Can't solve F a ~ Integer
+ rather than
+ Can't solve Integral (F a)
+
+ Moreover, floating out these "contaminated" constraints doesn't help
+ when generalising either. If we generalise over (Integral b), we still
+ can't solve the retained implication (forall a. F a ~ b). Indeed,
+ arguably that too would be a harder error to understand.
+
+But this transitive closure stuff gives rise to a complex rule for
+when defaulting actually happens, and one that was never documented.
+Moreover (Trac #12923), the more complex rule is sometimes NOT what
+you want. So I simply removed the extra code to implement the
+contamination stuff. There was zero effect on the testsuite (not even
+#8155).
+------ End of historical note -----------
+
Note [DefaultTyVar]
~~~~~~~~~~~~~~~~~~~
defaultTyVar is used on any un-instantiated meta type variables to
-default any RuntimeRep variables to PtrRepLifted. This is important
+default any RuntimeRep variables to LiftedRep. This is important
to ensure that instance declarations match. For example consider
instance Show (a->b)
whatever, because the type-class defaulting rules have yet to run.
An alternate implementation would be to emit a derived constraint setting
-the RuntimeRep variable to PtrRepLifted, but this seems unnecessarily indirect.
+the RuntimeRep variable to LiftedRep, but this seems unnecessarily indirect.
Note [Promote _and_ default when inferring]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
approximateWC to produce a list of candidate constraints. Then we MUST
a) Promote any meta-tyvars that have been floated out by
- approximateWC, to restore invariant (MetaTvInv) described in
+ approximateWC, to restore invariant (WantedInv) described in
Note [TcLevel and untouchable type variables] in TcType.
b) Default the kind of any meta-tyvars that are not mentioned in
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we float an equality out of an implication we must "promote" free
unification variables of the equality, in order to maintain Invariant
-(MetaTvInv) from Note [TcLevel and untouchable type variables] in TcType. for the
-leftover implication.
+(WantedInv) from Note [TcLevel and untouchable type variables] in
+TcType. for the leftover implication.
This is absolutely necessary. Consider the following example. We start
with two implications and a class with a functional dependency.
in (g1 '3', g2 undefined)
-Note [Solving Family Equations]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-After we are done with simplification we may be left with constraints of the form:
- [Wanted] F xis ~ beta
-If 'beta' is a touchable unification variable not already bound in the TyBinds
-then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
-
-When is it ok to do so?
- 1) 'beta' must not already be defaulted to something. Example:
-
- [Wanted] F Int ~ beta <~ Will default [beta := F Int]
- [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
- have to report this as unsolved.
-
- 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
- set [beta := F xis] only if beta is not among the free variables of xis.
-
- 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
- of type family equations. See Inert Set invariants in TcInteract.
-
-This solving is now happening during zonking, see Note [Unflattening while zonking]
-in TcMType.
-
*********************************************************************************
* *
they carry evidence).
-}
-floatEqualities :: [TcTyVar] -> Bool
+floatEqualities :: [TcTyVar] -> [EvId] -> EvBindsVar -> Bool
-> WantedConstraints
-> TcS (Cts, WantedConstraints)
-- Main idea: see Note [Float Equalities out of Implications]
--
-- Subtleties: Note [Float equalities from under a skolem binding]
-- Note [Skolem escape]
-floatEqualities skols no_given_eqs
+-- Note [What prevents a constraint from floating]
+floatEqualities skols given_ids ev_binds_var no_given_eqs
wanteds@(WC { wc_simple = simples })
| not no_given_eqs -- There are some given equalities, so don't float
= return (emptyBag, wanteds) -- Note [Float Equalities out of Implications]
+
| otherwise
- = do { outer_tclvl <- TcS.getTcLevel
- ; mapM_ (promoteTyVarTcS outer_tclvl)
- (tyCoVarsOfCtsList float_eqs)
- -- See Note [Promoting unification variables]
+ = do { -- First zonk: the inert set (from whence they came) is fully
+ -- zonked, but unflattening may have filled in unification
+ -- variables, and we /must/ see them. Otherwise we may float
+ -- constraints that mention the skolems!
+ simples <- TcS.zonkSimples simples
+ ; binds <- TcS.getTcEvBindsMap ev_binds_var
+
+ -- Now we can pick the ones to float
+ -- The constraints are un-flattened and de-canonicalised
+ ; let seed_skols = mkVarSet skols `unionVarSet`
+ mkVarSet given_ids `unionVarSet`
+ foldEvBindMap add_one emptyVarSet binds
+ add_one bind acc = extendVarSet acc (evBindVar bind)
+ -- seed_skols: See Note [What prevents a constraint from floating] (1,2,3)
+
+ (eqs, non_eqs) = partitionBag is_eq_ct simples
+ extended_skols = transCloVarSet (extra_skols eqs) seed_skols
+ (flt_eqs, no_flt_eqs) = partitionBag (is_floatable extended_skols) eqs
+ remaining_simples = non_eqs `andCts` no_flt_eqs
+ -- extended_skols: See Note [What prevents a constraint from floating] (3)
+
+ -- Promote any unification variables mentioned in the floated equalities
+ -- See Note [Promoting unification variables]
+ ; mapM_ promoteTyVarTcS (tyCoVarsOfCtsList flt_eqs)
; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols
+ , text "Extended skols =" <+> ppr extended_skols
, text "Simples =" <+> ppr simples
- , text "Floated eqs =" <+> ppr float_eqs])
- ; return ( float_eqs
- , wanteds { wc_simple = remaining_simples } ) }
- where
- skol_set = mkVarSet skols
- (float_eqs, remaining_simples) = partitionBag (usefulToFloat skol_set) simples
+ , text "Eqs =" <+> ppr eqs
+ , text "Floated eqs =" <+> ppr flt_eqs])
+ ; return ( flt_eqs, wanteds { wc_simple = remaining_simples } ) }
-usefulToFloat :: VarSet -> Ct -> Bool
-usefulToFloat skol_set ct -- The constraint is un-flattened and de-canonicalised
- = is_meta_var_eq pred &&
- (tyCoVarsOfType pred `disjointVarSet` skol_set)
where
- pred = ctPred ct
+ is_floatable :: VarSet -> Ct -> Bool
+ is_floatable skols ct
+ | isDerivedCt ct = not (tyCoVarsOfCt ct `intersectsVarSet` skols)
+ | otherwise = not (ctEvId ct `elemVarSet` skols)
+
+ is_eq_ct ct | CTyEqCan {} <- ct = True
+ | is_homo_eq (ctPred ct) = True
+ | otherwise = False
+
+ extra_skols :: Cts -> VarSet -> VarSet
+ extra_skols eqs skols = foldrBag extra_skol emptyVarSet eqs
+ where
+ extra_skol ct acc
+ | isDerivedCt ct = acc
+ | tyCoVarsOfCt ct `intersectsVarSet` skols = extendVarSet acc (ctEvId ct)
+ | otherwise = acc
-- Float out alpha ~ ty, or ty ~ alpha
-- which might be unified outside
-- See Note [Which equalities to float]
- is_meta_var_eq pred
+ is_homo_eq pred
| EqPred NomEq ty1 ty2 <- classifyPredType pred
+ , typeKind ty1 `tcEqType` typeKind ty2
= case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of
(Just tv1, _) -> float_tv_eq tv1 ty2
(_, Just tv2) -> float_tv_eq tv2 ty1
= isMetaTyVar tv1
&& (not (isSigTyVar tv1) || isTyVarTy ty2)
+
{- Note [Float equalities from under a skolem binding]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Which of the simple equalities can we float out? Obviously, only
is a decent chance that floating outwards will allow unification to
happen. In particular:
- Float out equalities of form (alpha ~ ty) or (ty ~ alpha), where
+ Float out homogeneous equalities of form (alpha ~ ty) or (ty ~ alpha), where
* alpha is a meta-tyvar.
case, floating out won't help either, and it may affect grouping
of error messages.
+Why homogeneous (i.e., the kinds of the types are the same)? Because heterogeneous
+equalities have derived kind equalities. See Note [Equalities with incompatible kinds]
+in TcCanonical. If we float out a hetero equality, then it will spit out the
+same derived kind equality again, which might create duplicate error messages.
+Instead, we do float out the kind equality (if it's worth floating out, as
+above). If/when we solve it, we'll be able to rewrite the original hetero equality
+to be homogeneous, and then perhaps make progress / float it out. The duplicate
+error message was spotted in typecheck/should_fail/T7368.
+
Note [Skolem escape]
~~~~~~~~~~~~~~~~~~~~
You might worry about skolem escape with all this floating.
But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2]
to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be.
+Note [What prevents a constraint from floating]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+What /prevents/ a constraint from floating? If it mentions one of the
+"bound variables of the implication". What are they?
+
+The "bound variables of the implication" are
+
+ 1. The skolem type variables `ic_skols`
+
+ 2. The "given" evidence variables `ic_given`. Example:
+ forall a. (co :: t1 ~# t2) => [W] co : (a ~# b |> co)
+
+ 3. The binders of all evidence bindings in `ic_binds`. Example
+ forall a. (d :: t1 ~ t2)
+ EvBinds { (co :: t1 ~# t2) = superclass-sel d }
+ => [W] co2 : (a ~# b |> co)
+ Here `co` is gotten by superclass selection from `d`, and the
+ wanted constraint co2 must not float.
+
+ 4. And the evidence variable of any equality constraint (incl
+ Wanted ones) whose type mentions a bound variable. Example:
+ forall k. [W] co1 :: t1 ~# t2 |> co2
+ [W] co2 :: k ~# *
+ Here, since `k` is bound, so is `co2` and hence so is `co1`.
+
+Here (1,2,3) are handled by the "seed_skols" calculation, and
+(4) is done by the transCloVarSet call.
+
+The possible dependence on givens, and evidence bindings, is more
+subtle than we'd realised at first. See Trac #14584.
+
*********************************************************************************
* *
-* Defaulting and disamgiguation *
+* Defaulting and disambiguation *
* *
*********************************************************************************
-}
applyDefaultingRules :: WantedConstraints -> TcS Bool
-- True <=> I did some defaulting, by unifying a meta-tyvar
--- Imput WantedConstraints are not necessarily zonked
+-- Input WantedConstraints are not necessarily zonked
applyDefaultingRules wanteds
| isEmptyWC wanteds
= []
| otherwise
= [ (tv, map fstOf3 group)
- | group@((_,_,tv):_) <- unary_groups
+ | group'@((_,_,tv) :| _) <- unary_groups
+ , let group = toList group'
, defaultable_tyvar tv
, defaultable_classes (map sndOf3 group) ]
where
- simples = approximateWC wanteds
+ simples = approximateWC True wanteds
(unaries, non_unaries) = partitionWith find_unary (bagToList simples)
unary_groups = equivClasses cmp_tv unaries
- unary_groups :: [[(Ct, Class, TcTyVar)]] -- (C tv) constraints
- unaries :: [(Ct, Class, TcTyVar)] -- (C tv) constraints
- non_unaries :: [Ct] -- and *other* constraints
+ 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:*)) (Trac #8931)
+ find_unary :: Ct -> Either (Ct, Class, TyVar) Ct
find_unary cc
| Just (cls,tys) <- getClassPredTys_maybe (ctPred cc)
, [ty] <- filterOutInvisibleTypes (classTyCon cls) tys
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` bad_tvs)
- in b1 && b2
+ in b1 && (b2 || extended_defaults) -- Note [Multi-parameter defaults]
+ defaultable_classes :: [Class] -> Bool
defaultable_classes clss
| extended_defaults = any (isInteractiveClass ovl_strings) clss
| otherwise = all is_std_class clss && (any (isNumClass ovl_strings) clss)
= do { traceTcS "disambigGroup {" (vcat [ ppr default_ty, ppr the_tv, ppr wanteds ])
; fake_ev_binds_var <- TcS.newTcEvBinds
; tclvl <- TcS.getTcLevel
- ; (success, _) <- nestImplicTcS (Just fake_ev_binds_var) emptyVarSet
- (pushTcLevel tclvl) try_group
+ ; success <- nestImplicTcS fake_ev_binds_var (pushTcLevel tclvl) try_group
; if success then
-- Success: record the type variable binding, and return
try_group
| Just subst <- mb_subst
= do { lcl_env <- TcS.getLclEnv
- ; let loc = CtLoc { ctl_origin = GivenOrigin UnkSkol
- , ctl_env = lcl_env
- , ctl_t_or_k = Nothing
- , ctl_depth = initialSubGoalDepth }
+ ; tc_lvl <- TcS.getTcLevel
+ ; let loc = mkGivenLoc tc_lvl UnkSkol lcl_env
; wanted_evs <- mapM (newWantedEvVarNC loc . substTy subst . ctPred)
wanteds
; fmap isEmptyWC $
= return False
the_ty = mkTyVarTy the_tv
- mb_subst = tcMatchTy the_ty default_ty
- -- Make sure the kinds match too; hence this call to tcMatchTy
+ mb_subst = tcMatchTyKi the_ty default_ty
+ -- 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.
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).
-}
git.haskell.org / ghc.git / blobdiff