\begin{code}
module TcSimplify(
- simplifyInfer, simplifySuperClass,
+ simplifyInfer,
simplifyDefault, simplifyDeriv, simplifyBracket,
simplifyRule, simplifyTop, simplifyInteractive
) where
import HsSyn
import TcRnMonad
import TcErrors
-import TcCanonical
import TcMType
import TcType
import TcSMonad
\begin{code}
simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
-- Simplify top-level constraints
--- Usually these will be implications, when there is
--- nothing to quanitfy we don't wrap in a degenerate implication,
--- so we do that here instead
+-- Usually these will be implications,
+-- but when there is nothing to quantify we don't wrap
+-- in a degenerate implication, so we do that here instead
simplifyTop wanteds
= simplifyCheck SimplCheck wanteds
*********************************************************************************
* *
-* Superclasses *
-* *
-***********************************************************************************
-
-When constructing evidence for superclasses in an instance declaration,
- * we MUST have the "self" dictionary available, but
- * we must NOT have its superclasses derived from "self"
-
-Moreover, we must *completely* solve the constraints right now,
-not wrap them in an implication constraint to solve later. Why?
-Because when that implication constraint is solved there may
-be some unrelated other solved top-level constraints that
-recursively depend on the superclass we are building. Consider
- class Ord a => C a where
- instance C [Int] where ...
-Then we get
- dCListInt :: C [Int]
- dCListInt = MkC $cNum ...
-
- $cNum :: Ord [Int] -- The superclass
- $cNum = let self = dCListInt in <solve Ord [Int]>
-
-Now, if there is some *other* top-level constraint solved
-looking like
- foo :: Ord [Int]
- foo = scsel dCInt
-we must not solve the (Ord [Int]) wanted from foo!!
-
-\begin{code}
-simplifySuperClass :: EvVar -- The "self" dictionary
- -> WantedConstraints
- -> TcM ()
-simplifySuperClass self wanteds
- = do { wanteds <- mapBagM zonkWanted wanteds
- ; loc <- getCtLoc NoScSkol
- ; ((unsolved_flats,unsolved_impls), frozen_errors, ev_binds)
- <- runTcS SimplCheck NoUntouchables $
- do { can_self <- canGivens loc [self]
- ; let inert = foldlBag updInertSet emptyInert can_self
- -- No need for solveInteract; we know it's inert
-
- ; solveWanteds inert wanteds }
-
- ; ASSERT2( isEmptyBag ev_binds, ppr ev_binds )
- reportUnsolved (unsolved_flats,unsolved_impls) frozen_errors }
-\end{code}
-
-
-*********************************************************************************
-* *
* RULES *
* *
***********************************************************************************
Note [Simplifying RULE lhs constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-On the LHS of transformation rules we only simplify only equalitis,
+On the LHS of transformation rules we only simplify only equalities,
but not dictionaries. We want to keep dictionaries unsimplified, to
serve as the available stuff for the RHS of the rule. We *do* want to
simplify equalities, however, to detect ill-typed rules that cannot be
-- out of one or more of the implications
solveWanteds inert wanteds
= do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds
- ; can_flats <- canWanteds $ bagToList flat_wanteds
; traceTcS "solveWanteds {" $
vcat [ text "wanteds =" <+> ppr wanteds
, text "inert =" <+> ppr inert ]
; (unsolved_flats, unsolved_implics)
- <- simpl_loop 1 inert can_flats implic_wanteds
+ <- simpl_loop 1 inert flat_wanteds implic_wanteds
; bb <- getTcEvBindsBag
; tb <- getTcSTyBindsMap
; traceTcS "solveWanteds }" $
where
simpl_loop :: Int
-> InertSet
- -> CanonicalCts -- May inlude givens (in the recursive call)
+ -> Bag WantedEvVar
-> Bag Implication
-> TcS (CanonicalCts, Bag Implication)
- simpl_loop n inert can_ws implics
+ simpl_loop n inert work_items implics
| n>10
- = trace "solveWanteds: loop" $ -- Always bleat
+ = trace "solveWanteds: loop" $ -- Always bleat
do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively
- ; return (can_ws, implics) }
+
+ -- We don't want to call the canonicalizer on those wanted ev vars
+ -- so try one last time to solveInteract them
+ ; inert1 <- solveInteract inert $
+ mapBag (\(WantedEvVar ev wloc) -> (Wanted wloc, ev)) work_items
+ ; let (_, unsolved_cans) = extractUnsolved inert1
+ ; return (unsolved_cans, implics) }
| otherwise
= do { traceTcS "solveWanteds: simpl_loop start {" $
vcat [ text "n =" <+> ppr n
- , text "can_ws =" <+> ppr can_ws
+ , text "work_items =" <+> ppr work_items
, text "implics =" <+> ppr implics
, text "inert =" <+> ppr inert ]
- ; inert1 <- solveInteract inert can_ws
- ; let (inert2, unsolved_flats) = extractUnsolved inert1
+ ; inert1 <- solveInteract inert $
+ mapBag (\(WantedEvVar ev wloc) -> (Wanted wloc,ev)) work_items
+ ; let (inert2, unsolved_cans) = extractUnsolved inert1
+ unsolved_wevvars
+ = mapBag (\ct -> WantedEvVar (cc_id ct) (getWantedLoc ct)) unsolved_cans
-- NB: Importantly, inerts2 may contain *more* givens than inert
-- because of having solved equalities from can_ws
; traceTcS "solveWanteds: done flats" $
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 ]
+ , text "unsolved =" <+> ppr unsolved_cans ]
+
+ -- Go inside each implication
+ ; (implic_eqs, unsolved_implics)
+ <- solveNestedImplications inert2 unsolved_wevvars implics
-- Apply defaulting rules if and only if there
-- no floated equalities. If there are, they may
-- solve the remaining wanteds, so don't do defaulting.
; final_eqs <- if not (isEmptyBag implic_eqs)
then return implic_eqs
- else applyDefaultingRules inert2 unsolved_flats
-
- -- default_eqs are *givens*, so simpl_loop may
- -- recurse with givens in the argument
+ else applyDefaultingRules inert2 unsolved_cans
; traceTcS "solveWanteds: simpl_loop end }" $
vcat [ text "final_eqs =" <+> ppr final_eqs
- , text "unsolved_flats =" <+> ppr unsolved_flats
+ , text "unsolved_flats =" <+> ppr unsolved_cans
, text "unsolved_implics =" <+> ppr unsolved_implics ]
; if isEmptyBag final_eqs then
- return (unsolved_flats, unsolved_implics)
+ return (unsolved_cans, unsolved_implics)
else
- do { can_final_eqs <- canWanteds (Bag.bagToList final_eqs)
- -- final eqs is *just* a bunch of WantedEvVars
- ; simpl_loop (n+1) inert2
- (can_final_eqs `andCCan` unsolved_flats) unsolved_implics
+ simpl_loop (n+1) inert2 -- final_eqs are just some WantedEvVars
+ (final_eqs `unionBags` unsolved_wevvars) unsolved_implics
-- 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)
+ -- some wanteds in the incoming can_ws
+ }
+
+solveNestedImplications :: InertSet -> Bag WantedEvVar -> 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
do { traceTcS "solveImplication {" (ppr imp)
-- Solve flat givens
- ; can_givens <- canGivens loc givens
- ; given_inert <- solveInteract inert can_givens
+-- ; can_givens <- canGivens loc givens
+-- ; let given_fl = Given loc
+ ; given_inert <- solveInteract inert $
+ mapBag (\c -> (Given loc,c)) (listToBag givens)
-- Simplify the wanteds
; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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
\begin{code}
applyDefaultingRules :: InertSet
- -> CanonicalCts -- All wanteds
+ -> CanonicalCts -- All wanteds
-> TcS (Bag WantedEvVar) -- All wanteds again!
-- Return some *extra* givens, which express the
-- type-class-default choice
; 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))
= do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
; let ct_loc = get_ct_loc (cc_flavor the_ct)
; ev <- TcSMonad.newWantedCoVar (mkTyVarTy the_tv) default_ty
- ; let wanted_eq = CTyEqCan { cc_id = ev
- , cc_flavor = Wanted ct_loc
- , cc_tyvar = the_tv
- , cc_rhs = default_ty }
; success <- tryTcS $
- do { final_inert <- solveInteract inert(listToBag $ wanted_eq:wanteds)
- ; let (_, unsolved) = extractUnsolved final_inert
- ; errs <- getTcSErrorsBag
+ do { final_inert <- solveInteract inert $
+ consBag (Wanted ct_loc, ev) wanted_to_solve
+ ; let (_, unsolved) = extractUnsolved final_inert
+ ; errs <- getTcSErrorsBag
; return (isEmptyBag unsolved && isEmptyBag errs) }
-
; case success of
True -> -- Success: record the type variable binding, and return
do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
; disambigGroup default_tys inert group } }
where
((the_ct,the_tv):_) = group
- wanteds = map fst group
- wanted_ev_vars = map deCanonicaliseWanted wanteds
+ wanteds = map fst group
+ wanted_ev_vars = map deCanonicaliseWanted wanteds
+ wanted_to_solve = listToBag $
+ map (\(WantedEvVar ev wloc) -> (Wanted wloc,ev)) wanted_ev_vars
get_ct_loc (Wanted l) = l
get_ct_loc _ = panic "Asked to disambiguate given or derived!"
projects / ghc-hetmet.git / blobdiff