extendFamInstEnv, extendFamInstEnvList,
famInstEnvElts, familyInstances,
- lookupFamInstEnv, lookupFamInstEnvUnify,
+ lookupFamInstEnv, lookupFamInstEnvConflicts,
-- Normalisation
topNormaliseType
import Maybes
import Util
import FastString
-
-import Maybe
\end{code}
2 (ptext (sLit "--") <+> pprNameLoc (getName famInst))
pprFamInstHdr :: FamInst -> SDoc
-pprFamInstHdr (FamInst {fi_fam = fam, fi_tys = tys, fi_tycon = tycon})
- = pprTyConSort <+> pprHead
+pprFamInstHdr (FamInst {fi_tycon = rep_tc})
+ = pprTyConSort <+> pp_instance <+> pprHead
where
- pprHead = pprTypeApp fam tys
- pprTyConSort | isDataTyCon tycon = ptext (sLit "data instance")
- | isNewTyCon tycon = ptext (sLit "newtype instance")
- | isSynTyCon tycon = ptext (sLit "type instance")
- | otherwise = panic "FamInstEnv.pprFamInstHdr"
+ Just (fam_tc, tys) = tyConFamInst_maybe rep_tc
+
+ -- For *associated* types, say "type T Int = blah"
+ -- For *top level* type instances, say "type instance T Int = blah"
+ pp_instance
+ | isTyConAssoc fam_tc = empty
+ | otherwise = ptext (sLit "instance")
+
+ pprHead = pprTypeApp fam_tc tys
+ pprTyConSort | isDataTyCon rep_tc = ptext (sLit "data")
+ | isNewTyCon rep_tc = ptext (sLit "newtype")
+ | isSynTyCon rep_tc = ptext (sLit "type")
+ | isAbstractTyCon rep_tc = ptext (sLit "data")
+ | otherwise = panic "FamInstEnv.pprFamInstHdr"
pprFamInsts :: [FamInst] -> SDoc
pprFamInsts finsts = vcat (map pprFamInst finsts)
%* *
%************************************************************************
-InstEnv maps a family name to the list of known instances for that family.
+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 contructors
+and pattern matching.
+
+Neverthless 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]
\begin{code}
type FamInstEnv = UniqFM FamilyInstEnv -- Maps a family to its instances
+ -- See Note [FamInstEnv]
type FamInstEnvs = (FamInstEnv, FamInstEnv)
- -- External package inst-env, Home-package inst-env
+ -- External package inst-env, Home-package inst-env
data FamilyInstEnv
= FamIE [FamInst] -- The instances for a particular family, in any order
we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
-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)
+\begin{code}
+type FamInstMatch = (FamInst, [Type]) -- Matching type instance
+ -- See Note [Over-saturated matches]
-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))
+lookupFamInstEnv
+ :: FamInstEnvs
+ -> TyCon -> [Type] -- What we are looking for
+ -> [FamInstMatch] -- Successful matches
+-- Precondition: the tycon is saturated (or over-saturated)
+
+lookupFamInstEnv
+ = lookup_fam_inst_env match True
+ where
+ match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
+
+lookupFamInstEnvConflicts
+ :: FamInstEnvs
+ -> FamInst -- Putative new instance
+ -> [TyVar] -- Unique tyvars, matching arity of FamInst
+ -> [FamInstMatch] -- Conflicting matches
+-- E.g. when we are about to add
+-- f : type instance F [a] = a->a
+-- we do (lookupFamInstConflicts f [b])
+-- to find conflicting matches
+-- The skolem tyvars are needed because we don't have a
+-- unique supply to hand
+--
+-- Precondition: the tycon is saturated (or over-saturated)
-Then looking up (F (Int,Bool) Char) will return a FamInstMatch
- (FPair, [Int,Bool,Char])
+lookupFamInstEnvConflicts envs fam_inst skol_tvs
+ = lookup_fam_inst_env my_unify False envs fam tys'
+ where
+ inst_tycon = famInstTyCon fam_inst
+ (fam, tys) = expectJust "FamInstEnv.lookuFamInstEnvConflicts"
+ (tyConFamInst_maybe inst_tycon)
+ skol_tys = mkTyVarTys skol_tvs
+ tys' = substTys (zipTopTvSubst (tyConTyVars inst_tycon) skol_tys) tys
+ -- In example above, fam tys' = F [b]
+
+ my_unify old_fam_inst tpl_tvs tpl_tys match_tys
+ = ASSERT2( tyVarsOfTypes 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
+ case tcUnifyTys instanceBindFun tpl_tys match_tys of
+ Just subst | conflicting old_fam_inst subst -> Just subst
+ _other -> Nothing
+
+ -- - 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. We require that they are syntactically equal;
+ -- anything else would be difficult to test for at this stage.
+ conflicting old_fam_inst subst
+ | isAlgTyCon fam = True
+ | otherwise = not (old_rhs `tcEqType` new_rhs)
+ where
+ old_tycon = famInstTyCon old_fam_inst
+ old_tvs = tyConTyVars old_tycon
+ old_rhs = mkTyConApp old_tycon (substTyVars subst old_tvs)
+ new_rhs = mkTyConApp inst_tycon (substTyVars subst skol_tvs)
+\end{code}
-The "extra" type argument [Char] just stays on the end.
+While @lookupFamInstEnv@ uses a one-way match, the next function
+@lookupFamInstEnvConflicts@ uses two-way matching (ie, unification). This is
+needed to check for overlapping instances.
+For class instances, these two variants of lookup are combined into one
+function (cf, @InstEnv@). We don't do that for family instances as the
+results of matching and unification are used in two different contexts.
+Moreover, matching is the wildly more frequently used operation in the case of
+indexed synonyms and we don't want to slow that down by needless unification.
\begin{code}
-type FamInstMatch = (FamInst, [Type]) -- Matching type instance
- -- See Note [Over-saturated matches]
-
-lookupFamInstEnv :: FamInstEnvs
- -> TyCon -> [Type] -- What we are looking for
- -> [FamInstMatch] -- Successful matches
-lookupFamInstEnv (pkg_ie, home_ie) fam tys
- | not (isOpenTyCon fam)
+------------------------------------------------------------
+-- 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 TvSubst
+
+type OneSidedMatch = Bool -- Are optimisations that are only valid for
+ -- one sided matches allowed?
+
+lookup_fam_inst_env -- The worker, local to this module
+ :: MatchFun
+ -> OneSidedMatch
+ -> FamInstEnvs
+ -> TyCon -> [Type] -- What we are looking for
+ -> [FamInstMatch] -- Successful matches
+
+-- Precondition: the tycon is saturated (or over-saturated)
+
+lookup_fam_inst_env match_fun one_sided (pkg_ie, home_ie) fam tys
+ | not (isFamilyTyCon fam)
= []
| otherwise
- = ASSERT( n_tys >= arity ) -- Family type applications must be saturated
+ = ASSERT2( n_tys >= arity, ppr fam <+> ppr tys ) -- Family type applications must be saturated
home_matches ++ pkg_matches
where
- rough_tcs = roughMatchTcs tys
- all_tvs = all isNothing rough_tcs
home_matches = lookup home_ie
pkg_matches = lookup pkg_ie
-- The second case is the common one, hence functional representation
--------------
+ rough_tcs = roughMatchTcs match_tys
+ all_tvs = all isNothing rough_tcs && one_sided
+
+ --------------
lookup env = case lookupUFM env fam of
Nothing -> [] -- No instances for this class
Just (FamIE insts has_tv_insts)
= find rest
-- Proper check
- | Just subst <- tcMatchTys tpl_tvs tpl_tys match_tys
+ | Just subst <- match_fun item tpl_tvs tpl_tys match_tys
= (item, add_extra_tys $ substTyVars subst (tyConTyVars tycon)) : find rest
-- No match => try next
= find rest
\end{code}
-While @lookupFamInstEnv@ uses a one-way match, the next function
-@lookupFamInstEnvUnify@ uses two-way matching (ie, unification). This is
-needed to check for overlapping instances.
+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)
-For class instances, these two variants of lookup are combined into one
-function (cf, @InstEnv@). We don't do that for family instances as the
-results of matching and unification are used in two different contexts.
-Moreover, matching is the wildly more frequently used operation in the case of
-indexed synonyms and we don't want to slow that down by needless unification.
+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))
-\begin{code}
-lookupFamInstEnvUnify :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type]
- -> [(FamInstMatch, TvSubst)]
-lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
- | not (isOpenTyCon fam)
- = []
- | otherwise
- = home_matches ++ pkg_matches
- where
- rough_tcs = roughMatchTcs tys
- all_tvs = all isNothing rough_tcs
- home_matches = lookup home_ie
- pkg_matches = lookup pkg_ie
+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.
- --------------
- lookup env = case lookupUFM env fam of
- Nothing -> [] -- No instances for this class
- Just (FamIE insts has_tv_insts)
- -- Short cut for common case:
- -- The thing we are looking up is of form (C a
- -- b c), and the FamIE has no instances of
- -- that form, so don't bother to search
- | all_tvs && not has_tv_insts -> []
- | otherwise -> find insts
- --------------
- find [] = []
- find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs,
- fi_tys = tpl_tys, fi_tycon = tycon }) : rest)
- -- Fast check for no match, uses the "rough match" fields
- | instanceCantMatch rough_tcs mb_tcs
- = find rest
- | otherwise
- = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
- (ppr fam <+> ppr tys <+> ppr all_tvs) $$
- (ppr tycon <+> ppr tpl_tvs <+> ppr tpl_tys)
- )
- -- Unification will break badly if the variables overlap
- -- They shouldn't because we allocate separate uniques for them
- case tcUnifyTys instanceBindFun tpl_tys tys of
- Just subst -> let rep_tys = substTyVars subst (tyConTyVars tycon)
- in
- ((item, rep_tys), subst) : find rest
- Nothing -> find rest
-\end{code}
%************************************************************************
%* *
| otherwise = rec_nts
go rec_nts (TyConApp tc tys) -- Expand open tycons
- | isOpenTyCon tc
+ | isFamilyTyCon tc
, (ACo co, ty) <- normaliseTcApp env tc tys
= -- The ACo says "something happened"
-- Note that normaliseType fully normalises, but it has do to so
---------------
normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (CoercionI, Type)
normaliseTcApp env tc tys
- = let -- First normalise the arg types so that they'll match
+ | isFamilyTyCon tc
+ , tyConArity tc <= length tys -- Unsaturated data families are possible
+ , [(fam_inst, inst_tys)] <- lookupFamInstEnv env tc ntys
+ = let -- A matching family instance exists
+ rep_tc = famInstTyCon fam_inst
+ co_tycon = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
+ co = mkTyConApp co_tycon inst_tys
+ first_coi = mkTransCoI tycon_coi (ACo co)
+ (rest_coi, nty) = normaliseType env (mkTyConApp rep_tc inst_tys)
+ fix_coi = mkTransCoI first_coi rest_coi
+ in
+ (fix_coi, nty)
+
+ | otherwise
+ = (tycon_coi, TyConApp tc ntys)
+
+ where
+ -- Normalise the arg types so that they'll match
-- when we lookup in in the instance envt
- (cois, ntys) = mapAndUnzip (normaliseType env) tys
- tycon_coi = mkTyConAppCoI tc ntys cois
- in -- Now try the top-level redex
- case lookupFamInstEnv env tc ntys of
- -- A matching family instance exists
- [(fam_inst, tys)] -> (fix_coi, nty)
- where
- rep_tc = famInstTyCon fam_inst
- co_tycon = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
- co = mkTyConApp co_tycon tys
- first_coi = mkTransCoI tycon_coi (ACo co)
- (rest_coi,nty) = normaliseType env (mkTyConApp rep_tc tys)
- fix_coi = mkTransCoI first_coi rest_coi
-
- -- No unique matching family instance exists;
- -- we do not do anything
- _ -> (tycon_coi, TyConApp tc ntys)
+ (cois, ntys) = mapAndUnzip (normaliseType env) tys
+ tycon_coi = mkTyConAppCoI tc cois
+
---------------
normaliseType :: FamInstEnvs -- environment with family instances
-> Type -- old type
normaliseType env (AppTy ty1 ty2)
= let (coi1,nty1) = normaliseType env ty1
(coi2,nty2) = normaliseType env ty2
- in (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
+ in (mkAppTyCoI coi1 coi2, mkAppTy nty1 nty2)
normaliseType env (FunTy ty1 ty2)
= let (coi1,nty1) = normaliseType env ty1
(coi2,nty2) = normaliseType env ty2
- in (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
+ in (mkFunTyCoI coi1 coi2, mkFunTy nty1 nty2)
normaliseType env (ForAllTy tyvar ty1)
= let (coi,nty1) = normaliseType env ty1
- in (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
+ in (mkForAllTyCoI tyvar coi, ForAllTy tyvar nty1)
normaliseType _ ty@(TyVarTy _)
- = (IdCo,ty)
+ = (IdCo ty,ty)
normaliseType env (PredTy predty)
= normalisePred env predty
normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type)
normalisePred env (ClassP cls tys)
= let (cois,tys') = mapAndUnzip (normaliseType env) tys
- in (mkClassPPredCoI cls tys' cois, PredTy $ ClassP cls tys')
+ in (mkClassPPredCoI cls cois, PredTy $ ClassP cls tys')
normalisePred env (IParam ipn ty)
= let (coi,ty') = normaliseType env ty
in (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
normalisePred env (EqPred ty1 ty2)
= let (coi1,ty1') = normaliseType env ty1
(coi2,ty2') = normaliseType env ty2
- in (mkEqPredCoI ty1' coi1 ty2' coi2, PredTy $ EqPred ty1' ty2')
+ in (mkEqPredCoI coi1 coi2, PredTy $ EqPred ty1' ty2')
\end{code}