+++ /dev/null
-Normalisation of type terms relative to type instances as well as
-normalisation and entailment checking of equality constraints.
-
-\begin{code}
-module TcTyFuns (
- -- type normalisation wrt to toplevel equalities only
- tcNormaliseFamInst,
-
- -- instance normalisation wrt to equalities
- tcReduceEqs,
-
- -- errors
- misMatchMsg, failWithMisMatch,
-
-) where
-
-
-#include "HsVersions.h"
-
---friends
-import TcRnMonad
-import TcEnv
-import Inst
-import TcType
-import TcMType
-
--- GHC
-import Coercion
-import Type
-import TypeRep ( Type(..) )
-import TyCon
-import HsSyn
-import VarEnv
-import VarSet
-import Var
-import Name
-import Bag
-import Outputable
-import SrcLoc ( Located(..) )
-import Maybes
-import FastString
-
--- standard
-import Data.List
-import Control.Monad
-\end{code}
-
-
-%************************************************************************
-%* *
- Normalisation of types wrt toplevel equality schemata
-%* *
-%************************************************************************
-
-Unfold a single synonym family instance and yield the witnessing coercion.
-Return 'Nothing' if the given type is either not synonym family instance
-or is a synonym family instance that has no matching instance declaration.
-(Applies only if the type family application is outermost.)
-
-For example, if we have
-
- :Co:R42T a :: T [a] ~ :R42T a
-
-then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
-
-\begin{code}
-tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
-tcUnfoldSynFamInst (TyConApp tycon tys)
- | not (isSynFamilyTyCon tycon) -- unfold *only* _synonym_ family instances
- = return Nothing
- | otherwise
- = do { -- The TyCon might be over-saturated, but that's ok for tcLookupFamInst
- ; maybeFamInst <- tcLookupFamInst tycon tys
- ; case maybeFamInst of
- Nothing -> return Nothing
- Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys,
- mkTyConApp coe_tc rep_tys)
- where
- coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst"
- (tyConFamilyCoercion_maybe rep_tc)
- }
-tcUnfoldSynFamInst _other = return Nothing
-\end{code}
-
-Normalise 'Type's and 'PredType's by unfolding type family applications where
-possible (ie, we treat family instances as a TRS). Also zonk meta variables.
-
- tcNormaliseFamInst ty = (co, ty')
- then co : ty ~ ty'
-
-\begin{code}
--- |Normalise the given type as far as possible with toplevel equalities.
--- This results in a coercion witnessing the type equality, in addition to the
--- normalised type.
---
-tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
-tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
-\end{code}
-
-Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
-apply the normalisation function gives as the first argument to every TyConApp
-and every TyVarTy subterm.
-
- tcGenericNormaliseFamInst fun ty = (co, ty')
- then co : ty ~ ty'
-
-This function is (by way of using smart constructors) careful to ensure that
-the returned coercion is exactly IdCo (and not some semantically equivalent,
-but syntactically different coercion) whenever (ty' `tcEqType` ty). This
-makes it easy for the caller to determine whether the type changed. BUT
-even if we return IdCo, ty' may be *syntactically* different from ty due to
-unfolded closed type synonyms (by way of tcCoreView). In the interest of
-good error messages, callers should discard ty' in favour of ty in this case.
-
-\begin{code}
-tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
- -- what to do with type functions and tyvars
- -> TcType -- old type
- -> TcM (CoercionI, TcType) -- (coercion, new type)
-tcGenericNormaliseFamInst fun ty
- | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
-tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
- = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
- ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
- ; maybe_ty_co <- fun (mkTyConApp tyCon ntys) -- use normalised args!
- ; case maybe_ty_co of
- -- a matching family instance exists
- Just (ty', co) ->
- do { let first_coi = mkTransCoI tycon_coi (ACo co)
- ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
- ; let fix_coi = mkTransCoI first_coi rest_coi
- ; return (fix_coi, nty)
- }
- -- no matching family instance exists
- -- we do not do anything
- Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
- }
-tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
- = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
- ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
- ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
- }
-tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
- = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
- ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
- ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
- }
-tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
- = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
- ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
- }
-tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
- | isTcTyVar tv
- = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
- ; res <- lookupTcTyVar tv
- ; case res of
- DoneTv _ ->
- do { maybe_ty' <- fun ty
- ; case maybe_ty' of
- Nothing -> return (IdCo, ty)
- Just (ty', co1) ->
- do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
- ; return (ACo co1 `mkTransCoI` coi2, ty'')
- }
- }
- IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
- }
- | otherwise
- = return (IdCo, ty)
-tcGenericNormaliseFamInst fun (PredTy predty)
- = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
- ; return (coi, PredTy pred') }
-
----------------------------------
-tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
- -> TcPredType
- -> TcM (CoercionI, TcPredType)
-
-tcGenericNormaliseFamInstPred fun (ClassP cls tys)
- = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
- ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
- }
-tcGenericNormaliseFamInstPred fun (IParam ipn ty)
- = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
- ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
- }
-tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
- = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
- ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
- ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
-\end{code}
-
-
-%************************************************************************
-%* *
- Normalisation of instances wrt to equalities
-%* *
-%************************************************************************
-
-Given a set of given, local constraints and a set of wanted constraints,
-simplify the wanted equalities as far as possible and normalise both local and
-wanted dictionaries with respect to the equalities.
-
-In addition to the normalised local dictionaries and simplified wanteds, the
-function yields bindings for instantiated meta variables (due to solving
-equality constraints) and dictionary bindings (due to simplifying class
-constraints). The bag of type variable bindings only contains bindings for
-non-local variables - i.e., type variables other than those newly created by
-the present function. Consequently, type improvement took place iff the bag
-of bindings contains any bindings for proper type variables (not just covars).
-The solver does not instantiate any non-local variables; i.e., the bindings
-must be executed by the caller.
-
-All incoming constraints are assumed to be zonked already. All outgoing
-constraints will be zonked again.
-
-NB: The solver only has local effects that cannot be observed from outside.
- In particular, it can be executed twice on the same constraint set with
- the same result (modulo generated variables names).
-
-\begin{code}
-tcReduceEqs :: [Inst] -- locals
- -> [Inst] -- wanteds
- -> TcM ([Inst], -- normalised locals (w/o equalities)
- [Inst], -- normalised wanteds (including equalities)
- TcTyVarBinds, -- bindings for meta type variables
- TcDictBinds) -- bindings for all simplified dictionaries
-tcReduceEqs locals wanteds
- = do { ((locals, wanteds, dictBinds), tyBinds) <- getTcTyVarBinds $
- do { let (local_eqs , local_dicts) = partition isEqInst locals
- (wanteds_eqs, wanteds_dicts) = partition isEqInst wanteds
- ; eqCfg1 <- normaliseEqs (local_eqs ++ wanteds_eqs)
- ; eqCfg2 <- normaliseDicts False local_dicts
- ; eqCfg3 <- normaliseDicts True wanteds_dicts
- ; eqCfg <- propagateEqs (eqCfg1 `unionEqConfig`
- eqCfg2 `unionEqConfig`
- eqCfg3)
- ; finaliseEqsAndDicts freeFlexibles eqCfg
- }
- -- execute type bindings of skolem flexibles...
- ; tyBinds_pruned <- pruneTyBinds tyBinds freeFlexibles
- -- ...and zonk the constraints to propagate the bindings
- ; locals_z <- zonkInsts locals
- ; wanteds_z <- zonkInsts wanteds
- ; return (locals_z, wanteds_z, tyBinds_pruned, dictBinds)
- }
- where
- -- unification variables that appear in the environment and may not be
- -- instantiated - this includes coercion variables
- freeFlexibles = tcTyVarsOfInsts locals `unionVarSet`
- tcTyVarsOfInsts wanteds
-
- pruneTyBinds tybinds freeFlexibles
- = do { let tybinds' = bagToList tybinds
- (skolem_tybinds, env_tybinds) = partition isSkolem tybinds'
- ; execTcTyVarBinds (listToBag skolem_tybinds)
- ; return $ listToBag env_tybinds
- }
- where
- isSkolem (TcTyVarBind tv _ ) = not (tv `elemVarSet` freeFlexibles)
-\end{code}
-
-
-%************************************************************************
-%* *
- Equality Configurations
-%* *
-%************************************************************************
-
-We maintain normalised equalities together with the skolems introduced as
-intermediates during flattening of equalities as well as
-
-\begin{code}
--- |Configuration of normalised equalities used during solving.
---
-data EqConfig = EqConfig { eqs :: [RewriteInst] -- all equalities
- , locals :: [Inst] -- given dicts
- , wanteds :: [Inst] -- wanted dicts
- , binds :: TcDictBinds -- bindings
- }
-
-addEq :: EqConfig -> RewriteInst -> EqConfig
-addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg}
-
-unionEqConfig :: EqConfig -> EqConfig -> EqConfig
-unionEqConfig eqc1 eqc2 = EqConfig
- { eqs = eqs eqc1 ++ eqs eqc2
- , locals = locals eqc1 ++ locals eqc2
- , wanteds = wanteds eqc1 ++ wanteds eqc2
- , binds = binds eqc1 `unionBags` binds eqc2
- }
-
-emptyEqConfig :: EqConfig
-emptyEqConfig = EqConfig
- { eqs = []
- , locals = []
- , wanteds = []
- , binds = emptyBag
- }
-
-instance Outputable EqConfig where
- ppr (EqConfig {eqs = eqs, locals = locals, wanteds = wanteds, binds = binds})
- = vcat [ppr eqs, ppr locals, ppr wanteds, ppr binds]
-\end{code}
-
-The set of operations on an equality configuration. We obtain the initialise
-configuration by normalisation ('normaliseEqs'), solve the equalities by
-propagation ('propagateEqs'), and eventually finalise the configuration when
-no further propoagation is possible.
-
-\begin{code}
--- |Turn a set of equalities into an equality configuration for solving.
---
--- Precondition: The Insts are zonked.
---
-normaliseEqs :: [Inst] -> TcM EqConfig
-normaliseEqs eqs
- = do { WARNM2( anyM wantedEqInstIsUnsolved eqs, ppr eqs )
- ; traceTc $ ptext (sLit "Entering normaliseEqs")
-
- ; eqss <- mapM normEqInst eqs
- ; return $ emptyEqConfig { eqs = concat eqss }
- }
-
--- |Flatten the type arguments of all dictionaries, returning the result as a
--- equality configuration. The dictionaries go into the 'wanted' component if
--- the second argument is 'True'.
---
--- Precondition: The Insts are zonked.
---
-normaliseDicts :: Bool -> [Inst] -> TcM EqConfig
-normaliseDicts isWanted insts
- = do { traceTc $ hang (ptext (sLit "Entering normaliseDicts") <+>
- ptext (if isWanted then sLit "[Wanted] for"
- else sLit "[Local] for"))
- 4 (ppr insts)
-
- ; (insts', eqss, bindss) <- mapAndUnzip3M (normDict isWanted) insts
-
- ; traceTc $ hang (ptext (sLit "normaliseDicts returns"))
- 4 (ppr insts' $$ ppr eqss)
- ; return $ emptyEqConfig { eqs = concat eqss
- , locals = if isWanted then [] else insts'
- , wanteds = if isWanted then insts' else []
- , binds = unionManyBags bindss
- }
- }
-
--- |Solves the equalities as far as possible by applying propagation rules.
---
-propagateEqs :: EqConfig -> TcM EqConfig
-propagateEqs eqCfg@(EqConfig {eqs = todoEqs})
- = do { traceTc $ hang (ptext (sLit "Entering propagateEqs:"))
- 4 (ppr eqCfg)
-
- ; propagate todoEqs (eqCfg {eqs = []})
- }
-
--- |Finalise a set of equalities and associated dictionaries after
--- propagation. The first returned set of instances are the locals (without
--- equalities) and the second set are all residual wanteds, including
--- equalities. In addition, we return all generated dictionary bindings.
---
-finaliseEqsAndDicts :: TcTyVarSet -> EqConfig
- -> TcM ([Inst], [Inst], TcDictBinds)
-finaliseEqsAndDicts freeFlexibles (EqConfig { eqs = eqs
- , locals = locals
- , wanteds = wanteds
- , binds = binds
- })
- = do { traceTc $ ptext (sLit "finaliseEqsAndDicts")
-
- ; (eqs', subst_binds, locals', wanteds')
- <- substitute eqs locals wanteds checkingMode freeFlexibles
- ; eqs'' <- bindAndExtract eqs' checkingMode freeFlexibles
- ; let final_binds = subst_binds `unionBags` binds
-
- -- Assert that all cotvs of wanted equalities are still unfilled, and
- -- zonk all final insts, to make any improvement visible
- ; ASSERTM2( allM wantedEqInstIsUnsolved eqs'', ppr eqs'' )
- ; zonked_locals <- zonkInsts locals'
- ; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds')
- ; return (zonked_locals, zonked_wanteds, final_binds)
- }
- where
- checkingMode = length eqs > length wanteds || not (null locals)
- -- no local equalities or dicts => checking mode
-\end{code}
-
-
-%************************************************************************
-%* *
- Normalisation of equalities
-%* *
-%************************************************************************
-
-A normal equality is a properly oriented equality with associated coercion
-that contains at most one family equality (in its left-hand side) is oriented
-such that it may be used as a rewrite rule. It has one of the following two
-forms:
-
-(1) co :: F t1..tn ~ t (family equalities)
-(2) co :: x ~ t (variable equalities)
-
-Variable equalities fall again in two classes:
-
-(2a) co :: x ~ t, where t is *not* a variable, or
-(2b) co :: x ~ y, where x > y.
-
-The types t, t1, ..., tn may not contain any occurrences of synonym
-families. Moreover, in Forms (2) & (3), the left-hand side may not occur in
-the right-hand side, and the relation x > y is an (nearly) arbitrary, but
-total order on type variables. The only restriction that we impose on that
-order is that for x > y, we are happy to instantiate x with y taking into
-account kinds, signature skolems etc (cf, TcUnify.uUnfilledVars).
-
-\begin{code}
-data RewriteInst
- = RewriteVar -- Form (2) above
- { rwi_var :: TyVar -- may be rigid or flexible
- , rwi_right :: TcType -- contains no synonym family applications
- , rwi_co :: EqInstCo -- the wanted or given coercion
- , rwi_loc :: InstLoc
- , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
- , rwi_swapped :: Bool -- swapped orientation of original EqInst
- }
- | RewriteFam -- Forms (1) above
- { rwi_fam :: TyCon -- synonym family tycon
- , rwi_args :: [Type] -- contain no synonym family applications
- , rwi_right :: TcType -- contains no synonym family applications
- , rwi_co :: EqInstCo -- the wanted or given coercion
- , rwi_loc :: InstLoc
- , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
- , rwi_swapped :: Bool -- swapped orientation of original EqInst
- }
-
-isWantedRewriteInst :: RewriteInst -> Bool
-isWantedRewriteInst = isWantedCo . rwi_co
-
-isRewriteVar :: RewriteInst -> Bool
-isRewriteVar (RewriteVar {}) = True
-isRewriteVar _ = False
-
-tyVarsOfRewriteInst :: RewriteInst -> TyVarSet
-tyVarsOfRewriteInst (RewriteVar {rwi_var = tv, rwi_right = ty})
- = unitVarSet tv `unionVarSet` tyVarsOfType ty
-tyVarsOfRewriteInst (RewriteFam {rwi_args = args, rwi_right = ty})
- = tyVarsOfTypes args `unionVarSet` tyVarsOfType ty
-
-rewriteInstToInst :: RewriteInst -> TcM Inst
-rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
- = deriveEqInst eq (mkTyVarTy tv) (rwi_right eq) (rwi_co eq)
-rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
- = deriveEqInst eq (mkTyConApp fam args) (rwi_right eq) (rwi_co eq)
-
--- Derive an EqInst based from a RewriteInst, possibly swapping the types
--- around.
---
-deriveEqInst :: RewriteInst -> TcType -> TcType -> EqInstCo -> TcM Inst
-deriveEqInst rewrite ty1 ty2 co
- = do { co_adjusted <- if not swapped then return co
- else mkSymEqInstCo co (ty2, ty1)
- ; return $ EqInst
- { tci_left = left
- , tci_right = right
- , tci_co = co_adjusted
- , tci_loc = rwi_loc rewrite
- , tci_name = rwi_name rewrite
- }
- }
- where
- swapped = rwi_swapped rewrite
- (left, right) = if not swapped then (ty1, ty2) else (ty2, ty1)
-
-instance Outputable RewriteInst where
- ppr (RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = rhs, rwi_co =co})
- = hsep [ pprEqInstCo co <+> text "::"
- , ppr (mkTyConApp fam args)
- , text "~>"
- , ppr rhs
- ]
- ppr (RewriteVar {rwi_var = tv, rwi_right = rhs, rwi_co =co})
- = hsep [ pprEqInstCo co <+> text "::"
- , ppr tv
- , text "~>"
- , ppr rhs
- ]
-
-pprEqInstCo :: EqInstCo -> SDoc
-pprEqInstCo (Left cotv) = ptext (sLit "Wanted") <+> ppr cotv
-pprEqInstCo (Right co) = ptext (sLit "Local") <+> ppr co
-\end{code}
-
-The following functions turn an arbitrary equality into a set of normal
-equalities. This implements the WFlat and LFlat rules of the paper in one
-sweep. However, we use flexible variables for both locals and wanteds, and
-avoid to carry around the unflattening substitution \Sigma (for locals) by
-already updating the skolems for locals with the family application that they
-represent - i.e., they will turn into that family application on the next
-zonking (which only happens after finalisation).
-
-In a corresponding manner, normDict normalises class dictionaries by
-extracting any synonym family applications and generation appropriate normal
-equalities.
-
-Whenever we encounter a loopy equality (of the form a ~ T .. (F ...a...) ...),
-we drop that equality and raise an error if it is a wanted or a warning if it
-is a local.
-
-\begin{code}
-normEqInst :: Inst -> TcM [RewriteInst]
--- Normalise one equality.
-normEqInst inst
- = ASSERT( isEqInst inst )
- do { traceTc $ ptext (sLit "normEqInst of ") <+>
- pprEqInstCo co <+> text "::" <+>
- ppr ty1 <+> text "~" <+> ppr ty2
- ; res <- go ty1 ty2 co
-
- ; traceTc $ ptext (sLit "normEqInst returns") <+> ppr res
- ; return res
- }
- where
- (ty1, ty2) = eqInstTys inst
- co = eqInstCoercion inst
-
- -- look through synonyms
- go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
- go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
-
- -- left-to-right rule with type family head
- go ty1@(TyConApp con args) ty2 co
- | isSynFamilyTyConApp ty1 -- only if not oversaturated
- = mkRewriteFam False con args ty2 co
-
- -- right-to-left rule with type family head
- go ty1 ty2@(TyConApp con args) co
- | isSynFamilyTyConApp ty2 -- only if not oversaturated
- = do { co' <- mkSymEqInstCo co (ty2, ty1)
- ; mkRewriteFam True con args ty1 co'
- }
-
- -- no outermost family
- go ty1 ty2 co
- = do { (ty1', co1, ty1_eqs) <- flattenType inst ty1
- ; (ty2', co2, ty2_eqs) <- flattenType inst ty2
- ; let ty12_eqs = ty1_eqs ++ ty2_eqs
- sym_co2 = mkSymCoercion co2
- eqTys = (ty1', ty2')
- ; (co', ty12_eqs') <- adjustCoercions co co1 sym_co2 eqTys ty12_eqs
- ; eqs <- checkOrientation ty1' ty2' co' inst
- ; if isLoopyEquality eqs ty12_eqs'
- then do { if isWantedCo (tci_co inst)
- then
- addErrCtxt (ptext (sLit "Rejecting loopy equality")) $
- eqInstMisMatch inst
- else
- warnDroppingLoopyEquality ty1 ty2
- ; return ([]) -- drop the equality
- }
- else
- return (eqs ++ ty12_eqs')
- }
-
- mkRewriteFam swapped con args ty2 co
- = do { (args', cargs, args_eqss) <- mapAndUnzip3M (flattenType inst) args
- ; (ty2', co2, ty2_eqs) <- flattenType inst ty2
- ; let co1 = mkTyConApp con cargs
- sym_co2 = mkSymCoercion co2
- all_eqs = concat args_eqss ++ ty2_eqs
- eqTys = (mkTyConApp con args', ty2')
- ; (co', all_eqs') <- adjustCoercions co co1 sym_co2 eqTys all_eqs
- ; let thisRewriteFam = RewriteFam
- { rwi_fam = con
- , rwi_args = args'
- , rwi_right = ty2'
- , rwi_co = co'
- , rwi_loc = tci_loc inst
- , rwi_name = tci_name inst
- , rwi_swapped = swapped
- }
- ; return $ thisRewriteFam : all_eqs'
- }
-
- -- If the original equality has the form a ~ T .. (F ...a...) ..., we will
- -- have a variable equality with 'a' on the lhs as the first equality.
- -- Then, check whether 'a' occurs in the lhs of any family equality
- -- generated by flattening.
- isLoopyEquality (RewriteVar {rwi_var = tv}:_) eqs = any inRewriteFam eqs
- where
- inRewriteFam (RewriteFam {rwi_args = args})
- = tv `elemVarSet` tyVarsOfTypes args
- inRewriteFam _ = False
- isLoopyEquality _ _ = False
-
-normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds)
--- Normalise one dictionary or IP constraint.
-normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
- = do { (args', cargs, args_eqss) <- mapAndUnzip3M (flattenType inst) args
- ; let rewriteCo = PredTy $ ClassP clas cargs
- eqs = concat args_eqss
- pred' = ClassP clas args'
- ; if null eqs
- then -- don't generate a binding if there is nothing to flatten
- return (inst, [], emptyBag)
- else do {
- ; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred'
- ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
- ; return (inst', eqs', bind)
- }}
-normDict _isWanted inst
- = return (inst, [], emptyBag)
--- !!!TODO: Still need to normalise IP constraints.
-
-checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
--- Performs the occurs check, decomposition, and proper orientation
--- (returns a singleton, or an empty list in case of a trivial equality)
--- NB: We cannot assume that the two types already have outermost type
--- synonyms expanded due to the recursion in the case of type applications.
-checkOrientation ty1 ty2 co inst
- = go ty1 ty2
- where
- -- look through synonyms
- go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
- go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
-
- -- identical types => trivial
- go ty1 ty2
- | ty1 `tcEqType` ty2
- = do { mkIdEqInstCo co ty1
- ; return []
- }
-
- -- two tvs (distinct tvs, due to previous equation)
- go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
- = do { isBigger <- tv1 `tvIsBigger` tv2
- ; if isBigger -- left greater
- then mkRewriteVar False tv1 ty2 co -- => unchanged
- else do { co' <- mkSymEqInstCo co (ty2, ty1) -- right greater
- ; mkRewriteVar True tv2 ty1 co' -- => swap
- }
- }
-
- -- only lhs is a tv => unchanged
- go ty1@(TyVarTy tv1) ty2
- | ty1 `tcPartOfType` ty2 -- occurs check!
- = occurCheckErr ty1 ty2
- | otherwise
- = mkRewriteVar False tv1 ty2 co
-
- -- only rhs is a tv => swap
- go ty1 ty2@(TyVarTy tv2)
- | ty2 `tcPartOfType` ty1 -- occurs check!
- = occurCheckErr ty2 ty1
- | otherwise
- = do { co' <- mkSymEqInstCo co (ty2, ty1)
- ; mkRewriteVar True tv2 ty1 co'
- }
-
- -- data type constructor application => decompose
- -- NB: Special cased for efficiency - could be handled as type application
- go (TyConApp con1 args1) (TyConApp con2 args2)
- | con1 == con2
- && isInjectiveTyCon con1 -- don't match family synonym apps
- = do { co_args <- mkTyConEqInstCo co con1 (zip args1 args2)
- ; eqss <- zipWith3M (\ty1 ty2 co -> checkOrientation ty1 ty2 co inst)
- args1 args2 co_args
- ; return $ concat eqss
- }
-
- -- function type => decompose
- -- NB: Special cased for efficiency - could be handled as type application
- go (FunTy ty1_l ty1_r) (FunTy ty2_l ty2_r)
- = do { (co_l, co_r) <- mkFunEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
- ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
- ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
- ; return $ eqs_l ++ eqs_r
- }
-
- -- type applications => decompose
- go ty1 ty2
- | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1 -- won't split fam apps
- , Just (ty2_l, ty2_r) <- repSplitAppTy_maybe ty2
- = do { (co_l, co_r) <- mkAppEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
- ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
- ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
- ; return $ eqs_l ++ eqs_r
- }
-
- -- inconsistency => type error
- go ty1 ty2
- = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) )
- eqInstMisMatch inst
-
- mkRewriteVar swapped tv ty co = return [RewriteVar
- { rwi_var = tv
- , rwi_right = ty
- , rwi_co = co
- , rwi_loc = tci_loc inst
- , rwi_name = tci_name inst
- , rwi_swapped = swapped
- }]
-
- -- if tv1 `tvIsBigger` tv2, we make a rewrite rule tv1 ~> tv2
- tvIsBigger :: TcTyVar -> TcTyVar -> TcM Bool
- tvIsBigger tv1 tv2
- = isBigger tv1 (tcTyVarDetails tv1) tv2 (tcTyVarDetails tv2)
- where
- isBigger tv1 (SkolemTv _) tv2 (SkolemTv _)
- = return $ tv1 > tv2
- isBigger _ (MetaTv _ _) _ (SkolemTv _)
- = return True
- isBigger _ (SkolemTv _) _ (MetaTv _ _)
- = return False
- isBigger tv1 (MetaTv info1 _) tv2 (MetaTv info2 _)
- -- meta variable meets meta variable
- -- => be clever about which of the two to update
- -- (from TcUnify.uUnfilledVars minus boxy stuff)
- = case (info1, info2) of
- -- Avoid SigTvs if poss
- (SigTv _, SigTv _) -> return $ tv1 > tv2
- (SigTv _, _ ) | k1_sub_k2 -> return False
- (_, SigTv _) | k2_sub_k1 -> return True
-
- (_, _)
- | k1_sub_k2 &&
- k2_sub_k1
- -> case (nicer_to_update tv1, nicer_to_update tv2) of
- (True, False) -> return True
- (False, True) -> return False
- _ -> return $ tv1 > tv2
- | k1_sub_k2 -> return False
- | k2_sub_k1 -> return True
- | otherwise -> kind_err >> return True
- -- Update the variable with least kind info
- -- See notes on type inference in Kind.lhs
- -- The "nicer to" part only applies if the two kinds are the same,
- -- so we can choose which to do.
- where
- kind_err = addErrCtxtM (unifyKindCtxt False tv1 (mkTyVarTy tv2)) $
- unifyKindMisMatch k1 k2
-
- k1 = tyVarKind tv1
- k2 = tyVarKind tv2
- k1_sub_k2 = k1 `isSubKind` k2
- k2_sub_k1 = k2 `isSubKind` k1
-
- nicer_to_update tv = isSystemName (Var.varName tv)
- -- Try to update sys-y type variables in preference to ones
- -- gotten (say) by instantiating a polymorphic function with
- -- a user-written type sig
-
-flattenType :: Inst -- context to get location & name
- -> Type -- the type to flatten
- -> TcM (Type, -- the flattened type
- Coercion, -- coercion witness of flattening wanteds
- [RewriteInst]) -- extra equalities
--- Removes all family synonyms from a type by moving them into extra equalities
-flattenType inst ty = go ty
- where
- -- look through synonyms
- go ty | Just ty' <- tcView ty
- = do { (ty_flat, co, eqs) <- go ty'
- ; if null eqs
- then -- unchanged, keep the old type with folded synonyms
- return (ty, ty, [])
- else
- return (ty_flat, co, eqs)
- }
-
- -- type variable => nothing to do
- go ty@(TyVarTy _)
- = return (ty, ty, [])
-
- -- type family application & family arity matches number of args
- -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh)
- go ty@(TyConApp con args)
- | isSynFamilyTyConApp ty -- only if not oversaturated
- = do { (args', cargs, args_eqss) <- mapAndUnzip3M go args
- ; alpha <- newFlexiTyVar (typeKind ty)
- ; let alphaTy = mkTyVarTy alpha
- ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy
- ; let thisRewriteFam = RewriteFam
- { rwi_fam = con
- , rwi_args = args'
- , rwi_right = alphaTy
- , rwi_co = mkWantedCo cotv
- , rwi_loc = tci_loc inst
- , rwi_name = tci_name inst
- , rwi_swapped = True
- }
- ; return (alphaTy,
- mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv,
- thisRewriteFam : concat args_eqss)
- }
-
- -- datatype constructor application => flatten subtypes
- -- NB: Special cased for efficiency - could be handled as type application
- go ty@(TyConApp con args)
- | not (isSynFamilyTyCon con) -- don't match oversaturated family apps
- = do { (args', cargs, args_eqss) <- mapAndUnzip3M go args
- ; let args_eqs = concat args_eqss
- ; if null args_eqs
- then -- unchanged, keep the old type with folded synonyms
- return (ty, ty, [])
- else
- return (mkTyConApp con args',
- mkTyConApp con cargs,
- args_eqs)
- }
-
- -- function type => flatten subtypes
- -- NB: Special cased for efficiency - could be handled as type application
- go ty@(FunTy ty_l ty_r)
- = do { (ty_l', co_l, eqs_l) <- go ty_l
- ; (ty_r', co_r, eqs_r) <- go ty_r
- ; if null eqs_l && null eqs_r
- then -- unchanged, keep the old type with folded synonyms
- return (ty, ty, [])
- else
- return (mkFunTy ty_l' ty_r',
- mkFunTy co_l co_r,
- eqs_l ++ eqs_r)
- }
-
- -- type application => flatten subtypes
- go ty
- | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
- -- need to use the smart split as ty may be an
- -- oversaturated family application
- = do { (ty_l', co_l, eqs_l) <- go ty_l
- ; (ty_r', co_r, eqs_r) <- go ty_r
- ; if null eqs_l && null eqs_r
- then -- unchanged, keep the old type with folded synonyms
- return (ty, ty, [])
- else
- return (mkAppTy ty_l' ty_r',
- mkAppTy co_l co_r,
- eqs_l ++ eqs_r)
- }
-
- -- forall type => panic if the body contains a type family
- -- !!!TODO: As long as the family does not contain a quantified variable
- -- we might pull it out, but what if it does contain a quantified
- -- variable???
- go ty@(ForAllTy _ body)
- | null (tyFamInsts body)
- = return (ty, ty, [])
- | otherwise
- = panic "TcTyFuns.flattenType: synonym family in a rank-n type"
-
- -- predicate type => handle like a datatype constructor application
- go (PredTy (ClassP cls tys))
- = do { (tys', ctys, tys_eqss) <- mapAndUnzip3M go tys
- ; let tys_eqs = concat tys_eqss
- ; if null tys_eqs
- then -- unchanged, keep the old type with folded synonyms
- return (ty, ty, [])
- else
- return (PredTy (ClassP cls tys'),
- PredTy (ClassP cls ctys),
- tys_eqs)
- }
-
- -- implicit parameter => flatten subtype
- go ty@(PredTy (IParam ipn ity))
- = do { (ity', co, eqs) <- go ity
- ; if null eqs
- then return (ty, ty, [])
- else return (PredTy (IParam ipn ity'),
- PredTy (IParam ipn co),
- eqs)
- }
-
- -- we should never see a equality
- go (PredTy (EqPred _ _))
- = panic "TcTyFuns.flattenType: malformed type"
-
- go _ = panic "TcTyFuns: suppress bogus warning"
-
-adjustCoercions :: EqInstCo -- coercion of original equality
- -> Coercion -- coercion witnessing the left rewrite
- -> Coercion -- coercion witnessing the right rewrite
- -> (Type, Type) -- types of flattened equality
- -> [RewriteInst] -- equalities from flattening
- -> TcM (EqInstCo, -- coercion for flattened equality
- [RewriteInst]) -- final equalities from flattening
--- Depending on whether we flattened a local or wanted equality, that equality's
--- coercion and that of the new equalities produced during flattening are
--- adjusted .
-adjustCoercions (Left cotv) co1 co2 (ty_l, ty_r) all_eqs
- -- wanted => generate a fresh coercion variable for the flattened equality
- = do { cotv' <- newMetaCoVar ty_l ty_r
- ; bindMetaTyVar cotv $
- (co1 `mkTransCoercion` TyVarTy cotv' `mkTransCoercion` co2)
- ; return (Left cotv', all_eqs)
- }
-
-adjustCoercions co@(Right _) _co1 _co2 _eqTys all_eqs
- -- local => turn all new equalities into locals and update (but not zonk)
- -- the skolem
- = do { all_eqs' <- mapM wantedToLocal all_eqs
- ; return (co, all_eqs')
- }
-
-mkDictBind :: Inst -- original instance
- -> Bool -- is this a wanted contraint?
- -> Coercion -- coercion witnessing the rewrite
- -> PredType -- coerced predicate
- -> TcM (Inst, -- new inst
- TcDictBinds) -- binding for coerced dictionary
-mkDictBind dict isWanted rewriteCo pred
- = do { dict' <- newCtGiven loc pred
- -- relate the old inst to the new one
- -- target_dict = source_dict `cast` st_co
- ; let (target_dict, source_dict, st_co)
- | isWanted = (dict, dict', mkSymCoercion rewriteCo)
- | otherwise = (dict', dict, rewriteCo)
- -- we have
- -- co :: dict ~ dict'
- -- hence, if isWanted
- -- dict = dict' `cast` sym co
- -- else
- -- dict' = dict `cast` co
- expr = HsVar $ instToId source_dict
- cast_expr = HsWrap (WpCast st_co) expr
- rhs = L (instLocSpan loc) cast_expr
- binds = instToDictBind target_dict rhs
- ; return (dict', binds)
- }
- where
- loc = tci_loc dict
-
--- gamma ::^l Fam args ~ alpha
--- => gamma ::^w Fam args ~ alpha, with alpha := Fam args & gamma := Fam args
--- (the update of alpha will not be apparent during propagation, as we
--- never follow the indirections of meta variables; it will be revealed
--- when the equality is zonked)
---
--- NB: It's crucial to update *both* alpha and gamma, as gamma may already
--- have escaped into some other coercions during normalisation.
---
--- We do actually update alpha and gamma by side effect (instead of
--- only remembering the binding with `bindMetaTyVar', as we do for all
--- other tyvars). We can do this as the side effects are strictly
--- *local*; we know that both alpha and gamma were just a moment ago
--- introduced by normalisation.
---
-wantedToLocal :: RewriteInst -> TcM RewriteInst
-wantedToLocal eq@(RewriteFam {rwi_fam = fam,
- rwi_args = args,
- rwi_right = TyVarTy alpha,
- rwi_co = Left gamma})
- = do { writeMetaTyVar alpha (mkTyConApp fam args)
- ; writeMetaTyVar gamma (mkTyConApp fam args)
- ; return $ eq {rwi_co = mkGivenCo $ mkTyVarTy gamma}
- }
-wantedToLocal _ = panic "TcTyFuns.wantedToLocal"
-\end{code}
-
-
-%************************************************************************
-%* *
- Propagation of equalities
-%* *
-%************************************************************************
-
-Apply the propagation rules exhaustively.
-
-\begin{code}
-propagate :: [RewriteInst] -> EqConfig -> TcM EqConfig
-propagate [] eqCfg = return eqCfg
-propagate (eq:eqs) eqCfg
- = do { optEqs <- applyTop eq
- ; case optEqs of
-
- -- Top applied to 'eq' => retry with new equalities
- Just eqs2 -> propagate (eqs2 ++ eqs) eqCfg
-
- -- Top doesn't apply => try subst rules with all other
- -- equalities, after that 'eq' can go into the residual list
- Nothing -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
- ; propagate eqs' (eqCfg' `addEq` eq)
- }
- }
-
-applySubstRules :: RewriteInst -- currently considered eq
- -> [RewriteInst] -- todo eqs list
- -> EqConfig -- residual
- -> TcM ([RewriteInst], EqConfig) -- new todo & residual
-applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
- = do { (newEqs_t, unchangedEqs_t) <- mapSubstRules eq todoEqs
- ; (newEqs_r, unchangedEqs_r) <- mapSubstRules eq resEqs
- ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
- eqConfig {eqs = unchangedEqs_r})
- }
-
-mapSubstRules :: RewriteInst -- try substituting this equality
- -> [RewriteInst] -- into these equalities
- -> TcM ([RewriteInst], [RewriteInst])
-mapSubstRules eq eqs
- = do { (newEqss, unchangedEqss) <- mapAndUnzipM (substRules eq) eqs
- ; return (concat newEqss, concat unchangedEqss)
- }
- where
- substRules eq1 eq2
- = do {traceTc $ hang (ptext (sLit "Trying subst rules with"))
- 4 (ppr eq1 $$ ppr eq2)
-
- -- try the SubstFam rule
- ; optEqs <- applySubstFam eq1 eq2
- ; case optEqs of
- Just eqs -> return (eqs, [])
- Nothing -> do
- { -- try the SubstVarVar rule
- optEqs <- applySubstVarVar eq1 eq2
- ; case optEqs of
- Just eqs -> return (eqs, [])
- Nothing -> do
- { -- try the SubstVarFam rule
- optEqs <- applySubstVarFam eq1 eq2
- ; case optEqs of
- Just eq -> return ([eq], [])
- Nothing -> return ([], [eq2])
- -- if no rule matches, we return the equlity we tried to
- -- substitute into unchanged
- }}}
-\end{code}
-
-Attempt to apply the Top rule. The rule is
-
- co :: F t1..tn ~ t
- =(Top)=>
- co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'
-
-where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.
-
-Returns Nothing if the rule could not be applied. Otherwise, the resulting
-equality is normalised and a list of the normal equalities is returned.
-
-\begin{code}
-applyTop :: RewriteInst -> TcM (Maybe [RewriteInst])
-
-applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
- = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
- ; case optTyCo of
- Nothing -> return Nothing
- Just (lhs, rewrite_co)
- -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
- ; eq' <- deriveEqInst eq lhs rhs co'
- ; liftM Just $ normEqInst eq'
- }
- }
- where
- co = rwi_co eq
- rhs = rwi_right eq
-
-applyTop _ = return Nothing
-\end{code}
-
-Attempt to apply the SubstFam rule. The rule is
-
- co1 :: F t1..tn ~ t & co2 :: F t1..tn ~ s
- =(SubstFam)=>
- co1 :: F t1..tn ~ t & co2' :: t ~ s with co2 = co1 |> co2'
-
-where co1 may be a wanted only if co2 is a wanted, too.
-
-Returns Nothing if the rule could not be applied. Otherwise, the equality
-co2' is normalised and a list of the normal equalities is returned. (The
-equality co1 is not returned as it remain unaltered.)
-
-\begin{code}
-applySubstFam :: RewriteInst
- -> RewriteInst
- -> TcM (Maybe ([RewriteInst]))
-applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
- eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
-
- -- rule matches => rewrite
- | fam1 == fam2 && tcEqTypes args1 args2 &&
- (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
- = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
- ; eq2' <- deriveEqInst eq2 lhs rhs co2'
- ; liftM Just $ normEqInst eq2'
- }
-
- -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
- | fam1 == fam2 && tcEqTypes args1 args2 &&
- (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
- = return $ Just [eq2]
-
- where
- lhs = rwi_right eq1
- rhs = rwi_right eq2
- co1 = eqInstCoType (rwi_co eq1)
- co2 = rwi_co eq2
-
-applySubstFam _ _ = return Nothing
-\end{code}
-
-Attempt to apply the SubstVarVar rule. The rule is
-
- co1 :: x ~ t & co2 :: x ~ s
- =(SubstVarVar)=>
- co1 :: x ~ t & co2' :: t ~ s with co2 = co1 |> co2'
-
-where co1 may be a wanted only if co2 is a wanted, too.
-
-Returns Nothing if the rule could not be applied. Otherwise, the equality
-co2' is normalised and a list of the normal equalities is returned. (The
-equality co1 is not returned as it remain unaltered.)
-
-\begin{code}
-applySubstVarVar :: RewriteInst -> RewriteInst -> TcM (Maybe [RewriteInst])
-applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
- eq2@(RewriteVar {rwi_var = tv2})
-
- -- rule matches => rewrite
- | tv1 == tv2 &&
- (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
- = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
- ; eq2' <- deriveEqInst eq2 lhs rhs co2'
- ; liftM Just $ normEqInst eq2'
- }
-
- -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
- | tv1 == tv2 &&
- (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
- = return $ Just [eq2]
-
- where
- lhs = rwi_right eq1
- rhs = rwi_right eq2
- co1 = eqInstCoType (rwi_co eq1)
- co2 = rwi_co eq2
-
-applySubstVarVar _ _ = return Nothing
-\end{code}
-
-Attempt to apply the SubstVarFam rule. The rule is
-
- co1 :: x ~ t & co2 :: F s1..sn ~ s
- =(SubstVarFam)=>
- co1 :: x ~ t & co2' :: [t/x](F s1..sn) ~ s
- with co2 = [co1/x](F s1..sn) |> co2'
-
-where x occurs in F s1..sn. (co1 may be local or wanted.)
-
-Returns Nothing if the rule could not be applied. Otherwise, the equality
-co2' is returned. (The equality co1 is not returned as it remain unaltered.)
-
-\begin{code}
-applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
-
- -- rule matches => rewrite
-applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
- eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
- | tv1 `elemVarSet` tyVarsOfTypes args2
- = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2)
- args2' = substTysWith [tv1] [rhs1] args2
- lhs2 = mkTyConApp fam2 args2'
- ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2)
- ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'})
- }
- where
- rhs1 = rwi_right eq1
- rhs2 = rwi_right eq2
- co1 = eqInstCoType (rwi_co eq1)
- co2 = rwi_co eq2
-
- -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
-applySubstVarFam (RewriteFam {rwi_args = args1})
- eq2@(RewriteVar {rwi_var = tv2})
- | tv2 `elemVarSet` tyVarsOfTypes args1
- = return $ Just eq2
-
-applySubstVarFam _ _ = return Nothing
-\end{code}
-
-
-%************************************************************************
-%* *
- Finalisation of equalities
-%* *
-%************************************************************************
-
-Exhaustive substitution of all variable equalities of the form co :: x ~ t
-(both local and wanted) into the right-hand sides of all other equalities and
-of family equalities of the form co :: F t1..tn ~ alpha into both sides of all
-other *family* equalities. This may lead to recursive equalities; i.e., (1)
-we need to apply the substitution implied by one equality exhaustively before
-turning to the next and (2) we need an occurs check.
-
-We also apply the same substitutions to the local and wanted class and IP
-dictionaries.
-
-We perform the substitutions in two steps:
-
- Step A: Substitute variable equalities into the right-hand sides of all
- other equalities (but wanted only into wanteds) and into class and IP
- constraints (again wanteds only into wanteds).
-
- Step B: Substitute wanted family equalities `co :: F t1..tn ~ alpha', where
- 'alpha' is a skolem flexible (i.e., not free in the environment),
- into the right-hand sides of all wanted variable equalities and into
- both sides of all wanted family equalities.
-
- Step C: Substitute the remaining wanted family equalities `co :: F t1..tn ~
- alpha' into the right-hand sides of all wanted variable equalities
- and into both sides of all wanted family equalities.
-
-In inference mode, we do not substitute into variable equalities in Steps B & C.
-
-The treatment of flexibles in wanteds is quite subtle. We absolutely want to
-substitute variable equalities first; e.g., consider
-
- F s ~ alpha, alpha ~ t
-
-If we don't substitute `alpha ~ t', we may instantiate `t' with `F s' instead.
-This would be bad as `F s' is less useful, eg, as an argument to a class
-constraint.
-
-The restriction on substituting locals is necessary due to examples, such as
-
- F delta ~ alpha, F alpha ~ delta,
-
-where `alpha' is a skolem flexible and `delta' a environment flexible. We need
-to produce `F (F delta) ~ delta' (and not `F (F alpha) ~ alpha'). Otherwise,
-we may wrongly claim to having performed an improvement, which can lead to
-non-termination of the combined class-family solver.
-
-We do also substitute flexibles, as in `alpha ~ t' into class constraints.
-When `alpha' is later instantiated, we'd get the same effect, but in the
-meantime the class constraint would miss some information, which would be a
-problem in an integrated equality-class solver.
-
-NB:
-* Given that we apply the substitution corresponding to a single equality
- exhaustively, before turning to the next, and because we eliminate recursive
- equalities, all opportunities for subtitution will have been exhausted after
- we have considered each equality once.
-
-\begin{code}
-substitute :: [RewriteInst] -- equalities
- -> [Inst] -- local class dictionaries
- -> [Inst] -- wanted class dictionaries
- -> Bool -- True ~ checking mode; False ~ inference
- -> TyVarSet -- flexibles free in the environment
- -> TcM ([RewriteInst], -- equalities after substitution
- TcDictBinds, -- all newly generated dictionary bindings
- [Inst], -- local dictionaries after substitution
- [Inst]) -- wanted dictionaries after substitution
-substitute eqs locals wanteds checkingMode freeFlexibles
- = -- We achieve the sequencing of "Step A", "Step B", and "Step C" above by
- -- sorting the equalities appropriately: first all variable, then all
- -- family/skolem, and then the remaining family equalities.
- let (var_eqs, fam_eqs) = partition isRewriteVar eqs
- (fam_skolem_eqs, fam_eqs_rest) = partition isFamSkolemEq fam_eqs
- in
- subst (var_eqs ++ fam_skolem_eqs ++ fam_eqs_rest) [] emptyBag locals wanteds
- where
- isFamSkolemEq (RewriteFam {rwi_right = ty})
- | Just tv <- tcGetTyVar_maybe ty = not (tv `elemVarSet` freeFlexibles)
- isFamSkolemEq _ = False
-
- subst [] res binds locals wanteds
- = return (res, binds, locals, wanteds)
-
- -- co :: x ~ t
- subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs)
- res binds locals wanteds
- = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteVar]:") <+>
- ppr eq
-
- -- create the substitution
- ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
- tySubst = zipOpenTvSubst [tv] [ty]
-
- -- substitute into all other equalities
- ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
- ; res' <- mapM (substEq eq coSubst tySubst) res
-
- -- only substitute local equalities into local dictionaries
- ; (lbinds, locals') <- if not (isWantedCo co)
- then
- mapAndUnzipM
- (substDict eq coSubst tySubst False)
- locals
- else
- return ([], locals)
-
- -- substitute all equalities into wanteds dictionaries
- ; (wbinds, wanteds') <- mapAndUnzipM
- (substDict eq coSubst tySubst True)
- wanteds
-
- ; let binds' = unionManyBags $ binds : lbinds ++ wbinds
- ; subst eqs' (eq:res') binds' locals' wanteds'
- }
-
- -- co ::^w F t1..tn ~ alpha
- subst (eq@(RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = ty,
- rwi_co = co}):eqs)
- res binds locals wanteds
- | Just tv <- tcGetTyVar_maybe ty
- , isMetaTyVar tv
- , isWantedCo co
- = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteFam]:") <+>
- ppr eq
-
- -- create the substitution
- ; let coSubst = zipOpenTvSubst [tv] [mkSymCoercion $ eqInstCoType co]
- tySubst = zipOpenTvSubst [tv] [mkTyConApp fam args]
-
- -- substitute into other wanted equalities (`substEq' makes sure
- -- that we only substitute into wanteds)
- ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
- ; res' <- mapM (substEq eq coSubst tySubst) res
-
- ; subst eqs' (eq:res') binds locals wanteds
- }
-
- subst (eq:eqs) res binds locals wanteds
- = subst eqs (eq:res) binds locals wanteds
-
- -- We have, co :: tv ~ ty
- -- => apply [ty/tv] to right-hand side of eq2
- -- (but only if tv actually occurs in the right-hand side of eq2
- -- and if eq2 is a local, co :: tv ~ ty needs to be a local, too)
- substEq (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co})
- coSubst tySubst eq2
- | tv `elemVarSet` tyVarsOfType (rwi_right eq2)
- && (isWantedRewriteInst eq2 || not (isWantedCo co))
- = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
- right2' = substTy tySubst (rwi_right eq2)
- left2 = case eq2 of
- RewriteVar {rwi_var = tv2} -> mkTyVarTy tv2
- RewriteFam {rwi_fam = fam,
- rwi_args = args} ->mkTyConApp fam args
- ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
- ; case eq2 of
- RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty
- -> occurCheckErr left2 right2'
- _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
- }
-
- -- We have, co ::^w F t1..tn ~ tv
- -- => apply [F t1..tn/tv] to eq2
- -- (but only if tv actually occurs in eq2
- -- and eq2 is a wanted equality
- -- and we are either in checking mode or eq2 is a family equality)
- substEq (RewriteFam {rwi_args = args, rwi_right = ty})
- coSubst tySubst eq2
- | Just tv <- tcGetTyVar_maybe ty
- , tv `elemVarSet` tyVarsOfRewriteInst eq2
- , isWantedRewriteInst eq2
- , checkingMode || not (isRewriteVar eq2)
- = do { -- substitute into the right-hand side
- ; let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
- right2' = substTy tySubst (rwi_right eq2)
- left2 = case eq2 of
- RewriteVar {rwi_var = tv2} -> mkTyVarTy tv2
- RewriteFam {rwi_fam = fam,
- rwi_args = args} -> mkTyConApp fam args
- ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
- ; case eq2 of
- RewriteVar {rwi_var = tv2}
- -- variable equality: perform an occurs check
- | tv2 `elemVarSet` tyVarsOfTypes args
- -> occurCheckErr left2 right2'
- | otherwise
- -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
- RewriteFam {rwi_fam = fam}
- -- family equality: substitute also into the left-hand side
- -> do { let co1Subst = substTy coSubst left2
- args2' = substTys tySubst (rwi_args eq2)
- left2' = mkTyConApp fam args2'
- ; co2'' <- mkRightTransEqInstCo co2' co1Subst
- (left2', right2')
- ; return $ eq2 {rwi_args = args2', rwi_right = right2',
- rwi_co = co2''}
- }
- }
-
- -- unchanged
- substEq _ _ _ eq2
- = return eq2
-
- -- We have, co :: tv ~ ty
- -- => apply [ty/tv] to dictionary predicate
- -- (but only if tv actually occurs in the predicate)
- substDict (RewriteVar {rwi_var = tv}) coSubst tySubst isWanted dict
- | isClassDict dict
- , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
- = do { let co1Subst = PredTy (substPred coSubst (tci_pred dict))
- pred' = substPred tySubst (tci_pred dict)
- ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred'
- ; return (binds, dict')
- }
-
- -- unchanged
- substDict _ _ _ _ dict
- = return (emptyBag, dict)
--- !!!TODO: Still need to substitute into IP constraints.
-\end{code}
-
-For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
-alpha, we record a binding of alpha with t or a, respectively, and for co :=
-id. We do the same for equalities of the form co :: F t1..tn ~ alpha unless
-we are in inference mode and alpha appears in the environment - i.e., it is
-not a flexible introduced by flattening locals or it is local, but was
-propagated into the environment by the instantiation of a variable equality.
-
-We proceed in two phases: (1) first we consider all variable equalities and then
-(2) we consider all family equalities. The two phase structure is required as
-the recorded variable equalities determine which skolems flexibles escape, and
-hence, which family equalities may be recorded as bindings.
-
-We return all wanted equalities for which we did not generate a binding.
-(These can be skolem variable equalities, cyclic variable equalities, and
-family equalities.)
-
-We don't update any meta variables. Instead, instantiation simply implies
-putting a type variable binding into the binding pool of TcM.
-
-NB:
- * We may encounter filled flexibles due to the instant filling of local
- skolems in local-given constraints during flattening.
- * Be careful with SigTVs. They can only be instantiated with other SigTVs or
- rigid skolems.
-
-\begin{code}
-bindAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM [Inst]
-bindAndExtract eqs checkingMode freeFlexibles
- = do { traceTc $ hang (ptext (sLit "bindAndExtract:"))
- 4 (ppr eqs $$ ppr freeFlexibles)
- ; residuals1 <- mapMaybeM instVarEq (filter isWantedRewriteInst eqs)
- ; escapingSkolems <- getEscapingSkolems
- ; let newFreeFlexibles = freeFlexibles `unionVarSet` escapingSkolems
- ; residuals2 <- mapMaybeM (instFamEq newFreeFlexibles) residuals1
- ; mapM rewriteInstToInst residuals2
- }
- where
- -- NB: we don't have to transitively chase the relation as the substitution
- -- process applied before generating the bindings was exhaustive
- getEscapingSkolems
- = do { tybinds_rel <- getTcTyVarBindsRelation
- ; return (unionVarSets . map snd . filter isFree $ tybinds_rel)
- }
- where
- isFree (tv, _) = tv `elemVarSet` freeFlexibles
-
- -- co :: alpha ~ t or co :: a ~ alpha
- instVarEq eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
- = do { flexi_tv1 <- isFlexible tv1
- ; maybe_flexi_tv2 <- isFlexibleTy ty2
- ; case (flexi_tv1, maybe_flexi_tv2) of
- (True, Just tv2)
- | isSigTyVar tv1 && isSigTyVar tv2
- -> -- co :: alpha ~ beta, where both a SigTvs
- doInst (rwi_swapped eq) tv1 ty2 co eq
- (True, Nothing)
- | Just tv2 <- tcGetTyVar_maybe ty2
- , isSigTyVar tv1
- , isSkolemTyVar tv2
- -> -- co :: alpha ~ a, where alpha is a SigTv
- doInst (rwi_swapped eq) tv1 ty2 co eq
- (True, _)
- | not (isSigTyVar tv1)
- -> -- co :: alpha ~ t, where alpha is not a SigTv
- doInst (rwi_swapped eq) tv1 ty2 co eq
- (False, Just tv2)
- | isSigTyVar tv2
- , isSkolemTyVar tv1
- -> -- co :: a ~ alpha, where alpha is a SigTv
- doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
- | not (isSigTyVar tv2)
- -> -- co :: a ~ alpha, where alpha is not a SigTv
- -- ('a' may be filled)
- doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
- _ -> return $ Just eq
- }
- instVarEq eq = return $ Just eq
-
- -- co :: F args ~ alpha,
- -- and we are either in checking mode or alpha is a skolem flexible that
- -- doesn't escape
- instFamEq newFreeFlexibles eq@(RewriteFam {rwi_fam = fam, rwi_args = args,
- rwi_right = ty2, rwi_co = co})
- | Just tv2 <- tcGetTyVar_maybe ty2
- , checkingMode || not (tv2 `elemVarSet` newFreeFlexibles)
- = do { flexi_tv2 <- isFlexible tv2
- ; if flexi_tv2
- then
- doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
- else
- return $ Just eq
- }
- instFamEq _ eq = return $ Just eq
-
- -- tv is a meta var, but not a SigTV and not filled
- isFlexible tv
- | isMetaTyVar tv = liftM isFlexi $ readMetaTyVar tv
- | otherwise = return False
-
- -- type is a tv that is a meta var, but not a SigTV and not filled
- isFlexibleTy ty
- | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible tv
- ; if flexi then return $ Just tv
- else return Nothing
- }
- | otherwise = return Nothing
-
- doInst _swapped _tv _ty (Right ty) _eq
- = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty)
- doInst swapped tv ty (Left cotv) eq
- = do { lookupTV <- lookupTcTyVar tv
- ; bMeta swapped tv lookupTV ty cotv
- }
- where
- -- Try to create a binding for a meta variable. There is *no* need to
- -- consider reorienting the underlying equality; `checkOrientation'
- -- makes sure that we get variable-variable equalities only in the
- -- appropriate orientation.
- --
- bMeta :: Bool -- is this a swapped equality?
- -> TcTyVar -- tyvar to instantiate
- -> LookupTyVarResult -- lookup result of that tyvar
- -> TcType -- to to instantiate tyvar with
- -> TcTyVar -- coercion tyvar of current equality
- -> TcM (Maybe RewriteInst) -- returns the original equality if
- -- the tyvar could not be instantiated,
- -- and hence, the equality must be kept
-
- -- meta variable has been filled already
- -- => this should never happen due to the use of `isFlexible' above
- bMeta _swapped tv (IndirectTv fill_ty) ty _cotv
- = pprPanic "TcTyFuns.bMeta" $
- ptext (sLit "flexible") <+> ppr tv <+>
- ptext (sLit "already filled with") <+> ppr fill_ty <+>
- ptext (sLit "meant to fill with") <+> ppr ty
-
- -- type variable meets type variable
- -- => `checkOrientation' already ensures that it is fine to instantiate
- -- tv1 with tv2, but chase tv2's instantiations if necessary, so that
- -- we eventually can perform a kinds check in bMetaInst
- -- NB: tv's instantiations won't alter the orientation in which we
- -- want to instantiate as they either constitute a family
- -- application or are themselves due to a properly oriented
- -- instantiation
- bMeta swapped tv1 details1@(DoneTv (MetaTv _ _)) ty@(TyVarTy tv2) cotv
- = do { lookupTV2 <- lookupTcTyVar tv2
- ; case lookupTV2 of
- IndirectTv ty' -> bMeta swapped tv1 details1 ty' cotv
- DoneTv _ -> bMetaInst swapped tv1 ty cotv
- }
-
- -- updatable meta variable meets non-variable type
- -- => occurs check, monotype check, and kinds match check, then bind
- bMeta swapped tv (DoneTv (MetaTv _ _ref)) non_tv_ty cotv
- = bMetaInst swapped tv non_tv_ty cotv
-
- bMeta _ _ _ _ _ = panic "TcTyFuns.bMeta"
-
- -- We know `tv' can be instantiated; check that `ty' is alright for
- -- instantiating `tv' with and then record a binding; we return the
- -- original equality if it is cyclic through a synonym family
- bMetaInst swapped tv ty cotv
- = do { -- occurs + monotype check
- ; mb_ty' <- checkTauTvUpdate tv ty
-
- ; case mb_ty' of
- Nothing ->
- -- there may be a family in non_tv_ty due to an unzonked,
- -- but updated skolem for a local equality
- -- (cf `wantedToLocal')
- return $ Just eq
- Just ty' ->
- do { checkKinds swapped tv ty'
- ; bindMetaTyVar tv ty' -- bind meta var
- ; bindMetaTyVar cotv ty' -- bind co var
- ; return Nothing
- }
- }
-\end{code}
-
-
-%************************************************************************
-%* *
-\section{Errors}
-%* *
-%************************************************************************
-
-The infamous couldn't match expected type soandso against inferred type
-somethingdifferent message.
-
-\begin{code}
-eqInstMisMatch :: Inst -> TcM a
-eqInstMisMatch inst
- = ASSERT( isEqInst inst )
- setInstCtxt (instLoc inst) $ failWithMisMatch ty_act ty_exp
- where
- (ty_act, ty_exp) = eqInstTys inst
-
------------------------
-failWithMisMatch :: TcType -> TcType -> TcM a
--- Generate the message when two types fail to match,
--- going to some trouble to make it helpful.
--- The argument order is: actual type, expected type
-failWithMisMatch ty_act ty_exp
- = do { env0 <- tcInitTidyEnv
- ; ty_exp <- zonkTcType ty_exp
- ; ty_act <- zonkTcType ty_act
- ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
- }
-
-misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
-misMatchMsg env0 (ty_act, ty_exp)
- = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
- (env2, pp_act, extra_act) = ppr_ty env1 ty_act
- msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp,
- nest 7 $
- ptext (sLit "against inferred type") <+> pp_act],
- nest 2 (extra_exp $$ extra_act $$ extra_tyfun) ]
- -- See Note [Non-injective type functions]
- in
- (env2, msg)
-
- where
- extra_tyfun
- = case (tcSplitTyConApp_maybe ty_act, tcSplitTyConApp_maybe ty_exp) of
- (Just (tc_act,_), Just (tc_exp,_)) | tc_act == tc_exp
- -> if isOpenSynTyCon tc_act then pp_open_tc tc_act
- else WARN( True, ppr tc_act) -- If there's a mis-match, then
- empty -- it should be a family
- _ -> empty
-
-
- pp_open_tc tc = ptext (sLit "NB:") <+> quotes (ppr tc)
- <+> ptext (sLit "is a type function") <> pp_inj
- where
- pp_inj | isInjectiveTyCon tc = empty
- | otherwise = ptext (sLit (", and may not be injective"))
-
- ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
- ppr_ty env ty
- = let (env1, tidy_ty) = tidyOpenType env ty
- (env2, extra) = ppr_extra env1 tidy_ty
- in
- (env2, quotes (ppr tidy_ty), extra)
-
- -- (ppr_extra env ty) shows extra info about 'ty'
- ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
- ppr_extra env (TyVarTy tv)
- | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
- = (env1, pprSkolTvBinding tv1)
- where
- (env1, tv1) = tidySkolemTyVar env tv
-
- ppr_extra env _ty = (env, empty) -- Normal case
-\end{code}
-
-Note [Non-injective type functions]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-It's very confusing to get a message like
- Couldn't match expected type `Depend s'
- against inferred type `Depend s1'
-so pp_open_tc adds:
- NB: `Depend' is type function, and hence may not be injective
-
-Warn of loopy local equalities that were dropped.
-
-\begin{code}
-warnDroppingLoopyEquality :: TcType -> TcType -> TcM ()
-warnDroppingLoopyEquality ty1 ty2
- = do { env0 <- tcInitTidyEnv
- ; ty1 <- zonkTcType ty1
- ; ty2 <- zonkTcType ty2
- ; let (env1 , tidy_ty1) = tidyOpenType env0 ty1
- (_env2, tidy_ty2) = tidyOpenType env1 ty2
- ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality"))
- 2 (quotes (ppr tidy_ty1 <+> text "~" <+> ppr tidy_ty2))
- }
-\end{code}
+++ /dev/null
-{-# LANGUAGE NamedFieldPuns #-}
-
--- | The Vectorisation monad.
-module VectMonad (
- VM,
-
- noV, traceNoV, ensureV, traceEnsureV, tryV, maybeV, traceMaybeV, orElseV,
- onlyIfV, fixV, localV, closedV,
- initV, cantVectorise, maybeCantVectorise, maybeCantVectoriseM,
- liftDs,
- cloneName, cloneId, cloneVar,
- newExportedVar, newLocalVar, newLocalVars, newDummyVar, newTyVar,
-
- Builtins(..), sumTyCon, prodTyCon, prodDataCon,
- selTy, selReplicate, selPick, selTags, selElements,
- combinePDVar, scalarZip, closureCtrFun,
- builtin, builtins,
-
- setFamInstEnv,
- readGEnv, setGEnv, updGEnv,
-
- readLEnv, setLEnv, updLEnv,
-
- getBindName, inBind,
-
- lookupVar, defGlobalVar, globalScalars,
- lookupTyCon, defTyCon,
- lookupDataCon, defDataCon,
- lookupTyConPA, defTyConPA, defTyConPAs,
- lookupTyConPR,
- lookupBoxedTyCon,
- lookupPrimMethod, lookupPrimPArray,
- lookupTyVarPA, defLocalTyVar, defLocalTyVarWithPA, localTyVars,
-
- lookupInst, lookupFamInst
-) where
-
-#include "HsVersions.h"
-
-import VectBuiltIn
-import Vectorise.Env
-
-import HscTypes hiding ( MonadThings(..) )
-import Module ( PackageId )
-import CoreSyn
-import Class
-import TyCon
-import DataCon
-import Type
-import Var
-import VarSet
-import VarEnv
-import Id
-import Name
-import NameEnv
-
-import DsMonad
-
-import InstEnv
-import FamInstEnv
-
-import Outputable
-import FastString
-import SrcLoc ( noSrcSpan )
-
-import Control.Monad
-
--- | Indicates what scope something (a variable) is in.
-data Scope a b = Global a | Local b
-
-
--- | The global environment.
-data GlobalEnv = GlobalEnv {
- -- | Mapping from global variables to their vectorised versions.
- --
- global_vars :: VarEnv Var
-
- -- | Purely scalar variables. Code which mentions only these
- -- variables doesn't have to be lifted.
- , global_scalars :: VarSet
-
- -- | Exported variables which have a vectorised version
- --
- , global_exported_vars :: VarEnv (Var, Var)
-
- -- | Mapping from TyCons to their vectorised versions.
- -- TyCons which do not have to be vectorised are mapped to
- -- themselves.
- --
- , global_tycons :: NameEnv TyCon
-
- -- | Mapping from DataCons to their vectorised versions
- --
- , global_datacons :: NameEnv DataCon
-
- -- | Mapping from TyCons to their PA dfuns
- --
- , global_pa_funs :: NameEnv Var
-
- -- | Mapping from TyCons to their PR dfuns
- , global_pr_funs :: NameEnv Var
-
- -- | Mapping from unboxed TyCons to their boxed versions
- , global_boxed_tycons :: NameEnv TyCon
-
- -- | External package inst-env & home-package inst-env for class
- -- instances
- --
- , global_inst_env :: (InstEnv, InstEnv)
-
- -- | External package inst-env & home-package inst-env for family
- -- instances
- --
- , global_fam_inst_env :: FamInstEnvs
-
- -- | Hoisted bindings
- , global_bindings :: [(Var, CoreExpr)]
- }
-
--- | The local environment.
-data LocalEnv = LocalEnv {
- -- Mapping from local variables to their vectorised and
- -- lifted versions
- --
- local_vars :: VarEnv (Var, Var)
-
- -- In-scope type variables
- --
- , local_tyvars :: [TyVar]
-
- -- Mapping from tyvars to their PA dictionaries
- , local_tyvar_pa :: VarEnv CoreExpr
-
- -- Local binding name
- , local_bind_name :: FastString
- }
-
-
--- | Create an initial global environment
-initGlobalEnv :: VectInfo -> (InstEnv, InstEnv) -> FamInstEnvs -> GlobalEnv
-initGlobalEnv info instEnvs famInstEnvs
- = GlobalEnv {
- global_vars = mapVarEnv snd $ vectInfoVar info
- , global_scalars = emptyVarSet
- , global_exported_vars = emptyVarEnv
- , global_tycons = mapNameEnv snd $ vectInfoTyCon info
- , global_datacons = mapNameEnv snd $ vectInfoDataCon info
- , global_pa_funs = mapNameEnv snd $ vectInfoPADFun info
- , global_pr_funs = emptyNameEnv
- , global_boxed_tycons = emptyNameEnv
- , global_inst_env = instEnvs
- , global_fam_inst_env = famInstEnvs
- , global_bindings = []
- }
-
-
--- Operators on Global Environments -------------------------------------------
-extendImportedVarsEnv :: [(Var, Var)] -> GlobalEnv -> GlobalEnv
-extendImportedVarsEnv ps genv
- = genv { global_vars = extendVarEnvList (global_vars genv) ps }
-
-extendScalars :: [Var] -> GlobalEnv -> GlobalEnv
-extendScalars vs genv
- = genv { global_scalars = extendVarSetList (global_scalars genv) vs }
-
-setFamInstEnv :: FamInstEnv -> GlobalEnv -> GlobalEnv
-setFamInstEnv l_fam_inst genv
- = genv { global_fam_inst_env = (g_fam_inst, l_fam_inst) }
- where
- (g_fam_inst, _) = global_fam_inst_env genv
-
-extendTyConsEnv :: [(Name, TyCon)] -> GlobalEnv -> GlobalEnv
-extendTyConsEnv ps genv
- = genv { global_tycons = extendNameEnvList (global_tycons genv) ps }
-
-extendDataConsEnv :: [(Name, DataCon)] -> GlobalEnv -> GlobalEnv
-extendDataConsEnv ps genv
- = genv { global_datacons = extendNameEnvList (global_datacons genv) ps }
-
-extendPAFunsEnv :: [(Name, Var)] -> GlobalEnv -> GlobalEnv
-extendPAFunsEnv ps genv
- = genv { global_pa_funs = extendNameEnvList (global_pa_funs genv) ps }
-
-setPRFunsEnv :: [(Name, Var)] -> GlobalEnv -> GlobalEnv
-setPRFunsEnv ps genv
- = genv { global_pr_funs = mkNameEnv ps }
-
-setBoxedTyConsEnv :: [(Name, TyCon)] -> GlobalEnv -> GlobalEnv
-setBoxedTyConsEnv ps genv
- = genv { global_boxed_tycons = mkNameEnv ps }
-
-
--- | Create an empty local environment.
-emptyLocalEnv :: LocalEnv
-emptyLocalEnv = LocalEnv {
- local_vars = emptyVarEnv
- , local_tyvars = []
- , local_tyvar_pa = emptyVarEnv
- , local_bind_name = fsLit "fn"
- }
-
--- FIXME
-updVectInfo :: GlobalEnv -> TypeEnv -> VectInfo -> VectInfo
-updVectInfo env tyenv info
- = info {
- vectInfoVar = global_exported_vars env
- , vectInfoTyCon = mk_env typeEnvTyCons global_tycons
- , vectInfoDataCon = mk_env typeEnvDataCons global_datacons
- , vectInfoPADFun = mk_env typeEnvTyCons global_pa_funs
- }
- where
- mk_env :: NamedThing from =>
- (TypeEnv -> [from])
- -> (GlobalEnv -> NameEnv to)
- -> NameEnv (from,to)
- mk_env from_tyenv from_env = mkNameEnv [(name, (from,to))
- | from <- from_tyenv tyenv
- , let name = getName from
- , Just to <- [lookupNameEnv (from_env env) name]]
-
--- The Vectorisation Monad ----------------------------------------------------
-
--- Vectorisation can either succeed with new envionment and a value,
--- or return with failure.
---
-data VResult a = Yes GlobalEnv LocalEnv a | No
-
-newtype VM a = VM { runVM :: Builtins -> GlobalEnv -> LocalEnv -> DsM (VResult a) }
-
-instance Monad VM where
- return x = VM $ \_ genv lenv -> return (Yes genv lenv x)
- VM p >>= f = VM $ \bi genv lenv -> do
- r <- p bi genv lenv
- case r of
- Yes genv' lenv' x -> runVM (f x) bi genv' lenv'
- No -> return No
-
-
--- | Throw an error saying we can't vectorise something
-cantVectorise :: String -> SDoc -> a
-cantVectorise s d = pgmError
- . showSDocDump
- $ vcat [text "*** Vectorisation error ***",
- nest 4 $ sep [text s, nest 4 d]]
-
-maybeCantVectorise :: String -> SDoc -> Maybe a -> a
-maybeCantVectorise s d Nothing = cantVectorise s d
-maybeCantVectorise _ _ (Just x) = x
-
-maybeCantVectoriseM :: Monad m => String -> SDoc -> m (Maybe a) -> m a
-maybeCantVectoriseM s d p
- = do
- r <- p
- case r of
- Just x -> return x
- Nothing -> cantVectorise s d
-
-
--- Control --------------------------------------------------------------------
--- | Return some result saying we've failed.
-noV :: VM a
-noV = VM $ \_ _ _ -> return No
-
-traceNoV :: String -> SDoc -> VM a
-traceNoV s d = pprTrace s d noV
-
-
--- | If True then carry on, otherwise fail.
-ensureV :: Bool -> VM ()
-ensureV False = noV
-ensureV True = return ()
-
-
--- | If True then return the first argument, otherwise fail.
-onlyIfV :: Bool -> VM a -> VM a
-onlyIfV b p = ensureV b >> p
-
-traceEnsureV :: String -> SDoc -> Bool -> VM ()
-traceEnsureV s d False = traceNoV s d
-traceEnsureV _ _ True = return ()
-
-
--- | Try some vectorisation computaton.
--- If it succeeds then return Just the result,
--- otherwise return Nothing.
-tryV :: VM a -> VM (Maybe a)
-tryV (VM p) = VM $ \bi genv lenv ->
- do
- r <- p bi genv lenv
- case r of
- Yes genv' lenv' x -> return (Yes genv' lenv' (Just x))
- No -> return (Yes genv lenv Nothing)
-
-
-maybeV :: VM (Maybe a) -> VM a
-maybeV p = maybe noV return =<< p
-
-traceMaybeV :: String -> SDoc -> VM (Maybe a) -> VM a
-traceMaybeV s d p = maybe (traceNoV s d) return =<< p
-
-orElseV :: VM a -> VM a -> VM a
-orElseV p q = maybe q return =<< tryV p
-
-fixV :: (a -> VM a) -> VM a
-fixV f = VM (\bi genv lenv -> fixDs $ \r -> runVM (f (unYes r)) bi genv lenv )
- where
- -- NOTE: It is essential that we are lazy in r above so do not replace
- -- calls to this function by an explicit case.
- unYes (Yes _ _ x) = x
- unYes No = panic "VectMonad.fixV: no result"
-
-
--- Local Environments ---------------------------------------------------------
--- | Perform a computation in its own local environment.
--- This does not alter the environment of the current state.
-localV :: VM a -> VM a
-localV p = do
- env <- readLEnv id
- x <- p
- setLEnv env
- return x
-
--- | Perform a computation in an empty local environment.
-closedV :: VM a -> VM a
-closedV p = do
- env <- readLEnv id
- setLEnv (emptyLocalEnv { local_bind_name = local_bind_name env })
- x <- p
- setLEnv env
- return x
-
--- Lifting --------------------------------------------------------------------
--- | Lift a desugaring computation into the vectorisation monad.
-liftDs :: DsM a -> VM a
-liftDs p = VM $ \_ genv lenv -> do { x <- p; return (Yes genv lenv x) }
-
-
-
--- Builtins -------------------------------------------------------------------
--- Operations on Builtins
-liftBuiltinDs :: (Builtins -> DsM a) -> VM a
-liftBuiltinDs p = VM $ \bi genv lenv -> do { x <- p bi; return (Yes genv lenv x)}
-
-
--- | Project something from the set of builtins.
-builtin :: (Builtins -> a) -> VM a
-builtin f = VM $ \bi genv lenv -> return (Yes genv lenv (f bi))
-
-builtins :: (a -> Builtins -> b) -> VM (a -> b)
-builtins f = VM $ \bi genv lenv -> return (Yes genv lenv (`f` bi))
-
-
--- Environments ---------------------------------------------------------------
--- | Project something from the global environment.
-readGEnv :: (GlobalEnv -> a) -> VM a
-readGEnv f = VM $ \_ genv lenv -> return (Yes genv lenv (f genv))
-
-setGEnv :: GlobalEnv -> VM ()
-setGEnv genv = VM $ \_ _ lenv -> return (Yes genv lenv ())
-
-updGEnv :: (GlobalEnv -> GlobalEnv) -> VM ()
-updGEnv f = VM $ \_ genv lenv -> return (Yes (f genv) lenv ())
-
-
--- | Project something from the local environment.
-readLEnv :: (LocalEnv -> a) -> VM a
-readLEnv f = VM $ \_ genv lenv -> return (Yes genv lenv (f lenv))
-
--- | Set the local environment.
-setLEnv :: LocalEnv -> VM ()
-setLEnv lenv = VM $ \_ genv _ -> return (Yes genv lenv ())
-
--- | Update the enviroment using a provided function.
-updLEnv :: (LocalEnv -> LocalEnv) -> VM ()
-updLEnv f = VM $ \_ genv lenv -> return (Yes genv (f lenv) ())
-
-
--- InstEnv --------------------------------------------------------------------
-getInstEnv :: VM (InstEnv, InstEnv)
-getInstEnv = readGEnv global_inst_env
-
-getFamInstEnv :: VM FamInstEnvs
-getFamInstEnv = readGEnv global_fam_inst_env
-
-
--- Names ----------------------------------------------------------------------
--- | Get the name of the local binding currently being vectorised.
-getBindName :: VM FastString
-getBindName = readLEnv local_bind_name
-
-inBind :: Id -> VM a -> VM a
-inBind id p
- = do updLEnv $ \env -> env { local_bind_name = occNameFS (getOccName id) }
- p
-
-cloneName :: (OccName -> OccName) -> Name -> VM Name
-cloneName mk_occ name = liftM make (liftDs newUnique)
- where
- occ_name = mk_occ (nameOccName name)
-
- make u | isExternalName name = mkExternalName u (nameModule name)
- occ_name
- (nameSrcSpan name)
- | otherwise = mkSystemName u occ_name
-
-cloneId :: (OccName -> OccName) -> Id -> Type -> VM Id
-cloneId mk_occ id ty
- = do
- name <- cloneName mk_occ (getName id)
- let id' | isExportedId id = Id.mkExportedLocalId name ty
- | otherwise = Id.mkLocalId name ty
- return id'
-
--- Make a fresh instance of this var, with a new unique.
-cloneVar :: Var -> VM Var
-cloneVar var = liftM (setIdUnique var) (liftDs newUnique)
-
-newExportedVar :: OccName -> Type -> VM Var
-newExportedVar occ_name ty
- = do
- mod <- liftDs getModuleDs
- u <- liftDs newUnique
-
- let name = mkExternalName u mod occ_name noSrcSpan
-
- return $ Id.mkExportedLocalId name ty
-
-newLocalVar :: FastString -> Type -> VM Var
-newLocalVar fs ty
- = do
- u <- liftDs newUnique
- return $ mkSysLocal fs u ty
-
-newLocalVars :: FastString -> [Type] -> VM [Var]
-newLocalVars fs = mapM (newLocalVar fs)
-
-newDummyVar :: Type -> VM Var
-newDummyVar = newLocalVar (fsLit "vv")
-
-newTyVar :: FastString -> Kind -> VM Var
-newTyVar fs k
- = do
- u <- liftDs newUnique
- return $ mkTyVar (mkSysTvName u fs) k
-
-
--- | Add a mapping between a global var and its vectorised version to the state.
-defGlobalVar :: Var -> Var -> VM ()
-defGlobalVar v v' = updGEnv $ \env ->
- env { global_vars = extendVarEnv (global_vars env) v v'
- , global_exported_vars = upd (global_exported_vars env)
- }
- where
- upd env | isExportedId v = extendVarEnv env v (v, v')
- | otherwise = env
-
--- Var ------------------------------------------------------------------------
--- | Lookup the vectorised and\/or lifted versions of this variable.
--- If it's in the global environment we get the vectorised version.
--- If it's in the local environment we get both the vectorised and lifted version.
---
-lookupVar :: Var -> VM (Scope Var (Var, Var))
-lookupVar v
- = do r <- readLEnv $ \env -> lookupVarEnv (local_vars env) v
- case r of
- Just e -> return (Local e)
- Nothing -> liftM Global
- . maybeCantVectoriseVarM v
- . readGEnv $ \env -> lookupVarEnv (global_vars env) v
-
-maybeCantVectoriseVarM :: Monad m => Var -> m (Maybe Var) -> m Var
-maybeCantVectoriseVarM v p
- = do r <- p
- case r of
- Just x -> return x
- Nothing -> dumpVar v
-
-dumpVar :: Var -> a
-dumpVar var
- | Just _ <- isClassOpId_maybe var
- = cantVectorise "ClassOpId not vectorised:" (ppr var)
-
- | otherwise
- = cantVectorise "Variable not vectorised:" (ppr var)
-
--------------------------------------------------------------------------------
-globalScalars :: VM VarSet
-globalScalars = readGEnv global_scalars
-
-lookupTyCon :: TyCon -> VM (Maybe TyCon)
-lookupTyCon tc
- | isUnLiftedTyCon tc || isTupleTyCon tc = return (Just tc)
-
- | otherwise = readGEnv $ \env -> lookupNameEnv (global_tycons env) (tyConName tc)
-
-defTyCon :: TyCon -> TyCon -> VM ()
-defTyCon tc tc' = updGEnv $ \env ->
- env { global_tycons = extendNameEnv (global_tycons env) (tyConName tc) tc' }
-
-lookupDataCon :: DataCon -> VM (Maybe DataCon)
-lookupDataCon dc
- | isTupleTyCon (dataConTyCon dc) = return (Just dc)
- | otherwise = readGEnv $ \env -> lookupNameEnv (global_datacons env) (dataConName dc)
-
-defDataCon :: DataCon -> DataCon -> VM ()
-defDataCon dc dc' = updGEnv $ \env ->
- env { global_datacons = extendNameEnv (global_datacons env) (dataConName dc) dc' }
-
-lookupPrimPArray :: TyCon -> VM (Maybe TyCon)
-lookupPrimPArray = liftBuiltinDs . primPArray
-
-lookupPrimMethod :: TyCon -> String -> VM (Maybe Var)
-lookupPrimMethod tycon = liftBuiltinDs . primMethod tycon
-
-lookupTyConPA :: TyCon -> VM (Maybe Var)
-lookupTyConPA tc = readGEnv $ \env -> lookupNameEnv (global_pa_funs env) (tyConName tc)
-
-defTyConPA :: TyCon -> Var -> VM ()
-defTyConPA tc pa = updGEnv $ \env ->
- env { global_pa_funs = extendNameEnv (global_pa_funs env) (tyConName tc) pa }
-
-defTyConPAs :: [(TyCon, Var)] -> VM ()
-defTyConPAs ps = updGEnv $ \env ->
- env { global_pa_funs = extendNameEnvList (global_pa_funs env)
- [(tyConName tc, pa) | (tc, pa) <- ps] }
-
-lookupTyVarPA :: Var -> VM (Maybe CoreExpr)
-lookupTyVarPA tv = readLEnv $ \env -> lookupVarEnv (local_tyvar_pa env) tv
-
-lookupTyConPR :: TyCon -> VM (Maybe Var)
-lookupTyConPR tc = readGEnv $ \env -> lookupNameEnv (global_pr_funs env) (tyConName tc)
-
-lookupBoxedTyCon :: TyCon -> VM (Maybe TyCon)
-lookupBoxedTyCon tc = readGEnv $ \env -> lookupNameEnv (global_boxed_tycons env)
- (tyConName tc)
-
-defLocalTyVar :: TyVar -> VM ()
-defLocalTyVar tv = updLEnv $ \env ->
- env { local_tyvars = tv : local_tyvars env
- , local_tyvar_pa = local_tyvar_pa env `delVarEnv` tv
- }
-
-defLocalTyVarWithPA :: TyVar -> CoreExpr -> VM ()
-defLocalTyVarWithPA tv pa = updLEnv $ \env ->
- env { local_tyvars = tv : local_tyvars env
- , local_tyvar_pa = extendVarEnv (local_tyvar_pa env) tv pa
- }
-
-localTyVars :: VM [TyVar]
-localTyVars = readLEnv (reverse . local_tyvars)
-
--- Look up the dfun of a class instance.
---
--- The match must be unique - ie, match exactly one instance - but the
--- type arguments used for matching may be more specific than those of
--- the class instance declaration. The found class instances must not have
--- any type variables in the instance context that do not appear in the
--- instances head (i.e., no flexi vars); for details for what this means,
--- see the docs at InstEnv.lookupInstEnv.
---
-lookupInst :: Class -> [Type] -> VM (DFunId, [Type])
-lookupInst cls tys
- = do { instEnv <- getInstEnv
- ; case lookupInstEnv instEnv cls tys of
- ([(inst, inst_tys)], _)
- | noFlexiVar -> return (instanceDFunId inst, inst_tys')
- | otherwise -> pprPanic "VectMonad.lookupInst: flexi var: "
- (ppr $ mkTyConApp (classTyCon cls) tys)
- where
- inst_tys' = [ty | Right ty <- inst_tys]
- noFlexiVar = all isRight inst_tys
- _other ->
- pprPanic "VectMonad.lookupInst: not found " (ppr cls <+> ppr tys)
- }
- where
- isRight (Left _) = False
- isRight (Right _) = True
-
--- Look up the representation tycon of a family instance.
---
--- The match must be unique - ie, match exactly one instance - but the
--- type arguments used for matching may be more specific than those of
--- the family instance declaration.
---
--- Return the instance tycon and its type instance. For example, if we have
---
--- lookupFamInst 'T' '[Int]' yields (':R42T', 'Int')
---
--- then we have a coercion (ie, type instance of family instance coercion)
---
--- :Co:R42T Int :: T [Int] ~ :R42T Int
---
--- which implies that :R42T was declared as 'data instance T [a]'.
---
-lookupFamInst :: TyCon -> [Type] -> VM (TyCon, [Type])
-lookupFamInst tycon tys
- = ASSERT( isFamilyTyCon tycon )
- do { instEnv <- getFamInstEnv
- ; case lookupFamInstEnv instEnv tycon tys of
- [(fam_inst, rep_tys)] -> return (famInstTyCon fam_inst, rep_tys)
- _other ->
- pprPanic "VectMonad.lookupFamInst: not found: "
- (ppr $ mkTyConApp tycon tys)
- }
-
-
--- | Run a vectorisation computation.
-initV :: PackageId -> HscEnv -> ModGuts -> VectInfo -> VM a -> IO (Maybe (VectInfo, a))
-initV pkg hsc_env guts info p
- = do
- -- XXX: ignores error messages and warnings, check that this is
- -- indeed ok (the use of "Just r" suggests so)
- (_,Just r) <- initDs hsc_env (mg_module guts)
- (mg_rdr_env guts)
- (mg_types guts)
- go
- return r
- where
-
- go =
- do
- builtins <- initBuiltins pkg
- builtin_vars <- initBuiltinVars builtins
- builtin_tycons <- initBuiltinTyCons builtins
- let builtin_datacons = initBuiltinDataCons builtins
- builtin_boxed <- initBuiltinBoxedTyCons builtins
- builtin_scalars <- initBuiltinScalars builtins
-
- eps <- liftIO $ hscEPS hsc_env
- let famInstEnvs = (eps_fam_inst_env eps, mg_fam_inst_env guts)
- instEnvs = (eps_inst_env eps, mg_inst_env guts)
-
- builtin_prs <- initBuiltinPRs builtins instEnvs
- builtin_pas <- initBuiltinPAs builtins instEnvs
-
- let genv = extendImportedVarsEnv builtin_vars
- . extendScalars builtin_scalars
- . extendTyConsEnv builtin_tycons
- . extendDataConsEnv builtin_datacons
- . extendPAFunsEnv builtin_pas
- . setPRFunsEnv builtin_prs
- . setBoxedTyConsEnv builtin_boxed
- $ initGlobalEnv info instEnvs famInstEnvs
-
- r <- runVM p builtins genv emptyLocalEnv
- case r of
- Yes genv _ x -> return $ Just (new_info genv, x)
- No -> return Nothing
-
- new_info genv = updVectInfo genv (mg_types guts) info
-
projects / ghc-hetmet.git / commitdiff