-- (c) The University of Glasgow 2006 -- -- FamInstEnv: Type checked family instance declarations {-# LANGUAGE CPP, GADTs, ScopedTypeVariables, BangPatterns, TupleSections, DeriveFunctor #-} module FamInstEnv ( FamInst(..), FamFlavor(..), famInstAxiom, famInstTyCon, famInstRHS, famInstsRepTyCons, famInstRepTyCon_maybe, dataFamInstRepTyCon, pprFamInst, pprFamInsts, mkImportedFamInst, FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs, extendFamInstEnv, extendFamInstEnvList, famInstEnvElts, famInstEnvSize, familyInstances, -- * CoAxioms mkCoAxBranch, mkBranchedCoAxiom, mkUnbranchedCoAxiom, mkSingleCoAxiom, mkNewTypeCoAxiom, FamInstMatch(..), lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvByTyCon, isDominatedBy, apartnessCheck, -- Injectivity InjectivityCheckResult(..), lookupFamInstEnvInjectivityConflicts, injectiveBranches, -- Normalisation topNormaliseType, topNormaliseType_maybe, normaliseType, normaliseTcApp, normaliseTcArgs, reduceTyFamApp_maybe, -- Flattening flattenTys ) where #include "HsVersions.h" import GhcPrelude import Unify import Type import TyCoRep import TyCon import Coercion import CoAxiom import VarSet import VarEnv import Name import PrelNames ( eqPrimTyConKey ) import UniqDFM import Outputable import Maybes import CoreMap import Unique import Util import Var import Pair import SrcLoc import FastString import Control.Monad import Data.List( mapAccumL ) import Data.Array( Array, assocs ) {- ************************************************************************ * * Type checked family instance heads * * ************************************************************************ Note [FamInsts and CoAxioms] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * CoAxioms and FamInsts are just like DFunIds and ClsInsts * A CoAxiom is a System-FC thing: it can relate any two types * A FamInst is a Haskell source-language thing, corresponding to a type/data family instance declaration. - The FamInst contains a CoAxiom, which is the evidence for the instance - The LHS of the CoAxiom is always of form F ty1 .. tyn where F is a type family -} data FamInst -- See Note [FamInsts and CoAxioms] = FamInst { FamInst -> CoAxiom Unbranched fi_axiom :: CoAxiom Unbranched -- The new coercion axiom -- introduced by this family -- instance -- INVARIANT: apart from freshening (see below) -- fi_tvs = cab_tvs of the (single) axiom branch -- fi_cvs = cab_cvs ...ditto... -- fi_tys = cab_lhs ...ditto... -- fi_rhs = cab_rhs ...ditto... , FamInst -> FamFlavor fi_flavor :: FamFlavor -- Everything below here is a redundant, -- cached version of the two things above -- except that the TyVars are freshened , FamInst -> Name fi_fam :: Name -- Family name -- Used for "rough matching"; same idea as for class instances -- See Note [Rough-match field] in InstEnv , FamInst -> [Maybe Name] fi_tcs :: [Maybe Name] -- Top of type args -- INVARIANT: fi_tcs = roughMatchTcs fi_tys -- Used for "proper matching"; ditto , FamInst -> [TyVar] fi_tvs :: [TyVar] -- Template tyvars for full match , FamInst -> [TyVar] fi_cvs :: [CoVar] -- Template covars for full match -- Like ClsInsts, these variables are always fresh -- See Note [Template tyvars are fresh] in InstEnv , FamInst -> [Type] fi_tys :: [Type] -- The LHS type patterns -- May be eta-reduced; see Note [Eta reduction for data families] , FamInst -> Type fi_rhs :: Type -- the RHS, with its freshened vars } data FamFlavor = SynFamilyInst -- A synonym family | DataFamilyInst TyCon -- A data family, with its representation TyCon {- Note [Arity of data families] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Data family instances might legitimately be over- or under-saturated. Under-saturation has two potential causes: U1) Eta reduction. See Note [Eta reduction for data families]. U2) When the user has specified a return kind instead of written out patterns. Example: data family Sing (a :: k) data instance Sing :: Bool -> Type The data family tycon Sing has an arity of 2, the k and the a. But the data instance has only one pattern, Bool (standing in for k). This instance is equivalent to `data instance Sing (a :: Bool)`, but without the last pattern, we have an under-saturated data family instance. On its own, this example is not compelling enough to add support for under-saturation, but U1 makes this feature more compelling. Over-saturation is also possible: O1) If the data family's return kind is a type variable (see also #12369), an instance might legitimately have more arguments than the family. Example: data family Fix :: (Type -> k) -> k data instance Fix f = MkFix1 (f (Fix f)) data instance Fix f x = MkFix2 (f (Fix f x) x) In the first instance here, the k in the data family kind is chosen to be Type. In the second, it's (Type -> Type). However, we require that any over-saturation is eta-reducible. That is, we require that any extra patterns be bare unrepeated type variables; see Note [Eta reduction for data families]. Accordingly, the FamInst is never over-saturated. Why can we allow such flexibility for data families but not for type families? Because data families can be decomposed -- that is, they are generative and injective. A Type family is neither and so always must be applied to all its arguments. -} -- Obtain the axiom of a family instance famInstAxiom :: FamInst -> CoAxiom Unbranched famInstAxiom :: FamInst -> CoAxiom Unbranched famInstAxiom = FamInst -> CoAxiom Unbranched fi_axiom -- Split the left-hand side of the FamInst famInstSplitLHS :: FamInst -> (TyCon, [Type]) famInstSplitLHS :: FamInst -> (TyCon, [Type]) famInstSplitLHS (FamInst { fi_axiom :: FamInst -> CoAxiom Unbranched fi_axiom = CoAxiom Unbranched axiom, fi_tys :: FamInst -> [Type] fi_tys = [Type] lhs }) = (CoAxiom Unbranched -> TyCon forall (br :: BranchFlag). CoAxiom br -> TyCon coAxiomTyCon CoAxiom Unbranched axiom, [Type] lhs) -- Get the RHS of the FamInst famInstRHS :: FamInst -> Type famInstRHS :: FamInst -> Type famInstRHS = FamInst -> Type fi_rhs -- Get the family TyCon of the FamInst famInstTyCon :: FamInst -> TyCon famInstTyCon :: FamInst -> TyCon famInstTyCon = CoAxiom Unbranched -> TyCon forall (br :: BranchFlag). CoAxiom br -> TyCon coAxiomTyCon (CoAxiom Unbranched -> TyCon) -> (FamInst -> CoAxiom Unbranched) -> FamInst -> TyCon forall b c a. (b -> c) -> (a -> b) -> a -> c . FamInst -> CoAxiom Unbranched famInstAxiom -- Return the representation TyCons introduced by data family instances, if any famInstsRepTyCons :: [FamInst] -> [TyCon] famInstsRepTyCons :: [FamInst] -> [TyCon] famInstsRepTyCons [FamInst] fis = [TyCon tc | FamInst { fi_flavor :: FamInst -> FamFlavor fi_flavor = DataFamilyInst TyCon tc } <- [FamInst] fis] -- Extracts the TyCon for this *data* (or newtype) instance famInstRepTyCon_maybe :: FamInst -> Maybe TyCon famInstRepTyCon_maybe :: FamInst -> Maybe TyCon famInstRepTyCon_maybe FamInst fi = case FamInst -> FamFlavor fi_flavor FamInst fi of DataFamilyInst TyCon tycon -> TyCon -> Maybe TyCon forall a. a -> Maybe a Just TyCon tycon FamFlavor SynFamilyInst -> Maybe TyCon forall a. Maybe a Nothing dataFamInstRepTyCon :: FamInst -> TyCon dataFamInstRepTyCon :: FamInst -> TyCon dataFamInstRepTyCon FamInst fi = case FamInst -> FamFlavor fi_flavor FamInst fi of DataFamilyInst TyCon tycon -> TyCon tycon FamFlavor SynFamilyInst -> String -> SDoc -> TyCon forall a. HasCallStack => String -> SDoc -> a pprPanic String "dataFamInstRepTyCon" (FamInst -> SDoc forall a. Outputable a => a -> SDoc ppr FamInst fi) {- ************************************************************************ * * Pretty printing * * ************************************************************************ -} instance NamedThing FamInst where getName :: FamInst -> Name getName = CoAxiom Unbranched -> Name forall (br :: BranchFlag). CoAxiom br -> Name coAxiomName (CoAxiom Unbranched -> Name) -> (FamInst -> CoAxiom Unbranched) -> FamInst -> Name forall b c a. (b -> c) -> (a -> b) -> a -> c . FamInst -> CoAxiom Unbranched fi_axiom instance Outputable FamInst where ppr :: FamInst -> SDoc ppr = FamInst -> SDoc pprFamInst pprFamInst :: FamInst -> SDoc -- Prints the FamInst as a family instance declaration -- NB: This function, FamInstEnv.pprFamInst, is used only for internal, -- debug printing. See PprTyThing.pprFamInst for printing for the user pprFamInst :: FamInst -> SDoc pprFamInst (FamInst { fi_flavor :: FamInst -> FamFlavor fi_flavor = FamFlavor flavor, fi_axiom :: FamInst -> CoAxiom Unbranched fi_axiom = CoAxiom Unbranched ax , fi_tvs :: FamInst -> [TyVar] fi_tvs = [TyVar] tvs, fi_tys :: FamInst -> [Type] fi_tys = [Type] tys, fi_rhs :: FamInst -> Type fi_rhs = Type rhs }) = SDoc -> Int -> SDoc -> SDoc hang (SDoc ppr_tc_sort SDoc -> SDoc -> SDoc <+> String -> SDoc text String "instance" SDoc -> SDoc -> SDoc <+> TyCon -> CoAxBranch -> SDoc pprCoAxBranchUser (CoAxiom Unbranched -> TyCon forall (br :: BranchFlag). CoAxiom br -> TyCon coAxiomTyCon CoAxiom Unbranched ax) (CoAxiom Unbranched -> CoAxBranch coAxiomSingleBranch CoAxiom Unbranched ax)) Int 2 (SDoc -> SDoc whenPprDebug SDoc debug_stuff) where ppr_tc_sort :: SDoc ppr_tc_sort = case FamFlavor flavor of FamFlavor SynFamilyInst -> String -> SDoc text String "type" DataFamilyInst TyCon tycon | TyCon -> Bool isDataTyCon TyCon tycon -> String -> SDoc text String "data" | TyCon -> Bool isNewTyCon TyCon tycon -> String -> SDoc text String "newtype" | TyCon -> Bool isAbstractTyCon TyCon tycon -> String -> SDoc text String "data" | Bool otherwise -> String -> SDoc text String "WEIRD" SDoc -> SDoc -> SDoc <+> TyCon -> SDoc forall a. Outputable a => a -> SDoc ppr TyCon tycon debug_stuff :: SDoc debug_stuff = [SDoc] -> SDoc vcat [ String -> SDoc text String "Coercion axiom:" SDoc -> SDoc -> SDoc <+> CoAxiom Unbranched -> SDoc forall a. Outputable a => a -> SDoc ppr CoAxiom Unbranched ax , String -> SDoc text String "Tvs:" SDoc -> SDoc -> SDoc <+> [TyVar] -> SDoc forall a. Outputable a => a -> SDoc ppr [TyVar] tvs , String -> SDoc text String "LHS:" SDoc -> SDoc -> SDoc <+> [Type] -> SDoc forall a. Outputable a => a -> SDoc ppr [Type] tys , String -> SDoc text String "RHS:" SDoc -> SDoc -> SDoc <+> Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type rhs ] pprFamInsts :: [FamInst] -> SDoc pprFamInsts :: [FamInst] -> SDoc pprFamInsts [FamInst] finsts = [SDoc] -> SDoc vcat ((FamInst -> SDoc) -> [FamInst] -> [SDoc] forall a b. (a -> b) -> [a] -> [b] map FamInst -> SDoc pprFamInst [FamInst] finsts) {- Note [Lazy axiom match] ~~~~~~~~~~~~~~~~~~~~~~~ It is Vitally Important that mkImportedFamInst is *lazy* in its axiom parameter. The axiom is loaded lazily, via a forkM, in TcIface. Sometime later, mkImportedFamInst is called using that axiom. However, the axiom may itself depend on entities which are not yet loaded as of the time of the mkImportedFamInst. Thus, if mkImportedFamInst eagerly looks at the axiom, a dependency loop spontaneously appears and GHC hangs. The solution is simply for mkImportedFamInst never, ever to look inside of the axiom until everything else is good and ready to do so. We can assume that this readiness has been achieved when some other code pulls on the axiom in the FamInst. Thus, we pattern match on the axiom lazily (in the where clause, not in the parameter list) and we assert the consistency of names there also. -} -- Make a family instance representation from the information found in an -- interface file. In particular, we get the rough match info from the iface -- (instead of computing it here). mkImportedFamInst :: Name -- Name of the family -> [Maybe Name] -- Rough match info -> CoAxiom Unbranched -- Axiom introduced -> FamInst -- Resulting family instance mkImportedFamInst :: Name -> [Maybe Name] -> CoAxiom Unbranched -> FamInst mkImportedFamInst Name fam [Maybe Name] mb_tcs CoAxiom Unbranched axiom = FamInst :: CoAxiom Unbranched -> FamFlavor -> Name -> [Maybe Name] -> [TyVar] -> [TyVar] -> [Type] -> Type -> FamInst FamInst { fi_fam :: Name fi_fam = Name fam, fi_tcs :: [Maybe Name] fi_tcs = [Maybe Name] mb_tcs, fi_tvs :: [TyVar] fi_tvs = [TyVar] tvs, fi_cvs :: [TyVar] fi_cvs = [TyVar] cvs, fi_tys :: [Type] fi_tys = [Type] tys, fi_rhs :: Type fi_rhs = Type rhs, fi_axiom :: CoAxiom Unbranched fi_axiom = CoAxiom Unbranched axiom, fi_flavor :: FamFlavor fi_flavor = FamFlavor flavor } where -- See Note [Lazy axiom match] ~(CoAxBranch { cab_lhs :: CoAxBranch -> [Type] cab_lhs = [Type] tys , cab_tvs :: CoAxBranch -> [TyVar] cab_tvs = [TyVar] tvs , cab_cvs :: CoAxBranch -> [TyVar] cab_cvs = [TyVar] cvs , cab_rhs :: CoAxBranch -> Type cab_rhs = Type rhs }) = CoAxiom Unbranched -> CoAxBranch coAxiomSingleBranch CoAxiom Unbranched axiom -- Derive the flavor for an imported FamInst rather disgustingly -- Maybe we should store it in the IfaceFamInst? flavor :: FamFlavor flavor = case HasDebugCallStack => Type -> Maybe (TyCon, [Type]) Type -> Maybe (TyCon, [Type]) splitTyConApp_maybe Type rhs of Just (TyCon tc, [Type] _) | Just CoAxiom Unbranched ax' <- TyCon -> Maybe (CoAxiom Unbranched) tyConFamilyCoercion_maybe TyCon tc , CoAxiom Unbranched ax' CoAxiom Unbranched -> CoAxiom Unbranched -> Bool forall a. Eq a => a -> a -> Bool == CoAxiom Unbranched axiom -> TyCon -> FamFlavor DataFamilyInst TyCon tc Maybe (TyCon, [Type]) _ -> FamFlavor SynFamilyInst {- ************************************************************************ * * FamInstEnv * * ************************************************************************ Note [FamInstEnv] ~~~~~~~~~~~~~~~~~ A FamInstEnv maps a family name to the list of known instances for that family. The same FamInstEnv includes both 'data family' and 'type family' instances. Type families are reduced during type inference, but not data families; the user explains when to use a data family instance by using constructors and pattern matching. Nevertheless it is still useful to have data families in the FamInstEnv: - For finding overlaps and conflicts - For finding the representation type...see FamInstEnv.topNormaliseType and its call site in Simplify - In standalone deriving instance Eq (T [Int]) we need to find the representation type for T [Int] Note [Varying number of patterns for data family axioms] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ For data families, the number of patterns may vary between instances. For example data family T a b data instance T Int a = T1 a | T2 data instance T Bool [a] = T3 a Then we get a data type for each instance, and an axiom: data TInt a = T1 a | T2 data TBoolList a = T3 a axiom ax7 :: T Int ~ TInt -- Eta-reduced axiom ax8 a :: T Bool [a] ~ TBoolList a These two axioms for T, one with one pattern, one with two; see Note [Eta reduction for data families] Note [FamInstEnv determinism] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We turn FamInstEnvs into a list in some places that don't directly affect the ABI. That happens in family consistency checks and when producing output for `:info`. Unfortunately that nondeterminism is nonlocal and it's hard to tell what it affects without following a chain of functions. It's also easy to accidentally make that nondeterminism affect the ABI. Furthermore the envs should be relatively small, so it should be free to use deterministic maps here. Testing with nofib and validate detected no difference between UniqFM and UniqDFM. See Note [Deterministic UniqFM]. -} type FamInstEnv = UniqDFM FamilyInstEnv -- Maps a family to its instances -- See Note [FamInstEnv] -- See Note [FamInstEnv determinism] type FamInstEnvs = (FamInstEnv, FamInstEnv) -- External package inst-env, Home-package inst-env newtype FamilyInstEnv = FamIE [FamInst] -- The instances for a particular family, in any order instance Outputable FamilyInstEnv where ppr :: FamilyInstEnv -> SDoc ppr (FamIE [FamInst] fs) = String -> SDoc text String "FamIE" SDoc -> SDoc -> SDoc <+> [SDoc] -> SDoc vcat ((FamInst -> SDoc) -> [FamInst] -> [SDoc] forall a b. (a -> b) -> [a] -> [b] map FamInst -> SDoc forall a. Outputable a => a -> SDoc ppr [FamInst] fs) -- INVARIANTS: -- * The fs_tvs are distinct in each FamInst -- of a range value of the map (so we can safely unify them) emptyFamInstEnvs :: (FamInstEnv, FamInstEnv) emptyFamInstEnvs :: (FamInstEnv, FamInstEnv) emptyFamInstEnvs = (FamInstEnv emptyFamInstEnv, FamInstEnv emptyFamInstEnv) emptyFamInstEnv :: FamInstEnv emptyFamInstEnv :: FamInstEnv emptyFamInstEnv = FamInstEnv forall elt. UniqDFM elt emptyUDFM famInstEnvElts :: FamInstEnv -> [FamInst] famInstEnvElts :: FamInstEnv -> [FamInst] famInstEnvElts FamInstEnv fi = [FamInst elt | FamIE [FamInst] elts <- FamInstEnv -> [FamilyInstEnv] forall elt. UniqDFM elt -> [elt] eltsUDFM FamInstEnv fi, FamInst elt <- [FamInst] elts] -- See Note [FamInstEnv determinism] famInstEnvSize :: FamInstEnv -> Int famInstEnvSize :: FamInstEnv -> Int famInstEnvSize = (FamilyInstEnv -> Int -> Int) -> Int -> FamInstEnv -> Int forall elt a. (elt -> a -> a) -> a -> UniqDFM elt -> a nonDetFoldUDFM (\(FamIE [FamInst] elt) Int sum -> Int sum Int -> Int -> Int forall a. Num a => a -> a -> a + [FamInst] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length [FamInst] elt) Int 0 -- It's OK to use nonDetFoldUDFM here since we're just computing the -- size. familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst] familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst] familyInstances (FamInstEnv pkg_fie, FamInstEnv home_fie) TyCon fam = FamInstEnv -> [FamInst] get FamInstEnv home_fie [FamInst] -> [FamInst] -> [FamInst] forall a. [a] -> [a] -> [a] ++ FamInstEnv -> [FamInst] get FamInstEnv pkg_fie where get :: FamInstEnv -> [FamInst] get FamInstEnv env = case FamInstEnv -> TyCon -> Maybe FamilyInstEnv forall key elt. Uniquable key => UniqDFM elt -> key -> Maybe elt lookupUDFM FamInstEnv env TyCon fam of Just (FamIE [FamInst] insts) -> [FamInst] insts Maybe FamilyInstEnv Nothing -> [] extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv extendFamInstEnvList FamInstEnv inst_env [FamInst] fis = (FamInstEnv -> FamInst -> FamInstEnv) -> FamInstEnv -> [FamInst] -> FamInstEnv forall (t :: * -> *) b a. Foldable t => (b -> a -> b) -> b -> t a -> b foldl' FamInstEnv -> FamInst -> FamInstEnv extendFamInstEnv FamInstEnv inst_env [FamInst] fis extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv extendFamInstEnv FamInstEnv inst_env ins_item :: FamInst ins_item@(FamInst {fi_fam :: FamInst -> Name fi_fam = Name cls_nm}) = (FamilyInstEnv -> FamilyInstEnv -> FamilyInstEnv) -> FamInstEnv -> Name -> FamilyInstEnv -> FamInstEnv forall key elt. Uniquable key => (elt -> elt -> elt) -> UniqDFM elt -> key -> elt -> UniqDFM elt addToUDFM_C FamilyInstEnv -> FamilyInstEnv -> FamilyInstEnv add FamInstEnv inst_env Name cls_nm ([FamInst] -> FamilyInstEnv FamIE [FamInst ins_item]) where add :: FamilyInstEnv -> FamilyInstEnv -> FamilyInstEnv add (FamIE [FamInst] items) FamilyInstEnv _ = [FamInst] -> FamilyInstEnv FamIE (FamInst ins_itemFamInst -> [FamInst] -> [FamInst] forall a. a -> [a] -> [a] :[FamInst] items) {- ************************************************************************ * * Compatibility * * ************************************************************************ Note [Apartness] ~~~~~~~~~~~~~~~~ In dealing with closed type families, we must be able to check that one type will never reduce to another. This check is called /apartness/. The check is always between a target (which may be an arbitrary type) and a pattern. Here is how we do it: apart(target, pattern) = not (unify(flatten(target), pattern)) where flatten (implemented in flattenTys, below) converts all type-family applications into fresh variables. (See Note [Flattening].) Note [Compatibility] ~~~~~~~~~~~~~~~~~~~~ Two patterns are /compatible/ if either of the following conditions hold: 1) The patterns are apart. 2) The patterns unify with a substitution S, and their right hand sides equal under that substitution. For open type families, only compatible instances are allowed. For closed type families, the story is slightly more complicated. Consider the following: type family F a where F Int = Bool F a = Int g :: Show a => a -> F a g x = length (show x) Should that type-check? No. We need to allow for the possibility that 'a' might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int only when we can be sure that 'a' is not Int. To achieve this, after finding a possible match within the equations, we have to go back to all previous equations and check that, under the substitution induced by the match, other branches are surely apart. (See Note [Apartness].) This is similar to what happens with class instance selection, when we need to guarantee that there is only a match and no unifiers. The exact algorithm is different here because the potentially-overlapping group is closed. As another example, consider this: type family G x where G Int = Bool G a = Double type family H y -- no instances Now, we want to simplify (G (H Char)). We can't, because (H Char) might later simplify to be Int. So, (G (H Char)) is stuck, for now. While everything above is quite sound, it isn't as expressive as we'd like. Consider this: type family J a where J Int = Int J a = a Can we simplify (J b) to b? Sure we can. Yes, the first equation matches if b is instantiated with Int, but the RHSs coincide there, so it's all OK. So, the rule is this: when looking up a branch in a closed type family, we find a branch that matches the target, but then we make sure that the target is apart from every previous *incompatible* branch. We don't check the branches that are compatible with the matching branch, because they are either irrelevant (clause 1 of compatible) or benign (clause 2 of compatible). Note [Compatibility of eta-reduced axioms] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In newtype instances of data families we eta-reduce the axioms, See Note [Eta reduction for data families] in FamInstEnv. This means that we sometimes need to test compatibility of two axioms that were eta-reduced to different degrees, e.g.: data family D a b c newtype instance D a Int c = DInt (Maybe a) -- D a Int ~ Maybe -- lhs = [a, Int] newtype instance D Bool Int Char = DIntChar Float -- D Bool Int Char ~ Float -- lhs = [Bool, Int, Char] These are obviously incompatible. We could detect this by saturating (eta-expanding) the shorter LHS with fresh tyvars until the lists are of equal length, but instead we can just remove the tail of the longer list, as those types will simply unify with the freshly introduced tyvars. By doing this, in case the LHS are unifiable, the yielded substitution won't mention the tyvars that appear in the tail we dropped off, and we might try to test equality RHSes of different kinds, but that's fine since this case occurs only for data families, where the RHS is a unique tycon and the equality fails anyway. -} -- See Note [Compatibility] compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool compatibleBranches (CoAxBranch { cab_lhs :: CoAxBranch -> [Type] cab_lhs = [Type] lhs1, cab_rhs :: CoAxBranch -> Type cab_rhs = Type rhs1 }) (CoAxBranch { cab_lhs :: CoAxBranch -> [Type] cab_lhs = [Type] lhs2, cab_rhs :: CoAxBranch -> Type cab_rhs = Type rhs2 }) = let ([Type] commonlhs1, [Type] commonlhs2) = [Type] -> [Type] -> ([Type], [Type]) forall a b. [a] -> [b] -> ([a], [b]) zipAndUnzip [Type] lhs1 [Type] lhs2 -- See Note [Compatibility of eta-reduced axioms] in case (TyVar -> BindFlag) -> [Type] -> [Type] -> UnifyResult tcUnifyTysFG (BindFlag -> TyVar -> BindFlag forall a b. a -> b -> a const BindFlag BindMe) [Type] commonlhs1 [Type] commonlhs2 of UnifyResult SurelyApart -> Bool True Unifiable TCvSubst subst | TCvSubst -> Type -> Type Type.substTyAddInScope TCvSubst subst Type rhs1 Type -> Type -> Bool `eqType` TCvSubst -> Type -> Type Type.substTyAddInScope TCvSubst subst Type rhs2 -> Bool True UnifyResult _ -> Bool False -- | Result of testing two type family equations for injectiviy. data InjectivityCheckResult = InjectivityAccepted -- ^ Either RHSs are distinct or unification of RHSs leads to unification of -- LHSs | InjectivityUnified CoAxBranch CoAxBranch -- ^ RHSs unify but LHSs don't unify under that substitution. Relevant for -- closed type families where equation after unification might be -- overlpapped (in which case it is OK if they don't unify). Constructor -- stores axioms after unification. -- | Check whether two type family axioms don't violate injectivity annotation. injectiveBranches :: [Bool] -> CoAxBranch -> CoAxBranch -> InjectivityCheckResult injectiveBranches :: [Bool] -> CoAxBranch -> CoAxBranch -> InjectivityCheckResult injectiveBranches [Bool] injectivity ax1 :: CoAxBranch ax1@(CoAxBranch { cab_lhs :: CoAxBranch -> [Type] cab_lhs = [Type] lhs1, cab_rhs :: CoAxBranch -> Type cab_rhs = Type rhs1 }) ax2 :: CoAxBranch ax2@(CoAxBranch { cab_lhs :: CoAxBranch -> [Type] cab_lhs = [Type] lhs2, cab_rhs :: CoAxBranch -> Type cab_rhs = Type rhs2 }) -- See Note [Verifying injectivity annotation], case 1. = let getInjArgs :: [Type] -> [Type] getInjArgs = [Bool] -> [Type] -> [Type] forall a. [Bool] -> [a] -> [a] filterByList [Bool] injectivity in case Bool -> Type -> Type -> Maybe TCvSubst tcUnifyTyWithTFs Bool True Type rhs1 Type rhs2 of -- True = two-way pre-unification Maybe TCvSubst Nothing -> InjectivityCheckResult InjectivityAccepted -- RHS are different, so equations are injective. -- This is case 1A from Note [Verifying injectivity annotation] Just TCvSubst subst -> -- RHS unify under a substitution let lhs1Subst :: [Type] lhs1Subst = HasCallStack => TCvSubst -> [Type] -> [Type] TCvSubst -> [Type] -> [Type] Type.substTys TCvSubst subst ([Type] -> [Type] getInjArgs [Type] lhs1) lhs2Subst :: [Type] lhs2Subst = HasCallStack => TCvSubst -> [Type] -> [Type] TCvSubst -> [Type] -> [Type] Type.substTys TCvSubst subst ([Type] -> [Type] getInjArgs [Type] lhs2) -- If LHSs are equal under the substitution used for RHSs then this pair -- of equations does not violate injectivity annotation. If LHSs are not -- equal under that substitution then this pair of equations violates -- injectivity annotation, but for closed type families it still might -- be the case that one LHS after substitution is unreachable. in if [Type] -> [Type] -> Bool eqTypes [Type] lhs1Subst [Type] lhs2Subst -- check case 1B1 from Note. then InjectivityCheckResult InjectivityAccepted else CoAxBranch -> CoAxBranch -> InjectivityCheckResult InjectivityUnified ( CoAxBranch ax1 { cab_lhs :: [Type] cab_lhs = HasCallStack => TCvSubst -> [Type] -> [Type] TCvSubst -> [Type] -> [Type] Type.substTys TCvSubst subst [Type] lhs1 , cab_rhs :: Type cab_rhs = HasCallStack => TCvSubst -> Type -> Type TCvSubst -> Type -> Type Type.substTy TCvSubst subst Type rhs1 }) ( CoAxBranch ax2 { cab_lhs :: [Type] cab_lhs = HasCallStack => TCvSubst -> [Type] -> [Type] TCvSubst -> [Type] -> [Type] Type.substTys TCvSubst subst [Type] lhs2 , cab_rhs :: Type cab_rhs = HasCallStack => TCvSubst -> Type -> Type TCvSubst -> Type -> Type Type.substTy TCvSubst subst Type rhs2 }) -- payload of InjectivityUnified used only for check 1B2, only -- for closed type families -- takes a CoAxiom with unknown branch incompatibilities and computes -- the compatibilities -- See Note [Storing compatibility] in CoAxiom computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch] computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch] computeAxiomIncomps [CoAxBranch] branches = ([CoAxBranch], [CoAxBranch]) -> [CoAxBranch] forall a b. (a, b) -> b snd (([CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)) -> [CoAxBranch] -> [CoAxBranch] -> ([CoAxBranch], [CoAxBranch]) forall (t :: * -> *) a b c. Traversable t => (a -> b -> (a, c)) -> a -> t b -> (a, t c) mapAccumL [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch) go [] [CoAxBranch] branches) where go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch) go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch) go [CoAxBranch] prev_brs CoAxBranch cur_br = (CoAxBranch cur_br CoAxBranch -> [CoAxBranch] -> [CoAxBranch] forall a. a -> [a] -> [a] : [CoAxBranch] prev_brs, CoAxBranch new_br) where new_br :: CoAxBranch new_br = CoAxBranch cur_br { cab_incomps :: [CoAxBranch] cab_incomps = [CoAxBranch] -> CoAxBranch -> [CoAxBranch] mk_incomps [CoAxBranch] prev_brs CoAxBranch cur_br } mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch] mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch] mk_incomps [CoAxBranch] prev_brs CoAxBranch cur_br = (CoAxBranch -> Bool) -> [CoAxBranch] -> [CoAxBranch] forall a. (a -> Bool) -> [a] -> [a] filter (Bool -> Bool not (Bool -> Bool) -> (CoAxBranch -> Bool) -> CoAxBranch -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . CoAxBranch -> CoAxBranch -> Bool compatibleBranches CoAxBranch cur_br) [CoAxBranch] prev_brs {- ************************************************************************ * * Constructing axioms These functions are here because tidyType / tcUnifyTysFG are not available in CoAxiom Also computeAxiomIncomps is too sophisticated for CoAxiom * * ************************************************************************ Note [Tidy axioms when we build them] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Like types and classes, we build axioms fully quantified over all their variables, and tidy them when we build them. For example, we print out axioms and don't want to print stuff like F k k a b = ... Instead we must tidy those kind variables. See #7524. We could instead tidy when we print, but that makes it harder to get things like injectivity errors to come out right. Danger of Type family equation violates injectivity annotation. Kind variable ‘k’ cannot be inferred from the right-hand side. In the type family equation: PolyKindVars @[k1] @[k2] ('[] @k1) = '[] @k2 Note [Always number wildcard types in CoAxBranch] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider the following example (from the DataFamilyInstanceLHS test case): data family Sing (a :: k) data instance Sing (_ :: MyKind) where SingA :: Sing A SingB :: Sing B If we're not careful during tidying, then when this program is compiled with -ddump-types, we'll get the following information: COERCION AXIOMS axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 :: Sing _ = DataFamilyInstanceLHS.R:SingMyKind_ _ It's misleading to have a wildcard type appearing on the RHS like that. To avoid this issue, when building a CoAxiom (which is what eventually gets printed above), we tidy all the variables in an env that already contains '_'. Thus, any variable named '_' will be renamed, giving us the nicer output here: COERCION AXIOMS axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 :: Sing _1 = DataFamilyInstanceLHS.R:SingMyKind_ _1 Which is at least legal syntax. See also Note [CoAxBranch type variables] in CoAxiom; note that we are tidying (changing OccNames only), not freshening, in accordance with that Note. -} -- all axiom roles are Nominal, as this is only used with type families mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars -> [TyVar] -- Extra eta tyvars -> [CoVar] -- possibly stale covars -> [Type] -- LHS patterns -> Type -- RHS -> [Role] -> SrcSpan -> CoAxBranch mkCoAxBranch :: [TyVar] -> [TyVar] -> [TyVar] -> [Type] -> Type -> [Role] -> SrcSpan -> CoAxBranch mkCoAxBranch [TyVar] tvs [TyVar] eta_tvs [TyVar] cvs [Type] lhs Type rhs [Role] roles SrcSpan loc = CoAxBranch :: SrcSpan -> [TyVar] -> [TyVar] -> [TyVar] -> [Role] -> [Type] -> Type -> [CoAxBranch] -> CoAxBranch CoAxBranch { cab_tvs :: [TyVar] cab_tvs = [TyVar] tvs' , cab_eta_tvs :: [TyVar] cab_eta_tvs = [TyVar] eta_tvs' , cab_cvs :: [TyVar] cab_cvs = [TyVar] cvs' , cab_lhs :: [Type] cab_lhs = TidyEnv -> [Type] -> [Type] tidyTypes TidyEnv env [Type] lhs , cab_roles :: [Role] cab_roles = [Role] roles , cab_rhs :: Type cab_rhs = TidyEnv -> Type -> Type tidyType TidyEnv env Type rhs , cab_loc :: SrcSpan cab_loc = SrcSpan loc , cab_incomps :: [CoAxBranch] cab_incomps = [CoAxBranch] placeHolderIncomps } where (TidyEnv env1, [TyVar] tvs') = TidyEnv -> [TyVar] -> (TidyEnv, [TyVar]) tidyVarBndrs TidyEnv init_tidy_env [TyVar] tvs (TidyEnv env2, [TyVar] eta_tvs') = TidyEnv -> [TyVar] -> (TidyEnv, [TyVar]) tidyVarBndrs TidyEnv env1 [TyVar] eta_tvs (TidyEnv env, [TyVar] cvs') = TidyEnv -> [TyVar] -> (TidyEnv, [TyVar]) tidyVarBndrs TidyEnv env2 [TyVar] cvs -- See Note [Tidy axioms when we build them] -- See also Note [CoAxBranch type variables] in CoAxiom init_occ_env :: TidyOccEnv init_occ_env = [OccName] -> TidyOccEnv initTidyOccEnv [String -> OccName mkTyVarOcc String "_"] init_tidy_env :: TidyEnv init_tidy_env = TidyOccEnv -> TidyEnv mkEmptyTidyEnv TidyOccEnv init_occ_env -- See Note [Always number wildcard types in CoAxBranch] -- all of the following code is here to avoid mutual dependencies with -- Coercion mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched mkBranchedCoAxiom Name ax_name TyCon fam_tc [CoAxBranch] branches = CoAxiom :: forall (br :: BranchFlag). Unique -> Name -> Role -> TyCon -> Branches br -> Bool -> CoAxiom br CoAxiom { co_ax_unique :: Unique co_ax_unique = Name -> Unique nameUnique Name ax_name , co_ax_name :: Name co_ax_name = Name ax_name , co_ax_tc :: TyCon co_ax_tc = TyCon fam_tc , co_ax_role :: Role co_ax_role = Role Nominal , co_ax_implicit :: Bool co_ax_implicit = Bool False , co_ax_branches :: Branches Branched co_ax_branches = [CoAxBranch] -> Branches Branched manyBranches ([CoAxBranch] -> [CoAxBranch] computeAxiomIncomps [CoAxBranch] branches) } mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched mkUnbranchedCoAxiom Name ax_name TyCon fam_tc CoAxBranch branch = CoAxiom :: forall (br :: BranchFlag). Unique -> Name -> Role -> TyCon -> Branches br -> Bool -> CoAxiom br CoAxiom { co_ax_unique :: Unique co_ax_unique = Name -> Unique nameUnique Name ax_name , co_ax_name :: Name co_ax_name = Name ax_name , co_ax_tc :: TyCon co_ax_tc = TyCon fam_tc , co_ax_role :: Role co_ax_role = Role Nominal , co_ax_implicit :: Bool co_ax_implicit = Bool False , co_ax_branches :: Branches Unbranched co_ax_branches = CoAxBranch -> Branches Unbranched unbranched (CoAxBranch branch { cab_incomps :: [CoAxBranch] cab_incomps = [] }) } mkSingleCoAxiom :: Role -> Name -> [TyVar] -> [TyVar] -> [CoVar] -> TyCon -> [Type] -> Type -> CoAxiom Unbranched -- Make a single-branch CoAxiom, incluidng making the branch itself -- Used for both type family (Nominal) and data family (Representational) -- axioms, hence passing in the Role mkSingleCoAxiom :: Role -> Name -> [TyVar] -> [TyVar] -> [TyVar] -> TyCon -> [Type] -> Type -> CoAxiom Unbranched mkSingleCoAxiom Role role Name ax_name [TyVar] tvs [TyVar] eta_tvs [TyVar] cvs TyCon fam_tc [Type] lhs_tys Type rhs_ty = CoAxiom :: forall (br :: BranchFlag). Unique -> Name -> Role -> TyCon -> Branches br -> Bool -> CoAxiom br CoAxiom { co_ax_unique :: Unique co_ax_unique = Name -> Unique nameUnique Name ax_name , co_ax_name :: Name co_ax_name = Name ax_name , co_ax_tc :: TyCon co_ax_tc = TyCon fam_tc , co_ax_role :: Role co_ax_role = Role role , co_ax_implicit :: Bool co_ax_implicit = Bool False , co_ax_branches :: Branches Unbranched co_ax_branches = CoAxBranch -> Branches Unbranched unbranched (CoAxBranch branch { cab_incomps :: [CoAxBranch] cab_incomps = [] }) } where branch :: CoAxBranch branch = [TyVar] -> [TyVar] -> [TyVar] -> [Type] -> Type -> [Role] -> SrcSpan -> CoAxBranch mkCoAxBranch [TyVar] tvs [TyVar] eta_tvs [TyVar] cvs [Type] lhs_tys Type rhs_ty ((TyVar -> Role) -> [TyVar] -> [Role] forall a b. (a -> b) -> [a] -> [b] map (Role -> TyVar -> Role forall a b. a -> b -> a const Role Nominal) [TyVar] tvs) (Name -> SrcSpan forall a. NamedThing a => a -> SrcSpan getSrcSpan Name ax_name) -- | Create a coercion constructor (axiom) suitable for the given -- newtype 'TyCon'. The 'Name' should be that of a new coercion -- 'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and -- the type the appropriate right hand side of the @newtype@, with -- the free variables a subset of those 'TyVar's. mkNewTypeCoAxiom :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched mkNewTypeCoAxiom :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched mkNewTypeCoAxiom Name name TyCon tycon [TyVar] tvs [Role] roles Type rhs_ty = CoAxiom :: forall (br :: BranchFlag). Unique -> Name -> Role -> TyCon -> Branches br -> Bool -> CoAxiom br CoAxiom { co_ax_unique :: Unique co_ax_unique = Name -> Unique nameUnique Name name , co_ax_name :: Name co_ax_name = Name name , co_ax_implicit :: Bool co_ax_implicit = Bool True -- See Note [Implicit axioms] in TyCon , co_ax_role :: Role co_ax_role = Role Representational , co_ax_tc :: TyCon co_ax_tc = TyCon tycon , co_ax_branches :: Branches Unbranched co_ax_branches = CoAxBranch -> Branches Unbranched unbranched (CoAxBranch branch { cab_incomps :: [CoAxBranch] cab_incomps = [] }) } where branch :: CoAxBranch branch = [TyVar] -> [TyVar] -> [TyVar] -> [Type] -> Type -> [Role] -> SrcSpan -> CoAxBranch mkCoAxBranch [TyVar] tvs [] [] ([TyVar] -> [Type] mkTyVarTys [TyVar] tvs) Type rhs_ty [Role] roles (Name -> SrcSpan forall a. NamedThing a => a -> SrcSpan getSrcSpan Name name) {- ************************************************************************ * * Looking up a family instance * * ************************************************************************ @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match. Multiple matches are only possible in case of type families (not data families), and then, it doesn't matter which match we choose (as the instances are guaranteed confluent). We return the matching family instances and the type instance at which it matches. For example, if we lookup 'T [Int]' and have a family instance data instance T [a] = .. desugared to data :R42T a = .. coe :Co:R42T a :: T [a] ~ :R42T a we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'. -} -- when matching a type family application, we get a FamInst, -- and the list of types the axiom should be applied to data FamInstMatch = FamInstMatch { FamInstMatch -> FamInst fim_instance :: FamInst , FamInstMatch -> [Type] fim_tys :: [Type] , FamInstMatch -> [Coercion] fim_cos :: [Coercion] } -- See Note [Over-saturated matches] instance Outputable FamInstMatch where ppr :: FamInstMatch -> SDoc ppr (FamInstMatch { fim_instance :: FamInstMatch -> FamInst fim_instance = FamInst inst , fim_tys :: FamInstMatch -> [Type] fim_tys = [Type] tys , fim_cos :: FamInstMatch -> [Coercion] fim_cos = [Coercion] cos }) = String -> SDoc text String "match with" SDoc -> SDoc -> SDoc <+> SDoc -> SDoc parens (FamInst -> SDoc forall a. Outputable a => a -> SDoc ppr FamInst inst) SDoc -> SDoc -> SDoc <+> [Type] -> SDoc forall a. Outputable a => a -> SDoc ppr [Type] tys SDoc -> SDoc -> SDoc <+> [Coercion] -> SDoc forall a. Outputable a => a -> SDoc ppr [Coercion] cos lookupFamInstEnvByTyCon :: FamInstEnvs -> TyCon -> [FamInst] lookupFamInstEnvByTyCon :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst] lookupFamInstEnvByTyCon (FamInstEnv pkg_ie, FamInstEnv home_ie) TyCon fam_tc = FamInstEnv -> [FamInst] get FamInstEnv pkg_ie [FamInst] -> [FamInst] -> [FamInst] forall a. [a] -> [a] -> [a] ++ FamInstEnv -> [FamInst] get FamInstEnv home_ie where get :: FamInstEnv -> [FamInst] get FamInstEnv ie = case FamInstEnv -> TyCon -> Maybe FamilyInstEnv forall key elt. Uniquable key => UniqDFM elt -> key -> Maybe elt lookupUDFM FamInstEnv ie TyCon fam_tc of Maybe FamilyInstEnv Nothing -> [] Just (FamIE [FamInst] fis) -> [FamInst] fis lookupFamInstEnv :: FamInstEnvs -> TyCon -> [Type] -- What we are looking for -> [FamInstMatch] -- Successful matches -- Precondition: the tycon is saturated (or over-saturated) lookupFamInstEnv :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> [FamInstMatch] lookupFamInstEnv = MatchFun -> (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> [FamInstMatch] lookup_fam_inst_env MatchFun forall p p. p -> p -> [Type] -> [Type] -> Maybe TCvSubst match where match :: p -> p -> [Type] -> [Type] -> Maybe TCvSubst match p _ p _ [Type] tpl_tys [Type] tys = [Type] -> [Type] -> Maybe TCvSubst tcMatchTys [Type] tpl_tys [Type] tys lookupFamInstEnvConflicts :: FamInstEnvs -> FamInst -- Putative new instance -> [FamInstMatch] -- Conflicting matches (don't look at the fim_tys field) -- E.g. when we are about to add -- f : type instance F [a] = a->a -- we do (lookupFamInstConflicts f [b]) -- to find conflicting matches -- -- Precondition: the tycon is saturated (or over-saturated) lookupFamInstEnvConflicts :: (FamInstEnv, FamInstEnv) -> FamInst -> [FamInstMatch] lookupFamInstEnvConflicts (FamInstEnv, FamInstEnv) envs fam_inst :: FamInst fam_inst@(FamInst { fi_axiom :: FamInst -> CoAxiom Unbranched fi_axiom = CoAxiom Unbranched new_axiom }) = MatchFun -> (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> [FamInstMatch] lookup_fam_inst_env MatchFun my_unify (FamInstEnv, FamInstEnv) envs TyCon fam [Type] tys where (TyCon fam, [Type] tys) = FamInst -> (TyCon, [Type]) famInstSplitLHS FamInst fam_inst -- In example above, fam tys' = F [b] my_unify :: MatchFun my_unify (FamInst { fi_axiom :: FamInst -> CoAxiom Unbranched fi_axiom = CoAxiom Unbranched old_axiom }) VarSet tpl_tvs [Type] tpl_tys [Type] _ = ASSERT2( tyCoVarsOfTypes tys `disjointVarSet` tpl_tvs, (ppr fam <+> ppr tys) $$ (ppr tpl_tvs <+> ppr tpl_tys) ) -- Unification will break badly if the variables overlap -- They shouldn't because we allocate separate uniques for them if CoAxBranch -> CoAxBranch -> Bool compatibleBranches (CoAxiom Unbranched -> CoAxBranch coAxiomSingleBranch CoAxiom Unbranched old_axiom) CoAxBranch new_branch then Maybe TCvSubst forall a. Maybe a Nothing else TCvSubst -> Maybe TCvSubst forall a. a -> Maybe a Just TCvSubst forall a. a noSubst -- Note [Family instance overlap conflicts] noSubst :: a noSubst = String -> a forall a. String -> a panic String "lookupFamInstEnvConflicts noSubst" new_branch :: CoAxBranch new_branch = CoAxiom Unbranched -> CoAxBranch coAxiomSingleBranch CoAxiom Unbranched new_axiom -------------------------------------------------------------------------------- -- Type family injectivity checking bits -- -------------------------------------------------------------------------------- {- Note [Verifying injectivity annotation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Injectivity means that the RHS of a type family uniquely determines the LHS (see Note [Type inference for type families with injectivity]). The user informs us about injectivity using an injectivity annotation and it is GHC's task to verify that this annotation is correct w.r.t. type family equations. Whenever we see a new equation of a type family we need to make sure that adding this equation to the already known equations of a type family does not violate the injectivity annotation supplied by the user (see Note [Injectivity annotation]). Of course if the type family has no injectivity annotation then no check is required. But if a type family has injectivity annotation we need to make sure that the following conditions hold: 1. For each pair of *different* equations of a type family, one of the following conditions holds: A: RHSs are different. (Check done in FamInstEnv.injectiveBranches) B1: OPEN TYPE FAMILIES: If the RHSs can be unified under some substitution then it must be possible to unify the LHSs under the same substitution. Example: type family FunnyId a = r | r -> a type instance FunnyId Int = Int type instance FunnyId a = a RHSs of these two equations unify under [ a |-> Int ] substitution. Under this substitution LHSs are equal therefore these equations don't violate injectivity annotation. (Check done in FamInstEnv.injectiveBranches) B2: CLOSED TYPE FAMILIES: If the RHSs can be unified under some substitution then either the LHSs unify under the same substitution or the LHS of the latter equation is overlapped by earlier equations. Example 1: type family SwapIntChar a = r | r -> a where SwapIntChar Int = Char SwapIntChar Char = Int SwapIntChar a = a Say we are checking the last two equations. RHSs unify under [ a |-> Int ] substitution but LHSs don't. So we apply the substitution to LHS of last equation and check whether it is overlapped by any of previous equations. Since it is overlapped by the first equation we conclude that pair of last two equations does not violate injectivity annotation. (Check done in TcValidity.checkValidCoAxiom#gather_conflicts) A special case of B is when RHSs unify with an empty substitution ie. they are identical. If any of the above two conditions holds we conclude that the pair of equations does not violate injectivity annotation. But if we find a pair of equations where neither of the above holds we report that this pair violates injectivity annotation because for a given RHS we don't have a unique LHS. (Note that (B) actually implies (A).) Note that we only take into account these LHS patterns that were declared as injective. 2. If an RHS of a type family equation is a bare type variable then all LHS variables (including implicit kind variables) also have to be bare. In other words, this has to be a sole equation of that type family and it has to cover all possible patterns. So for example this definition will be rejected: type family W1 a = r | r -> a type instance W1 [a] = a If it were accepted we could call `W1 [W1 Int]`, which would reduce to `W1 Int` and then by injectivity we could conclude that `[W1 Int] ~ Int`, which is bogus. Checked FamInst.bareTvInRHSViolated. 3. If the RHS of a type family equation is a type family application then the type family is rejected as not injective. This is checked by FamInst.isTFHeaded. 4. If a LHS type variable that is declared as injective is not mentioned in an injective position in the RHS then the type family is rejected as not injective. "Injective position" means either an argument to a type constructor or argument to a type family on injective position. There are subtleties here. See Note [Coverage condition for injective type families] in FamInst. Check (1) must be done for all family instances (transitively) imported. Other checks (2-4) should be done just for locally written equations, as they are checks involving just a single equation, not about interactions. Doing the other checks for imported equations led to #17405, as the behavior of check (4) depends on -XUndecidableInstances (see Note [Coverage condition for injective type families] in FamInst), which may vary between modules. See also Note [Injective type families] in TyCon -} -- | Check whether an open type family equation can be added to already existing -- instance environment without causing conflicts with supplied injectivity -- annotations. Returns list of conflicting axioms (type instance -- declarations). lookupFamInstEnvInjectivityConflicts :: [Bool] -- injectivity annotation for this type family instance -- INVARIANT: list contains at least one True value -> FamInstEnvs -- all type instances seens so far -> FamInst -- new type instance that we're checking -> [CoAxBranch] -- conflicting instance declarations lookupFamInstEnvInjectivityConflicts :: [Bool] -> (FamInstEnv, FamInstEnv) -> FamInst -> [CoAxBranch] lookupFamInstEnvInjectivityConflicts [Bool] injList (FamInstEnv pkg_ie, FamInstEnv home_ie) fam_inst :: FamInst fam_inst@(FamInst { fi_axiom :: FamInst -> CoAxiom Unbranched fi_axiom = CoAxiom Unbranched new_axiom }) -- See Note [Verifying injectivity annotation]. This function implements -- check (1.B1) for open type families described there. = FamInstEnv -> [CoAxBranch] lookup_inj_fam_conflicts FamInstEnv home_ie [CoAxBranch] -> [CoAxBranch] -> [CoAxBranch] forall a. [a] -> [a] -> [a] ++ FamInstEnv -> [CoAxBranch] lookup_inj_fam_conflicts FamInstEnv pkg_ie where fam :: TyCon fam = FamInst -> TyCon famInstTyCon FamInst fam_inst new_branch :: CoAxBranch new_branch = CoAxiom Unbranched -> CoAxBranch coAxiomSingleBranch CoAxiom Unbranched new_axiom -- filtering function used by `lookup_inj_fam_conflicts` to check whether -- a pair of equations conflicts with the injectivity annotation. isInjConflict :: FamInst -> Bool isInjConflict (FamInst { fi_axiom :: FamInst -> CoAxiom Unbranched fi_axiom = CoAxiom Unbranched old_axiom }) | InjectivityCheckResult InjectivityAccepted <- [Bool] -> CoAxBranch -> CoAxBranch -> InjectivityCheckResult injectiveBranches [Bool] injList (CoAxiom Unbranched -> CoAxBranch coAxiomSingleBranch CoAxiom Unbranched old_axiom) CoAxBranch new_branch = Bool False -- no conflict | Bool otherwise = Bool True lookup_inj_fam_conflicts :: FamInstEnv -> [CoAxBranch] lookup_inj_fam_conflicts FamInstEnv ie | TyCon -> Bool isOpenFamilyTyCon TyCon fam, Just (FamIE [FamInst] insts) <- FamInstEnv -> TyCon -> Maybe FamilyInstEnv forall key elt. Uniquable key => UniqDFM elt -> key -> Maybe elt lookupUDFM FamInstEnv ie TyCon fam = (FamInst -> CoAxBranch) -> [FamInst] -> [CoAxBranch] forall a b. (a -> b) -> [a] -> [b] map (CoAxiom Unbranched -> CoAxBranch coAxiomSingleBranch (CoAxiom Unbranched -> CoAxBranch) -> (FamInst -> CoAxiom Unbranched) -> FamInst -> CoAxBranch forall b c a. (b -> c) -> (a -> b) -> a -> c . FamInst -> CoAxiom Unbranched fi_axiom) ([FamInst] -> [CoAxBranch]) -> [FamInst] -> [CoAxBranch] forall a b. (a -> b) -> a -> b $ (FamInst -> Bool) -> [FamInst] -> [FamInst] forall a. (a -> Bool) -> [a] -> [a] filter FamInst -> Bool isInjConflict [FamInst] insts | Bool otherwise = [] -------------------------------------------------------------------------------- -- Type family overlap checking bits -- -------------------------------------------------------------------------------- {- Note [Family instance overlap conflicts] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - In the case of data family instances, any overlap is fundamentally a conflict (as these instances imply injective type mappings). - In the case of type family instances, overlap is admitted as long as the right-hand sides of the overlapping rules coincide under the overlap substitution. eg type instance F a Int = a type instance F Int b = b These two overlap on (F Int Int) but then both RHSs are Int, so all is well. We require that they are syntactically equal; anything else would be difficult to test for at this stage. -} ------------------------------------------------------------ -- Might be a one-way match or a unifier type MatchFun = FamInst -- The FamInst template -> TyVarSet -> [Type] -- fi_tvs, fi_tys of that FamInst -> [Type] -- Target to match against -> Maybe TCvSubst lookup_fam_inst_env' -- The worker, local to this module :: MatchFun -> FamInstEnv -> TyCon -> [Type] -- What we are looking for -> [FamInstMatch] lookup_fam_inst_env' :: MatchFun -> FamInstEnv -> TyCon -> [Type] -> [FamInstMatch] lookup_fam_inst_env' MatchFun match_fun FamInstEnv ie TyCon fam [Type] match_tys | TyCon -> Bool isOpenFamilyTyCon TyCon fam , Just (FamIE [FamInst] insts) <- FamInstEnv -> TyCon -> Maybe FamilyInstEnv forall key elt. Uniquable key => UniqDFM elt -> key -> Maybe elt lookupUDFM FamInstEnv ie TyCon fam = [FamInst] -> [FamInstMatch] find [FamInst] insts -- The common case | Bool otherwise = [] where find :: [FamInst] -> [FamInstMatch] find [] = [] find (item :: FamInst item@(FamInst { fi_tcs :: FamInst -> [Maybe Name] fi_tcs = [Maybe Name] mb_tcs, fi_tvs :: FamInst -> [TyVar] fi_tvs = [TyVar] tpl_tvs, fi_cvs :: FamInst -> [TyVar] fi_cvs = [TyVar] tpl_cvs , fi_tys :: FamInst -> [Type] fi_tys = [Type] tpl_tys }) : [FamInst] rest) -- Fast check for no match, uses the "rough match" fields | [Maybe Name] -> [Maybe Name] -> Bool instanceCantMatch [Maybe Name] rough_tcs [Maybe Name] mb_tcs = [FamInst] -> [FamInstMatch] find [FamInst] rest -- Proper check | Just TCvSubst subst <- MatchFun match_fun FamInst item ([TyVar] -> VarSet mkVarSet [TyVar] tpl_tvs) [Type] tpl_tys [Type] match_tys1 = (FamInstMatch :: FamInst -> [Type] -> [Coercion] -> FamInstMatch FamInstMatch { fim_instance :: FamInst fim_instance = FamInst item , fim_tys :: [Type] fim_tys = TCvSubst -> [TyVar] -> [Type] substTyVars TCvSubst subst [TyVar] tpl_tvs [Type] -> [Type] -> [Type] forall a. [a] -> [a] -> [a] `chkAppend` [Type] match_tys2 , fim_cos :: [Coercion] fim_cos = ASSERT( all (isJust . lookupCoVar subst) tpl_cvs ) TCvSubst -> [TyVar] -> [Coercion] substCoVars TCvSubst subst [TyVar] tpl_cvs }) FamInstMatch -> [FamInstMatch] -> [FamInstMatch] forall a. a -> [a] -> [a] : [FamInst] -> [FamInstMatch] find [FamInst] rest -- No match => try next | Bool otherwise = [FamInst] -> [FamInstMatch] find [FamInst] rest where ([Maybe Name] rough_tcs, [Type] match_tys1, [Type] match_tys2) = [Type] -> ([Maybe Name], [Type], [Type]) split_tys [Type] tpl_tys -- Precondition: the tycon is saturated (or over-saturated) -- Deal with over-saturation -- See Note [Over-saturated matches] split_tys :: [Type] -> ([Maybe Name], [Type], [Type]) split_tys [Type] tpl_tys | TyCon -> Bool isTypeFamilyTyCon TyCon fam = ([Maybe Name], [Type], [Type]) pre_rough_split_tys | Bool otherwise = let ([Type] match_tys1, [Type] match_tys2) = [Type] -> [Type] -> ([Type], [Type]) forall b a. [b] -> [a] -> ([a], [a]) splitAtList [Type] tpl_tys [Type] match_tys rough_tcs :: [Maybe Name] rough_tcs = [Type] -> [Maybe Name] roughMatchTcs [Type] match_tys1 in ([Maybe Name] rough_tcs, [Type] match_tys1, [Type] match_tys2) ([Type] pre_match_tys1, [Type] pre_match_tys2) = Int -> [Type] -> ([Type], [Type]) forall a. Int -> [a] -> ([a], [a]) splitAt (TyCon -> Int tyConArity TyCon fam) [Type] match_tys pre_rough_split_tys :: ([Maybe Name], [Type], [Type]) pre_rough_split_tys = ([Type] -> [Maybe Name] roughMatchTcs [Type] pre_match_tys1, [Type] pre_match_tys1, [Type] pre_match_tys2) lookup_fam_inst_env -- The worker, local to this module :: MatchFun -> FamInstEnvs -> TyCon -> [Type] -- What we are looking for -> [FamInstMatch] -- Successful matches -- Precondition: the tycon is saturated (or over-saturated) lookup_fam_inst_env :: MatchFun -> (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> [FamInstMatch] lookup_fam_inst_env MatchFun match_fun (FamInstEnv pkg_ie, FamInstEnv home_ie) TyCon fam [Type] tys = MatchFun -> FamInstEnv -> TyCon -> [Type] -> [FamInstMatch] lookup_fam_inst_env' MatchFun match_fun FamInstEnv home_ie TyCon fam [Type] tys [FamInstMatch] -> [FamInstMatch] -> [FamInstMatch] forall a. [a] -> [a] -> [a] ++ MatchFun -> FamInstEnv -> TyCon -> [Type] -> [FamInstMatch] lookup_fam_inst_env' MatchFun match_fun FamInstEnv pkg_ie TyCon fam [Type] tys {- Note [Over-saturated matches] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ It's ok to look up an over-saturated type constructor. E.g. type family F a :: * -> * type instance F (a,b) = Either (a->b) The type instance gives rise to a newtype TyCon (at a higher kind which you can't do in Haskell!): newtype FPair a b = FP (Either (a->b)) Then looking up (F (Int,Bool) Char) will return a FamInstMatch (FPair, [Int,Bool,Char]) The "extra" type argument [Char] just stays on the end. We handle data families and type families separately here: * For type families, all instances of a type family must have the same arity, so we can precompute the split between the match_tys and the overflow tys. This is done in pre_rough_split_tys. * For data family instances, though, we need to re-split for each instance, because the breakdown might be different for each instance. Why? Because of eta reduction; see Note [Eta reduction for data families]. -} -- checks if one LHS is dominated by a list of other branches -- in other words, if an application would match the first LHS, it is guaranteed -- to match at least one of the others. The RHSs are ignored. -- This algorithm is conservative: -- True -> the LHS is definitely covered by the others -- False -> no information -- It is currently (Oct 2012) used only for generating errors for -- inaccessible branches. If these errors go unreported, no harm done. -- This is defined here to avoid a dependency from CoAxiom to Unify isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool isDominatedBy CoAxBranch branch [CoAxBranch] branches = [Bool] -> Bool forall (t :: * -> *). Foldable t => t Bool -> Bool or ([Bool] -> Bool) -> [Bool] -> Bool forall a b. (a -> b) -> a -> b $ (CoAxBranch -> Bool) -> [CoAxBranch] -> [Bool] forall a b. (a -> b) -> [a] -> [b] map CoAxBranch -> Bool match [CoAxBranch] branches where lhs :: [Type] lhs = CoAxBranch -> [Type] coAxBranchLHS CoAxBranch branch match :: CoAxBranch -> Bool match (CoAxBranch { cab_lhs :: CoAxBranch -> [Type] cab_lhs = [Type] tys }) = Maybe TCvSubst -> Bool forall a. Maybe a -> Bool isJust (Maybe TCvSubst -> Bool) -> Maybe TCvSubst -> Bool forall a b. (a -> b) -> a -> b $ [Type] -> [Type] -> Maybe TCvSubst tcMatchTys [Type] tys [Type] lhs {- ************************************************************************ * * Choosing an axiom application * * ************************************************************************ The lookupFamInstEnv function does a nice job for *open* type families, but we also need to handle closed ones when normalising a type: -} reduceTyFamApp_maybe :: FamInstEnvs -> Role -- Desired role of result coercion -> TyCon -> [Type] -> Maybe (Coercion, Type) -- Attempt to do a *one-step* reduction of a type-family application -- but *not* newtypes -- Works on type-synonym families always; data-families only if -- the role we seek is representational -- It does *not* normlise the type arguments first, so this may not -- go as far as you want. If you want normalised type arguments, -- use normaliseTcArgs first. -- -- The TyCon can be oversaturated. -- Works on both open and closed families -- -- Always returns a *homogeneous* coercion -- type family reductions are always -- homogeneous reduceTyFamApp_maybe :: (FamInstEnv, FamInstEnv) -> Role -> TyCon -> [Type] -> Maybe (Coercion, Type) reduceTyFamApp_maybe (FamInstEnv, FamInstEnv) envs Role role TyCon tc [Type] tys | Role Phantom <- Role role = Maybe (Coercion, Type) forall a. Maybe a Nothing | case Role role of Role Representational -> TyCon -> Bool isOpenFamilyTyCon TyCon tc Role _ -> TyCon -> Bool isOpenTypeFamilyTyCon TyCon tc -- If we seek a representational coercion -- (e.g. the call in topNormaliseType_maybe) then we can -- unwrap data families as well as type-synonym families; -- otherwise only type-synonym families , FamInstMatch { fim_instance :: FamInstMatch -> FamInst fim_instance = FamInst { fi_axiom :: FamInst -> CoAxiom Unbranched fi_axiom = CoAxiom Unbranched ax } , fim_tys :: FamInstMatch -> [Type] fim_tys = [Type] inst_tys , fim_cos :: FamInstMatch -> [Coercion] fim_cos = [Coercion] inst_cos } : [FamInstMatch] _ <- (FamInstEnv, FamInstEnv) -> TyCon -> [Type] -> [FamInstMatch] lookupFamInstEnv (FamInstEnv, FamInstEnv) envs TyCon tc [Type] tys -- NB: Allow multiple matches because of compatible overlap = let co :: Coercion co = Role -> CoAxiom Unbranched -> [Type] -> [Coercion] -> Coercion mkUnbranchedAxInstCo Role role CoAxiom Unbranched ax [Type] inst_tys [Coercion] inst_cos ty :: Type ty = Pair Type -> Type forall a. Pair a -> a pSnd (Coercion -> Pair Type coercionKind Coercion co) in (Coercion, Type) -> Maybe (Coercion, Type) forall a. a -> Maybe a Just (Coercion co, Type ty) | Just CoAxiom Branched ax <- TyCon -> Maybe (CoAxiom Branched) isClosedSynFamilyTyConWithAxiom_maybe TyCon tc , Just (Int ind, [Type] inst_tys, [Coercion] inst_cos) <- CoAxiom Branched -> [Type] -> Maybe (Int, [Type], [Coercion]) chooseBranch CoAxiom Branched ax [Type] tys = let co :: Coercion co = Role -> CoAxiom Branched -> Int -> [Type] -> [Coercion] -> Coercion forall (br :: BranchFlag). Role -> CoAxiom br -> Int -> [Type] -> [Coercion] -> Coercion mkAxInstCo Role role CoAxiom Branched ax Int ind [Type] inst_tys [Coercion] inst_cos ty :: Type ty = Pair Type -> Type forall a. Pair a -> a pSnd (Coercion -> Pair Type coercionKind Coercion co) in (Coercion, Type) -> Maybe (Coercion, Type) forall a. a -> Maybe a Just (Coercion co, Type ty) | Just BuiltInSynFamily ax <- TyCon -> Maybe BuiltInSynFamily isBuiltInSynFamTyCon_maybe TyCon tc , Just (CoAxiomRule coax,[Type] ts,Type ty) <- BuiltInSynFamily -> [Type] -> Maybe (CoAxiomRule, [Type], Type) sfMatchFam BuiltInSynFamily ax [Type] tys = let co :: Coercion co = CoAxiomRule -> [Coercion] -> Coercion mkAxiomRuleCo CoAxiomRule coax ((Role -> Type -> Coercion) -> [Role] -> [Type] -> [Coercion] forall a b c. (a -> b -> c) -> [a] -> [b] -> [c] zipWith Role -> Type -> Coercion mkReflCo (CoAxiomRule -> [Role] coaxrAsmpRoles CoAxiomRule coax) [Type] ts) in (Coercion, Type) -> Maybe (Coercion, Type) forall a. a -> Maybe a Just (Coercion co, Type ty) | Bool otherwise = Maybe (Coercion, Type) forall a. Maybe a Nothing -- The axiom can be oversaturated. (Closed families only.) chooseBranch :: CoAxiom Branched -> [Type] -> Maybe (BranchIndex, [Type], [Coercion]) -- found match, with args chooseBranch :: CoAxiom Branched -> [Type] -> Maybe (Int, [Type], [Coercion]) chooseBranch CoAxiom Branched axiom [Type] tys = do { let num_pats :: Int num_pats = CoAxiom Branched -> Int forall (br :: BranchFlag). CoAxiom br -> Int coAxiomNumPats CoAxiom Branched axiom ([Type] target_tys, [Type] extra_tys) = Int -> [Type] -> ([Type], [Type]) forall a. Int -> [a] -> ([a], [a]) splitAt Int num_pats [Type] tys branches :: Branches Branched branches = CoAxiom Branched -> Branches Branched forall (br :: BranchFlag). CoAxiom br -> Branches br coAxiomBranches CoAxiom Branched axiom ; (Int ind, [Type] inst_tys, [Coercion] inst_cos) <- Array Int CoAxBranch -> [Type] -> Maybe (Int, [Type], [Coercion]) findBranch (Branches Branched -> Array Int CoAxBranch forall (br :: BranchFlag). Branches br -> Array Int CoAxBranch unMkBranches Branches Branched branches) [Type] target_tys ; (Int, [Type], [Coercion]) -> Maybe (Int, [Type], [Coercion]) forall (m :: * -> *) a. Monad m => a -> m a return ( Int ind, [Type] inst_tys [Type] -> [Type] -> [Type] forall a. [a] -> [a] -> [a] `chkAppend` [Type] extra_tys, [Coercion] inst_cos ) } -- The axiom must *not* be oversaturated findBranch :: Array BranchIndex CoAxBranch -> [Type] -> Maybe (BranchIndex, [Type], [Coercion]) -- coercions relate requested types to returned axiom LHS at role N findBranch :: Array Int CoAxBranch -> [Type] -> Maybe (Int, [Type], [Coercion]) findBranch Array Int CoAxBranch branches [Type] target_tys = ((Int, CoAxBranch) -> Maybe (Int, [Type], [Coercion]) -> Maybe (Int, [Type], [Coercion])) -> Maybe (Int, [Type], [Coercion]) -> [(Int, CoAxBranch)] -> Maybe (Int, [Type], [Coercion]) forall (t :: * -> *) a b. Foldable t => (a -> b -> b) -> b -> t a -> b foldr (Int, CoAxBranch) -> Maybe (Int, [Type], [Coercion]) -> Maybe (Int, [Type], [Coercion]) go Maybe (Int, [Type], [Coercion]) forall a. Maybe a Nothing (Array Int CoAxBranch -> [(Int, CoAxBranch)] forall i e. Ix i => Array i e -> [(i, e)] assocs Array Int CoAxBranch branches) where go :: (BranchIndex, CoAxBranch) -> Maybe (BranchIndex, [Type], [Coercion]) -> Maybe (BranchIndex, [Type], [Coercion]) go :: (Int, CoAxBranch) -> Maybe (Int, [Type], [Coercion]) -> Maybe (Int, [Type], [Coercion]) go (Int index, CoAxBranch branch) Maybe (Int, [Type], [Coercion]) other = let (CoAxBranch { cab_tvs :: CoAxBranch -> [TyVar] cab_tvs = [TyVar] tpl_tvs, cab_cvs :: CoAxBranch -> [TyVar] cab_cvs = [TyVar] tpl_cvs , cab_lhs :: CoAxBranch -> [Type] cab_lhs = [Type] tpl_lhs , cab_incomps :: CoAxBranch -> [CoAxBranch] cab_incomps = [CoAxBranch] incomps }) = CoAxBranch branch in_scope :: InScopeSet in_scope = VarSet -> InScopeSet mkInScopeSet ([VarSet] -> VarSet unionVarSets ([VarSet] -> VarSet) -> [VarSet] -> VarSet forall a b. (a -> b) -> a -> b $ (CoAxBranch -> VarSet) -> [CoAxBranch] -> [VarSet] forall a b. (a -> b) -> [a] -> [b] map ([Type] -> VarSet tyCoVarsOfTypes ([Type] -> VarSet) -> (CoAxBranch -> [Type]) -> CoAxBranch -> VarSet forall b c a. (b -> c) -> (a -> b) -> a -> c . CoAxBranch -> [Type] coAxBranchLHS) [CoAxBranch] incomps) -- See Note [Flattening] below flattened_target :: [Type] flattened_target = InScopeSet -> [Type] -> [Type] flattenTys InScopeSet in_scope [Type] target_tys in case [Type] -> [Type] -> Maybe TCvSubst tcMatchTys [Type] tpl_lhs [Type] target_tys of Just TCvSubst subst -- matching worked. now, check for apartness. | [Type] -> CoAxBranch -> Bool apartnessCheck [Type] flattened_target CoAxBranch branch -> -- matching worked & we're apart from all incompatible branches. -- success ASSERT( all (isJust . lookupCoVar subst) tpl_cvs ) (Int, [Type], [Coercion]) -> Maybe (Int, [Type], [Coercion]) forall a. a -> Maybe a Just (Int index, TCvSubst -> [TyVar] -> [Type] substTyVars TCvSubst subst [TyVar] tpl_tvs, TCvSubst -> [TyVar] -> [Coercion] substCoVars TCvSubst subst [TyVar] tpl_cvs) -- failure. keep looking Maybe TCvSubst _ -> Maybe (Int, [Type], [Coercion]) other -- | Do an apartness check, as described in the "Closed Type Families" paper -- (POPL '14). This should be used when determining if an equation -- ('CoAxBranch') of a closed type family can be used to reduce a certain target -- type family application. apartnessCheck :: [Type] -- ^ /flattened/ target arguments. Make sure -- they're flattened! See Note [Flattening]. -- (NB: This "flat" is a different -- "flat" than is used in TcFlatten.) -> CoAxBranch -- ^ the candidate equation we wish to use -- Precondition: this matches the target -> Bool -- ^ True <=> equation can fire apartnessCheck :: [Type] -> CoAxBranch -> Bool apartnessCheck [Type] flattened_target (CoAxBranch { cab_incomps :: CoAxBranch -> [CoAxBranch] cab_incomps = [CoAxBranch] incomps }) = (CoAxBranch -> Bool) -> [CoAxBranch] -> Bool forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool all (UnifyResult -> Bool forall a. UnifyResultM a -> Bool isSurelyApart (UnifyResult -> Bool) -> (CoAxBranch -> UnifyResult) -> CoAxBranch -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . (TyVar -> BindFlag) -> [Type] -> [Type] -> UnifyResult tcUnifyTysFG (BindFlag -> TyVar -> BindFlag forall a b. a -> b -> a const BindFlag BindMe) [Type] flattened_target ([Type] -> UnifyResult) -> (CoAxBranch -> [Type]) -> CoAxBranch -> UnifyResult forall b c a. (b -> c) -> (a -> b) -> a -> c . CoAxBranch -> [Type] coAxBranchLHS) [CoAxBranch] incomps where isSurelyApart :: UnifyResultM a -> Bool isSurelyApart UnifyResultM a SurelyApart = Bool True isSurelyApart UnifyResultM a _ = Bool False {- ************************************************************************ * * Looking up a family instance * * ************************************************************************ Note [Normalising types] ~~~~~~~~~~~~~~~~~~~~~~~~ The topNormaliseType function removes all occurrences of type families and newtypes from the top-level structure of a type. normaliseTcApp does the type family lookup and is fairly straightforward. normaliseType is a little more involved. The complication comes from the fact that a type family might be used in the kind of a variable bound in a forall. We wish to remove this type family application, but that means coming up with a fresh variable (with the new kind). Thus, we need a substitution to be built up as we recur through the type. However, an ordinary TCvSubst just won't do: when we hit a type variable whose kind has changed during normalisation, we need both the new type variable *and* the coercion. We could conjure up a new VarEnv with just this property, but a usable substitution environment already exists: LiftingContexts from the liftCoSubst family of functions, defined in Coercion. A LiftingContext maps a type variable to a coercion and a coercion variable to a pair of coercions. Let's ignore coercion variables for now. Because the coercion a type variable maps to contains the destination type (via coercionKind), we don't need to store that destination type separately. Thus, a LiftingContext has what we need: a map from type variables to (Coercion, Type) pairs. We also benefit because we can piggyback on the liftCoSubstVarBndr function to deal with binders. However, I had to modify that function to work with this application. Thus, we now have liftCoSubstVarBndrUsing, which takes a function used to process the kind of the binder. We don't wish to lift the kind, but instead normalise it. So, we pass in a callback function that processes the kind of the binder. After that brilliant explanation of all this, I'm sure you've forgotten the dangling reference to coercion variables. What do we do with those? Nothing at all. The point of normalising types is to remove type family applications, but there's no sense in removing these from coercions. We would just get back a new coercion witnessing the equality between the same types as the original coercion. Because coercions are irrelevant anyway, there is no point in doing this. So, whenever we encounter a coercion, we just say that it won't change. That's what the CoercionTy case is doing within normalise_type. Note [Normalisation and type synonyms] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We need to be a bit careful about normalising in the presence of type synonyms (#13035). Suppose S is a type synonym, and we have S t1 t2 If S is family-free (on its RHS) we can just normalise t1 and t2 and reconstruct (S t1' t2'). Expanding S could not reveal any new redexes because type families are saturated. But if S has a type family on its RHS we expand /before/ normalising the args t1, t2. If we normalise t1, t2 first, we'll re-normalise them after expansion, and that can lead to /exponential/ behavour; see #13035. Notice, though, that expanding first can in principle duplicate t1,t2, which might contain redexes. I'm sure you could conjure up an exponential case by that route too, but it hasn't happened in practice yet! -} topNormaliseType :: FamInstEnvs -> Type -> Type topNormaliseType :: (FamInstEnv, FamInstEnv) -> Type -> Type topNormaliseType (FamInstEnv, FamInstEnv) env Type ty = case (FamInstEnv, FamInstEnv) -> Type -> Maybe (Coercion, Type) topNormaliseType_maybe (FamInstEnv, FamInstEnv) env Type ty of Just (Coercion _co, Type ty') -> Type ty' Maybe (Coercion, Type) Nothing -> Type ty topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Coercion, Type) -- ^ Get rid of *outermost* (or toplevel) -- * type function redex -- * data family redex -- * newtypes -- returning an appropriate Representational coercion. Specifically, if -- topNormaliseType_maybe env ty = Just (co, ty') -- then -- (a) co :: ty ~R ty' -- (b) ty' is not a newtype, and is not a type-family or data-family redex -- -- However, ty' can be something like (Maybe (F ty)), where -- (F ty) is a redex. -- -- Always operates homogeneously: the returned type has the same kind as the -- original type, and the returned coercion is always homogeneous. topNormaliseType_maybe :: (FamInstEnv, FamInstEnv) -> Type -> Maybe (Coercion, Type) topNormaliseType_maybe (FamInstEnv, FamInstEnv) env Type ty = do { ((Coercion co, MCoercionN mkind_co), Type nty) <- NormaliseStepper (Coercion, MCoercionN) -> ((Coercion, MCoercionN) -> (Coercion, MCoercionN) -> (Coercion, MCoercionN)) -> Type -> Maybe ((Coercion, MCoercionN), Type) forall ev. NormaliseStepper ev -> (ev -> ev -> ev) -> Type -> Maybe (ev, Type) topNormaliseTypeX NormaliseStepper (Coercion, MCoercionN) stepper (Coercion, MCoercionN) -> (Coercion, MCoercionN) -> (Coercion, MCoercionN) combine Type ty ; (Coercion, Type) -> Maybe (Coercion, Type) forall (m :: * -> *) a. Monad m => a -> m a return ((Coercion, Type) -> Maybe (Coercion, Type)) -> (Coercion, Type) -> Maybe (Coercion, Type) forall a b. (a -> b) -> a -> b $ case MCoercionN mkind_co of MCoercionN MRefl -> (Coercion co, Type nty) MCo Coercion kind_co -> let nty_casted :: Type nty_casted = Type nty Type -> Coercion -> Type `mkCastTy` Coercion -> Coercion mkSymCo Coercion kind_co final_co :: Coercion final_co = Role -> Type -> Coercion -> Coercion -> Coercion mkCoherenceRightCo Role Representational Type nty (Coercion -> Coercion mkSymCo Coercion kind_co) Coercion co in (Coercion final_co, Type nty_casted) } where stepper :: NormaliseStepper (Coercion, MCoercionN) stepper = NormaliseStepper (Coercion, MCoercionN) unwrapNewTypeStepper' NormaliseStepper (Coercion, MCoercionN) -> NormaliseStepper (Coercion, MCoercionN) -> NormaliseStepper (Coercion, MCoercionN) forall ev. NormaliseStepper ev -> NormaliseStepper ev -> NormaliseStepper ev `composeSteppers` NormaliseStepper (Coercion, MCoercionN) tyFamStepper combine :: (Coercion, MCoercionN) -> (Coercion, MCoercionN) -> (Coercion, MCoercionN) combine (Coercion c1, MCoercionN mc1) (Coercion c2, MCoercionN mc2) = (Coercion c1 Coercion -> Coercion -> Coercion `mkTransCo` Coercion c2, MCoercionN mc1 MCoercionN -> MCoercionN -> MCoercionN `mkTransMCo` MCoercionN mc2) unwrapNewTypeStepper' :: NormaliseStepper (Coercion, MCoercionN) unwrapNewTypeStepper' :: NormaliseStepper (Coercion, MCoercionN) unwrapNewTypeStepper' RecTcChecker rec_nts TyCon tc [Type] tys = (Coercion -> (Coercion, MCoercionN)) -> NormaliseStepResult Coercion -> NormaliseStepResult (Coercion, MCoercionN) forall ev1 ev2. (ev1 -> ev2) -> NormaliseStepResult ev1 -> NormaliseStepResult ev2 mapStepResult (, MCoercionN MRefl) (NormaliseStepResult Coercion -> NormaliseStepResult (Coercion, MCoercionN)) -> NormaliseStepResult Coercion -> NormaliseStepResult (Coercion, MCoercionN) forall a b. (a -> b) -> a -> b $ NormaliseStepper Coercion unwrapNewTypeStepper RecTcChecker rec_nts TyCon tc [Type] tys -- second coercion below is the kind coercion relating the original type's kind -- to the normalised type's kind tyFamStepper :: NormaliseStepper (Coercion, MCoercionN) tyFamStepper :: NormaliseStepper (Coercion, MCoercionN) tyFamStepper RecTcChecker rec_nts TyCon tc [Type] tys -- Try to step a type/data family = let (Coercion args_co, [Type] ntys, Coercion res_co) = (FamInstEnv, FamInstEnv) -> Role -> TyCon -> [Type] -> (Coercion, [Type], Coercion) normaliseTcArgs (FamInstEnv, FamInstEnv) env Role Representational TyCon tc [Type] tys in case (FamInstEnv, FamInstEnv) -> Role -> TyCon -> [Type] -> Maybe (Coercion, Type) reduceTyFamApp_maybe (FamInstEnv, FamInstEnv) env Role Representational TyCon tc [Type] ntys of Just (Coercion co, Type rhs) -> RecTcChecker -> Type -> (Coercion, MCoercionN) -> NormaliseStepResult (Coercion, MCoercionN) forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev NS_Step RecTcChecker rec_nts Type rhs (Coercion args_co Coercion -> Coercion -> Coercion `mkTransCo` Coercion co, Coercion -> MCoercionN MCo Coercion res_co) Maybe (Coercion, Type) _ -> NormaliseStepResult (Coercion, MCoercionN) forall ev. NormaliseStepResult ev NS_Done --------------- normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> (Coercion, Type) -- See comments on normaliseType for the arguments of this function normaliseTcApp :: (FamInstEnv, FamInstEnv) -> Role -> TyCon -> [Type] -> (Coercion, Type) normaliseTcApp (FamInstEnv, FamInstEnv) env Role role TyCon tc [Type] tys = (FamInstEnv, FamInstEnv) -> Role -> VarSet -> NormM (Coercion, Type) -> (Coercion, Type) forall a. (FamInstEnv, FamInstEnv) -> Role -> VarSet -> NormM a -> a initNormM (FamInstEnv, FamInstEnv) env Role role ([Type] -> VarSet tyCoVarsOfTypes [Type] tys) (NormM (Coercion, Type) -> (Coercion, Type)) -> NormM (Coercion, Type) -> (Coercion, Type) forall a b. (a -> b) -> a -> b $ TyCon -> [Type] -> NormM (Coercion, Type) normalise_tc_app TyCon tc [Type] tys -- See Note [Normalising types] about the LiftingContext normalise_tc_app :: TyCon -> [Type] -> NormM (Coercion, Type) normalise_tc_app :: TyCon -> [Type] -> NormM (Coercion, Type) normalise_tc_app TyCon tc [Type] tys | Just ([(TyVar, Type)] tenv, Type rhs, [Type] tys') <- TyCon -> [Type] -> Maybe ([(TyVar, Type)], Type, [Type]) forall tyco. TyCon -> [tyco] -> Maybe ([(TyVar, tyco)], Type, [tyco]) expandSynTyCon_maybe TyCon tc [Type] tys , Bool -> Bool not (TyCon -> Bool isFamFreeTyCon TyCon tc) -- Expand and try again = -- A synonym with type families in the RHS -- Expand and try again -- See Note [Normalisation and type synonyms] Type -> NormM (Coercion, Type) normalise_type (Type -> [Type] -> Type mkAppTys (HasCallStack => TCvSubst -> Type -> Type TCvSubst -> Type -> Type substTy ([(TyVar, Type)] -> TCvSubst mkTvSubstPrs [(TyVar, Type)] tenv) Type rhs) [Type] tys') | TyCon -> Bool isFamilyTyCon TyCon tc = -- A type-family application do { (FamInstEnv, FamInstEnv) env <- NormM (FamInstEnv, FamInstEnv) getEnv ; Role role <- NormM Role getRole ; (Coercion args_co, [Type] ntys, Coercion res_co) <- TyCon -> [Type] -> NormM (Coercion, [Type], Coercion) normalise_tc_args TyCon tc [Type] tys ; case (FamInstEnv, FamInstEnv) -> Role -> TyCon -> [Type] -> Maybe (Coercion, Type) reduceTyFamApp_maybe (FamInstEnv, FamInstEnv) env Role role TyCon tc [Type] ntys of Just (Coercion first_co, Type ty') -> do { (Coercion rest_co,Type nty) <- Type -> NormM (Coercion, Type) normalise_type Type ty' ; (Coercion, Type) -> NormM (Coercion, Type) forall (m :: * -> *) a. Monad m => a -> m a return (Role -> Type -> Coercion -> Coercion -> (Coercion, Type) assemble_result Role role Type nty (Coercion args_co Coercion -> Coercion -> Coercion `mkTransCo` Coercion first_co Coercion -> Coercion -> Coercion `mkTransCo` Coercion rest_co) Coercion res_co) } Maybe (Coercion, Type) _ -> -- No unique matching family instance exists; -- we do not do anything (Coercion, Type) -> NormM (Coercion, Type) forall (m :: * -> *) a. Monad m => a -> m a return (Role -> Type -> Coercion -> Coercion -> (Coercion, Type) assemble_result Role role (TyCon -> [Type] -> Type mkTyConApp TyCon tc [Type] ntys) Coercion args_co Coercion res_co) } | Bool otherwise = -- A synonym with no type families in the RHS; or data type etc -- Just normalise the arguments and rebuild do { (Coercion args_co, [Type] ntys, Coercion res_co) <- TyCon -> [Type] -> NormM (Coercion, [Type], Coercion) normalise_tc_args TyCon tc [Type] tys ; Role role <- NormM Role getRole ; (Coercion, Type) -> NormM (Coercion, Type) forall (m :: * -> *) a. Monad m => a -> m a return (Role -> Type -> Coercion -> Coercion -> (Coercion, Type) assemble_result Role role (TyCon -> [Type] -> Type mkTyConApp TyCon tc [Type] ntys) Coercion args_co Coercion res_co) } where assemble_result :: Role -- r, ambient role in NormM monad -> Type -- nty, result type, possibly of changed kind -> Coercion -- orig_ty ~r nty, possibly heterogeneous -> CoercionN -- typeKind(orig_ty) ~N typeKind(nty) -> (Coercion, Type) -- (co :: orig_ty ~r nty_casted, nty_casted) -- where nty_casted has same kind as orig_ty assemble_result :: Role -> Type -> Coercion -> Coercion -> (Coercion, Type) assemble_result Role r Type nty Coercion orig_to_nty Coercion kind_co = ( Coercion final_co, Type nty_old_kind ) where nty_old_kind :: Type nty_old_kind = Type nty Type -> Coercion -> Type `mkCastTy` Coercion -> Coercion mkSymCo Coercion kind_co final_co :: Coercion final_co = Role -> Type -> Coercion -> Coercion -> Coercion mkCoherenceRightCo Role r Type nty (Coercion -> Coercion mkSymCo Coercion kind_co) Coercion orig_to_nty --------------- -- | Normalise arguments to a tycon normaliseTcArgs :: FamInstEnvs -- ^ env't with family instances -> Role -- ^ desired role of output coercion -> TyCon -- ^ tc -> [Type] -- ^ tys -> (Coercion, [Type], CoercionN) -- ^ co :: tc tys ~ tc new_tys -- NB: co might not be homogeneous -- last coercion :: kind(tc tys) ~ kind(tc new_tys) normaliseTcArgs :: (FamInstEnv, FamInstEnv) -> Role -> TyCon -> [Type] -> (Coercion, [Type], Coercion) normaliseTcArgs (FamInstEnv, FamInstEnv) env Role role TyCon tc [Type] tys = (FamInstEnv, FamInstEnv) -> Role -> VarSet -> NormM (Coercion, [Type], Coercion) -> (Coercion, [Type], Coercion) forall a. (FamInstEnv, FamInstEnv) -> Role -> VarSet -> NormM a -> a initNormM (FamInstEnv, FamInstEnv) env Role role ([Type] -> VarSet tyCoVarsOfTypes [Type] tys) (NormM (Coercion, [Type], Coercion) -> (Coercion, [Type], Coercion)) -> NormM (Coercion, [Type], Coercion) -> (Coercion, [Type], Coercion) forall a b. (a -> b) -> a -> b $ TyCon -> [Type] -> NormM (Coercion, [Type], Coercion) normalise_tc_args TyCon tc [Type] tys normalise_tc_args :: TyCon -> [Type] -- tc tys -> NormM (Coercion, [Type], CoercionN) -- (co, new_tys), where -- co :: tc tys ~ tc new_tys; might not be homogeneous -- res_co :: typeKind(tc tys) ~N typeKind(tc new_tys) normalise_tc_args :: TyCon -> [Type] -> NormM (Coercion, [Type], Coercion) normalise_tc_args TyCon tc [Type] tys = do { Role role <- NormM Role getRole ; ([Coercion] args_cos, [Type] nargs, Coercion res_co) <- Type -> [Role] -> [Type] -> NormM ([Coercion], [Type], Coercion) normalise_args (TyCon -> Type tyConKind TyCon tc) (Role -> TyCon -> [Role] tyConRolesX Role role TyCon tc) [Type] tys ; (Coercion, [Type], Coercion) -> NormM (Coercion, [Type], Coercion) forall (m :: * -> *) a. Monad m => a -> m a return (HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion Role -> TyCon -> [Coercion] -> Coercion mkTyConAppCo Role role TyCon tc [Coercion] args_cos, [Type] nargs, Coercion res_co) } --------------- normaliseType :: FamInstEnvs -> Role -- desired role of coercion -> Type -> (Coercion, Type) normaliseType :: (FamInstEnv, FamInstEnv) -> Role -> Type -> (Coercion, Type) normaliseType (FamInstEnv, FamInstEnv) env Role role Type ty = (FamInstEnv, FamInstEnv) -> Role -> VarSet -> NormM (Coercion, Type) -> (Coercion, Type) forall a. (FamInstEnv, FamInstEnv) -> Role -> VarSet -> NormM a -> a initNormM (FamInstEnv, FamInstEnv) env Role role (Type -> VarSet tyCoVarsOfType Type ty) (NormM (Coercion, Type) -> (Coercion, Type)) -> NormM (Coercion, Type) -> (Coercion, Type) forall a b. (a -> b) -> a -> b $ Type -> NormM (Coercion, Type) normalise_type Type ty normalise_type :: Type -- old type -> NormM (Coercion, Type) -- (coercion, new type), where -- co :: old-type ~ new_type -- Normalise the input type, by eliminating *all* type-function redexes -- but *not* newtypes (which are visible to the programmer) -- Returns with Refl if nothing happens -- Does nothing to newtypes -- The returned coercion *must* be *homogeneous* -- See Note [Normalising types] -- Try not to disturb type synonyms if possible normalise_type :: Type -> NormM (Coercion, Type) normalise_type Type ty = Type -> NormM (Coercion, Type) go Type ty where go :: Type -> NormM (Coercion, Type) go (TyConApp TyCon tc [Type] tys) = TyCon -> [Type] -> NormM (Coercion, Type) normalise_tc_app TyCon tc [Type] tys go ty :: Type ty@(LitTy {}) = do { Role r <- NormM Role getRole ; (Coercion, Type) -> NormM (Coercion, Type) forall (m :: * -> *) a. Monad m => a -> m a return (Role -> Type -> Coercion mkReflCo Role r Type ty, Type ty) } go (AppTy Type ty1 Type ty2) = Type -> [Type] -> NormM (Coercion, Type) go_app_tys Type ty1 [Type ty2] go ty :: Type ty@(FunTy { ft_arg :: Type -> Type ft_arg = Type ty1, ft_res :: Type -> Type ft_res = Type ty2 }) = do { (Coercion co1, Type nty1) <- Type -> NormM (Coercion, Type) go Type ty1 ; (Coercion co2, Type nty2) <- Type -> NormM (Coercion, Type) go Type ty2 ; Role r <- NormM Role getRole ; (Coercion, Type) -> NormM (Coercion, Type) forall (m :: * -> *) a. Monad m => a -> m a return (Role -> Coercion -> Coercion -> Coercion mkFunCo Role r Coercion co1 Coercion co2, Type ty { ft_arg :: Type ft_arg = Type nty1, ft_res :: Type ft_res = Type nty2 }) } go (ForAllTy (Bndr TyVar tcvar ArgFlag vis) Type ty) = do { (LiftingContext lc', TyVar tv', Coercion h, Type ki') <- TyVar -> NormM (LiftingContext, TyVar, Coercion, Type) normalise_var_bndr TyVar tcvar ; (Coercion co, Type nty) <- LiftingContext -> NormM (Coercion, Type) -> NormM (Coercion, Type) forall a. LiftingContext -> NormM a -> NormM a withLC LiftingContext lc' (NormM (Coercion, Type) -> NormM (Coercion, Type)) -> NormM (Coercion, Type) -> NormM (Coercion, Type) forall a b. (a -> b) -> a -> b $ Type -> NormM (Coercion, Type) normalise_type Type ty ; let tv2 :: TyVar tv2 = TyVar -> Type -> TyVar setTyVarKind TyVar tv' Type ki' ; (Coercion, Type) -> NormM (Coercion, Type) forall (m :: * -> *) a. Monad m => a -> m a return (TyVar -> Coercion -> Coercion -> Coercion mkForAllCo TyVar tv' Coercion h Coercion co, VarBndr TyVar ArgFlag -> Type -> Type ForAllTy (TyVar -> ArgFlag -> VarBndr TyVar ArgFlag forall var argf. var -> argf -> VarBndr var argf Bndr TyVar tv2 ArgFlag vis) Type nty) } go (TyVarTy TyVar tv) = TyVar -> NormM (Coercion, Type) normalise_tyvar TyVar tv go (CastTy Type ty Coercion co) = do { (Coercion nco, Type nty) <- Type -> NormM (Coercion, Type) go Type ty ; LiftingContext lc <- NormM LiftingContext getLC ; let co' :: Coercion co' = LiftingContext -> Coercion -> Coercion substRightCo LiftingContext lc Coercion co ; (Coercion, Type) -> NormM (Coercion, Type) forall (m :: * -> *) a. Monad m => a -> m a return (Coercion -> Role -> Type -> Type -> Coercion -> Coercion -> Coercion castCoercionKind Coercion nco Role Nominal Type ty Type nty Coercion co Coercion co' , Type -> Coercion -> Type mkCastTy Type nty Coercion co') } go (CoercionTy Coercion co) = do { LiftingContext lc <- NormM LiftingContext getLC ; Role r <- NormM Role getRole ; let right_co :: Coercion right_co = LiftingContext -> Coercion -> Coercion substRightCo LiftingContext lc Coercion co ; (Coercion, Type) -> NormM (Coercion, Type) forall (m :: * -> *) a. Monad m => a -> m a return ( Role -> Coercion -> Coercion -> Coercion -> Coercion mkProofIrrelCo Role r (HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion Role -> LiftingContext -> Type -> Coercion liftCoSubst Role Nominal LiftingContext lc (Coercion -> Type coercionType Coercion co)) Coercion co Coercion right_co , Coercion -> Type mkCoercionTy Coercion right_co ) } go_app_tys :: Type -- function -> [Type] -- args -> NormM (Coercion, Type) -- cf. TcFlatten.flatten_app_ty_args go_app_tys :: Type -> [Type] -> NormM (Coercion, Type) go_app_tys (AppTy Type ty1 Type ty2) [Type] tys = Type -> [Type] -> NormM (Coercion, Type) go_app_tys Type ty1 (Type ty2 Type -> [Type] -> [Type] forall a. a -> [a] -> [a] : [Type] tys) go_app_tys Type fun_ty [Type] arg_tys = do { (Coercion fun_co, Type nfun) <- Type -> NormM (Coercion, Type) go Type fun_ty ; case HasCallStack => Type -> Maybe (TyCon, [Type]) Type -> Maybe (TyCon, [Type]) tcSplitTyConApp_maybe Type nfun of Just (TyCon tc, [Type] xis) -> do { (Coercion second_co, Type nty) <- Type -> NormM (Coercion, Type) go (TyCon -> [Type] -> Type mkTyConApp TyCon tc ([Type] xis [Type] -> [Type] -> [Type] forall a. [a] -> [a] -> [a] ++ [Type] arg_tys)) -- flatten_app_ty_args avoids redundantly processing the xis, -- but that's a much more performance-sensitive function. -- This type normalisation is not called in a loop. ; (Coercion, Type) -> NormM (Coercion, Type) forall (m :: * -> *) a. Monad m => a -> m a return (Coercion -> [Coercion] -> Coercion mkAppCos Coercion fun_co ((Type -> Coercion) -> [Type] -> [Coercion] forall a b. (a -> b) -> [a] -> [b] map Type -> Coercion mkNomReflCo [Type] arg_tys) Coercion -> Coercion -> Coercion `mkTransCo` Coercion second_co, Type nty) } Maybe (TyCon, [Type]) Nothing -> do { ([Coercion] args_cos, [Type] nargs, Coercion res_co) <- Type -> [Role] -> [Type] -> NormM ([Coercion], [Type], Coercion) normalise_args (HasDebugCallStack => Type -> Type Type -> Type typeKind Type nfun) (Role -> [Role] forall a. a -> [a] repeat Role Nominal) [Type] arg_tys ; Role role <- NormM Role getRole ; let nty :: Type nty = Type -> [Type] -> Type mkAppTys Type nfun [Type] nargs nco :: Coercion nco = Coercion -> [Coercion] -> Coercion mkAppCos Coercion fun_co [Coercion] args_cos nty_casted :: Type nty_casted = Type nty Type -> Coercion -> Type `mkCastTy` Coercion -> Coercion mkSymCo Coercion res_co final_co :: Coercion final_co = Role -> Type -> Coercion -> Coercion -> Coercion mkCoherenceRightCo Role role Type nty (Coercion -> Coercion mkSymCo Coercion res_co) Coercion nco ; (Coercion, Type) -> NormM (Coercion, Type) forall (m :: * -> *) a. Monad m => a -> m a return (Coercion final_co, Type nty_casted) } } normalise_args :: Kind -- of the function -> [Role] -- roles at which to normalise args -> [Type] -- args -> NormM ([Coercion], [Type], Coercion) -- returns (cos, xis, res_co), where each xi is the normalised -- version of the corresponding type, each co is orig_arg ~ xi, -- and the res_co :: kind(f orig_args) ~ kind(f xis) -- NB: The xis might *not* have the same kinds as the input types, -- but the resulting application *will* be well-kinded -- cf. TcFlatten.flatten_args_slow normalise_args :: Type -> [Role] -> [Type] -> NormM ([Coercion], [Type], Coercion) normalise_args Type fun_ki [Role] roles [Type] args = do { [(Type, Coercion)] normed_args <- (Role -> Type -> NormM (Type, Coercion)) -> [Role] -> [Type] -> NormM [(Type, Coercion)] forall (m :: * -> *) a b c. Applicative m => (a -> b -> m c) -> [a] -> [b] -> m [c] zipWithM Role -> Type -> NormM (Type, Coercion) normalise1 [Role] roles [Type] args ; let ([Type] xis, [Coercion] cos, Coercion res_co) = [TyCoBinder] -> Type -> VarSet -> [Role] -> [(Type, Coercion)] -> ([Type], [Coercion], Coercion) simplifyArgsWorker [TyCoBinder] ki_binders Type inner_ki VarSet fvs [Role] roles [(Type, Coercion)] normed_args ; ([Coercion], [Type], Coercion) -> NormM ([Coercion], [Type], Coercion) forall (m :: * -> *) a. Monad m => a -> m a return ((Coercion -> Coercion) -> [Coercion] -> [Coercion] forall a b. (a -> b) -> [a] -> [b] map Coercion -> Coercion mkSymCo [Coercion] cos, [Type] xis, Coercion -> Coercion mkSymCo Coercion res_co) } where ([TyCoBinder] ki_binders, Type inner_ki) = Type -> ([TyCoBinder], Type) splitPiTys Type fun_ki fvs :: VarSet fvs = [Type] -> VarSet tyCoVarsOfTypes [Type] args -- flattener conventions are different from ours impedance_match :: NormM (Coercion, Type) -> NormM (Type, Coercion) impedance_match :: NormM (Coercion, Type) -> NormM (Type, Coercion) impedance_match NormM (Coercion, Type) action = do { (Coercion co, Type ty) <- NormM (Coercion, Type) action ; (Type, Coercion) -> NormM (Type, Coercion) forall (m :: * -> *) a. Monad m => a -> m a return (Type ty, Coercion -> Coercion mkSymCo Coercion co) } normalise1 :: Role -> Type -> NormM (Type, Coercion) normalise1 Role role Type ty = NormM (Coercion, Type) -> NormM (Type, Coercion) impedance_match (NormM (Coercion, Type) -> NormM (Type, Coercion)) -> NormM (Coercion, Type) -> NormM (Type, Coercion) forall a b. (a -> b) -> a -> b $ Role -> NormM (Coercion, Type) -> NormM (Coercion, Type) forall a. Role -> NormM a -> NormM a withRole Role role (NormM (Coercion, Type) -> NormM (Coercion, Type)) -> NormM (Coercion, Type) -> NormM (Coercion, Type) forall a b. (a -> b) -> a -> b $ Type -> NormM (Coercion, Type) normalise_type Type ty normalise_tyvar :: TyVar -> NormM (Coercion, Type) normalise_tyvar :: TyVar -> NormM (Coercion, Type) normalise_tyvar TyVar tv = ASSERT( isTyVar tv ) do { LiftingContext lc <- NormM LiftingContext getLC ; Role r <- NormM Role getRole ; (Coercion, Type) -> NormM (Coercion, Type) forall (m :: * -> *) a. Monad m => a -> m a return ((Coercion, Type) -> NormM (Coercion, Type)) -> (Coercion, Type) -> NormM (Coercion, Type) forall a b. (a -> b) -> a -> b $ case LiftingContext -> Role -> TyVar -> Maybe Coercion liftCoSubstTyVar LiftingContext lc Role r TyVar tv of Just Coercion co -> (Coercion co, Pair Type -> Type forall a. Pair a -> a pSnd (Pair Type -> Type) -> Pair Type -> Type forall a b. (a -> b) -> a -> b $ Coercion -> Pair Type coercionKind Coercion co) Maybe Coercion Nothing -> (Role -> Type -> Coercion mkReflCo Role r Type ty, Type ty) } where ty :: Type ty = TyVar -> Type mkTyVarTy TyVar tv normalise_var_bndr :: TyCoVar -> NormM (LiftingContext, TyCoVar, Coercion, Kind) normalise_var_bndr :: TyVar -> NormM (LiftingContext, TyVar, Coercion, Type) normalise_var_bndr TyVar tcvar -- works for both tvar and covar = do { LiftingContext lc1 <- NormM LiftingContext getLC ; (FamInstEnv, FamInstEnv) env <- NormM (FamInstEnv, FamInstEnv) getEnv ; let callback :: LiftingContext -> Type -> (Coercion, Type) callback LiftingContext lc Type ki = NormM (Coercion, Type) -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> (Coercion, Type) forall a. NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a runNormM (Type -> NormM (Coercion, Type) normalise_type Type ki) (FamInstEnv, FamInstEnv) env LiftingContext lc Role Nominal ; (LiftingContext, TyVar, Coercion, Type) -> NormM (LiftingContext, TyVar, Coercion, Type) forall (m :: * -> *) a. Monad m => a -> m a return ((LiftingContext, TyVar, Coercion, Type) -> NormM (LiftingContext, TyVar, Coercion, Type)) -> (LiftingContext, TyVar, Coercion, Type) -> NormM (LiftingContext, TyVar, Coercion, Type) forall a b. (a -> b) -> a -> b $ (LiftingContext -> Type -> (Coercion, Type)) -> LiftingContext -> TyVar -> (LiftingContext, TyVar, Coercion, Type) forall a. (LiftingContext -> Type -> (Coercion, a)) -> LiftingContext -> TyVar -> (LiftingContext, TyVar, Coercion, a) liftCoSubstVarBndrUsing LiftingContext -> Type -> (Coercion, Type) callback LiftingContext lc1 TyVar tcvar } -- | a monad for the normalisation functions, reading 'FamInstEnvs', -- a 'LiftingContext', and a 'Role'. newtype NormM a = NormM { NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a runNormM :: FamInstEnvs -> LiftingContext -> Role -> a } deriving (a -> NormM b -> NormM a (a -> b) -> NormM a -> NormM b (forall a b. (a -> b) -> NormM a -> NormM b) -> (forall a b. a -> NormM b -> NormM a) -> Functor NormM forall a b. a -> NormM b -> NormM a forall a b. (a -> b) -> NormM a -> NormM b forall (f :: * -> *). (forall a b. (a -> b) -> f a -> f b) -> (forall a b. a -> f b -> f a) -> Functor f <$ :: a -> NormM b -> NormM a $c<$ :: forall a b. a -> NormM b -> NormM a fmap :: (a -> b) -> NormM a -> NormM b $cfmap :: forall a b. (a -> b) -> NormM a -> NormM b Functor) initNormM :: FamInstEnvs -> Role -> TyCoVarSet -- the in-scope variables -> NormM a -> a initNormM :: (FamInstEnv, FamInstEnv) -> Role -> VarSet -> NormM a -> a initNormM (FamInstEnv, FamInstEnv) env Role role VarSet vars (NormM (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a thing_inside) = (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a thing_inside (FamInstEnv, FamInstEnv) env LiftingContext lc Role role where in_scope :: InScopeSet in_scope = VarSet -> InScopeSet mkInScopeSet VarSet vars lc :: LiftingContext lc = InScopeSet -> LiftingContext emptyLiftingContext InScopeSet in_scope getRole :: NormM Role getRole :: NormM Role getRole = ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> Role) -> NormM Role forall a. ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a) -> NormM a NormM (\ (FamInstEnv, FamInstEnv) _ LiftingContext _ Role r -> Role r) getLC :: NormM LiftingContext getLC :: NormM LiftingContext getLC = ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> LiftingContext) -> NormM LiftingContext forall a. ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a) -> NormM a NormM (\ (FamInstEnv, FamInstEnv) _ LiftingContext lc Role _ -> LiftingContext lc) getEnv :: NormM FamInstEnvs getEnv :: NormM (FamInstEnv, FamInstEnv) getEnv = ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> (FamInstEnv, FamInstEnv)) -> NormM (FamInstEnv, FamInstEnv) forall a. ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a) -> NormM a NormM (\ (FamInstEnv, FamInstEnv) env LiftingContext _ Role _ -> (FamInstEnv, FamInstEnv) env) withRole :: Role -> NormM a -> NormM a withRole :: Role -> NormM a -> NormM a withRole Role r NormM a thing = ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a) -> NormM a forall a. ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a) -> NormM a NormM (((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a) -> NormM a) -> ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a) -> NormM a forall a b. (a -> b) -> a -> b $ \ (FamInstEnv, FamInstEnv) envs LiftingContext lc Role _old_r -> NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a forall a. NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a runNormM NormM a thing (FamInstEnv, FamInstEnv) envs LiftingContext lc Role r withLC :: LiftingContext -> NormM a -> NormM a withLC :: LiftingContext -> NormM a -> NormM a withLC LiftingContext lc NormM a thing = ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a) -> NormM a forall a. ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a) -> NormM a NormM (((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a) -> NormM a) -> ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a) -> NormM a forall a b. (a -> b) -> a -> b $ \ (FamInstEnv, FamInstEnv) envs LiftingContext _old_lc Role r -> NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a forall a. NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a runNormM NormM a thing (FamInstEnv, FamInstEnv) envs LiftingContext lc Role r instance Monad NormM where NormM a ma >>= :: NormM a -> (a -> NormM b) -> NormM b >>= a -> NormM b fmb = ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> b) -> NormM b forall a. ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a) -> NormM a NormM (((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> b) -> NormM b) -> ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> b) -> NormM b forall a b. (a -> b) -> a -> b $ \(FamInstEnv, FamInstEnv) env LiftingContext lc Role r -> let a :: a a = NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a forall a. NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a runNormM NormM a ma (FamInstEnv, FamInstEnv) env LiftingContext lc Role r in NormM b -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> b forall a. NormM a -> (FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a runNormM (a -> NormM b fmb a a) (FamInstEnv, FamInstEnv) env LiftingContext lc Role r instance Applicative NormM where pure :: a -> NormM a pure a x = ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a) -> NormM a forall a. ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a) -> NormM a NormM (((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a) -> NormM a) -> ((FamInstEnv, FamInstEnv) -> LiftingContext -> Role -> a) -> NormM a forall a b. (a -> b) -> a -> b $ \ (FamInstEnv, FamInstEnv) _ LiftingContext _ Role _ -> a x <*> :: NormM (a -> b) -> NormM a -> NormM b (<*>) = NormM (a -> b) -> NormM a -> NormM b forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b ap {- ************************************************************************ * * Flattening * * ************************************************************************ Note [Flattening] ~~~~~~~~~~~~~~~~~ As described in "Closed type families with overlapping equations" http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf we need to flatten core types before unifying them, when checking for "surely-apart" against earlier equations of a closed type family. Flattening means replacing all top-level uses of type functions with fresh variables, *taking care to preserve sharing*. That is, the type (Either (F a b) (F a b)) should flatten to (Either c c), never (Either c d). Here is a nice example of why it's all necessary: type family F a b where F Int Bool = Char F a b = Double type family G a -- open, no instances How do we reduce (F (G Float) (G Float))? The first equation clearly doesn't match, while the second equation does. But, before reducing, we must make sure that the target can never become (F Int Bool). Well, no matter what G Float becomes, it certainly won't become *both* Int and Bool, so indeed we're safe reducing (F (G Float) (G Float)) to Double. This is necessary not only to get more reductions (which we might be willing to give up on), but for substitutivity. If we have (F x x), we can see that (F x x) can reduce to Double. So, it had better be the case that (F blah blah) can reduce to Double, no matter what (blah) is! Flattening as done below ensures this. The algorithm works by building up a TypeMap TyVar, mapping type family applications to fresh variables. This mapping must be threaded through all the function calls, as any entry in the mapping must be propagated to all future nodes in the tree. The algorithm also must track the set of in-scope variables, in order to make fresh variables as it flattens. (We are far from a source of fresh Uniques.) See Wrinkle 2, below. There are wrinkles, of course: 1. The flattening algorithm must account for the possibility of inner `forall`s. (A `forall` seen here can happen only because of impredicativity. However, the flattening operation is an algorithm in Core, which is impredicative.) Suppose we have (forall b. F b) -> (forall b. F b). Of course, those two bs are entirely unrelated, and so we should certainly not flatten the two calls F b to the same variable. Instead, they must be treated separately. We thus carry a substitution that freshens variables; we must apply this substitution (in `coreFlattenTyFamApp`) before looking up an application in the environment. Note that the range of the substitution contains only TyVars, never anything else. For the sake of efficiency, we only apply this substitution when absolutely necessary. Namely: * We do not perform the substitution at all if it is empty. * We only need to worry about the arguments of a type family that are within the arity of said type family, so we can get away with not applying the substitution to any oversaturated type family arguments. * Importantly, we do /not/ achieve this substitution by recursively flattening the arguments, as this would be wrong. Consider `F (G a)`, where F and G are type families. We might decide that `F (G a)` flattens to `beta`. Later, the substitution is non-empty (but does not map `a`) and so we flatten `G a` to `gamma` and try to flatten `F gamma`. Of course, `F gamma` is unknown, and so we flatten it to `delta`, but it really should have been `beta`! Argh! Moral of the story: instead of flattening the arguments, just substitute them directly. 2. There are two different reasons we might add a variable to the in-scope set as we work: A. We have just invented a new flattening variable. B. We have entered a `forall`. Annoying here is that in-scope variable source (A) must be threaded through the calls. For example, consider (F b -> forall c. F c). Suppose that, when flattening F b, we invent a fresh variable c. Now, when we encounter (forall c. F c), we need to know c is already in scope so that we locally rename c to c'. However, if we don't thread through the in-scope set from one argument of (->) to the other, we won't know this and might get very confused. In contrast, source (B) increases only as we go deeper, as in-scope sets normally do. However, even here we must be careful. The TypeMap TyVar that contains mappings from type family applications to freshened variables will be threaded through both sides of (forall b. F b) -> (forall b. F b). We thus must make sure that the two `b`s don't get renamed to the same b1. (If they did, then looking up `F b1` would yield the same flatten var for each.) So, even though `forall`-bound variables should really be in the in-scope set only when they are in scope, we retain these variables even outside of their scope. This ensures that, if we enounter a fresh `forall`-bound b, we will rename it to b2, not b1. Note that keeping a larger in-scope set than strictly necessary is always OK, as in-scope sets are only ever used to avoid collisions. Sadly, the freshening substitution described in (1) really musn't bind variables outside of their scope: note that its domain is the *unrenamed* variables. This means that the substitution gets "pushed down" (like a reader monad) while the in-scope set gets threaded (like a state monad). Because a TCvSubst contains its own in-scope set, we don't carry a TCvSubst; instead, we just carry a TvSubstEnv down, tying it to the InScopeSet traveling separately as necessary. 3. Consider `F ty_1 ... ty_n`, where F is a type family with arity k: type family F ty_1 ... ty_k :: res_k It's tempting to just flatten `F ty_1 ... ty_n` to `alpha`, where alpha is a flattening skolem. But we must instead flatten it to `alpha ty_(k+1) ... ty_n`—that is, by only flattening up to the arity of the type family. Why is this better? Consider the following concrete example from #16995: type family Param :: Type -> Type type family LookupParam (a :: Type) :: Type where LookupParam (f Char) = Bool LookupParam x = Int foo :: LookupParam (Param ()) foo = 42 In order for `foo` to typecheck, `LookupParam (Param ())` must reduce to `Int`. But if we flatten `Param ()` to `alpha`, then GHC can't be sure if `alpha` is apart from `f Char`, so it won't fall through to the second equation. But since the `Param` type family has arity 0, we can instead flatten `Param ()` to `alpha ()`, about which GHC knows with confidence is apart from `f Char`, permitting the second equation to be reached. Not only does this allow more programs to be accepted, it's also important for correctness. Not doing this was the root cause of the Core Lint error in #16995. flattenTys is defined here because of module dependencies. -} data FlattenEnv = FlattenEnv { FlattenEnv -> TypeMap TyVar fe_type_map :: TypeMap TyVar -- domain: exactly-saturated type family applications -- range: fresh variables , FlattenEnv -> InScopeSet fe_in_scope :: InScopeSet } -- See Note [Flattening] emptyFlattenEnv :: InScopeSet -> FlattenEnv emptyFlattenEnv :: InScopeSet -> FlattenEnv emptyFlattenEnv InScopeSet in_scope = FlattenEnv :: TypeMap TyVar -> InScopeSet -> FlattenEnv FlattenEnv { fe_type_map :: TypeMap TyVar fe_type_map = TypeMap TyVar forall a. TypeMap a emptyTypeMap , fe_in_scope :: InScopeSet fe_in_scope = InScopeSet in_scope } updateInScopeSet :: FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv updateInScopeSet :: FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv updateInScopeSet FlattenEnv env InScopeSet -> InScopeSet upd = FlattenEnv env { fe_in_scope :: InScopeSet fe_in_scope = InScopeSet -> InScopeSet upd (FlattenEnv -> InScopeSet fe_in_scope FlattenEnv env) } flattenTys :: InScopeSet -> [Type] -> [Type] -- See Note [Flattening] -- NB: the returned types may mention fresh type variables, -- arising from the flattening. We don't return the -- mapping from those fresh vars to the ty-fam -- applications they stand for (we could, but no need) flattenTys :: InScopeSet -> [Type] -> [Type] flattenTys InScopeSet in_scope [Type] tys = (FlattenEnv, [Type]) -> [Type] forall a b. (a, b) -> b snd ((FlattenEnv, [Type]) -> [Type]) -> (FlattenEnv, [Type]) -> [Type] forall a b. (a -> b) -> a -> b $ TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type]) coreFlattenTys TvSubstEnv emptyTvSubstEnv (InScopeSet -> FlattenEnv emptyFlattenEnv InScopeSet in_scope) [Type] tys coreFlattenTys :: TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type]) coreFlattenTys :: TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type]) coreFlattenTys TvSubstEnv subst = (FlattenEnv -> Type -> (FlattenEnv, Type)) -> FlattenEnv -> [Type] -> (FlattenEnv, [Type]) forall (t :: * -> *) a b c. Traversable t => (a -> b -> (a, c)) -> a -> t b -> (a, t c) mapAccumL (TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type) coreFlattenTy TvSubstEnv subst) coreFlattenTy :: TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type) coreFlattenTy :: TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type) coreFlattenTy TvSubstEnv subst = FlattenEnv -> Type -> (FlattenEnv, Type) go where go :: FlattenEnv -> Type -> (FlattenEnv, Type) go FlattenEnv env Type ty | Just Type ty' <- Type -> Maybe Type coreView Type ty = FlattenEnv -> Type -> (FlattenEnv, Type) go FlattenEnv env Type ty' go FlattenEnv env (TyVarTy TyVar tv) | Just Type ty <- TvSubstEnv -> TyVar -> Maybe Type forall a. VarEnv a -> TyVar -> Maybe a lookupVarEnv TvSubstEnv subst TyVar tv = (FlattenEnv env, Type ty) | Bool otherwise = let (FlattenEnv env', Type ki) = FlattenEnv -> Type -> (FlattenEnv, Type) go FlattenEnv env (TyVar -> Type tyVarKind TyVar tv) in (FlattenEnv env', TyVar -> Type mkTyVarTy (TyVar -> Type) -> TyVar -> Type forall a b. (a -> b) -> a -> b $ TyVar -> Type -> TyVar setTyVarKind TyVar tv Type ki) go FlattenEnv env (AppTy Type ty1 Type ty2) = let (FlattenEnv env1, Type ty1') = FlattenEnv -> Type -> (FlattenEnv, Type) go FlattenEnv env Type ty1 (FlattenEnv env2, Type ty2') = FlattenEnv -> Type -> (FlattenEnv, Type) go FlattenEnv env1 Type ty2 in (FlattenEnv env2, Type -> Type -> Type AppTy Type ty1' Type ty2') go FlattenEnv env (TyConApp TyCon tc [Type] tys) -- NB: Don't just check if isFamilyTyCon: this catches *data* families, -- which are generative and thus can be preserved during flattening | Bool -> Bool not (TyCon -> Role -> Bool isGenerativeTyCon TyCon tc Role Nominal) = TvSubstEnv -> FlattenEnv -> TyCon -> [Type] -> (FlattenEnv, Type) coreFlattenTyFamApp TvSubstEnv subst FlattenEnv env TyCon tc [Type] tys | Bool otherwise = let (FlattenEnv env', [Type] tys') = TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type]) coreFlattenTys TvSubstEnv subst FlattenEnv env [Type] tys in (FlattenEnv env', TyCon -> [Type] -> Type mkTyConApp TyCon tc [Type] tys') go FlattenEnv env ty :: Type ty@(FunTy { ft_arg :: Type -> Type ft_arg = Type ty1, ft_res :: Type -> Type ft_res = Type ty2 }) = let (FlattenEnv env1, Type ty1') = FlattenEnv -> Type -> (FlattenEnv, Type) go FlattenEnv env Type ty1 (FlattenEnv env2, Type ty2') = FlattenEnv -> Type -> (FlattenEnv, Type) go FlattenEnv env1 Type ty2 in (FlattenEnv env2, Type ty { ft_arg :: Type ft_arg = Type ty1', ft_res :: Type ft_res = Type ty2' }) go FlattenEnv env (ForAllTy (Bndr TyVar tv ArgFlag vis) Type ty) = let (FlattenEnv env1, TvSubstEnv subst', TyVar tv') = TvSubstEnv -> FlattenEnv -> TyVar -> (FlattenEnv, TvSubstEnv, TyVar) coreFlattenVarBndr TvSubstEnv subst FlattenEnv env TyVar tv (FlattenEnv env2, Type ty') = TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type) coreFlattenTy TvSubstEnv subst' FlattenEnv env1 Type ty in (FlattenEnv env2, VarBndr TyVar ArgFlag -> Type -> Type ForAllTy (TyVar -> ArgFlag -> VarBndr TyVar ArgFlag forall var argf. var -> argf -> VarBndr var argf Bndr TyVar tv' ArgFlag vis) Type ty') go FlattenEnv env ty :: Type ty@(LitTy {}) = (FlattenEnv env, Type ty) go FlattenEnv env (CastTy Type ty Coercion co) = let (FlattenEnv env1, Type ty') = FlattenEnv -> Type -> (FlattenEnv, Type) go FlattenEnv env Type ty (FlattenEnv env2, Coercion co') = TvSubstEnv -> FlattenEnv -> Coercion -> (FlattenEnv, Coercion) coreFlattenCo TvSubstEnv subst FlattenEnv env1 Coercion co in (FlattenEnv env2, Type -> Coercion -> Type CastTy Type ty' Coercion co') go FlattenEnv env (CoercionTy Coercion co) = let (FlattenEnv env', Coercion co') = TvSubstEnv -> FlattenEnv -> Coercion -> (FlattenEnv, Coercion) coreFlattenCo TvSubstEnv subst FlattenEnv env Coercion co in (FlattenEnv env', Coercion -> Type CoercionTy Coercion co') -- when flattening, we don't care about the contents of coercions. -- so, just return a fresh variable of the right (flattened) type coreFlattenCo :: TvSubstEnv -> FlattenEnv -> Coercion -> (FlattenEnv, Coercion) coreFlattenCo :: TvSubstEnv -> FlattenEnv -> Coercion -> (FlattenEnv, Coercion) coreFlattenCo TvSubstEnv subst FlattenEnv env Coercion co = (FlattenEnv env2, TyVar -> Coercion mkCoVarCo TyVar covar) where fresh_name :: Name fresh_name = Name mkFlattenFreshCoName (FlattenEnv env1, Type kind') = TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type) coreFlattenTy TvSubstEnv subst FlattenEnv env (Coercion -> Type coercionType Coercion co) covar :: TyVar covar = InScopeSet -> TyVar -> TyVar uniqAway (FlattenEnv -> InScopeSet fe_in_scope FlattenEnv env1) (Name -> Type -> TyVar mkCoVar Name fresh_name Type kind') -- Add the covar to the FlattenEnv's in-scope set. -- See Note [Flattening], wrinkle 2A. env2 :: FlattenEnv env2 = FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv updateInScopeSet FlattenEnv env1 ((InScopeSet -> TyVar -> InScopeSet) -> TyVar -> InScopeSet -> InScopeSet forall a b c. (a -> b -> c) -> b -> a -> c flip InScopeSet -> TyVar -> InScopeSet extendInScopeSet TyVar covar) coreFlattenVarBndr :: TvSubstEnv -> FlattenEnv -> TyCoVar -> (FlattenEnv, TvSubstEnv, TyVar) coreFlattenVarBndr :: TvSubstEnv -> FlattenEnv -> TyVar -> (FlattenEnv, TvSubstEnv, TyVar) coreFlattenVarBndr TvSubstEnv subst FlattenEnv env TyVar tv = (FlattenEnv env2, TvSubstEnv subst', TyVar tv') where -- See Note [Flattening], wrinkle 2B. kind :: Type kind = TyVar -> Type varType TyVar tv (FlattenEnv env1, Type kind') = TvSubstEnv -> FlattenEnv -> Type -> (FlattenEnv, Type) coreFlattenTy TvSubstEnv subst FlattenEnv env Type kind tv' :: TyVar tv' = InScopeSet -> TyVar -> TyVar uniqAway (FlattenEnv -> InScopeSet fe_in_scope FlattenEnv env1) (TyVar -> Type -> TyVar setVarType TyVar tv Type kind') subst' :: TvSubstEnv subst' = TvSubstEnv -> TyVar -> Type -> TvSubstEnv forall a. VarEnv a -> TyVar -> a -> VarEnv a extendVarEnv TvSubstEnv subst TyVar tv (TyVar -> Type mkTyVarTy TyVar tv') env2 :: FlattenEnv env2 = FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv updateInScopeSet FlattenEnv env1 ((InScopeSet -> TyVar -> InScopeSet) -> TyVar -> InScopeSet -> InScopeSet forall a b c. (a -> b -> c) -> b -> a -> c flip InScopeSet -> TyVar -> InScopeSet extendInScopeSet TyVar tv') coreFlattenTyFamApp :: TvSubstEnv -> FlattenEnv -> TyCon -- type family tycon -> [Type] -- args, already flattened -> (FlattenEnv, Type) coreFlattenTyFamApp :: TvSubstEnv -> FlattenEnv -> TyCon -> [Type] -> (FlattenEnv, Type) coreFlattenTyFamApp TvSubstEnv tv_subst FlattenEnv env TyCon fam_tc [Type] fam_args = case TypeMap TyVar -> Type -> Maybe TyVar forall a. TypeMap a -> Type -> Maybe a lookupTypeMap TypeMap TyVar type_map Type fam_ty of Just TyVar tv -> (FlattenEnv env', Type -> [Type] -> Type mkAppTys (TyVar -> Type mkTyVarTy TyVar tv) [Type] leftover_args') Maybe TyVar Nothing -> let tyvar_name :: Name tyvar_name = TyCon -> Name forall a. Uniquable a => a -> Name mkFlattenFreshTyName TyCon fam_tc tv :: TyVar tv = InScopeSet -> TyVar -> TyVar uniqAway InScopeSet in_scope (TyVar -> TyVar) -> TyVar -> TyVar forall a b. (a -> b) -> a -> b $ Name -> Type -> TyVar mkTyVar Name tyvar_name (HasDebugCallStack => Type -> Type Type -> Type typeKind Type fam_ty) ty' :: Type ty' = Type -> [Type] -> Type mkAppTys (TyVar -> Type mkTyVarTy TyVar tv) [Type] leftover_args' env'' :: FlattenEnv env'' = FlattenEnv env' { fe_type_map :: TypeMap TyVar fe_type_map = TypeMap TyVar -> Type -> TyVar -> TypeMap TyVar forall a. TypeMap a -> Type -> a -> TypeMap a extendTypeMap TypeMap TyVar type_map Type fam_ty TyVar tv , fe_in_scope :: InScopeSet fe_in_scope = InScopeSet -> TyVar -> InScopeSet extendInScopeSet InScopeSet in_scope TyVar tv } in (FlattenEnv env'', Type ty') where arity :: Int arity = TyCon -> Int tyConArity TyCon fam_tc tcv_subst :: TCvSubst tcv_subst = InScopeSet -> TvSubstEnv -> CvSubstEnv -> TCvSubst TCvSubst (FlattenEnv -> InScopeSet fe_in_scope FlattenEnv env) TvSubstEnv tv_subst CvSubstEnv forall a. VarEnv a emptyVarEnv ([Type] sat_fam_args, [Type] leftover_args) = ASSERT( arity <= length fam_args ) Int -> [Type] -> ([Type], [Type]) forall a. Int -> [a] -> ([a], [a]) splitAt Int arity [Type] fam_args -- Apply the substitution before looking up an application in the -- environment. See Note [Flattening], wrinkle 1. -- NB: substTys short-cuts the common case when the substitution is empty. sat_fam_args' :: [Type] sat_fam_args' = HasCallStack => TCvSubst -> [Type] -> [Type] TCvSubst -> [Type] -> [Type] substTys TCvSubst tcv_subst [Type] sat_fam_args (FlattenEnv env', [Type] leftover_args') = TvSubstEnv -> FlattenEnv -> [Type] -> (FlattenEnv, [Type]) coreFlattenTys TvSubstEnv tv_subst FlattenEnv env [Type] leftover_args -- `fam_tc` may be over-applied to `fam_args` (see Note [Flattening], -- wrinkle 3), so we split it into the arguments needed to saturate it -- (sat_fam_args') and the rest (leftover_args') fam_ty :: Type fam_ty = TyCon -> [Type] -> Type mkTyConApp TyCon fam_tc [Type] sat_fam_args' FlattenEnv { fe_type_map :: FlattenEnv -> TypeMap TyVar fe_type_map = TypeMap TyVar type_map , fe_in_scope :: FlattenEnv -> InScopeSet fe_in_scope = InScopeSet in_scope } = FlattenEnv env' mkFlattenFreshTyName :: Uniquable a => a -> Name mkFlattenFreshTyName :: a -> Name mkFlattenFreshTyName a unq = Unique -> FastString -> Name mkSysTvName (a -> Unique forall a. Uniquable a => a -> Unique getUnique a unq) (String -> FastString fsLit String "flt") mkFlattenFreshCoName :: Name mkFlattenFreshCoName :: Name mkFlattenFreshCoName = Unique -> FastString -> Name mkSystemVarName (Unique -> Int -> Unique deriveUnique Unique eqPrimTyConKey Int 71) (String -> FastString fsLit String "flc")