FamInstEnv: Type checked family instance declarations
\begin{code}
-{-# OPTIONS -w #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and fix
--- any warnings in the module. See
--- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
--- for details
-
module FamInstEnv (
FamInst(..), famInstTyCon, famInstTyVars,
pprFamInst, pprFamInstHdr, pprFamInsts,
extendFamInstEnv, extendFamInstEnvList,
famInstEnvElts, familyInstances,
- lookupFamInstEnv, lookupFamInstEnvUnify,
+ lookupFamInstEnv, lookupFamInstEnvConflicts,
-- Normalisation
topNormaliseType
import InstEnv
import Unify
-import TcGadt
-import TcType
import Type
import TypeRep
import TyCon
import VarSet
import Var
import Name
-import OccName
-import SrcLoc
import UniqFM
import Outputable
import Maybes
import Util
+import FastString
import Maybe
\end{code}
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("--") <+> pprNameLoc (getName famInst))
+ 2 (ptext (sLit "--") <+> pprNameLoc (getName famInst))
pprFamInstHdr :: FamInst -> SDoc
pprFamInstHdr (FamInst {fi_fam = fam, fi_tys = tys, fi_tycon = tycon})
= pprTyConSort <+> pprHead
where
- pprHead = pprTypeApp fam (ppr fam) tys
- pprTyConSort | isDataTyCon tycon = ptext SLIT("data instance")
- | isNewTyCon tycon = ptext SLIT("newtype instance")
- | isSynTyCon tycon = ptext SLIT("type instance")
+ 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"
pprFamInsts :: [FamInst] -> SDoc
\begin{code}
type FamInstMatch = (FamInst, [Type]) -- Matching type instance
-
-lookupFamInstEnv :: FamInstEnvs
- -> TyCon -> [Type] -- What we are looking for
- -> [FamInstMatch] -- Successful matches
-lookupFamInstEnv (pkg_ie, home_ie) fam tys
- | not (isOpenTyCon fam)
- = []
- | otherwise
- = home_matches ++ pkg_matches
+ -- See Note [Over-saturated matches]
+
+lookupFamInstEnv
+ :: FamInstEnvs
+ -> TyCon -> [Type] -- What we are looking for
+ -> [FamInstMatch] -- Successful matches
+
+lookupFamInstEnv
+ = lookup_fam_inst_env match
+ 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
+
+lookupFamInstEnvConflicts envs fam_inst skol_tvs
+ = lookup_fam_inst_env my_unify envs fam tys'
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 -> [] -- 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
-
- -- Proper check
- | Just subst <- tcMatchTys tpl_tvs tpl_tys tys
- = (item, substTyVars subst (tyConTyVars tycon)) : find rest
-
- -- No match => try next
- | otherwise
- = find rest
+ 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_rhs = mkTyConApp old_tycon (substTyVars subst (tyConTyVars old_tycon))
+ new_rhs = mkTyConApp inst_tycon (substTyVars subst skol_tvs)
\end{code}
While @lookupFamInstEnv@ uses a one-way match, the next function
indexed synonyms and we don't want to slow that down by needless unification.
\begin{code}
-lookupFamInstEnvUnify :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type]
- -> [(FamInstMatch, TvSubst)]
-lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
+------------------------------------------------------------
+-- 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
+
+lookup_fam_inst_env -- The worker, local to this module
+ :: MatchFun
+ -> FamInstEnvs
+ -> TyCon -> [Type] -- What we are looking for
+ -> [FamInstMatch] -- Successful matches
+lookup_fam_inst_env match_fun (pkg_ie, home_ie) fam tys
| not (isOpenTyCon fam)
= []
| otherwise
- = home_matches ++ pkg_matches
+ = ASSERT( n_tys >= arity ) -- 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
+
--------------
lookup env = case lookupUFM env fam of
Nothing -> [] -- No instances for this class
| 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 bind_fn tpl_tys tys of
- Just subst -> let rep_tys = substTyVars subst (tyConTyVars tycon)
- in
- ((item, rep_tys), subst) : find rest
- Nothing -> 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
--- See explanation at @InstEnv.bind_fn@.
---
-bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
- | otherwise = BindMe
+ -- No match => try next
+ | 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)
+ -> Type
+ -> Maybe (Coercion, Type)
--- Get rid of *outermost* (or toplevel) type functions by rewriting them
+-- 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.
-topNormaliseType env ty
- | Just ty' <- tcView ty = topNormaliseType env ty'
-
-topNormaliseType env ty@(TyConApp tc tys)
- | isOpenTyCon tc
- , (ACo co, ty) <- normaliseType env ty
- = Just (co, ty)
+-- Its a bit like Type.repType, but handles type families too
topNormaliseType env ty
- = Nothing
+ = 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) -- Expand newtypes
+ | Just co_con <- newTyConCo_maybe tc -- See Note [Expanding newtypes]
+ = if tc `elem` rec_nts -- 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
+
+ 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')
-normaliseType :: FamInstEnvs -- environment with family instances
- -> Type -- old type
- -> (CoercionI,Type) -- (coercion,new type), where
- -- co :: old-type ~ new_type
--- Normalise the input type, by eliminating all type-function redexes
-
-normaliseType env ty
- | Just ty' <- coreView ty = normaliseType env ty'
-
-normaliseType env ty@(TyConApp tyCon tys)
- = let -- First normalise the arg types
+---------------
+normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (CoercionI, 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 tyCon ntys cois
+ tycon_coi = mkTyConAppCoI tc ntys cois
in -- Now try the top-level redex
- case lookupFamInstEnv env tyCon ntys of
+ case lookupFamInstEnv env tc ntys of
-- A matching family instance exists
[(fam_inst, tys)] -> (fix_coi, nty)
where
-- No unique matching family instance exists;
-- we do not do anything
- other -> (tycon_coi, TyConApp tyCon ntys)
-
- where
+ _ -> (tycon_coi, TyConApp tc ntys)
+---------------
+normaliseType :: FamInstEnvs -- environment with family instances
+ -> Type -- old type
+ -> (CoercionI, 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
-normaliseType env ty@(AppTy ty1 ty2)
- = let (coi1,nty1) = normaliseType env ty1
- (coi2,nty2) = normaliseType env ty2
- in (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
-normaliseType env ty@(FunTy ty1 ty2)
- = let (coi1,nty1) = normaliseType env ty1
- (coi2,nty2) = normaliseType env ty2
- in (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
-normaliseType env ty@(ForAllTy tyvar ty1)
- = let (coi,nty1) = normaliseType env ty1
- in (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
-normaliseType env ty@(NoteTy note ty1)
- = let (coi,nty1) = normaliseType env ty1
- in (mkNoteTyCoI note coi,NoteTy note nty1)
-normaliseType env ty@(TyVarTy _)
- = (IdCo,ty)
+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 nty1 coi1 nty2 coi2, AppTy 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)
+normaliseType env (ForAllTy tyvar ty1)
+ = let (coi,nty1) = normaliseType env ty1
+ in (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
+normaliseType _ ty@(TyVarTy _)
+ = (IdCo,ty)
normaliseType env (PredTy predty)
- = normalisePred env predty
+ = normalisePred env predty
+---------------
normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type)
normalisePred env (ClassP cls tys)
= let (cois,tys') = mapAndUnzip (normaliseType env) tys