import HsSyn
import TcRnMonad
import TcErrors
-import TcCanonical
import TcMType
import TcType
import TcSMonad
import Data.List ( partition )
import Outputable
import FastString
+import Control.Monad ( unless )
\end{code}
***********************************************************************************
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"
+ * we MUST have the "self" dictionary available
Moreover, we must *completely* solve the constraints right now,
not wrap them in an implication constraint to solve later. Why?
looking like
foo :: Ord [Int]
foo = scsel dCInt
-we must not solve the (Ord [Int]) wanted from foo!!
+we must not solve the (Ord [Int]) wanted from foo!
+
+Note [Dependencies in self dictionaries]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Moreover, notice that when solving for a superclass, we record the dependency of
+self on the superclass. This is because this dependency is not evident in the
+EvBind of the self dictionary, which only involves a call to a DFun. Example:
+
+class A a => C a
+instance B a => C a
+
+When we check the instance declaration, we pass in a self dictionary that is merely
+ self = dfun b
+But we will be asked to solve that from:
+ [Given] d : B a
+ [Derived] self : C a
+We can show:
+ [Wanted] sc : A a
+The problem is that self *depends* on the sc variable, but that is not apparent in
+the binding self = dfun b. So we record the extra dependency, using the evidence bind:
+ EvBind self (EvDFunApp dfun [b] [b,sc])
+It is these dependencies that are the ''true'' dependencies in an EvDFunApp, and those
+that we must chase in function isGoodRecEv (in TcSMonad)
\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)
+simplifySuperClass :: [TyVar]
+ -> [EvVar] -- givens
+ -> EvVar -- the superclass we must solve for
+ -> EvBind -- the 'self' evidence bind
+ -> TcM TcEvBinds
+-- Post:
+-- ev_binds <- simplifySuperClasses tvs inst_givens sc_dict self_ev_bind
+-- Then:
+-- 1) ev_binds already contains self_ev_bind
+-- 2) if successful then ev_binds contains binding for
+-- the wanted superclass, sc_dict
+simplifySuperClass tvs inst_givens sc_dict (EvBind self_dict self_ev)
+ = do { giv_loc <- getCtLoc InstSkol -- For the inst_givens
+ ; want_loc <- getCtLoc ScOrigin -- As wanted/derived (for the superclass and self)
+ ; lcl_env <- getLclTypeEnv
+
+ -- Record the dependency of self_dict to sc_dict, see Note [Dependencies in self dictionaries]
+ ; let wanted = unitBag $ WcEvVar $ WantedEvVar sc_dict want_loc
+ self_ev_with_dep
+ = case self_ev of
+ EvDFunApp df tys insts deps -> EvDFunApp df tys insts (sc_dict:deps)
+ _ -> panic "Self-dictionary not EvDFunApp!"
+
+ -- And solve for it
+ ; ((unsolved_flats, unsolved_implics), 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 }
+ do { -- Record a binding for self_dict that *depends on sc_dict*
+ -- And canonicalise self_dict (which adds its superclasses)
+ -- with a Derived origin, which in turn triggers the
+ -- goodRecEv recursive-evidence check
+ ; setEvBind self_dict self_ev_with_dep
+ -- The rest is just like solveImplication
+ ; let cts = mapBag (\d -> (Given giv_loc, d)) (listToBag inst_givens)
+ `snocBag` (Derived want_loc DerSelf, self_dict)
+ ; inert <- solveInteract emptyInert cts
+
+ ; solveWanteds inert wanted }
+
+ -- For error reporting, conjure up a fake implication,
+ -- so that we get decent error messages
+ ; let implic = Implic { ic_untch = NoUntouchables
+ , ic_env = lcl_env
+ , ic_skols = mkVarSet tvs
+ , ic_given = inst_givens
+ , ic_wanted = mapBag WcEvVar unsolved_flats
+ , ic_scoped = panic "super1"
+ , ic_binds = panic "super2"
+ , ic_loc = giv_loc }
+ ; ASSERT (isEmptyBag unsolved_implics) -- Impossible to have any implications!
+ unless (isEmptyBag unsolved_flats) $
+ reportUnsolved (emptyBag, unitBag implic) frozen_errors
+
+ ; return (EvBinds ev_binds) }
\end{code}
-- 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