unsafeCoercionTyCon, symCoercionTyCon,
transCoercionTyCon, leftCoercionTyCon,
- rightCoercionTyCon, instCoercionTyCon -- needed by TysWiredIn
+ rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
+
+ -- CoercionI
+ CoercionI(..),
+ isIdentityCoercion,
+ mkSymCoI, mkTransCoI,
+ mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
+ mkNoteTyCoI, mkForAllTyCoI,
+ fromCoI,
+ mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI,
+
) where
#include "HsVersions.h"
import TypeRep
import Type
import TyCon
+import Class
import Var
import Name
import OccName
co_con = maybe (pprPanic "splitNewTypeRepCo_maybe" (ppr tc)) id (newTyConCo_maybe tc)
splitNewTypeRepCo_maybe other = Nothing
\end{code}
+
+
+--------------------------------------
+-- CoercionI smart constructors
+-- lifted smart constructors of ordinary coercions
+
+
+\begin{code}
+
+ -- CoercionI is either
+ -- (a) proper coercion
+ -- (b) the identity coercion
+data CoercionI = IdCo | ACo Coercion
+
+isIdentityCoercion :: CoercionI -> Bool
+isIdentityCoercion IdCo = True
+isIdentityCoercion _ = False
+
+mkSymCoI :: CoercionI -> CoercionI
+mkSymCoI IdCo = IdCo
+mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co]
+ -- the smart constructor
+ -- is too smart with tyvars
+
+mkTransCoI :: CoercionI -> CoercionI -> CoercionI
+mkTransCoI IdCo aco = aco
+mkTransCoI aco IdCo = aco
+mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2
+
+mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
+mkTyConAppCoI tyCon tys cois =
+ let (anyAcon,co_args) = f tys cois
+ in if anyAcon
+ then ACo (TyConApp tyCon co_args)
+ else IdCo
+ where
+ f [] [] = (False,[])
+ f (x:xs) (y:ys) =
+ let (b,cos) = f xs ys
+ in case y of
+ IdCo -> (b,x:cos)
+ ACo co -> (True,co:cos)
+
+mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
+mkAppTyCoI ty1 IdCo ty2 IdCo = IdCo
+mkAppTyCoI ty1 coi1 ty2 coi2 =
+ ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
+
+mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
+mkFunTyCoI ty1 IdCo ty2 IdCo = IdCo
+mkFunTyCoI ty1 coi1 ty2 coi2 =
+ ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
+
+mkNoteTyCoI :: TyNote -> CoercionI -> CoercionI
+mkNoteTyCoI _ IdCo = IdCo
+mkNoteTyCoI note (ACo co) = ACo $ NoteTy note co
+
+mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
+mkForAllTyCoI _ IdCo = IdCo
+mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co
+
+fromCoI IdCo ty = ty
+fromCoI (ACo co) ty = co
+
+mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
+mkClassPPredCoI cls tys cois =
+ let (anyAcon,co_args) = f tys cois
+ in if anyAcon
+ then ACo $ PredTy $ ClassP cls co_args
+ else IdCo
+ where
+ f [] [] = (False,[])
+ f (x:xs) (y:ys) =
+ let (b,cos) = f xs ys
+ in case y of
+ IdCo -> (b,x:cos)
+ ACo co -> (True,co:cos)
+
+mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI
+mkIParamPredCoI ipn IdCo = IdCo
+mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co
+
+mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
+mkEqPredCoI _ IdCo _ IdCo = IdCo
+mkEqPredCoI ty1 IdCo _ (ACo co2) = ACo $ PredTy $ EqPred ty1 co2
+mkEqPredCoI ty1 (ACo co1) ty2 coi2 = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)
+
+\end{code}
+
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}
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}
projects / ghc-hetmet.git / commitdiff