CtFlavor (..), isWanted, isGiven, isDerived, isDerivedSC, isDerivedByInst,
isGivenCt, isWantedCt, pprFlavorArising,
+ isFlexiTcsTv,
+
DerivedOrig (..),
canRewrite, canSolve,
combineCtLoc, mkGivenFlavor, mkWantedFlavor,
compatKind,
+ TcsUntouchables,
isTouchableMetaTyVar,
isTouchableMetaTyVar_InRange,
-- 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
; 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
}
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
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)))
= 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
; 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
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
-- 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
-- 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
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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.
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}
-- [... 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
; 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
:: ( 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))
projects / ghc-hetmet.git / commitdiff