+++ /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 (isOpenSynTyCon 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
- | isOpenSynTyConApp 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
- | isOpenSynTyConApp 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)
- | isOpenSynTyConApp 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 (isOpenSynTyCon 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' <- newDictBndr 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}