pprFamInst, pprFamInstHdr, pprFamInsts,
famInstHead, mkLocalFamInst, mkImportedFamInst,
- FamInstEnv, emptyFamInstEnv, extendFamInstEnv, extendFamInstEnvList,
+ FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs,
+ extendFamInstEnv, extendFamInstEnvList,
famInstEnvElts, familyInstances,
- lookupFamInstEnv, lookupFamInstEnvUnify
+ lookupFamInstEnv, lookupFamInstEnvConflicts,
+
+ -- Normalisation
+ topNormaliseType
) where
#include "HsVersions.h"
import InstEnv
import Unify
-import TcGadt
-import TcType
import Type
+import TypeRep
import TyCon
+import Coercion
import VarSet
-import Var
import Name
-import OccName
-import SrcLoc
import UniqFM
import Outputable
-
-import Maybe
+import Maybes
+import Util
+import FastString
\end{code}
\begin{code}
data FamInst
= FamInst { fi_fam :: Name -- Family name
+ -- INVARIANT: fi_fam = case tyConFamInst_maybe fi_tycon of
+ -- Just (tc, tys) -> tc
-- Used for "rough matching"; same idea as for class instances
, fi_tcs :: [Maybe Name] -- Top of type args
+ -- INVARIANT: fi_tcs = roughMatchTcs fi_tys
-- Used for "proper matching"; ditto
, fi_tvs :: TyVarSet -- Template tyvars for full match
, fi_tys :: [Type] -- Full arg types
+ -- INVARIANT: fi_tvs = tyConTyVars fi_tycon
+ -- fi_tys = case tyConFamInst_maybe fi_tycon of
+ -- Just (_, tys) -> tys
, fi_tycon :: TyCon -- Representation tycon
}
famInstTyCon :: FamInst -> TyCon
famInstTyCon = fi_tycon
+famInstTyVars :: FamInst -> TyVarSet
famInstTyVars = fi_tvs
\end{code}
pprFamInst :: FamInst -> SDoc
pprFamInst famInst
= hang (pprFamInstHdr famInst)
- 2 (ptext SLIT("--") <+> (pprDefnLoc (getSrcLoc 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 = parenSymOcc (getOccName fam) (ppr fam) <+>
- sep (map pprParendType 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
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)
+emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
+emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
+
emptyFamInstEnv :: FamInstEnv
emptyFamInstEnv = emptyUFM
%************************************************************************
%* *
-\subsection{Looking up a family instance}
+ Looking up a family instance
%* *
%************************************************************************
-@lookupFamInstEnvExact@ looks up in a @FamInstEnv@ using an exact match.
-This is used when we want the @TyCon@ of a particular family instance (e.g.,
-during deriving classes).
-
-\begin{code}
-{- NOT NEEDED ANY MORE
-lookupFamInstEnvExact :: (FamInstEnv -- External package inst-env
- ,FamInstEnv) -- Home-package inst-env
- -> TyCon -> [Type] -- What we are looking for
- -> Maybe FamInst
-lookupFamInstEnvExact (pkg_ie, home_ie) fam tys
- = home_matches `mplus` pkg_matches
- where
- rough_tcs = roughMatchTcs tys
- all_tvs = all isNothing rough_tcs
- home_matches = lookup home_ie
- pkg_matches = lookup pkg_ie
-
- --------------
- lookup env = case lookupUFM env fam of
- Nothing -> 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 -> Nothing
- | otherwise -> find insts
-
- --------------
- find [] = Nothing
- find (item@(FamInst { fi_tcs = mb_tcs, fi_tys = tpl_tys }) : rest)
- -- Fast check for no match, uses the "rough match" fields
- | instanceCantMatch rough_tcs mb_tcs
- = find rest
-
- -- Proper check
- | tcEqTypes tpl_tys tys
- = Just item
-
- -- No match => try next
- | otherwise
- = find rest
--}
-\end{code}
-
@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).
-\begin{code}
-lookupFamInstEnv :: (FamInstEnv -- External package inst-env
- ,FamInstEnv) -- Home-package inst-env
- -> TyCon -> [Type] -- What we are looking for
- -> [(TvSubst, FamInst)] -- Successful matches
-lookupFamInstEnv (pkg_ie, home_ie) fam tys
- = 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
+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
- --------------
- 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
+ data instance T [a] = ..
- --------------
- 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
+desugared to
- -- Proper check
- | Just subst <- tcMatchTys tpl_tvs tpl_tys tys
- = (subst, item) : find rest
+ data :R42T a = ..
+ coe :Co:R42T a :: T [a] ~ :R42T a
- -- No match => try next
- | otherwise
- = find rest
+we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
+
+\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
+-- 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)
+
+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 `eqType` 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
-@lookupFamInstEnvUnify@ uses two-way matching (ie, unification). This is
+@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
indexed synonyms and we don't want to slow that down by needless unification.
\begin{code}
-lookupFamInstEnvUnify :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type]
- -> [(TvSubst, FamInst)]
-lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
- = home_matches ++ pkg_matches
+------------------------------------------------------------
+-- 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
+ = 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
+ -- See Note [Over-saturated matches]
+ 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)
+ -- 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
| instanceCantMatch rough_tcs mb_tcs
= find rest
+ -- Proper check
+ | 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
| 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 bind_fn tpl_tys tys of
- Just subst -> (subst, item) : find rest
- Nothing -> find rest
+ = find rest
+\end{code}
--- See explanation at @InstEnv.bind_fn@.
---
-bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
- | otherwise = BindMe
+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)
+
+-- Get rid of *outermost* (or toplevel)
+-- * type functions
+-- * newtypes
+-- using appropriate coercions.
+-- By "outer" we mean that toplevelNormaliseType guarantees to return
+-- a type that does not have a reducible redex (F ty1 .. tyn) as its
+-- outermost form. It *can* return something like (Maybe (F ty)), where
+-- (F ty) is a redex.
+
+-- Its a bit like Type.repType, but handles type families too
+
+topNormaliseType env ty
+ = go [] ty
+ where
+ go :: [TyCon] -> Type -> Maybe (Coercion, Type)
+ go rec_nts ty | Just ty' <- coreView ty -- Expand synonyms
+ = go rec_nts ty'
+
+ 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 = 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 (mkTransCo co co', ty')
+
+
+---------------
+normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (Coercion, Type)
+normaliseTcApp env tc tys
+ | 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)
+
+ 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
+ -> (Coercion, Type) -- (coercion,new type), where
+ -- co :: old-type ~ new_type
+-- Normalise the input type, by eliminating *all* type-function redexes
+-- Returns with Refl if nothing happens
+
+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 (mkAppCo coi1 coi2, mkAppTy nty1 nty2)
+normaliseType env (FunTy ty1 ty2)
+ = let (coi1,nty1) = normaliseType env ty1
+ (coi2,nty2) = normaliseType env ty2
+ in (mkFunCo coi1 coi2, mkFunTy nty1 nty2)
+normaliseType env (ForAllTy tyvar ty1)
+ = let (coi,nty1) = normaliseType env ty1
+ in (mkForAllCo tyvar coi, ForAllTy tyvar nty1)
+normaliseType _ ty@(TyVarTy _)
+ = (Refl ty,ty)
+normaliseType env (PredTy predty)
+ = normalisePred env predty
+
+---------------
+normalisePred :: FamInstEnvs -> PredType -> (Coercion,Type)
+normalisePred env (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 (co,ty') = normaliseType env ty
+ in (mkPredCo $ (IParam ipn co), PredTy $ IParam ipn ty')
+normalisePred env (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