diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/typecheck/TcCanonical.hs | 2 | ||||
| -rw-r--r-- | compiler/typecheck/TcErrors.hs | 34 | ||||
| -rw-r--r-- | compiler/typecheck/TcFlatten.hs | 78 | ||||
| -rw-r--r-- | compiler/typecheck/TcHsSyn.hs | 1 | ||||
| -rw-r--r-- | compiler/typecheck/TcInteract.hs | 13 | ||||
| -rw-r--r-- | compiler/typecheck/TcMType.hs | 18 | ||||
| -rw-r--r-- | compiler/typecheck/TcRnTypes.hs | 4 | ||||
| -rw-r--r-- | compiler/typecheck/TcSMonad.hs | 138 | ||||
| -rw-r--r-- | compiler/typecheck/TcSimplify.hs | 23 | ||||
| -rw-r--r-- | compiler/typecheck/TcType.hs | 40 | ||||
| -rw-r--r-- | compiler/typecheck/TcUnify.hs | 1 |
11 files changed, 221 insertions, 131 deletions
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index 5dddd5da0c..77bf63d98e 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -1538,7 +1538,7 @@ Suppose we have [G] Num (F [a]) then we flatten to [G] Num fsk [G] F [a] ~ fsk -where fsk is a flatten-skolem (FlatSkol). Suppose we have +where fsk is a flatten-skolem (FlatSkolTv). Suppose we have type instance F [a] = a then we'll reduce the second constraint to [G] a ~ fsk diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index eacdbb682f..c9e07fc43d 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -1466,7 +1466,7 @@ mkEqErr1 ctxt ct -- Wanted or derived; NomEq -> empty ReprEq -> mkCoercibleExplanation rdr_env fam_envs ty1 ty2 ; dflags <- getDynFlags - ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct)) + ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct) $$ ppr keep_going) ; let report = mconcat [important wanted_msg, important coercible_msg, relevant_bindings binds_msg] ; if keep_going @@ -1604,15 +1604,21 @@ reportEqErr ctxt report ct oriented ty1 ty2 where misMatch = important $ misMatchOrCND ctxt ct oriented ty1 ty2 eqInfo = important $ mkEqInfoMsg ct ty1 ty2 -mkTyVarEqErr :: DynFlags -> ReportErrCtxt -> Report -> Ct +mkTyVarEqErr, mkTyVarEqErr' + :: DynFlags -> ReportErrCtxt -> Report -> Ct -> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg -- tv1 and ty2 are already tidied mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2 - | isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar, or else the thing would + = do { traceTc "mkTyVarEqErr" (ppr ct $$ ppr tv1 $$ ppr ty2) + ; mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 } + +mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 + | not insoluble_occurs_check -- See Note [Occurs check wins] + , isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar, or else the thing would -- be oriented the other way round; -- see TcCanonical.canEqTyVarTyVar - || isSigTyVar tv1 && not (isTyVarTy ty2) - || ctEqRel ct == ReprEq && not insoluble_occurs_check + || isSigTyVar tv1 && not (isTyVarTy ty2) + || ctEqRel ct == ReprEq -- the cases below don't really apply to ReprEq (except occurs check) = mkErrorMsgFromCt ctxt ct $ mconcat [ important $ misMatchOrCND ctxt ct oriented ty1 ty2 @@ -1827,7 +1833,6 @@ extraTyVarInfo ctxt tv = ASSERT2( isTyVar tv, ppr tv ) case tcTyVarDetails tv of SkolemTv {} -> pprSkol implics tv - FlatSkol {} -> pp_tv <+> text "is a flattening type variable" RuntimeUnk {} -> pp_tv <+> text "is an interactive-debugger skolem" MetaTv {} -> empty where @@ -2016,7 +2021,22 @@ mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act mkExpectedActualMsg _ _ _ _ _ = panic "mkExpectedAcutalMsg" -{- +{- Note [Insoluble occurs check wins] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider [G] a ~ [a], [W] a ~ [a] (Trac #13674). The Given is insoluble +so we don't use it for rewriting. The Wanted is also insoluble, and +we don't solve it from the Given. It's very confusing to say + Cannot solve a ~ [a] from given constraints a ~ [a] + +And indeed even thinking about the Givens is silly; [W] a ~ [a] is +just as insoluble as Int ~ Bool. + +Conclusion: if there's an insoluble occurs check (isInsolubleOccursCheck) +then report it first. + +(NB: there are potentially-soluble ones, like (a ~ F a b), and we don't +wnat to be as draconian with them.) + Note [Expanding type synonyms to make types similar] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs index dc211c61e4..650cbd8219 100644 --- a/compiler/typecheck/TcFlatten.hs +++ b/compiler/typecheck/TcFlatten.hs @@ -4,7 +4,7 @@ module TcFlatten( FlattenMode(..), flatten, flattenManyNom, - unflatten, + unflattenWanteds ) where #include "HsVersions.h" @@ -36,31 +36,50 @@ import Control.Arrow ( first ) Note [The flattening story] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * A CFunEqCan is either of form - [G] <F xis> : F xis ~ fsk -- fsk is a FlatSkol - [W] x : F xis ~ fmv -- fmv is a unification variable, - -- but untouchable, - -- with MetaInfo = FlatMetaTv + [G] <F xis> : F xis ~ fsk -- fsk is a FlatSkolTv + [W] x : F xis ~ fmv -- fmv is a FlatMetaTv where x is the witness variable - fsk/fmv is a flatten skolem xis are function-free - CFunEqCans are always [Wanted], or [Given], never [Derived] + fsk/fmv is a flatten skolem; + it is always untouchable (level 0) - fmv untouchable just means that in a CTyVarEq, say, - fmv ~ Int - we do NOT unify fmv. +* CFunEqCans can have any flavour: [G], [W], [WD] or [D] * KEY INSIGHTS: - A given flatten-skolem, fsk, is known a-priori to be equal to - F xis (the LHS), with <F xis> evidence + F xis (the LHS), with <F xis> evidence. The fsk is still a + unification variable, but it is "owned" by its CFunEqCan, and + is filled in (unflattened) only by unflattenGivens. - A unification flatten-skolem, fmv, stands for the as-yet-unknown - type to which (F xis) will eventually reduce + type to which (F xis) will eventually reduce. It is filled in + only by dischargeFmv. -* Inert set invariant: if F xis1 ~ fsk1, F xis2 ~ fsk2 - then xis1 /= xis2 - i.e. at most one CFunEqCan with a particular LHS + - All fsk/fmv variables are "untouchable". To make it simple to test, + we simply give them TcLevel=0. This means that in a CTyVarEq, say, + fmv ~ Int + we NEVER unify fmv. + + - A unification flatten-skolems, fmv, ONLY gets unified when either + a) The CFunEqCan takes a step, using an axiom + b) By unflattenWanteds + They are never unified in any other form of equality. + For example [W] ffmv ~ Int is stuck; it does not unify with fmv. + +* We *never* substitute in the RHS (i.e. the fsk/fmv) of a CFunEqCan. + That would destroy the invariant about the shape of a CFunEqCan, + and it would risk wanted/wanted interactions. The only way we + learn information about fsk is when the CFunEqCan takes a step. + + However we *do* substitute in the LHS of a CFunEqCan (else it + would never get to fire!) + +* Unflattening: + - We unflatten Givens when leaving their scope (see unflattenGivens) + - We unflatten Wanteds at the end of each attempt to simplify the + wanteds; see unflattenWanteds, called from solveSimpleWanteds. * Each canonical [G], [W], or [WD] CFunEqCan x : F xis ~ fsk/fmv has its own distinct evidence variable x and flatten-skolem fsk/fmv. @@ -70,7 +89,11 @@ Note [The flattening story] In contrast a [D] CFunEqCan shares its fmv with its partner [W], but does not "own" it. If we reduce a [D] F Int ~ fmv, where say type instance F Int = ty, then we don't discharge fmv := ty. - Rather we simply generate [D] fmv ~ ty + Rather we simply generate [D] fmv ~ ty (in TcInteract.reduce_top_fun_eq) + +* Inert set invariant: if F xis1 ~ fsk1, F xis2 ~ fsk2 + then xis1 /= xis2 + i.e. at most one CFunEqCan with a particular LHS * Function applications can occur in the RHS of a CTyEqCan. No reason not allow this, and it reduces the amount of flattening that must occur. @@ -104,20 +127,6 @@ Note [The flattening story] - Add new wanted to flat cache - Discharge x = F cos ; x2 -* Unification flatten-skolems, fmv, ONLY get unified when either - a) The CFunEqCan takes a step, using an axiom - b) During un-flattening - They are never unified in any other form of equality. - For example [W] ffmv ~ Int is stuck; it does not unify with fmv. - -* We *never* substitute in the RHS (i.e. the fsk/fmv) of a CFunEqCan. - That would destroy the invariant about the shape of a CFunEqCan, - and it would risk wanted/wanted interactions. The only way we - learn information about fsk is when the CFunEqCan takes a step. - - However we *do* substitute in the LHS of a CFunEqCan (else it - would never get to fire!) - * [Interacting rule] (inert) [W] x1 : F tys ~ fmv1 (work item) [W] x2 : F tys ~ fmv2 @@ -1476,8 +1485,8 @@ flattens to We must solve both! -} -unflatten :: Cts -> Cts -> TcS Cts -unflatten tv_eqs funeqs +unflattenWanteds :: Cts -> Cts -> TcS Cts +unflattenWanteds tv_eqs funeqs = do { tclvl <- getTcLevel ; traceTcS "Unflattening" $ braces $ @@ -1506,10 +1515,7 @@ unflatten tv_eqs funeqs ; let all_flat = tv_eqs `andCts` funeqs ; traceTcS "Unflattening done" $ braces (pprCts all_flat) - -- Step 5: zonk the result - -- Motivation: makes them nice and ready for the next step - -- (see TcInteract.solveSimpleWanteds) - ; zonkSimples all_flat } + ; return all_flat } where ---------------- unflatten_funeq :: Ct -> Cts -> TcS Cts diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs index 1b9fed98b6..b75d59be67 100644 --- a/compiler/typecheck/TcHsSyn.hs +++ b/compiler/typecheck/TcHsSyn.hs @@ -1557,7 +1557,6 @@ zonkTyVarOcc env@(ZonkEnv zonk_unbound_tyvar tv_env _) tv = case tcTyVarDetails tv of SkolemTv {} -> lookup_in_env RuntimeUnk {} -> lookup_in_env - FlatSkol ty -> zonkTcTypeToType env ty MetaTv { mtv_ref = ref } -> do { cts <- readMutVar ref ; case cts of diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 4368fcbb1b..83dc10cae4 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -160,6 +160,7 @@ solveSimpleGivens givens solveSimpleWanteds :: Cts -> TcS WantedConstraints -- NB: 'simples' may contain /derived/ equalities, floated -- out from a nested implication. So don't discard deriveds! +-- The result is not necessarily zonked solveSimpleWanteds simples = do { traceTcS "solveSimpleWanteds {" (ppr simples) ; dflags <- getDynFlags @@ -199,12 +200,13 @@ solveSimpleWanteds simples solve_simple_wanteds :: WantedConstraints -> TcS (Int, WantedConstraints) -- Try solving these constraints -- Affects the unification state (of course) but not the inert set +-- The result is not necessarily zonked solve_simple_wanteds (WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 }) = nestTcS $ do { solveSimples simples1 ; (implics2, tv_eqs, fun_eqs, insols2, others) <- getUnsolvedInerts ; (unif_count, unflattened_eqs) <- reportUnifications $ - unflatten tv_eqs fun_eqs + unflattenWanteds tv_eqs fun_eqs -- See Note [Unflatten after solving the simple wanteds] ; return ( unif_count , WC { wc_simple = others `andCts` unflattened_eqs @@ -2241,6 +2243,13 @@ Other notes: - natural numbers - Typeable +* Flatten-skolems: we do not treat a flatten-skolem as unifiable + for this purpose. + E.g. f :: Eq (F a) => [a] -> [a] + f xs = ....(xs==xs)..... + Here we get [W] Eq [a], and we don't want to refrain from solving + it because of the given (Eq (F a)) constraint! + * The given-overlap problem is arguably not easy to appear in practice due to our aggressive prioritization of equality solving over other constraints, but it is possible. I've added a test case in @@ -2274,7 +2283,7 @@ Other notes: in point. All of this is disgustingly delicate, so to discourage people from writing -simplifiable class givens, we warn about signatures that contain them;# +simplifiable class givens, we warn about signatures that contain them; see TcValidity Note [Simplifiable given constraints]. -} diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index 1ae90661a8..d26b25758e 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -550,8 +550,13 @@ instSkolTyCoVarX mk_tcv subst tycovar newFskTyVar :: TcType -> TcM TcTyVar newFskTyVar fam_ty = do { uniq <- newUnique - ; let name = mkSysTvName uniq (fsLit "fsk") - ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) } + ; ref <- newMutVar Flexi + ; let details = MetaTv { mtv_info = FlatSkolTv + , mtv_ref = ref + , mtv_tclvl = fmvTcLevel } + name = mkMetaTyVarName uniq (fsLit "fsk") + ; return (mkTcTyVar name (typeKind fam_ty) details) } + {- Note [Kind substitution when instantiating] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -593,10 +598,9 @@ newFmvTyVar :: TcType -> TcM TcTyVar newFmvTyVar fam_ty = do { uniq <- newUnique ; ref <- newMutVar Flexi - ; cur_lvl <- getTcLevel ; let details = MetaTv { mtv_info = FlatMetaTv , mtv_ref = ref - , mtv_tclvl = fmvTcLevel cur_lvl } + , mtv_tclvl = fmvTcLevel } name = mkMetaTyVarName uniq (fsLit "s") ; return (mkTcTyVar name (typeKind fam_ty) details) } @@ -707,7 +711,7 @@ writeMetaTyVarRef tyvar ref ty tv_lvl = tcTyVarLevel tyvar ty_lvl = tcTypeLevel ty - level_check_ok = isFmvTyVar tyvar + level_check_ok = isFlattenTyVar tyvar || not (ty_lvl `strictlyDeeperThan` tv_lvl) level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty @@ -768,6 +772,7 @@ newAnonMetaTyVar meta_info kind s = case meta_info of TauTv -> fsLit "t" FlatMetaTv -> fsLit "fmv" + FlatSkolTv -> fsLit "fsk" SigTv -> fsLit "a" ; details <- newMetaDetails meta_info ; return (mkTcTyVar name kind details) } @@ -998,7 +1003,7 @@ zonkQuantifiedTyVar tv MetaTv {} -> skolemiseUnboundMetaTyVar tv - _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk + _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- RuntimeUnk defaultTyVar :: Bool -- True <=> please default this kind variable to * -> TcTyVar -- If it's a MetaTyVar then it is unbound @@ -1490,7 +1495,6 @@ zonkTcTyVar tv = case tcTyVarDetails tv of SkolemTv {} -> zonk_kind_and_return RuntimeUnk {} -> zonk_kind_and_return - FlatSkol ty -> zonkTcType ty MetaTv { mtv_ref = ref } -> do { cts <- readMutVar ref ; case cts of diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index e5e9eb2245..e018d5d7b6 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -1589,8 +1589,8 @@ data Ct -- *never* over-saturated (because if so -- we should have decomposed) - cc_fsk :: TcTyVar -- [Given] always a FlatSkol skolem - -- [Wanted] always a FlatMetaTv unification variable + cc_fsk :: TcTyVar -- [Given] always a FlatSkolTv + -- [Wanted] always a FlatMetaTv -- See Note [The flattening story] in TcFlatten } diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index f7153f8d2a..434553dec1 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -52,7 +52,7 @@ module TcSMonad ( getNoGivenEqs, setInertCans, getInertEqs, getInertCans, getInertGivens, getInertInsols, - emptyInert, getTcSInerts, setTcSInerts, + getTcSInerts, setTcSInerts, matchableGivens, prohibitedSuperClassSolve, getUnsolvedInerts, removeInertCts, getPendingScDicts, @@ -383,6 +383,16 @@ data InertSet -- Canonical Given, Wanted, Derived -- Sometimes called "the inert set" + , inert_fsks :: [(TcTyVar, TcType)] + -- A list of (fsk, ty) pairs; we add one element when we flatten + -- a function application in a Given constraint, creating + -- a new fsk in newFlattenSkolem. When leaving a nested scope, + -- unflattenGivens unifies fsk := ty + -- + -- We could also get this info from inert_funeqs, filtered by + -- level, but it seems simpler and more direct to capture the + -- fsk as we generate them. + , inert_flat_cache :: ExactFunEqMap (TcCoercion, TcType, CtFlavour) -- See Note [Type family equations] -- If F tys :-> (co, rhs, flav), @@ -421,6 +431,7 @@ emptyInert , inert_irreds = emptyCts , inert_insols = emptyCts } , inert_flat_cache = emptyExactFunEqs + , inert_fsks = [] , inert_solved_dicts = emptyDictMap } @@ -1814,24 +1825,21 @@ getNoGivenEqs :: TcLevel -- TcLevel of this implication -- See Note [When does an implication have given equalities?] getNoGivenEqs tclvl skol_tvs = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds - , inert_funeqs = funeqs , inert_insols = insols }) <- getInertCans - ; let local_fsks = foldFunEqs add_fsk funeqs emptyVarSet - - has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False + ; let has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False (iirreds `unionBags` insols) - || anyDVarEnv (eqs_given_here local_fsks) ieqs + || anyDVarEnv eqs_given_here ieqs ; traceTcS "getNoGivenEqs" (vcat [ ppr has_given_eqs, ppr inerts , ppr insols]) ; return (not has_given_eqs, insols) } where - eqs_given_here :: VarSet -> EqualCtList -> Bool - eqs_given_here local_fsks [CTyEqCan { cc_tyvar = tv, cc_ev = ev }] + eqs_given_here :: EqualCtList -> Bool + eqs_given_here [CTyEqCan { cc_tyvar = tv, cc_ev = ev }] -- Givens are always a sigleton - = not (skolem_bound_here local_fsks tv) && ev_given_here ev - eqs_given_here _ _ = False + = not (skolem_bound_here tv) && ev_given_here ev + eqs_given_here _ = False ev_given_here :: CtEvidence -> Bool -- True for a Given bound by the curent implication, @@ -1840,16 +1848,10 @@ getNoGivenEqs tclvl skol_tvs = isGiven ev && tclvl == ctLocLevel (ctEvLoc ev) - add_fsk :: Ct -> VarSet -> VarSet - add_fsk ct fsks | CFunEqCan { cc_fsk = tv, cc_ev = ev } <- ct - , isGiven ev = extendVarSet fsks tv - | otherwise = fsks - skol_tv_set = mkVarSet skol_tvs - skolem_bound_here local_fsks tv -- See Note [Let-bound skolems] + skolem_bound_here tv -- See Note [Let-bound skolems] = case tcTyVarDetails tv of SkolemTv {} -> tv `elemVarSet` skol_tv_set - FlatSkol {} -> not (tv `elemVarSet` local_fsks) _ -> False -- | Returns Given constraints that might, @@ -1889,9 +1891,11 @@ matchableGivens loc_w pred (IS { inert_cans = inert_cans }) -- bindable when unifying with givens. That ensures that we -- conservatively assume that a meta tyvar might get unified with -- something that matches the 'given', until demonstrated - -- otherwise. - bind_meta_tv tv | isMetaTyVar tv = BindMe - | otherwise = Skolem + -- otherwise. More info in Note [Instance and Given overlap] + -- in TcInteract + bind_meta_tv tv | isMetaTyVar tv + , not (isFskTyVar tv) = BindMe + | otherwise = Skolem prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool -- See Note [Solving superclass constraints] in TcInstDcls @@ -2413,6 +2417,8 @@ runTcSWithEvBinds ev_binds_var tcs ; when (count > 0) $ csTraceTcM $ return (text "Constraint solver steps =" <+> int count) + ; unflattenGivens inert_var + #if defined(DEBUG) ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var ; checkForCyclicBinds ev_binds @@ -2420,6 +2426,7 @@ runTcSWithEvBinds ev_binds_var tcs ; return res } +---------------------------- #if defined(DEBUG) checkForCyclicBinds :: EvBindMap -> TcM () checkForCyclicBinds ev_binds_map @@ -2447,6 +2454,7 @@ checkForCyclicBinds ev_binds_map -- Note [Deterministic SCC] in Digraph. #endif +---------------------------- setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a setEvBindsTcS ref (TcS thing_inside) = TcS $ \ env -> thing_inside (env { tcs_ev_binds = ref }) @@ -2460,8 +2468,9 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside) , tcs_count = count } -> do { inerts <- TcM.readTcRef old_inert_var - ; let nest_inert = inerts { inert_flat_cache = emptyExactFunEqs } - -- See Note [Do not inherit the flat cache] + ; let nest_inert = emptyInert { inert_cans = inert_cans inerts + , inert_solved_dicts = inert_solved_dicts inerts } + -- See Note [Do not inherit the flat cache] ; new_inert_var <- TcM.newTcRef nest_inert ; new_wl_var <- TcM.newTcRef emptyWorkList ; let nest_env = TcSEnv { tcs_ev_binds = ref @@ -2472,6 +2481,8 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside) ; res <- TcM.setTcLevel inner_tclvl $ thing_inside nest_env + ; unflattenGivens new_inert_var + #if defined(DEBUG) -- Perform a check that the thing_inside did not cause cycles ; ev_binds <- TcM.getTcEvBindsMap ref @@ -2627,15 +2638,6 @@ unifyTyVar tv ty ; TcM.writeMetaTyVar tv ty ; TcM.updTcRef (tcs_unified env) (+1) } -unflattenFmv :: TcTyVar -> TcType -> TcS () --- Fill a flatten-meta-var, simply by unifying it. --- This does NOT count as a unification in tcs_unified. -unflattenFmv tv ty - = ASSERT2( isMetaTyVar tv, ppr tv ) - TcS $ \ _ -> - do { TcM.traceTc "unflattenFmv" (ppr tv <+> text ":=" <+> ppr ty) - ; TcM.writeMetaTyVar tv ty } - reportUnifications :: TcS a -> TcS (Int, a) reportUnifications (TcS thing_inside) = TcS $ \ env -> @@ -2790,8 +2792,12 @@ which will result in two Deriveds to end up in the insoluble set: wc_insols = (c ~ [c]) [D], (c ~ [c]) [D] -} --- Flatten skolems --- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- ********************************************************************* +* * +* Flatten skolems * +* * +********************************************************************* -} + newFlattenSkolem :: CtFlavour -> CtLoc -> TyCon -> [TcType] -- F xis -> TcS (CtEvidence, Coercion, TcTyVar) -- [G/WD] x:: F xis ~ fsk @@ -2806,9 +2812,14 @@ newFlattenSkolem flav loc tc xis new_skolem | Given <- flav = do { fsk <- wrapTcS (TcM.newFskTyVar fam_ty) - ; let co = mkNomReflCo fam_ty - ; ev <- newGivenEvVar loc (mkPrimEqPred fam_ty (mkTyVarTy fsk), - EvCoercion co) + + -- Extend the inert_fsks list, for use by unflattenGivens + ; updInertTcS $ \is -> is { inert_fsks = (fsk, fam_ty) : inert_fsks is } + + -- Construct the Refl evidence + ; let pred = mkPrimEqPred fam_ty (mkTyVarTy fsk) + co = mkNomReflCo fam_ty + ; ev <- newGivenEvVar loc (pred, EvCoercion co) ; return (ev, co, fsk) } | otherwise -- Generate a [WD] for both Wanted and Derived @@ -2817,6 +2828,25 @@ newFlattenSkolem flav loc tc xis ; (ev, hole_co) <- newWantedEq loc Nominal fam_ty (mkTyVarTy fmv) ; return (ev, hole_co, fmv) } +---------------------------- +unflattenGivens :: IORef InertSet -> TcM () +-- Unflatten all the fsks created by flattening types in Given +-- constraints We must be sure to do this, else we end up with +-- flatten-skolems buried in any residual Wanteds +-- +-- NB: this is the /only/ way that a fsk (MetaDetails = FlatSkolTv) +-- is filled in. Nothing else does so. +-- +-- It's here (rather than in TcFlatten) becuause the Right Places +-- to call it are in runTcSWithEvBinds/nestImplicTcS, where it +-- is nicely paired with the creation an empty inert_fsks list. +unflattenGivens inert_var + = do { inerts <- TcM.readTcRef inert_var + ; mapM_ flatten_one (inert_fsks inerts) } + where + flatten_one (fsk, ty) = TcM.writeMetaTyVar fsk ty + +---------------------------- extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS () extendFlatCache tc xi_args stuff@(_, ty, fl) | isGivenOrWDeriv fl -- Maintain the invariant that inert_flat_cache @@ -2832,6 +2862,33 @@ extendFlatCache tc xi_args stuff@(_, ty, fl) | otherwise = return () +---------------------------- +unflattenFmv :: TcTyVar -> TcType -> TcS () +-- Fill a flatten-meta-var, simply by unifying it. +-- This does NOT count as a unification in tcs_unified. +unflattenFmv tv ty + = ASSERT2( isMetaTyVar tv, ppr tv ) + TcS $ \ _ -> + do { TcM.traceTc "unflattenFmv" (ppr tv <+> text ":=" <+> ppr ty) + ; TcM.writeMetaTyVar tv ty } + +---------------------------- +demoteUnfilledFmv :: TcTyVar -> TcS () +-- If a flatten-meta-var is still un-filled, +-- turn it into an ordinary meta-var +demoteUnfilledFmv fmv + = wrapTcS $ do { is_filled <- TcM.isFilledMetaTyVar fmv + ; unless is_filled $ + do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv) + ; TcM.writeMetaTyVar fmv tv_ty } } + + +{- ********************************************************************* +* * +* Instantaiation etc +* * +********************************************************************* -} + -- Instantiations -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2845,15 +2902,6 @@ newFlexiTcSTy knd = wrapTcS (TcM.newFlexiTyVarTy knd) cloneMetaTyVar :: TcTyVar -> TcS TcTyVar cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv) -demoteUnfilledFmv :: TcTyVar -> TcS () --- If a flatten-meta-var is still un-filled, --- turn it into an ordinary meta-var -demoteUnfilledFmv fmv - = wrapTcS $ do { is_filled <- TcM.isFilledMetaTyVar fmv - ; unless is_filled $ - do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv) - ; TcM.writeMetaTyVar fmv tv_ty } } - instFlexi :: [TKVar] -> TcS TCvSubst instFlexi = instFlexiX emptyTCvSubst diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index 557d40de1e..a611198253 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -615,8 +615,8 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds 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 + ; wanteds' <- solveWanteds wanteds + ; TcS.zonkWC wanteds' } -- Find quant_pred_candidates, the predicates that -- we'll consider quantifying over @@ -1953,20 +1953,29 @@ floatEqualities skols 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 + = do { -- First zonk: the inert set (from whence they came) are 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 + + -- Now we can pick the ones to float + ; let (float_eqs, remaining_simples) = partitionBag (usefulToFloat skol_set) simples + skol_set = mkVarSet skols + + -- Promote any unification variables mentioned in the floated equalities + -- See Note [Promoting unification variables] + ; outer_tclvl <- TcS.getTcLevel ; mapM_ (promoteTyVarTcS outer_tclvl) (tyCoVarsOfCtsList float_eqs) - -- See Note [Promoting unification variables] ; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr 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 usefulToFloat :: VarSet -> Ct -> Bool usefulToFloat skol_set ct -- The constraint is un-flattened and de-canonicalised diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index bd72981511..e22dfc3822 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -496,10 +496,6 @@ data TcTyVarDetails -- when looking up instances -- See Note [Binding when looking up instances] in InstEnv - | FlatSkol -- A flatten-skolem. It stands for the TcType, and zonking - TcType -- will replace it by that type. - -- See Note [The flattening story] in TcFlatten - | RuntimeUnk -- Stands for an as-yet-unknown type in the GHCi -- interactive context @@ -523,21 +519,26 @@ data MetaInfo -- never contains any ForAlls. | SigTv -- A variant of TauTv, except that it should not be - -- unified with a type, only with a type variable + -- unified with a type, only with a type variable -- See Note [Signature skolems] | FlatMetaTv -- A flatten meta-tyvar -- It is a meta-tyvar, but it is always untouchable, with level 0 -- See Note [The flattening story] in TcFlatten + | FlatSkolTv -- A flatten skolem tyvar + -- Just like FlatMetaTv, but is comletely "owned" by + -- its Given CFunEqCan. + -- It is filled in /only/ by unflattenGivens + -- See Note [The flattening story] in TcFlatten + instance Outputable MetaDetails where ppr Flexi = text "Flexi" ppr (Indirect ty) = text "Indirect" <+> ppr ty pprTcTyVarDetails :: TcTyVarDetails -> SDoc -- For debugging -pprTcTyVarDetails (RuntimeUnk {}) = text "rt" -pprTcTyVarDetails (FlatSkol {}) = text "fsk" +pprTcTyVarDetails (RuntimeUnk {}) = text "rt" pprTcTyVarDetails (SkolemTv lvl True) = text "ssk" <> colon <> ppr lvl pprTcTyVarDetails (SkolemTv lvl False) = text "sk" <> colon <> ppr lvl pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl }) @@ -546,7 +547,8 @@ pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl }) pp_info = case info of TauTv -> text "tau" SigTv -> text "sig" - FlatMetaTv -> text "fuv" + FlatMetaTv -> text "fmv" + FlatSkolTv -> text "fsk" {- ********************************************************************* @@ -715,7 +717,7 @@ Note [TcLevel assignment] ~~~~~~~~~~~~~~~~~~~~~~~~~ We arrange the TcLevels like this - 0 Level for flatten meta-vars + 0 Level for all flatten meta-vars 1 Top level 2 First-level implication constraints 3 Second-level implication constraints @@ -727,9 +729,9 @@ The flatten meta-vars are all at level 0, just to make them untouchable. maxTcLevel :: TcLevel -> TcLevel -> TcLevel maxTcLevel (TcLevel a) (TcLevel b) = TcLevel (a `max` b) -fmvTcLevel :: TcLevel -> TcLevel +fmvTcLevel :: TcLevel -- See Note [TcLevel assignment] -fmvTcLevel _ = TcLevel 0 +fmvTcLevel = TcLevel 0 topTcLevel :: TcLevel -- See Note [TcLevel assignment] @@ -763,7 +765,6 @@ tcTyVarLevel tv case tcTyVarDetails tv of MetaTv { mtv_tclvl = tv_lvl } -> tv_lvl SkolemTv tv_lvl _ -> tv_lvl - FlatSkol ty -> tcTypeLevel ty RuntimeUnk -> topTcLevel tcTypeLevel :: TcType -> TcLevel @@ -1167,20 +1168,15 @@ isFmvTyVar tv MetaTv { mtv_info = FlatMetaTv } -> True _ -> False --- | True of both given and wanted flatten-skolems (fak and usk) -isFlattenTyVar tv +isFskTyVar tv = ASSERT2( tcIsTcTyVar tv, ppr tv ) case tcTyVarDetails tv of - FlatSkol {} -> True - MetaTv { mtv_info = FlatMetaTv } -> True + MetaTv { mtv_info = FlatSkolTv } -> True _ -> False --- | True of FlatSkol skolems only -isFskTyVar tv - = ASSERT2( tcIsTcTyVar tv, ppr tv ) - case tcTyVarDetails tv of - FlatSkol {} -> True - _ -> False +-- | True of both given and wanted flatten-skolems (fak and usk) +isFlattenTyVar tv + = isFmvTyVar tv || isFskTyVar tv isSkolemTyVar tv = ASSERT2( tcIsTcTyVar tv, ppr tv ) diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index e103d20f0d..3f1d77a8f7 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -1603,7 +1603,6 @@ canSolveByUnification tclvl tv xi SigTv -> True _ -> False SkolemTv {} -> True - FlatSkol {} -> False RuntimeUnk -> True {- Note [Fmv Orientation Invariant] |