InstOrigin(..), InstLoc, pprInstLoc,
- mkWantedCo, mkGivenCo,
- isWantedCo, fromWantedCo, fromGivenCo, eqInstCoType,
- mkIdEqInstCo, mkSymEqInstCo, mkLeftTransEqInstCo,
- mkRightTransEqInstCo, mkAppEqInstCo,
- isValidWantedEqInst,
- eitherEqInst, mkEqInst, mkEqInsts, mkWantedEqInst,
- wantedToLocalEqInst, finalizeEqInst,
- eqInstType, updateEqInstCoercion,
- eqInstCoercion, eqInstTys
+ mkWantedCo, mkGivenCo, isWantedCo, eqInstCoType, mkIdEqInstCo,
+ mkSymEqInstCo, mkLeftTransEqInstCo, mkRightTransEqInstCo, mkAppEqInstCo,
+ wantedEqInstIsUnsolved, eitherEqInst, mkEqInst, mkWantedEqInst,
+ wantedToLocalEqInst, finalizeEqInst, eqInstType, eqInstCoercion,
+ eqInstTys
) where
#include "HsVersions.h"
instToVar (ImplicInst {tci_name = nm, tci_tyvars = tvs, tci_given = givens,
tci_wanted = wanteds})
= mkLocalId nm (mkImplicTy tvs givens wanteds)
-instToVar i@(EqInst {})
- = eitherEqInst i id (\(TyVarTy covar) -> covar)
+instToVar inst@(EqInst {})
+ = eitherEqInst inst id assertCoVar
+ where
+ assertCoVar (TyVarTy cotv) = cotv
+ assertCoVar coty = pprPanic "Inst.instToVar" (ppr coty)
instType :: Inst -> Type
instType (LitInst {tci_ty = ty}) = ty
isWantedCo (Left _) = True
isWantedCo _ = False
-fromGivenCo :: EqInstCo -> Coercion
-fromGivenCo (Right co) = co
-fromGivenCo _ = panic "fromGivenCo: not a wanted coercion"
-
-fromWantedCo :: String -> EqInstCo -> TcTyVar
-fromWantedCo _ (Left covar) = covar
-fromWantedCo msg _ =
- panic ("fromWantedCo: not a wanted coercion: " ++ msg)
-
eqInstCoType :: EqInstCo -> TcType
eqInstCoType (Left cotv) = mkTyVarTy cotv
eqInstCoType (Right co) = co
Operations on entire EqInst.
\begin{code}
--- For debugging, make sure the cotv of a wanted is not filled.
+-- |A wanted equality is unsolved as long as its cotv is unfilled.
--
-isValidWantedEqInst :: Inst -> TcM Bool
-isValidWantedEqInst (EqInst {tci_co = Left cotv})
+wantedEqInstIsUnsolved :: Inst -> TcM Bool
+wantedEqInstIsUnsolved (EqInst {tci_co = Left cotv})
= liftM not $ isFilledMetaTyVar cotv
-isValidWantedEqInst _ = return True
+wantedEqInstIsUnsolved _ = return True
eitherEqInst :: Inst -- given or wanted EqInst
-> (TcTyVar -> a) -- result if wanted
Right co -> withGiven co
eitherEqInst i _ _ = pprPanic "eitherEqInst" (ppr i)
-mkEqInsts :: [PredType] -> [EqInstCo] -> TcM [Inst]
-mkEqInsts preds cos = zipWithM mkEqInst preds cos
-
mkEqInst :: PredType -> EqInstCo -> TcM Inst
mkEqInst (EqPred ty1 ty2) co
= do { uniq <- newUnique
--
finalizeEqInst :: Inst -- wanted
-> TcM Inst -- given
-finalizeEqInst wanted@(EqInst{tci_left = ty1, tci_right = ty2, tci_name = name})
+finalizeEqInst wanted@(EqInst{tci_left = ty1, tci_right = ty2,
+ tci_name = name, tci_co = Left cotv})
= do { let var = Var.mkCoVar name (PredTy $ EqPred ty1 ty2)
-- fill the coercion hole
- ; let cotv = fromWantedCo "writeWantedCoercion" $ tci_co wanted
; writeMetaTyVar cotv (TyVarTy var)
-- set the new coercion
eqInstTys :: Inst -> (TcType, TcType)
eqInstTys inst = (tci_left inst, tci_right inst)
-
-updateEqInstCoercion :: (EqInstCo -> EqInstCo) -> Inst -> Inst
-updateEqInstCoercion f inst = inst {tci_co = f $ tci_co inst}
\end{code}
-> [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 / commitdiff