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 Maybe
+import FastString
\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")
- | otherwise = panic "FamInstEnv.pprFamInstHdr"
+ 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"
pprFamInsts :: [FamInst] -> SDoc
pprFamInsts finsts = vcat (map pprFamInst finsts)
\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 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
+
+lookupFamInstEnvConflicts envs fam_inst skol_tvs
+ = lookup_fam_inst_env my_unify False 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_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]
- -> [(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
+
+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
+lookup_fam_inst_env match_fun one_sided (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 && one_sided
+
--------------
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
-- to be sure that
add_co co rec_nts ty
- go rec_nts ty = Nothing
+ go _ _ = Nothing
add_co co rec_nts ty
= case go rec_nts ty of
-- No unique matching family instance exists;
-- we do not do anything
- other -> (tycon_coi, TyConApp tc ntys)
+ _ -> (tycon_coi, TyConApp tc ntys)
---------------
normaliseType :: FamInstEnvs -- environment with family instances
-> Type -- old type
normaliseType env ty
| Just ty' <- coreView ty = normaliseType env ty'
-normaliseType env ty@(TyConApp tc tys)
+normaliseType env (TyConApp tc tys)
= normaliseTcApp env tc tys
-normaliseType env ty@(AppTy ty1 ty2)
+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 ty@(FunTy ty1 ty2)
+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 ty@(ForAllTy tyvar ty1)
+normaliseType env (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 _)
+normaliseType _ ty@(TyVarTy _)
= (IdCo,ty)
normaliseType env (PredTy predty)
- = normalisePred env predty
+ = normalisePred env predty
---------------
normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type)