extendFamInstEnv, extendFamInstEnvList,
famInstEnvElts, familyInstances,
- lookupFamInstEnv, lookupFamInstEnvUnify
+ lookupFamInstEnv, lookupFamInstEnvUnify,
+
+ -- Normalisation
+ toplevelNormaliseFamInst
) where
#include "HsVersions.h"
import TcGadt
import TcType
import Type
+import TypeRep
import TyCon
+import Coercion
import VarSet
import Var
import Name
import SrcLoc
import UniqFM
import Outputable
+import Maybes
+import Util
import Maybe
\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
}
pprFamInst :: FamInst -> SDoc
pprFamInst famInst
= hang (pprFamInstHdr famInst)
- 2 (ptext SLIT("--") <+> (pprDefnLoc (getSrcLoc famInst)))
+ 2 (ptext SLIT("--") <+> (pprDefnLoc (getSrcSpan famInst)))
pprFamInstHdr :: FamInst -> SDoc
pprFamInstHdr (FamInst {fi_fam = fam, fi_tys = tys, fi_tycon = tycon})
= pprTyConSort <+> pprHead
where
- pprHead = parenSymOcc (getOccName fam) (ppr fam) <+>
- sep (map pprParendType tys)
+ pprHead = pprTypeApp (parenSymOcc (getOccName fam) (ppr fam)) tys
pprTyConSort | isDataTyCon tycon = ptext SLIT("data instance")
| isNewTyCon tycon = ptext SLIT("newtype instance")
| isSynTyCon tycon = ptext SLIT("type 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).
+@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}
-{- 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
+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 -> 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
+ data instance T [a] = ..
- --------------
- 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
+desugared to
- -- No match => try next
- | otherwise
- = find rest
--}
-\end{code}
+ data :R42T a = ..
+ coe :Co:R42T a :: T [a] ~ :R42T a
-@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 instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
\begin{code}
+type FamInstMatch = (FamInst, [Type]) -- Matching type instance
+
lookupFamInstEnv :: FamInstEnvs
-> TyCon -> [Type] -- What we are looking for
- -> [(TvSubst, FamInst)] -- Successful matches
+ -> [FamInstMatch] -- Successful matches
lookupFamInstEnv (pkg_ie, home_ie) fam tys
= home_matches ++ pkg_matches
where
-- Proper check
| Just subst <- tcMatchTys tpl_tvs tpl_tys tys
- = (subst, item) : find rest
+ = (item, substTyVars subst (tyConTyVars tycon)) : find rest
-- No match => try next
| otherwise
\begin{code}
lookupFamInstEnvUnify :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type]
- -> [(TvSubst, FamInst)]
+ -> [(FamInstMatch)]
lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
= home_matches ++ pkg_matches
where
-- 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
+ Just subst -> let rep_tys = substTyVars subst (tyConTyVars tycon)
+ in
+ (item, rep_tys) : find rest
Nothing -> find rest
-- See explanation at @InstEnv.bind_fn@.
bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
| otherwise = BindMe
\end{code}
+
+--------------------------------------
+-- Normalisation
+
+\begin{code}
+ -- get rid of TOPLEVEL type functions by rewriting them
+ -- i.e. treating their equations as a TRS
+toplevelNormaliseFamInst :: FamInstEnvs ->
+ Type ->
+ (CoercionI,Type)
+toplevelNormaliseFamInst env ty
+ | Just ty' <- tcView ty = normaliseFamInst env ty'
+toplevelNormaliseFamInst env ty@(TyConApp tyCon tys)
+ | isOpenTyCon tyCon
+ = normaliseFamInst env ty
+toplevelNormaliseFamInst env ty
+ = (IdCo,ty)
+
+
+ -- get rid of ALL type functions by rewriting them
+ -- i.e. treating their equations as a TRS
+normaliseFamInst :: FamInstEnvs -> -- environment with family instances
+ Type -> -- old type
+ (CoercionI,Type) -- (coercion,new type)
+normaliseFamInst env ty
+ | Just ty' <- tcView ty = normaliseFamInst env ty'
+normaliseFamInst env ty@(TyConApp tyCon tys) =
+ let (cois,ntys) = mapAndUnzip (normaliseFamInst env) tys
+ tycon_coi = mkTyConAppCoI tyCon ntys cois
+ maybe_ty_co = lookupFamInst env tyCon ntys
+ in case maybe_ty_co of
+ -- a matching family instance exists
+ Just (ty',co) ->
+ let first_coi = mkTransCoI tycon_coi (ACo co)
+ (rest_coi,nty) = normaliseFamInst env ty'
+ fix_coi = mkTransCoI first_coi rest_coi
+ in (fix_coi,nty)
+ -- no matching family instance exists
+ -- we do not do anything
+ Nothing ->
+ (tycon_coi,TyConApp tyCon ntys)
+normaliseFamInst env ty@(AppTy ty1 ty2) =
+ let (coi1,nty1) = normaliseFamInst env ty1
+ (coi2,nty2) = normaliseFamInst env ty2
+ in (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
+normaliseFamInst env ty@(FunTy ty1 ty2) =
+ let (coi1,nty1) = normaliseFamInst env ty1
+ (coi2,nty2) = normaliseFamInst env ty2
+ in (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
+normaliseFamInst env ty@(ForAllTy tyvar ty1) =
+ let (coi,nty1) = normaliseFamInst env ty1
+ in (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
+normaliseFamInst env ty@(NoteTy note ty1) =
+ let (coi,nty1) = normaliseFamInst env ty1
+ in (mkNoteTyCoI note coi,NoteTy note nty1)
+normaliseFamInst env ty@(TyVarTy _) =
+ (IdCo,ty)
+normaliseFamInst env (PredTy predty) =
+ normaliseFamInstPred env predty
+
+normaliseFamInstPred :: FamInstEnvs -> PredType -> (CoercionI,Type)
+normaliseFamInstPred env (ClassP cls tys) =
+ let (cois,tys') = mapAndUnzip (normaliseFamInst env) tys
+ in (mkClassPPredCoI cls tys' cois, PredTy $ ClassP cls tys')
+normaliseFamInstPred env (IParam ipn ty) =
+ let (coi,ty') = normaliseFamInst env ty
+ in (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
+normaliseFamInstPred env (EqPred ty1 ty2) =
+ let (coi1,ty1') = normaliseFamInst env ty1
+ (coi2,ty2') = normaliseFamInst env ty2
+ in (mkEqPredCoI ty1' coi1 ty2' coi2, PredTy $ EqPred ty1' ty2')
+
+lookupFamInst :: FamInstEnvs -> TyCon -> [Type] -> Maybe (Type,Coercion)
+
+-- (lookupFamInst F tys) looks for a top-level instance
+-- co : forall a. F tys' = G a
+-- (The rhs is always of form G a; see Note [The FamInst structure]
+-- in FamInst.)
+-- where we can instantiate 'a' with t to make tys'[t/a] = tys
+-- Hence (co t) : F tys ~ G t
+-- Then we return (Just (G t, co t))
+
+lookupFamInst env tycon tys
+ | not (isOpenTyCon tycon) -- Dead code; fix.
+ = Nothing
+ | otherwise
+ = case lookupFamInstEnv env tycon tys of
+ [(subst, fam_inst)] ->
+ Just (mkTyConApp rep_tc substituted_vars, mkTyConApp coercion_tycon substituted_vars)
+ where -- NB: invariant of lookupFamInstEnv is that (tyConTyVars rep_tc)
+ -- is in the domain of the substitution
+ rep_tc = famInstTyCon fam_inst
+ coercion_tycon = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
+ substituted_vars = substTyVars subst (tyConTyVars rep_tc)
+ other -> Nothing
+\end{code}