X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcTyFuns.lhs;h=c7fac2d1ce918444b9d3f5d8e9989e324d4f57cd;hp=0130aa6c4ebd984cff9d64ebfb7e48f10a2179ea;hb=296058a1cafa80dec0b3f998348bce7c65f668b0;hpb=c4b993f3433777eb070de3090d76754cd6b4e2ec diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs index 0130aa6..c7fac2d 100644 --- a/compiler/typecheck/TcTyFuns.lhs +++ b/compiler/typecheck/TcTyFuns.lhs @@ -1,98 +1,55 @@ +Normalisation of type terms relative to type instances as well as +normalisation and entailment checking of equality constraints. \begin{code} -{-# OPTIONS -w #-} --- The above warning supression flag is a temporary kludge. --- While working on this module you are encouraged to remove it and fix --- any warnings in the module. See --- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings --- for details +module TcTyFuns ( + -- type normalisation wrt to toplevel equalities only + tcNormaliseFamInst, -module TcTyFuns( - finalizeEqInst, - partitionWantedEqInsts, partitionGivenEqInsts, + -- instance normalisation wrt to equalities + tcReduceEqs, - tcNormalizeFamInst, + -- errors + misMatchMsg, failWithMisMatch, - normaliseGivens, normaliseGivenDicts, - normaliseWanteds, normaliseWantedDicts, - solveWanteds, - substEqInDictInsts, - - addBind -- should not be here - ) where +) where #include "HsVersions.h" -import HsSyn - +--friends import TcRnMonad import TcEnv import Inst -import FamInstEnv import TcType import TcMType + +-- GHC import Coercion -import TypeRep ( Type(..) ) -import TyCon -import Var ( mkCoVar, isTcTyVar ) import Type -import HscTypes ( ExternalPackageState(..) ) +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 MonadUtils +import FastString +-- standard import Data.List -\end{code} - -%************************************************************************ -%* * -\section{Eq Insts} -%* * -%************************************************************************ - -%************************************************************************ -%* * -\section{Utility Code} -%* * -%************************************************************************ - -\begin{code} -partitionWantedEqInsts - :: [Inst] -- wanted insts - -> ([Inst],[Inst]) -- (wanted equations,wanted dicts) -partitionWantedEqInsts = partitionEqInsts True - -partitionGivenEqInsts - :: [Inst] -- given insts - -> ([Inst],[Inst]) -- (given equations,given dicts) -partitionGivenEqInsts = partitionEqInsts False - - -partitionEqInsts - :: Bool -- <=> wanted - -> [Inst] -- insts - -> ([Inst],[Inst]) -- (equations,dicts) -partitionEqInsts wanted [] - = ([],[]) -partitionEqInsts wanted (i:is) - | isEqInst i - = (i:es,ds) - | otherwise - = (es,i:ds) - where (es,ds) = partitionEqInsts wanted is - -isEqDict :: Inst -> Bool -isEqDict (Dict {tci_pred = EqPred _ _}) = True -isEqDict _ = False - +import Control.Monad \end{code} %************************************************************************ %* * - Normalisation of types + Normalisation of types wrt toplevel equality schemata %* * %************************************************************************ @@ -113,13 +70,14 @@ tcUnfoldSynFamInst (TyConApp tycon tys) | not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances = return Nothing | otherwise - = do { maybeFamInst <- tcLookupFamInst tycon tys + = 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 "TcTyFun.tcUnfoldSynFamInst" + coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst" (tyConFamilyCoercion_maybe rep_tc) } tcUnfoldSynFamInst _other = return Nothing @@ -128,22 +86,23 @@ tcUnfoldSynFamInst _other = return Nothing 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. - tcNormalizeFamInst ty = (co, ty') + tcNormaliseFamInst ty = (co, ty') then co : ty ~ ty' \begin{code} -tcNormalizeFamInst :: Type -> TcM (CoercionI, Type) -tcNormalizeFamInst = tcGenericNormalizeFamInst tcUnfoldSynFamInst - -tcNormalizeFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType) -tcNormalizeFamInstPred = tcGenericNormalizeFamInstPred tcUnfoldSynFamInst +-- |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. - tcGenericNormalizeFamInst fun ty = (co, ty') + tcGenericNormaliseFamInst fun ty = (co, ty') then co : ty ~ ty' This function is (by way of using smart constructors) careful to ensure that @@ -155,49 +114,45 @@ 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} -tcGenericNormalizeFamInst :: (TcType -> TcM (Maybe (TcType,Coercion))) +tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion))) -- what to do with type functions and tyvars -> TcType -- old type - -> TcM (CoercionI, Type) -- (coercion, new type) -tcGenericNormalizeFamInst fun ty - | Just ty' <- tcView ty = tcGenericNormalizeFamInst fun ty' -tcGenericNormalizeFamInst fun ty@(TyConApp tyCon tys) - = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys + -> 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 (TyConApp tyCon ntys) -- use normalised args! + ; 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) <- tcGenericNormalizeFamInst fun ty' + ; (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, TyConApp tyCon ntys) + Nothing -> return (tycon_coi, mkTyConApp tyCon ntys) } -tcGenericNormalizeFamInst fun ty@(AppTy ty1 ty2) - = do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1 - ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2 - ; return (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2) +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) } -tcGenericNormalizeFamInst fun ty@(FunTy ty1 ty2) - = do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1 - ; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2 - ; return (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy 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) } -tcGenericNormalizeFamInst fun ty@(ForAllTy tyvar ty1) - = do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1 - ; return (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1) +tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1) + = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1 + ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1) } -tcGenericNormalizeFamInst fun ty@(NoteTy note ty1) - = do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1 - ; return (mkNoteTyCoI note coi,NoteTy note nty1) - } -tcGenericNormalizeFamInst fun ty@(TyVarTy tv) +tcGenericNormaliseFamInst fun ty@(TyVarTy tv) | isTcTyVar tv - = do { traceTc (text "tcGenericNormalizeFamInst" <+> ppr ty) + = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty) ; res <- lookupTcTyVar tv ; case res of DoneTv _ -> @@ -205,672 +160,1480 @@ tcGenericNormalizeFamInst fun ty@(TyVarTy tv) ; case maybe_ty' of Nothing -> return (IdCo, ty) Just (ty', co1) -> - do { (coi2, ty'') <- tcGenericNormalizeFamInst fun ty' + do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty' ; return (ACo co1 `mkTransCoI` coi2, ty'') } } - IndirectTv ty' -> tcGenericNormalizeFamInst fun ty' + IndirectTv ty' -> tcGenericNormaliseFamInst fun ty' } | otherwise = return (IdCo, ty) -tcGenericNormalizeFamInst fun (PredTy predty) - = do { (coi, pred') <- tcGenericNormalizeFamInstPred fun predty +tcGenericNormaliseFamInst fun (PredTy predty) + = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty ; return (coi, PredTy pred') } --------------------------------- -tcGenericNormalizeFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion))) +tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion))) -> TcPredType -> TcM (CoercionI, TcPredType) -tcGenericNormalizeFamInstPred fun (ClassP cls tys) - = do { (cois, tys')<- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys +tcGenericNormaliseFamInstPred fun (ClassP cls tys) + = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys') } -tcGenericNormalizeFamInstPred fun (IParam ipn ty) - = do { (coi, ty') <- tcGenericNormalizeFamInst fun ty +tcGenericNormaliseFamInstPred fun (IParam ipn ty) + = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty') } -tcGenericNormalizeFamInstPred fun (EqPred ty1 ty2) - = do { (coi1, ty1') <- tcGenericNormalizeFamInst fun ty1 - ; (coi2, ty2') <- tcGenericNormalizeFamInst fun ty2 +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} %************************************************************************ %* * -\section{Normalisation of Given Dictionaries} + 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} -normaliseGivenDicts, normaliseWantedDicts - :: [Inst] -- given equations - -> [Inst] -- dictionaries - -> TcM ([Inst],TcDictBinds) - -normaliseGivenDicts eqs dicts = normalise_dicts eqs dicts False -normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True - -normalise_dicts - :: [Inst] -- given equations - -> [Inst] -- dictionaries - -> Bool -- True <=> the dicts are wanted - -- Fals <=> they are given - -> TcM ([Inst],TcDictBinds) -normalise_dicts given_eqs dicts is_wanted - = do { traceTc $ text "normaliseGivenDicts <-" <+> ppr dicts <+> - text "with" <+> ppr given_eqs - ; (dicts0, binds0) <- normaliseInsts is_wanted dicts - ; (dicts1, binds1) <- substEqInDictInsts given_eqs dicts0 - ; let binds01 = binds0 `unionBags` binds1 - ; if isEmptyBag binds1 - then return (dicts1, binds01) - else do { (dicts2, binds2) <- normaliseGivenDicts given_eqs dicts1 - ; return (dicts2, binds01 `unionBags` binds2) } } +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} %************************************************************************ %* * -\section{Normalisation of Wanteds} + 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} -normaliseWanteds :: [Inst] -> TcM [Inst] -normaliseWanteds insts - = do { traceTc (text "normaliseWanteds" <+> ppr insts) - ; result <- eq_rewrite - [ ("(Occurs)", simple_rewrite_check $ occursCheckInsts) - , ("(ZONK)", simple_rewrite $ zonkInsts) - , ("(TRIVIAL)", trivialInsts) - , ("(SWAP)", swapInsts) - , ("(DECOMP)", decompInsts) - , ("(TOP)", topInsts) - , ("(SUBST)", substInsts) - , ("(UNIFY)", unifyInsts) - ] insts - ; traceTc (text "normaliseWanteds ->" <+> ppr result) - ; return result +-- |Turn a set of equalities into an equality configuration for solving. +-- +-- Precondition: The Insts are zonked. +-- +normaliseEqs :: [Inst] -> TcM EqConfig +normaliseEqs eqs + = do { ASSERTM2( allM 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} + %************************************************************************ %* * -\section{Normalisation of Givens} + 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 + && not (isOpenSynTyCon 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 + } -normaliseGivens :: [Inst] -> TcM ([Inst],TcM ()) -normaliseGivens givens = - do { traceTc (text "normaliseGivens <-" <+> ppr givens) - ; (result,action) <- given_eq_rewrite - ("(SkolemOccurs)", skolemOccurs) - (return ()) - [("(Occurs)", simple_rewrite_check $ occursCheckInsts), - ("(ZONK)", simple_rewrite $ zonkInsts), - ("(TRIVIAL)", trivialInsts), - ("(SWAP)", swapInsts), - ("(DECOMP)", decompInsts), - ("(TOP)", topInsts), - ("(SUBST)", substInsts)] - givens - ; traceTc (text "normaliseGivens ->" <+> ppr result) - ; return (result,action) - } - -skolemOccurs :: [Inst] -> TcM ([Inst],TcM ()) -skolemOccurs [] = return ([], return ()) -skolemOccurs (inst@(EqInst {}):insts) - = do { (insts',actions) <- skolemOccurs insts - -- check whether the current inst co :: ty1 ~ ty2 suffers - -- from the occurs check issue: F ty1 \in ty2 - ; let occurs = go False ty2 - ; if occurs - then - -- if it does generate two new coercions: - do { skolem_var <- newMetaTyVar TauTv (typeKind ty1) - ; let skolem_ty = TyVarTy skolem_var - -- ty1 :: ty1 ~ b - ; inst1 <- mkEqInst (EqPred ty1 skolem_ty) (mkGivenCo ty1) - -- sym co :: ty2 ~ b - ; inst2 <- mkEqInst (EqPred ty2 skolem_ty) (mkGivenCo $ fromACo $ mkSymCoI $ ACo $ fromGivenCo co) - -- to replace the old one - -- the corresponding action is - -- b := ty1 - ; let action = writeMetaTyVar skolem_var ty1 - ; return (inst1:inst2:insts', action >> actions) - } - else - return (inst:insts', actions) - } - where - ty1 = eqInstLeftTy inst - ty2 = eqInstRightTy inst - co = eqInstCoercion inst - check :: Bool -> TcType -> Bool - check flag ty - = if flag && ty1 `tcEqType` ty - then True - else go flag ty - - go flag (TyConApp con tys) = or $ map (check (isOpenSynTyCon con || flag)) tys - go flag (FunTy arg res) = or $ map (check flag) [arg,res] - go flag (AppTy fun arg) = or $ map (check flag) [fun,arg] - go flag ty = False + -- 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) + } + + -- data 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 + ; if null args_eqss + then -- unchanged, keep the old type with folded synonyms + return (ty, ty, []) + else + return (mkTyConApp con args', + mkTyConApp con cargs, + concat args_eqss) + } + + -- 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" + + -- we should never see a predicate type + go (PredTy _) + = panic "TcTyFuns.flattenType: unexpected PredType" + + 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} + %************************************************************************ %* * -\section{Solving of Wanteds} + 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} -solveWanteds :: - [Inst] -> -- givens - [Inst] -> -- wanteds - TcM [Inst] -- irreducible wanteds -solveWanteds givens wanteds = - do { traceTc (text "solveWanteds <-" <+> ppr wanteds <+> text "with" <+> ppr givens) - ; result <- eq_rewrite - [("(Occurs)", simple_rewrite_check $ occursCheckInsts), - ("(TRIVIAL)", trivialInsts), - ("(DECOMP)", decompInsts), - ("(TOP)", topInsts), - ("(GIVEN)", givenInsts givens), - ("(UNIFY)", unifyInsts)] - wanteds - ; traceTc (text "solveWanteds ->" <+> ppr result) - ; return result - } - - -givenInsts :: [Inst] -> [Inst] -> TcM ([Inst],Bool) -givenInsts [] wanteds - = return (wanteds,False) -givenInsts (g:gs) wanteds - = do { (wanteds1,changed1) <- givenInsts gs wanteds - ; (wanteds2,changed2) <- substInst g wanteds1 - ; return (wanteds2,changed1 || changed2) - } - - - - -- fixpoint computation - -- of a number of rewrites of equalities -eq_rewrite :: - [(String,[Inst] -> TcM ([Inst],Bool))] -> -- rewrite functions and descriptions - [Inst] -> -- initial equations - TcM [Inst] -- final equations (at fixed point) -eq_rewrite rewrites insts - = go rewrites insts - where - go _ [] -- return quickly when there's nothing to be done - = return [] - go [] insts - = return insts - go ((desc,r):rs) insts - = do { (insts',changed) <- r insts - ; traceTc (text desc <+> ppr insts') - ; if changed - then loop insts' - else go rs insts' - } - loop = eq_rewrite rewrites - - -- fixpoint computation - -- of a number of rewrites of equalities -given_eq_rewrite :: - - (String,[Inst] -> TcM ([Inst],TcM ())) -> - (TcM ()) -> - [(String,[Inst] -> TcM ([Inst],Bool))] -> -- rewrite functions and descriptions - [Inst] -> -- initial equations - TcM ([Inst],TcM ()) -- final equations (at fixed point) -given_eq_rewrite p@(desc,start) acc rewrites insts - = do { (insts',acc') <- start insts - ; go (acc >> acc') rewrites insts' - } - where - go acc _ [] -- return quickly when there's nothing to be done - = return ([],acc) - go acc [] insts - = return (insts,acc) - go acc ((desc,r):rs) insts - = do { (insts',changed) <- r insts - ; traceTc (text desc <+> ppr insts') - ; if changed - then loop acc insts' - else go acc rs insts' - } - loop acc = given_eq_rewrite p acc rewrites - -simple_rewrite :: - ([Inst] -> TcM [Inst]) -> - ([Inst] -> TcM ([Inst],Bool)) -simple_rewrite r insts - = do { insts' <- r insts - ; return (insts',False) - } - -simple_rewrite_check :: - ([Inst] -> TcM ()) -> - ([Inst] -> TcM ([Inst],Bool)) -simple_rewrite_check check insts - = check insts >> return (insts,False) - +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} + %************************************************************************ %* * -\section{Different forms of Inst rewritings} + Finalisation of equalities %* * %************************************************************************ -Rewrite schemata applied by way of eq_rewrite and friends. +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' + } - -- (Trivial) - -- g1 : t ~ t - -- >--> - -- g1 := t - -- -trivialInsts :: - [Inst] -> -- equations - TcM ([Inst],Bool) -- remaining equations, any changes? -trivialInsts [] - = return ([],False) -trivialInsts (i@(EqInst {}):is) - = do { (is',changed)<- trivialInsts is - ; if tcEqType ty1 ty2 - then do { eitherEqInst i - (\covar -> writeMetaTyVar covar ty1) - (\_ -> return ()) - ; return (is',True) - } - else return (i:is',changed) - } - where - ty1 = eqInstLeftTy i - ty2 = eqInstRightTy i - --- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -swapInsts :: [Inst] -> TcM ([Inst],Bool) --- All the inputs and outputs are equalities -swapInsts insts = mapAndUnzipM swapInst insts >>= \(insts',changeds) -> return (insts',or changeds) - - - -- (Swap) - -- g1 : c ~ Fd - -- >--> - -- g2 : Fd ~ c - -- g1 := sym g2 - -- -swapInst i@(EqInst {}) - = go ty1 ty2 - where - ty1 = eqInstLeftTy i - ty2 = eqInstRightTy i - go ty1 ty2 | Just ty1' <- tcView ty1 - = go ty1' ty2 - go ty1 ty2 | Just ty2' <- tcView ty2 - = go ty1 ty2' - go (TyConApp tyCon _) _ | isOpenSynTyCon tyCon - = return (i,False) - -- we should swap! - go ty1 ty2@(TyConApp tyCon _) - | isOpenSynTyCon tyCon - = do { wg_co <- eitherEqInst i - -- old_co := sym new_co - (\old_covar -> - do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty2 ty1) - ; let new_co = TyVarTy new_cotv - ; writeMetaTyVar old_covar (mkCoercion symCoercionTyCon [new_co]) - ; return $ mkWantedCo new_cotv - }) - -- new_co := sym old_co - (\old_co -> return $ mkGivenCo $ mkCoercion symCoercionTyCon [old_co]) - ; new_inst <- mkEqInst (EqPred ty2 ty1) wg_co - ; return (new_inst,True) - } - go _ _ = return (i,False) - --- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -decompInsts :: [Inst] -> TcM ([Inst],Bool) -decompInsts insts = do { (insts,bs) <- mapAndUnzipM decompInst insts - ; return (concat insts,or bs) - } - - -- (Decomp) - -- g1 : T cs ~ T ds - -- >--> - -- g21 : c1 ~ d1, ..., g2n : cn ~ dn - -- g1 := T g2s - -- - -- Works also for the case where T is actually an application of a - -- type family constructor to a set of types, provided the - -- applications on both sides of the ~ are identical; - -- see also Note [OpenSynTyCon app] in TcUnify - -- -decompInst :: Inst -> TcM ([Inst],Bool) -decompInst i@(EqInst {}) - = go ty1 ty2 - where - ty1 = eqInstLeftTy i - ty2 = eqInstRightTy i - go ty1 ty2 - | Just ty1' <- tcView ty1 = go ty1' ty2 - | Just ty2' <- tcView ty2 = go ty1 ty2' - - go ty1@(TyConApp con1 tys1) ty2@(TyConApp con2 tys2) - | con1 == con2 && identicalHead - = do { cos <- eitherEqInst i - -- old_co := Con1 cos - (\old_covar -> - do { cotvs <- zipWithM (\t1 t2 -> - newMetaTyVar TauTv - (mkCoKind t1 t2)) - tys1 tys2 - ; let cos = map TyVarTy cotvs - ; writeMetaTyVar old_covar (TyConApp con1 cos) - ; return $ map mkWantedCo cotvs - }) - -- co_i := Con_i old_co - (\old_co -> return $ - map mkGivenCo $ - mkRightCoercions (length tys1) old_co) - ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos - ; traceTc (text "decomp identicalHead" <+> ppr insts) - ; return (insts, not $ null insts) + -- 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 } - | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2) - -- not matching data constructors (of any flavour) are bad news - = do { env0 <- tcInitTidyEnv - ; let (env1, tidy_ty1) = tidyOpenType env0 ty1 - (env2, tidy_ty2) = tidyOpenType env1 ty2 - extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2] - msg = - ptext SLIT("Unsolvable equality constraint:") - ; failWithTcM (env2, hang msg 2 extra) + + 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'} } - where - n = tyConArity con1 - (idxTys1, tys1') = splitAt n tys1 - (idxTys2, tys2') = splitAt n tys2 - identicalHead = not (isOpenSynTyCon con1) || - idxTys1 `tcEqTypes` idxTys2 - - go _ _ = return ([i], False) - --- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -topInsts :: [Inst] -> TcM ([Inst],Bool) -topInsts insts - = do { (insts,bs) <- mapAndUnzipM topInst insts - ; return (insts,or bs) - } - - -- (Top) - -- g1 : t ~ s - -- >--> co1 :: t ~ t' / co2 :: s ~ s' - -- g2 : t' ~ s' - -- g1 := co1 * g2 * sym co2 -topInst :: Inst -> TcM (Inst,Bool) -topInst i@(EqInst {}) - = do { (coi1,ty1') <- tcNormalizeFamInst ty1 - ; (coi2,ty2') <- tcNormalizeFamInst ty2 - ; case (coi1,coi2) of - (IdCo,IdCo) -> - return (i,False) - _ -> - do { wg_co <- eitherEqInst i - -- old_co = co1 * new_co * sym co2 - (\old_covar -> - do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1 ty2) - ; let new_co = TyVarTy new_cotv - ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2) - ; writeMetaTyVar old_covar (fromACo old_coi) - ; return $ mkWantedCo new_cotv - }) - -- new_co = sym co1 * old_co * co2 - (\old_co -> return $ mkGivenCo $ fromACo $ mkSymCoI coi1 `mkTransCoI` ACo old_co `mkTransCoI` coi2) - ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co - ; return (new_inst,True) - } - } - where - ty1 = eqInstLeftTy i - ty2 = eqInstRightTy i - --- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -substInsts :: [Inst] -> TcM ([Inst],Bool) -substInsts insts = substInstsWorker insts [] - -substInstsWorker [] acc - = return (acc,False) -substInstsWorker (i:is) acc - | (TyConApp con _) <- tci_left i, isOpenSynTyCon con - = do { (is',change) <- substInst i (acc ++ is) - ; if change - then return ((i:is'),True) - else substInstsWorker is (i:acc) - } - | otherwise - = substInstsWorker is (i:acc) - - -- (Subst) - -- g : F c ~ t, - -- forall g1 : s1{F c} ~ s2{F c} - -- >--> - -- g2 : s1{t} ~ s2{t} - -- g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g} -substInst inst [] - = return ([],False) -substInst inst@(EqInst {tci_left = pattern, tci_right = target}) (i@(EqInst {tci_left = ty1, tci_right = ty2}):is) - = do { (is',changed) <- substInst inst is - ; (coi1,ty1') <- tcGenericNormalizeFamInst fun ty1 - ; (coi2,ty2') <- tcGenericNormalizeFamInst fun ty2 - ; case (coi1,coi2) of - (IdCo,IdCo) -> - return (i:is',changed) - _ -> - do { gw_co <- eitherEqInst i - -- old_co := co1 * new_co * sym co2 - (\old_covar -> - do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1' ty2') - ; let new_co = TyVarTy new_cotv - ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2) - ; writeMetaTyVar old_covar (fromACo old_coi) - ; return $ mkWantedCo new_cotv - }) - -- new_co := sym co1 * old_co * co2 - (\old_co -> return $ mkGivenCo $ fromACo $ (mkSymCoI coi1) `mkTransCoI` ACo old_co `mkTransCoI` coi2) - ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co - ; return (new_inst:is',True) - } - } - where fun ty = return $ if tcEqType pattern ty then Just (target,coercion) else Nothing - - coercion = eitherEqInst inst TyVarTy id --- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -unifyInsts - :: [Inst] -- wanted equations - -> TcM ([Inst],Bool) -unifyInsts insts - = do { (insts',changeds) <- mapAndUnzipM unifyInst insts - ; return (concat insts',or changeds) - } - - -- (UnifyMeta) - -- g : alpha ~ t - -- >--> - -- alpha := t - -- g := t - -- - -- TOMDO: you should only do this for certain `meta' type variables -unifyInst i@(EqInst {tci_left = ty1, tci_right = ty2}) - | TyVarTy tv1 <- ty1, isMetaTyVar tv1 = go ty2 tv1 - | TyVarTy tv2 <- ty2, isMetaTyVar tv2 = go ty1 tv2 - | otherwise = return ([i],False) - where go ty tv - = do { let cotv = fromWantedCo "unifyInst" $ eqInstCoercion i - ; writeMetaTyVar tv ty -- alpha := t - ; writeMetaTyVar cotv ty -- g := t - ; return ([],True) - } - --- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -occursCheckInsts :: [Inst] -> TcM () -occursCheckInsts insts = mappM_ occursCheckInst insts - - - -- (OccursCheck) - -- t ~ s[T t] - -- >--> - -- fail - -- -occursCheckInst :: Inst -> TcM () -occursCheckInst i@(EqInst {tci_left = ty1, tci_right = ty2}) - = go ty2 - where - check ty = if ty `tcEqType` ty1 - then occursError - else go ty - - go (TyConApp con tys) = if isOpenSynTyCon con then return () else mappM_ check tys - go (FunTy arg res) = mappM_ check [arg,res] - go (AppTy fun arg) = mappM_ check [fun,arg] - go _ = return () - - occursError = do { env0 <- tcInitTidyEnv - ; let (env1, tidy_ty1) = tidyOpenType env0 ty1 - (env2, tidy_ty2) = tidyOpenType env1 ty2 - extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2] - ; failWithTcM (env2, hang msg 2 extra) - } - where msg = ptext SLIT("Occurs check: cannot construct the infinite type") + + -- 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} -Normalises a set of dictionaries relative to a set of given equalities (which -are interpreted as rewrite rules). We only consider given equalities of the -form +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. - F ts ~ t +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.) -where F is a type family. +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} -substEqInDictInsts :: [Inst] -- given equalities (used as rewrite rules) - -> [Inst] -- dictinaries to be normalised - -> TcM ([Inst], TcDictBinds) -substEqInDictInsts eq_insts insts - = do { traceTc (text "substEqInDictInst <-" <+> ppr insts) - ; result <- foldlM rewriteWithOneEquality (insts, emptyBag) eq_insts - ; traceTc (text "substEqInDictInst ->" <+> ppr result) - ; return result +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 - -- (1) Given equality of form 'F ts ~ t': use for rewriting - rewriteWithOneEquality (insts, dictBinds) - inst@(EqInst {tci_left = pattern, - tci_right = target}) - | isOpenSynTyConApp pattern - = do { (insts', moreDictBinds) <- genericNormaliseInsts True {- wanted -} - applyThisEq insts - ; return (insts', dictBinds `unionBags` moreDictBinds) + -- 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 - applyThisEq = tcGenericNormalizeFamInstPred (return . matchResult) - - -- rewrite in case of an exact match - matchResult ty | tcEqType pattern ty = Just (target, eqInstType inst) - | otherwise = Nothing - - -- (2) Given equality has the wrong form: ignore - rewriteWithOneEquality (insts, dictBinds) _not_a_rewrite_rule - = return (insts, dictBinds) + 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} + %************************************************************************ %* * - Normalisation of Insts +\section{Errors} %* * %************************************************************************ -Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level -type-function equations, where +The infamous couldn't match expected type soandso against inferred type +somethingdifferent message. + +\begin{code} +eqInstMisMatch :: Inst -> TcM a +eqInstMisMatch inst + = ASSERT( isEqInst inst ) + setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp + where + (ty_act, ty_exp) = eqInstTys inst + InstLoc _ _ ctxt = instLoc 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)] + in + (env2, msg) + + where + 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 - (norm_insts, binds) = normaliseInsts is_wanted insts + ppr_extra env _ty = (env, empty) -- Normal case +\end{code} -If 'is_wanted' - = True, (binds + norm_insts) defines insts (wanteds) - = False, (binds + insts) defines norm_insts (givens) +Warn of loopy local equalities that were dropped. \begin{code} -normaliseInsts :: Bool -- True <=> wanted insts - -> [Inst] -- wanted or given insts - -> TcM ([Inst], TcDictBinds) -- normalized insts and bindings -normaliseInsts isWanted insts - = genericNormaliseInsts isWanted tcNormalizeFamInstPred insts - -genericNormaliseInsts :: Bool -- True <=> wanted insts - -> (TcPredType -> TcM (CoercionI, TcPredType)) - -- how to normalise - -> [Inst] -- wanted or given insts - -> TcM ([Inst], TcDictBinds) -- normalized insts & binds -genericNormaliseInsts isWanted fun insts - = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts - ; return (insts', unionManyBags binds) +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)) } - where - normaliseOneInst isWanted fun - dict@(Dict {tci_name = name, - tci_pred = pred, - tci_loc = loc}) - = do { traceTc (text "genericNormaliseInst 1") - ; (coi, pred') <- fun pred - ; traceTc (text "genericNormaliseInst 2") - - ; case coi of - IdCo -> return (dict, emptyBag) - -- don't use pred' in this case; otherwise, we get - -- more unfolded closed type synonyms in error messages - ACo co -> - do { -- an inst for the new pred - ; 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 co) - | otherwise = (dict', dict, co) - -- if isWanted - -- co :: dict ~ dict' - -- hence dict = dict' `cast` sym co - -- else - -- co :: dict ~ dict' - -- hence dict' = dict `cast` co - expr = HsVar $ instToId source_dict - cast_expr = HsWrap (WpCo st_co) expr - rhs = L (instLocSpan loc) cast_expr - binds = mkBind target_dict rhs - -- return the new inst - ; return (dict', binds) - } - } - - -- TOMDO: treat other insts appropriately - normaliseOneInst isWanted fun inst - = do { inst' <- zonkInst inst - ; return (inst', emptyBag) - } - -addBind binds inst rhs = binds `unionBags` mkBind inst rhs - -mkBind inst rhs = unitBag (L (instSpan inst) - (VarBind (instToId inst) rhs)) \end{code}