-> [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))
}
--
-- 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
- })
+ })
= do { -- Solve the sub-problem
; let try_me _ = ReduceMe -- Note [Freeness and implications]
env' = env { red_givens = extra_givens ++ red_givens env
-- 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!
+ 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
-
- (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!
- ; let 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
- <.> mkWpTyLams 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