import TyCon
import Coercion
import VarSet
-import Var
import Name
import UniqFM
import Outputable
pprFamInst :: FamInst -> SDoc
pprFamInst famInst
= hang (pprFamInstHdr famInst)
- 2 (ptext (sLit "--") <+> pprNameLoc (getName famInst))
+ 2 (vcat [ ifPprDebug (ptext (sLit "Coercion axiom:") <+> pp_ax)
+ , ptext (sLit "--") <+> pprNameLoc (getName famInst)])
+ where
+ pp_ax = case tyConFamilyCoercion_maybe (fi_tycon famInst) of
+ Just ax -> ppr ax
+ Nothing -> ptext (sLit "<not there!>")
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")
- | isAbstractTyCon tycon = ptext (sLit "data 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
-- If *not* then the common case of looking up
-- (T a b c) can fail immediately
+instance Outputable FamilyInstEnv where
+ ppr (FamIE fs b) = ptext (sLit "FamIE") <+> ppr b <+> vcat (map ppr fs)
+
-- INVARIANTS:
-- * The fs_tvs are distinct in each FamInst
-- of a range value of the map (so we can safely unify them)
:: 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
-- 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)
lookupFamInstEnvConflicts envs fam_inst skol_tvs
= lookup_fam_inst_env my_unify False envs fam tys'
-- 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)
+ | otherwise = not (old_rhs `eqType` new_rhs)
where
old_tycon = famInstTyCon old_fam_inst
old_tvs = tyConTyVars old_tycon
-> 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 (isOpenTyCon fam)
+ | 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
home_matches = lookup home_ie
go rec_nts ty | Just ty' <- coreView ty -- Expand synonyms
= go rec_nts ty'
- go rec_nts (TyConApp tc tys) -- Expand newtypes
- | Just co_con <- newTyConCo_maybe tc -- See Note [Expanding newtypes]
- = if tc `elem` rec_nts -- in Type.lhs
+ go rec_nts (TyConApp tc tys)
+ | isNewTyCon tc -- Expand newtypes
+ = if tc `elem` rec_nts -- See Note [Expanding newtypes] in Type.lhs
then Nothing
- else let nt_co = mkTyConApp co_con tys
- in add_co nt_co rec_nts' nt_rhs
- where
- nt_rhs = newTyConInstRhs tc tys
- rec_nts' | isRecursiveTyCon tc = tc:rec_nts
- | otherwise = rec_nts
-
- go rec_nts (TyConApp tc tys) -- Expand open tycons
- | isOpenTyCon tc
- , (ACo co, ty) <- normaliseTcApp env tc tys
- = -- The ACo says "something happened"
- -- Note that normaliseType fully normalises, but it has do to so
- -- to be sure that
- add_co co rec_nts ty
+ else let nt_co = mkAxInstCo (newTyConCo tc) tys
+ in add_co nt_co rec_nts' nt_rhs
+
+ | isFamilyTyCon tc -- Expand open tycons
+ , (co, ty) <- normaliseTcApp env tc tys
+ -- Note that normaliseType fully normalises,
+ -- but it has do to so to be sure that
+ , not (isReflCo co)
+ = add_co co rec_nts ty
+ where
+ nt_rhs = newTyConInstRhs tc tys
+ rec_nts' | isRecursiveTyCon tc = tc:rec_nts
+ | otherwise = rec_nts
go _ _ = Nothing
add_co co rec_nts ty
= case go rec_nts ty of
Nothing -> Just (co, ty)
- Just (co', ty') -> Just (mkTransCoercion co co', ty')
+ Just (co', ty') -> Just (mkTransCo co co', ty')
---------------
-normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (CoercionI, Type)
+normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (Coercion, Type)
normaliseTcApp env tc tys
- = let -- First 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;
+ | 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 = mkAxInstCo co_tycon inst_tys
+ first_coi = mkTransCo tycon_coi co
+ (rest_coi,nty) = normaliseType env (mkTyConApp rep_tc inst_tys)
+ fix_coi = mkTransCo first_coi rest_coi
+ in
+ (fix_coi, nty)
+
+ | otherwise -- No unique matching family instance exists;
-- we do not do anything
- _ -> (tycon_coi, TyConApp tc ntys)
+ = (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 = mkTyConAppCo tc cois
+
---------------
normaliseType :: FamInstEnvs -- environment with family instances
-> Type -- old type
- -> (CoercionI, Type) -- (coercion,new type), where
+ -> (Coercion, Type) -- (coercion,new type), where
-- co :: old-type ~ new_type
-- Normalise the input type, by eliminating *all* type-function redexes
--- Returns with IdCo if nothing happens
+-- Returns with Refl if nothing happens
normaliseType env ty
| Just ty' <- coreView ty = normaliseType env ty'
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 (mkAppCo 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 (mkFunCo coi1 coi2, mkFunTy nty1 nty2)
normaliseType env (ForAllTy tyvar ty1)
= let (coi,nty1) = normaliseType env ty1
- in (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
+ in (mkForAllCo tyvar coi, ForAllTy tyvar nty1)
normaliseType _ ty@(TyVarTy _)
- = (IdCo,ty)
+ = (Refl ty,ty)
normaliseType env (PredTy predty)
= normalisePred env predty
---------------
-normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type)
+normalisePred :: FamInstEnvs -> PredType -> (Coercion,Type)
normalisePred env (ClassP cls tys)
- = let (cois,tys') = mapAndUnzip (normaliseType env) tys
- in (mkClassPPredCoI cls tys' cois, PredTy $ ClassP cls tys')
+ = let (cos,tys') = mapAndUnzip (normaliseType env) tys
+ in (mkPredCo $ ClassP cls cos, PredTy $ ClassP cls tys')
normalisePred env (IParam ipn ty)
- = let (coi,ty') = normaliseType env ty
- in (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
+ = let (co,ty') = normaliseType env ty
+ in (mkPredCo $ (IParam ipn co), 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')
+ = let (co1,ty1') = normaliseType env ty1
+ (co2,ty2') = normaliseType env ty2
+ in (mkPredCo $ (EqPred co1 co2), PredTy $ EqPred ty1' ty2')
\end{code}
projects / ghc-hetmet.git / blobdiff