%
% (c) The University of Glasgow 2006
%
FamInstEnv: Type checked family instance declarations
\begin{code}
module FamInstEnv (
FamInst(..), famInstTyCon, famInstTyVars,
pprFamInst, pprFamInstHdr, pprFamInsts,
famInstHead, mkLocalFamInst, mkImportedFamInst,
FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs,
extendFamInstEnv, extendFamInstEnvList,
famInstEnvElts, familyInstances,
lookupFamInstEnv, lookupFamInstEnvConflicts,
topNormaliseType
) where
#include "HsVersions.h"
import InstEnv
import Unify
import Type
import TypeRep
import TyCon
import Coercion
import VarSet
import Var
import Name
import UniqFM
import Outputable
import Maybes
import Util
import FastString
\end{code}
%************************************************************************
%* *
\subsection{Type checked family instance heads}
%* *
%************************************************************************
\begin{code}
data FamInst
= FamInst { fi_fam :: Name
, fi_tcs :: [Maybe Name]
, fi_tvs :: TyVarSet
, fi_tys :: [Type]
, fi_tycon :: TyCon
}
famInstTyCon :: FamInst -> TyCon
famInstTyCon = fi_tycon
famInstTyVars :: FamInst -> TyVarSet
famInstTyVars = fi_tvs
\end{code}
\begin{code}
instance NamedThing FamInst where
getName = getName . fi_tycon
instance Outputable FamInst where
ppr = pprFamInst
pprFamInst :: FamInst -> SDoc
pprFamInst famInst
= hang (pprFamInstHdr famInst)
2 (ptext (sLit "--") <+> pprNameLoc (getName famInst))
pprFamInstHdr :: FamInst -> SDoc
pprFamInstHdr (FamInst {fi_tycon = rep_tc})
= pprTyConSort <+> pp_instance <+> pprHead
where
Just (fam_tc, tys) = tyConFamInst_maybe rep_tc
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)
famInstHead :: FamInst -> ([TyVar], TyCon, [Type])
famInstHead (FamInst {fi_tycon = tycon})
= case tyConFamInst_maybe tycon of
Nothing -> panic "FamInstEnv.famInstHead"
Just (fam, tys) -> (tyConTyVars tycon, fam, tys)
mkLocalFamInst :: TyCon -> FamInst
mkLocalFamInst tycon
= case tyConFamInst_maybe tycon of
Nothing -> panic "FamInstEnv.mkLocalFamInst"
Just (fam, tys) ->
FamInst {
fi_fam = tyConName fam,
fi_tcs = roughMatchTcs tys,
fi_tvs = mkVarSet . tyConTyVars $ tycon,
fi_tys = tys,
fi_tycon = tycon
}
mkImportedFamInst :: Name -> [Maybe Name] -> TyCon -> FamInst
mkImportedFamInst fam mb_tcs tycon
= FamInst {
fi_fam = fam,
fi_tcs = mb_tcs,
fi_tvs = mkVarSet . tyConTyVars $ tycon,
fi_tys = case tyConFamInst_maybe tycon of
Nothing -> panic "FamInstEnv.mkImportedFamInst"
Just (_, tys) -> tys,
fi_tycon = tycon
}
\end{code}
%************************************************************************
%* *
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 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
type FamInstEnvs = (FamInstEnv, FamInstEnv)
data FamilyInstEnv
= FamIE [FamInst]
Bool
instance Outputable FamilyInstEnv where
ppr (FamIE fs b) = ptext (sLit "FamIE") <+> ppr b <+> vcat (map ppr fs)
emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
emptyFamInstEnv :: FamInstEnv
emptyFamInstEnv = emptyUFM
famInstEnvElts :: FamInstEnv -> [FamInst]
famInstEnvElts fi = [elt | FamIE elts _ <- eltsUFM fi, elt <- elts]
familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
familyInstances (pkg_fie, home_fie) fam
= get home_fie ++ get pkg_fie
where
get env = case lookupUFM env fam of
Just (FamIE insts _) -> insts
Nothing -> []
extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis
extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs})
= addToUFM_C add inst_env cls_nm (FamIE [ins_item] ins_tyvar)
where
add (FamIE items tyvar) _ = FamIE (ins_item:items)
(ins_tyvar || tyvar)
ins_tyvar = not (any isJust mb_tcs)
\end{code}
%************************************************************************
%* *
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)'.
\begin{code}
type FamInstMatch = (FamInst, [Type])
lookupFamInstEnv
:: FamInstEnvs
-> TyCon -> [Type]
-> [FamInstMatch]
lookupFamInstEnv
= lookup_fam_inst_env match True
where
match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
lookupFamInstEnvConflicts
:: FamInstEnvs
-> FamInst
-> [TyVar]
-> [FamInstMatch]
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
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) )
case tcUnifyTys instanceBindFun tpl_tys match_tys of
Just subst | conflicting old_fam_inst subst -> Just subst
_other -> Nothing
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}
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 MatchFun = FamInst
-> TyVarSet -> [Type]
-> [Type]
-> Maybe TvSubst
type OneSidedMatch = Bool
lookup_fam_inst_env
:: MatchFun
-> OneSidedMatch
-> FamInstEnvs
-> TyCon -> [Type]
-> [FamInstMatch]
lookup_fam_inst_env match_fun one_sided (pkg_ie, home_ie) fam tys
| not (isFamilyTyCon fam)
= []
| otherwise
= ASSERT2( n_tys >= arity, ppr fam <+> ppr tys )
home_matches ++ pkg_matches
where
home_matches = lookup home_ie
pkg_matches = lookup pkg_ie
arity = tyConArity fam
n_tys = length tys
extra_tys = drop arity tys
(match_tys, add_extra_tys)
| arity > n_tys = (take arity tys, \res_tys -> res_tys ++ extra_tys)
| otherwise = (tys, \res_tys -> res_tys)
rough_tcs = roughMatchTcs match_tys
all_tvs = all isNothing rough_tcs && one_sided
lookup env = case lookupUFM env fam of
Nothing -> []
Just (FamIE insts has_tv_insts)
| 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)
| instanceCantMatch rough_tcs mb_tcs
= find rest
| Just subst <- match_fun item tpl_tvs tpl_tys match_tys
= (item, add_extra_tys $ substTyVars subst (tyConTyVars tycon)) : find rest
| otherwise
= find rest
\end{code}
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.
%************************************************************************
%* *
Looking up a family instance
%* *
%************************************************************************
\begin{code}
topNormaliseType :: FamInstEnvs
-> Type
-> Maybe (Coercion, Type)
topNormaliseType env ty
= go [] ty
where
go :: [TyCon] -> Type -> Maybe (Coercion, Type)
go rec_nts ty | Just ty' <- coreView ty
= go rec_nts ty'
go rec_nts (TyConApp tc tys)
| Just co_con <- newTyConCo_maybe tc
= if tc `elem` rec_nts
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)
| isFamilyTyCon tc
, (ACo co, ty) <- normaliseTcApp env tc tys
=
add_co co rec_nts ty
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')
normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (CoercionI, Type)
normaliseTcApp env tc tys
| isFamilyTyCon tc
, tyConArity tc <= length tys
, [(fam_inst, inst_tys)] <- lookupFamInstEnv env tc ntys
= let
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
(cois, ntys) = mapAndUnzip (normaliseType env) tys
tycon_coi = mkTyConAppCoI tc cois
normaliseType :: FamInstEnvs
-> Type
-> (CoercionI, Type)
normaliseType env ty
| Just ty' <- coreView ty = normaliseType env ty'
normaliseType env (TyConApp tc tys)
= normaliseTcApp env tc tys
normaliseType env (AppTy ty1 ty2)
= let (coi1,nty1) = normaliseType env ty1
(coi2,nty2) = normaliseType env ty2
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 coi1 coi2, mkFunTy nty1 nty2)
normaliseType env (ForAllTy tyvar ty1)
= let (coi,nty1) = normaliseType env ty1
in (mkForAllTyCoI tyvar coi, ForAllTy tyvar nty1)
normaliseType _ ty@(TyVarTy _)
= (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 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 coi1 coi2, PredTy $ EqPred ty1' ty2')
\end{code}