diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/typecheck/TcCanonical.lhs | 4 | ||||
| -rw-r--r-- | compiler/typecheck/TcInteract.lhs | 10 | ||||
| -rw-r--r-- | compiler/typecheck/TcSMonad.lhs | 33 | ||||
| -rw-r--r-- | compiler/typecheck/TcSimplify.lhs | 98 |
4 files changed, 110 insertions, 35 deletions
diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs index ffe0a7e520..bd8b911090 100644 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@ -546,7 +546,7 @@ classify ty | Just ty' <- tcView ty = OtherCls ty -- See note [Canonical ordering for equality constraints]. -reOrient :: Untouchables -> TypeClassifier -> TypeClassifier -> Bool +reOrient :: TcsUntouchables -> TypeClassifier -> TypeClassifier -> Bool -- (t1 `reOrient` t2) responds True -- iff we should flip to (t2~t1) -- We try to say False if possible, to minimise evidence generation @@ -579,7 +579,7 @@ reOrient _untch (FskCls {}) (FunCls {}) = True reOrient _untch (FskCls {}) (OtherCls {}) = False ------------------ -canEqLeaf :: Untouchables +canEqLeaf :: TcsUntouchables -> CtFlavor -> CoVar -> TypeClassifier -> TypeClassifier -> TcS CanonicalCts -- Canonicalizing "leaf" equality constraints which cannot be diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index 44e8479d33..fd3cc1ee83 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -1,6 +1,6 @@ \begin{code} module TcInteract ( - solveInteract, AtomicInert, + solveInteract, AtomicInert, tyVarsOfInert, InertSet, emptyInert, updInertSet, extractUnsolved, solveOne, foldISEqCts ) where @@ -134,6 +134,14 @@ data InertSet -- and reside either in the worklist or in the inerts } +tyVarsOfInert :: InertSet -> TcTyVarSet +tyVarsOfInert (IS { inert_eqs = eqs + , inert_dicts = dictmap + , inert_ips = ipmap + , inert_funeqs = funeqmap }) = tyVarsOfCanonicals cts + where cts = eqs `andCCan` cCanMapToBag dictmap + `andCCan` cCanMapToBag ipmap `andCCan` cCanMapToBag funeqmap + type FDImprovement = (PredType,PredType) type FDImprovements = [(PredType,PredType)] diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index 0a6865082a..d688af9513 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -14,6 +14,8 @@ module TcSMonad ( CtFlavor (..), isWanted, isGiven, isDerived, isDerivedSC, isDerivedByInst, isGivenCt, isWantedCt, pprFlavorArising, + isFlexiTcsTv, + DerivedOrig (..), canRewrite, canSolve, combineCtLoc, mkGivenFlavor, mkWantedFlavor, @@ -55,6 +57,7 @@ module TcSMonad ( compatKind, + TcsUntouchables, isTouchableMetaTyVar, isTouchableMetaTyVar_InRange, @@ -418,9 +421,14 @@ data TcSEnv -- Frozen errors that we defer reporting as much as possible, in order to -- make them as informative as possible. See Note [Frozen Errors] - tcs_untch :: Untouchables + tcs_untch :: TcsUntouchables } +type TcsUntouchables = (Untouchables,TcTyVarSet) +-- Like the TcM Untouchables, +-- but records extra TcsTv variables generated during simplification +-- See Note [Extra TcsTv untouchables] in TcSimplify + data FrozenError = FrozenError ErrorKind CtFlavor TcType TcType @@ -535,7 +543,7 @@ runTcS context untouch tcs ; let env = TcSEnv { tcs_ev_binds = ev_binds_var , tcs_ty_binds = ty_binds_var , tcs_context = context - , tcs_untch = untouch + , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet , tcs_errors = err_ref } @@ -552,9 +560,11 @@ runTcS context untouch tcs where do_unification (tv,ty) = TcM.writeMetaTyVar tv ty -nestImplicTcS :: EvBindsVar -> Untouchables -> TcS a -> TcS a +nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a nestImplicTcS ref untch (TcS thing_inside) - = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt, tcs_errors = err_ref } -> + = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, + tcs_context = ctxt, + tcs_errors = err_ref } -> let nest_env = TcSEnv { tcs_ev_binds = ref , tcs_ty_binds = ty_binds @@ -598,7 +608,7 @@ getTcSContext = TcS (return . tcs_context) getTcEvBinds :: TcS EvBindsVar getTcEvBinds = TcS (return . tcs_ev_binds) -getUntouchables :: TcS Untouchables +getUntouchables :: TcS TcsUntouchables getUntouchables = TcS (return . tcs_untch) getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType))) @@ -724,10 +734,11 @@ isTouchableMetaTyVar tv = do { untch <- getUntouchables ; return $ isTouchableMetaTyVar_InRange untch tv } -isTouchableMetaTyVar_InRange :: Untouchables -> TcTyVar -> Bool -isTouchableMetaTyVar_InRange untch tv +isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool +isTouchableMetaTyVar_InRange (untch,untch_tcs) tv = case tcTyVarDetails tv of - MetaTv TcsTv _ -> True -- See Note [Touchable meta type variables] + MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs) + -- See Note [Touchable meta type variables] MetaTv {} -> inTouchableRange untch tv _ -> False @@ -792,6 +803,12 @@ newFlexiTcSTy knd ; let name = mkSysTvName uniq (fsLit "uf") ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) } +isFlexiTcsTv :: TyVar -> Bool +isFlexiTcsTv tv + | not (isTcTyVar tv) = False + | MetaTv TcsTv _ <- tcTyVarDetails tv = True + | otherwise = False + newKindConstraint :: TcTyVar -> Kind -> TcS CoVar -- Create new wanted CoVar that constrains the type to have the specified kind. newKindConstraint tv knd diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index a4bf30f691..f6b9ed23ff 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -689,17 +689,9 @@ solveWanteds inert wanteds vcat [ text "inerts =" <+> ppr inert2 , text "unsolved =" <+> ppr unsolved_flats ] - -- See Note [Preparing inert set for implications] - ; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats) - ; traceTcS "solveWanteds: doing nested implications {" $ - vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics - , text "implics =" <+> ppr implics ] - ; (implic_eqs, unsolved_implics) - <- flatMapBagPairM (solveImplication inert_for_implics) implics - - ; traceTcS "solveWanteds: done nested implications }" $ - vcat [ text "implic_eqs =" <+> ppr implic_eqs - , text "unsolved_implics =" <+> ppr unsolved_implics ] + -- Go inside each implication + ; (implic_eqs, unsolved_implics) + <- solveNestedImplications inert2 unsolved_flats implics -- Apply defaulting rules if and only if there -- no floated equalities. If there are, they may @@ -726,12 +718,41 @@ solveWanteds inert wanteds -- Important: reiterate with inert2, not plainly inert -- because inert2 may contain more givens, as the result of solving -- some wanteds in the incoming can_ws - } } - -solveImplication :: InertSet -- Given - -> Implication -- Wanted - -> TcS (Bag WantedEvVar, -- Unsolved unification var = type - Bag Implication) -- Unsolved rest (always empty or singleton) + } + } + +solveNestedImplications :: InertSet -> CanonicalCts -> Bag Implication + -> TcS (Bag WantedEvVar, Bag Implication) +solveNestedImplications inerts unsolved implics + | isEmptyBag implics + = return (emptyBag, emptyBag) + | otherwise + = do { -- See Note [Preparing inert set for implications] + traceTcS "solveWanteds: preparing inerts for implications {" empty + ; inert_for_implics <- solveInteract inerts (makeGivens unsolved) + ; traceTcS "}" empty + + ; traceTcS "solveWanteds: doing nested implications {" $ + vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics + , text "implics =" <+> ppr implics ] + + ; let tcs_untouchables = filterVarSet isFlexiTcsTv $ + tyVarsOfInert inert_for_implics + -- See Note [Extra TcsTv untouchables] + ; (implic_eqs, unsolved_implics) + <- flatMapBagPairM (solveImplication tcs_untouchables inert_for_implics) implics + + ; traceTcS "solveWanteds: done nested implications }" $ + vcat [ text "implic_eqs =" <+> ppr implic_eqs + , text "unsolved_implics =" <+> ppr unsolved_implics ] + + ; return (implic_eqs, unsolved_implics) } + +solveImplication :: TcTyVarSet -- Untouchable TcS unification variables + -> InertSet -- Given + -> Implication -- Wanted + -> TcS (Bag WantedEvVar, -- Unsolved unification var = type + Bag Implication) -- Unsolved rest (always empty or singleton) -- Returns: -- 1. A bag of floatable wanted constraints, not mentioning any skolems, -- that are of the form unification var = type @@ -739,14 +760,14 @@ solveImplication :: InertSet -- Given -- 2. Maybe a unsolved implication, empty if entirely solved! -- -- Precondition: everything is zonked by now -solveImplication inert +solveImplication tcs_untouchables inert imp@(Implic { ic_untch = untch , ic_binds = ev_binds , ic_skols = skols , ic_given = givens , ic_wanted = wanteds , ic_loc = loc }) - = nestImplicTcS ev_binds untch $ + = nestImplicTcS ev_binds (untch, tcs_untouchables) $ recoverTcS (return (emptyBag, emptyBag)) $ -- Recover from nested failures. Even the top level is -- just a bunch of implications, so failing at the first @@ -825,9 +846,11 @@ Note [Preparing inert set for implications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Before solving the nested implications, we convert any unsolved flat wanteds to givens, and add them to the inert set. Reasons: - a) In checking mode, suppresses unnecessary errors. We already have + + a) In checking mode, suppresses unnecessary errors. We already have on unsolved-wanted error; adding it to the givens prevents any consequential errors from showing uop + b) More importantly, in inference mode, we are going to quantify over this constraint, and we *don't* want to quantify over any constraints that are deducible from it. @@ -840,7 +863,34 @@ Hence the call to solveInteract. Example: We were not able to solve (a ~w [beta]) but we can't just assume it as given because the resulting set is not inert. Hence we have to do a -'solveInteract' step first +'solveInteract' step first. + +Note [Extra TcsTv untouchables] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Furthemore, we record the inert set simplifier-generated unification variables of the TcsTv +kind (such as variables from instance that have been applied, or unification flattens). These +variables must be passed to the implications as extra untouchable variables. Otherwise +we have the danger of double unifications. Example (from trac ticket #4494): + + (F Int ~ uf) /\ (forall a. C a => F Int ~ beta) + +In this example, beta is touchable inside the implication. The first solveInteract step +leaves 'uf' ununified. Then we move inside the implication where a new constraint + uf ~ beta +emerges. We may spontaneously solve it to get uf := beta, so the whole implication disappears +but when we pop out again we are left with (F Int ~ uf) which will be unified by our final +solveCTyFunEqs stage and uf will get unified *once more* to (F Int). + +The solution is to record the TcsTvs (i.e. the simplifier-generated unification variables) +that are generated when solving the flats, and make them untouchables for the nested +implication. In the example above uf would become untouchable, so beta would be forced to +be unified as beta := uf. + +NB: A consequence is that every simplifier-generated TcsTv variable that gets floated out + of an implication becomes now untouchable next time we go inside that implication to + solve any residual constraints. In effect, by floating an equality out of the implication + we are committing to have it solved in the outside. + \begin{code} @@ -893,7 +943,7 @@ type FunEqBinds = [(TcTyVar,(TcType,CoVar,CtFlavor))] -- [... a -> (ta,...) ... b -> (tb,...) ... ] -- then 'ta' cannot mention 'b' -getSolvableCTyFunEqs :: Untouchables +getSolvableCTyFunEqs :: TcsUntouchables -> CanonicalCts -- Precondition: all wanteds -> (CanonicalCts, FunEqBinds) -- Postcondition: returns the unsolvables getSolvableCTyFunEqs untch cts @@ -1008,7 +1058,7 @@ applyDefaultingRules inert wanteds ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) } ------------------ -defaultTyVar :: Untouchables -> TcTyVar -> TcS (Bag WantedEvVar) +defaultTyVar :: TcsUntouchables -> TcTyVar -> TcS (Bag WantedEvVar) -- defaultTyVar is used on any un-instantiated meta type variables to -- default the kind of ? and ?? etc to *. This is important to ensure -- that instance declarations match. For example consider @@ -1041,7 +1091,7 @@ findDefaultableGroups :: ( SimplContext , [Type] , (Bool,Bool) ) -- (Overloaded strings, extended default rules) - -> Untouchables -- Untouchable + -> TcsUntouchables -- Untouchable -> CanonicalCts -- Unsolved -> [[(CanonicalCt,TcTyVar)]] findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults)) |