-> [Inst] -> [Inst]
-> TcM ([Inst], TcDictBinds)
-- Make a binding that binds 'irreds', by generating an implication
--- constraint for them, *and* throwing the constraint into the LIE
+-- constraint for them.
+--
-- The binding looks like
-- (ir1, .., irn) = f qtvs givens
-- where f is (evidence for) the new implication constraint
--- f :: forall qtvs. {reft} givens => (ir1, .., irn)
--- qtvs includes coercion variables
+-- f :: forall qtvs. givens => (ir1, .., irn)
+-- qtvs includes coercion variables.
--
-- This binding must line up the 'rhs' in reduceImplication
makeImplicationBind loc all_tvs
- givens -- Guaranteed all Dicts
- -- or EqInsts
+ givens -- Guaranteed all Dicts or EqInsts
irreds
| null irreds -- If there are no irreds, we are done
= return ([], emptyBag)
= do { uniq <- newUnique
; span <- getSrcSpanM
; let (eq_givens, dict_givens) = partition isEqInst givens
- eq_tyvar_cos = mkTyVarTys (varSetElems $ tyVarsOfTypes $ map eqInstType eq_givens)
- -- Urgh! See line 2187 or thereabouts. I believe that all these
- -- 'givens' must be a simple CoVar. This MUST be cleaned up.
- ; let name = mkInternalName uniq (mkVarOcc "ic") span
+ -- extract equality binders
+ eq_cotvs = map eqInstType eq_givens
+
+ -- make the implication constraint instance
+ name = mkInternalName uniq (mkVarOcc "ic") span
implic_inst = ImplicInst { tci_name = name,
tci_tyvars = all_tvs,
tci_given = (eq_givens ++ dict_givens),
- tci_wanted = irreds, tci_loc = loc }
- ; let -- only create binder for dict_irreds
- (_, dict_irreds) = partition isEqInst irreds
+ -- same order as binders
+ tci_wanted = irreds,
+ tci_loc = loc }
+
+ -- create binders for the irreducible dictionaries
+ dict_irreds = filter (not . isEqInst) irreds
dict_irred_ids = map instToId dict_irreds
lpat = mkBigLHsPatTup (map (L span . VarPat) dict_irred_ids)
- rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
- co = mkWpApps (map instToId dict_givens)
- <.> mkWpTyApps eq_tyvar_cos
- <.> mkWpTyApps (mkTyVarTys all_tvs)
- bind | [dict_irred_id] <- dict_irred_ids = VarBind dict_irred_id rhs
- | otherwise = PatBind { pat_lhs = lpat,
- pat_rhs = unguardedGRHSs rhs,
- pat_rhs_ty = hsLPatType lpat,
- bind_fvs = placeHolderNames }
+
+ -- create the binding
+ rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
+ co = mkWpApps (map instToId dict_givens)
+ <.> mkWpTyApps eq_cotvs
+ <.> mkWpTyApps (mkTyVarTys all_tvs)
+ bind | [dict_irred_id] <- dict_irred_ids
+ = VarBind dict_irred_id rhs
+ | otherwise
+ = PatBind { pat_lhs = lpat
+ , pat_rhs = unguardedGRHSs rhs
+ , pat_rhs_ty = hsLPatType lpat
+ , bind_fvs = placeHolderNames
+ }
+
; traceTc $ text "makeImplicationBind" <+> ppr implic_inst
; return ([implic_inst], unitBag (L span bind))
}
; let env = mkRedEnv doc try_me given_ips'
; (improved, binds, irreds) <- reduceContext env wanteds'
- ; if not improved then
+ ; if null irreds || not improved then
ASSERT( all is_free irreds )
do { extendLIEs irreds
; return binds }
- else
- tcSimplifyIPs given_ips wanteds }
+ else do
+ -- If improvement did some unification, we go round again.
+ -- We start again with irreds, not wanteds
+ -- Using an instance decl might have introduced a fresh type
+ -- variable which might have been unified, so we'd get an
+ -- infinite loop if we started again with wanteds!
+ -- See Note [LOOP]
+ { binds1 <- tcSimplifyIPs given_ips' irreds
+ ; return $ binds `unionBags` binds1
+ } }
where
doc = text "tcSimplifyIPs" <+> ppr given_ips
ip_set = mkNameSet (ipNamesOfInsts given_ips)
-- This may expose some further equational constraints...
; let (wanted_implics, wanted_dicts) = partition isImplicInst wanteds'
; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
+ -- The getLIE is reqd because reduceList does improvement
+ -- (via extendAvails) which may in turn do unification
; (dict_binds,
bound_dicts,
dict_irreds) <- extractResults avails wanted_dicts
-- improvement (i.e., instantiated type variables).
-- (2) If we uncovered extra equalities. We will try to solve them
-- in the next iteration.
+ -- (3) If we reduced dictionaries (i.e., got dictionary bindings),
+ -- they may have exposed further opportunities to normalise
+ -- family applications. See Note [Dictionary Improvement]
; let all_irreds = dict_irreds ++ implic_irreds ++ extra_eqs
avails_improved = availsImproved avails
improvedFlexible = avails_improved || eq_improved
extraEqs = (not . null) extra_eqs
- improved = improvedFlexible || extraEqs
+ reduced_dicts = not (isEmptyBag dict_binds)
+ improved = improvedFlexible || extraEqs || reduced_dicts
--
improvedHint = (if avails_improved then " [AVAILS]" else "") ++
(if eq_improved then " [EQ]" else "") ++
; return (tidy_env, msg) }
\end{code}
+Note [Dictionary Improvement]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In reduceContext, we first reduce equalities and then class constraints.
+However, the letter may expose further opportunities for the former. Hence,
+we need to go around again if dictionary reduction produced any dictionary
+bindings. The following example demonstrated the point:
+
+ data EX _x _y (p :: * -> *)
+ data ANY
+
+ class Base p
+
+ class Base (Def p) => Prop p where
+ type Def p
+
+ instance Base ()
+ instance Prop () where
+ type Def () = ()
+
+ instance (Base (Def (p ANY))) => Base (EX _x _y p)
+ instance (Prop (p ANY)) => Prop (EX _x _y p) where
+ type Def (EX _x _y p) = EX _x _y p
+
+ data FOO x
+ instance Prop (FOO x) where
+ type Def (FOO x) = ()
+
+ data BAR
+ instance Prop BAR where
+ type Def BAR = EX () () FOO
+
+During checking the last instance declaration, we need to check the superclass
+cosntraint Base (Def BAR), which family normalisation reduced to
+Base (EX () () FOO). Chasing the instance for Base (EX _x _y p), gives us
+Base (Def (FOO ANY)), which again requires family normalisation of Def to
+Base () before we can finish.
+
+
The main context-reduction function is @reduce@. Here's its game plan.
\begin{code}
--
-- Note on coercion variables:
--
- -- The extra given coercion variables are bound at two different sites:
+ -- The extra given coercion variables are bound at two different
+ -- sites:
+ --
-- -) in the creation context of the implication constraint
-- the solved equational constraints use these binders
--
-- -) at the solving site of the implication constraint
- -- the solved dictionaries use these binders
+ -- the solved dictionaries use these binders;
-- these binders are generated by reduceImplication
--
+ -- Note [Binders for equalities]
+ -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ -- To reuse the binders of local/given equalities in the binders of
+ -- implication constraints, it is crucial that these given equalities
+ -- always have the form
+ -- cotv :: t1 ~ t2
+ -- where cotv is a simple coercion type variable (and not a more
+ -- complex coercion term). We require that the extra_givens always
+ -- have this form and exploit the special form when generating binders.
reduceImplication env
orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc,
tci_tyvars = tvs,
- tci_given = extra_givens, tci_wanted = wanteds })
+ tci_given = extra_givens, tci_wanted = wanteds
+ })
= do { -- Solve the sub-problem
; let try_me _ = ReduceMe -- Note [Freeness and implications]
env' = env { red_givens = extra_givens ++ red_givens env
[ ppr (red_givens env), ppr extra_givens,
ppr wanteds])
; (irreds, binds) <- checkLoop env' wanteds
- ; let (extra_eq_givens, extra_dict_givens) = partition isEqInst extra_givens
- -- SLPJ Sept 07: I think this is bogus; currently
- -- there are no Eqinsts in extra_givens
- dict_ids = map instToId extra_dict_givens
-
- -- Note [Reducing implication constraints]
- -- Tom -- update note, put somewhere!
; traceTc (text "reduceImplication result" <+> vcat
[ppr irreds, ppr binds])
-- SLPJ Sept 07: what if improvement happened inside the checkLoop?
-- Then we must iterate the outer loop too!
+ ; didntSolveWantedEqs <- allM wantedEqInstIsUnsolved wanteds
+ -- we solve wanted eqs by side effect!
+
+ -- Progress is no longer measered by the number of bindings
+ -- If there are any irreds, but no bindings and no solved
+ -- equalities, we back off and do nothing
; let backOff = isEmptyLHsBinds binds && -- no new bindings
(not $ null irreds) && -- but still some irreds
- all (not . isEqInst) wanteds
- -- we may have instantiated a cotv
- -- => must make a new implication constraint!
-
- ; traceTc $ text "reduceImplication condition" <+> ppr backOff
+ didntSolveWantedEqs -- no instantiated cotv
- -- Progress is no longer measered by the number of bindings
; if backOff then -- No progress
- -- If there are any irreds, we back off and do nothing
return (emptyBag, [orig_implic])
else do
{ (simpler_implic_insts, bind)
-- case. After all, we only try hard to reduce at top level, or
-- when inferring types.
- ; let dict_wanteds = filter (not . isEqInst) wanteds
- -- TOMDO: given equational constraints bug!
- -- we need a different evidence for given
- -- equations depending on whether we solve
- -- dictionary constraints or equational constraints
-
- eq_tyvars = varSetElems $ tyVarsOfTypes $ map eqInstType extra_eq_givens
- -- SLPJ Sept07: this looks Utterly Wrong to me, but I think
- -- that current extra_givens has no EqInsts, so
- -- it makes no difference
- co = wrap_inline -- Note [Always inline implication constraints]
- <.> mkWpTyLams tvs
- <.> mkWpLams eq_tyvars
- <.> mkWpLams dict_ids
- <.> WpLet (binds `unionBags` bind)
- wrap_inline | null dict_ids = idHsWrapper
- | otherwise = WpInline
- rhs = mkLHsWrap co payload
- loc = instLocSpan inst_loc
- payload = mkBigLHsTup (map (L loc . HsVar . instToId) dict_wanteds)
+ ; let -- extract Id binders for dicts and CoTyVar binders for eqs;
+ -- see Note [Binders for equalities]
+ (extra_eq_givens, extra_dict_givens) = partition isEqInst
+ extra_givens
+ eq_cotvs = map instToVar extra_eq_givens
+ dict_ids = map instToId extra_dict_givens
+
+ -- Note [Always inline implication constraints]
+ wrap_inline | null dict_ids = idHsWrapper
+ | otherwise = WpInline
+ co = wrap_inline
+ <.> mkWpTyLams tvs
+ <.> mkWpTyLams eq_cotvs
+ <.> mkWpLams dict_ids
+ <.> WpLet (binds `unionBags` bind)
+ rhs = mkLHsWrap co payload
+ loc = instLocSpan inst_loc
+ -- wanted equalities are solved by updating their
+ -- cotv; we don't generate bindings for them
+ dict_bndrs = map (L loc . HsVar . instToId)
+ . filter (not . isEqInst)
+ $ wanteds
+ payload = mkBigLHsTup dict_bndrs
; traceTc (vcat [text "reduceImplication" <+> ppr name,
projects / ghc-hetmet.git / blobdiff