\begin{code}
module Type (
-- re-exports from TypeRep
- TyThing(..), Type, PredType(..), ThetaType, TyVarSubst,
+ TyThing(..), Type, PredType(..), ThetaType,
funTyCon,
-- Re-exports from Kind
mkAppTy, mkAppTys, splitAppTy, splitAppTys, splitAppTy_maybe,
- mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe, splitFunTys,
+ mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
+ splitFunTys, splitFunTysN,
funResultTy, funArgTy, zipFunTys, isFunTy,
mkGenTyConApp, mkTyConApp, mkTyConTy,
mkSynTy,
- repType, typePrimRep,
+ repType, typePrimRep, coreView, deepCoreView,
mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys,
applyTy, applyTys, isForAllTy, dropForAlls,
tidyTopType, tidyPred,
-- Comparison
- eqType,
+ coreEqType, tcEqType, tcEqTypes, tcCmpType, tcCmpTypes,
+ tcEqPred, tcCmpPred, tcEqTypeX,
-- Seq
seqType, seqTypes,
+ -- Type substitutions
+ TvSubst(..), -- Representation visible to a few friends
+ TvSubstEnv, emptyTvSubst,
+ mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst,
+ getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
+ extendTvSubst, extendTvSubstList, isInScope,
+
+ -- Performing substitution on types
+ substTy, substTys, substTyWith, substTheta, substTyVar,
+ deShadowTy,
+
-- Pretty-printing
- pprType, pprParendType,
+ pprType, pprParendType, pprTyThingCategory,
pprPred, pprTheta, pprThetaArrow, pprClassPred
) where
import TypeRep
--- Other imports:
-
-import {-# SOURCE #-} Subst ( substTyWith )
-
-- friends:
import Kind
-import Var ( TyVar, tyVarKind, tyVarName, setTyVarName )
+import Var ( Var, TyVar, tyVarKind, tyVarName, setTyVarName )
import VarEnv
import VarSet
import TyCon ( TyCon, isRecursiveTyCon, isPrimTyCon,
isUnboxedTupleTyCon, isUnLiftedTyCon,
isFunTyCon, isNewTyCon, newTyConRep, newTyConRhs,
- isAlgTyCon, isSynTyCon, tyConArity,
+ isAlgTyCon, isSynTyCon, tyConArity, newTyConRhs_maybe,
tyConKind, getSynTyConDefn, PrimRep(..), tyConPrimRep,
)
import CmdLineOpts ( opt_DictsStrict )
import SrcLoc ( noSrcLoc )
import Unique ( Uniquable(..) )
-import Util ( mapAccumL, seqList, lengthIs, snocView )
+import Util ( mapAccumL, seqList, lengthIs, snocView, thenCmp, isEqual )
import Outputable
import UniqSet ( sizeUniqSet ) -- Should come via VarSet
import Maybe ( isJust )
%************************************************************************
%* *
+ Type representation
+%* *
+%************************************************************************
+
+In Core, we "look through" non-recursive newtypes and PredTypes.
+
+\begin{code}
+{-# INLINE coreView #-}
+coreView :: Type -> Maybe Type
+-- Srips off the *top layer only* of a type to give
+-- its underlying representation type.
+-- Returns Nothing if there is nothing to look through.
+--
+-- By being non-recursive and inlined, this case analysis gets efficiently
+-- joined onto the case analysis that the caller is already doing
+coreView (NoteTy _ ty) = Just ty
+coreView (PredTy p) = Just (predTypeRep p)
+coreView (TyConApp tc tys) = expandNewTcApp tc tys
+coreView ty = Nothing
+
+deepCoreView :: Type -> Type
+-- Apply coreView recursively
+deepCoreView ty
+ | Just ty' <- coreView ty = deepCoreView ty'
+deepCoreView (TyVarTy tv) = TyVarTy tv
+deepCoreView (TyConApp tc tys) = TyConApp tc (map deepCoreView tys)
+deepCoreView (AppTy t1 t2) = AppTy (deepCoreView t1) (deepCoreView t2)
+deepCoreView (FunTy t1 t2) = FunTy (deepCoreView t1) (deepCoreView t2)
+deepCoreView (ForAllTy tv ty) = ForAllTy tv (deepCoreView ty)
+ -- No NoteTy, no PredTy
+
+expandNewTcApp :: TyCon -> [Type] -> Maybe Type
+-- A local helper function (not exported)
+-- Expands *the outermoset level of* a newtype application to
+-- *either* a vanilla TyConApp (recursive newtype, or non-saturated)
+-- *or* the newtype representation (otherwise), meaning the
+-- type written in the RHS of the newtype decl,
+-- which may itself be a newtype
+--
+-- Example: newtype R = MkR S
+-- newtype S = MkS T
+-- newtype T = MkT (T -> T)
+-- expandNewTcApp on R gives Just S
+-- on S gives Just T
+-- on T gives Nothing (no expansion)
+
+expandNewTcApp tc tys = case newTyConRhs_maybe tc tys of
+ Nothing -> Nothing
+ Just (tenv, rhs) -> Just (substTy (mkTopTvSubst tenv) rhs)
+\end{code}
+
+
+%************************************************************************
+%* *
\subsection{Constructor-specific functions}
%* *
%************************************************************************
isTyVarTy ty = isJust (getTyVar_maybe ty)
getTyVar_maybe :: Type -> Maybe TyVar
-getTyVar_maybe (TyVarTy tv) = Just tv
-getTyVar_maybe (NoteTy _ t) = getTyVar_maybe t
-getTyVar_maybe (PredTy p) = getTyVar_maybe (predTypeRep p)
-getTyVar_maybe (NewTcApp tc tys) = getTyVar_maybe (newTypeRep tc tys)
-getTyVar_maybe other = Nothing
+getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
+getTyVar_maybe (TyVarTy tv) = Just tv
+getTyVar_maybe other = Nothing
\end{code}
= mk_app orig_ty1
where
mk_app (NoteTy _ ty1) = mk_app ty1
- mk_app (NewTcApp tc tys) = NewTcApp tc (tys ++ [orig_ty2])
mk_app (TyConApp tc tys) = mkGenTyConApp tc (tys ++ [orig_ty2])
mk_app ty1 = AppTy orig_ty1 orig_ty2
-- We call mkGenTyConApp because the TyConApp could be an
= mk_app orig_ty1
where
mk_app (NoteTy _ ty1) = mk_app ty1
- mk_app (NewTcApp tc tys) = NewTcApp tc (tys ++ orig_tys2)
- mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ orig_tys2)
- -- Use mkTyConApp in case tc is (->)
+ mk_app (TyConApp tc tys) = mkGenTyConApp tc (tys ++ orig_tys2)
+ -- mkGenTyConApp: see notes with mkAppTy
mk_app ty1 = foldl AppTy orig_ty1 orig_tys2
splitAppTy_maybe :: Type -> Maybe (Type, Type)
+splitAppTy_maybe ty | Just ty' <- coreView ty = splitAppTy_maybe ty'
splitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
splitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
-splitAppTy_maybe (NoteTy _ ty) = splitAppTy_maybe ty
-splitAppTy_maybe (PredTy p) = splitAppTy_maybe (predTypeRep p)
-splitAppTy_maybe (NewTcApp tc tys) = splitAppTy_maybe (newTypeRep tc tys)
splitAppTy_maybe (TyConApp tc tys) = case snocView tys of
- Nothing -> Nothing
- Just (tys',ty') -> Just (mkGenTyConApp tc tys', ty')
- -- mkGenTyConApp just in case the tc is a newtype
-
+ Nothing -> Nothing
+ Just (tys',ty') -> Just (TyConApp tc tys', ty')
splitAppTy_maybe other = Nothing
splitAppTy :: Type -> (Type, Type)
splitAppTys :: Type -> (Type, [Type])
splitAppTys ty = split ty ty []
where
+ split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
split orig_ty (AppTy ty arg) args = split ty ty (arg:args)
- split orig_ty (NoteTy _ ty) args = split orig_ty ty args
- split orig_ty (PredTy p) args = split orig_ty (predTypeRep p) args
- split orig_ty (NewTcApp tc tc_args) args = split orig_ty (newTypeRep tc tc_args) args
- split orig_ty (TyConApp tc tc_args) args = (mkGenTyConApp tc [], tc_args ++ args)
- -- mkGenTyConApp just in case the tc is a newtype
+ split orig_ty (TyConApp tc tc_args) args = (TyConApp tc [], tc_args ++ args)
split orig_ty (FunTy ty1 ty2) args = ASSERT( null args )
(TyConApp funTyCon [], [ty1,ty2])
split orig_ty ty args = (orig_ty, args)
isFunTy ty = isJust (splitFunTy_maybe ty)
splitFunTy :: Type -> (Type, Type)
+splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
splitFunTy (FunTy arg res) = (arg, res)
-splitFunTy (NoteTy _ ty) = splitFunTy ty
-splitFunTy (PredTy p) = splitFunTy (predTypeRep p)
-splitFunTy (NewTcApp tc tys) = splitFunTy (newTypeRep tc tys)
splitFunTy other = pprPanic "splitFunTy" (ppr other)
splitFunTy_maybe :: Type -> Maybe (Type, Type)
+splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
splitFunTy_maybe (FunTy arg res) = Just (arg, res)
-splitFunTy_maybe (NoteTy _ ty) = splitFunTy_maybe ty
-splitFunTy_maybe (PredTy p) = splitFunTy_maybe (predTypeRep p)
-splitFunTy_maybe (NewTcApp tc tys) = splitFunTy_maybe (newTypeRep tc tys)
splitFunTy_maybe other = Nothing
splitFunTys :: Type -> ([Type], Type)
splitFunTys ty = split [] ty ty
where
+ split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
split args orig_ty (FunTy arg res) = split (arg:args) res res
- split args orig_ty (NoteTy _ ty) = split args orig_ty ty
- split args orig_ty (PredTy p) = split args orig_ty (predTypeRep p)
- split args orig_ty (NewTcApp tc tys) = split args orig_ty (newTypeRep tc tys)
split args orig_ty ty = (reverse args, orig_ty)
+splitFunTysN :: Int -> Type -> ([Type], Type)
+-- Split off exactly n arg tys
+splitFunTysN 0 ty = ([], ty)
+splitFunTysN n ty = case splitFunTy ty of { (arg, res) ->
+ case splitFunTysN (n-1) res of { (args, res) ->
+ (arg:args, res) }}
+
zipFunTys :: Outputable a => [a] -> Type -> ([(a,Type)], Type)
zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
where
split acc [] nty ty = (reverse acc, nty)
+ split acc xs nty ty
+ | Just ty' <- coreView ty = split acc xs nty ty'
split acc (x:xs) nty (FunTy arg res) = split ((x,arg):acc) xs res res
- split acc xs nty (NoteTy _ ty) = split acc xs nty ty
- split acc xs nty (PredTy p) = split acc xs nty (predTypeRep p)
- split acc xs nty (NewTcApp tc tys) = split acc xs nty (newTypeRep tc tys)
split acc (x:xs) nty ty = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
funResultTy :: Type -> Type
+funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
funResultTy (FunTy arg res) = res
-funResultTy (NoteTy _ ty) = funResultTy ty
-funResultTy (PredTy p) = funResultTy (predTypeRep p)
-funResultTy (NewTcApp tc tys) = funResultTy (newTypeRep tc tys)
funResultTy ty = pprPanic "funResultTy" (ppr ty)
funArgTy :: Type -> Type
+funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
funArgTy (FunTy arg res) = arg
-funArgTy (NoteTy _ ty) = funArgTy ty
-funArgTy (PredTy p) = funArgTy (predTypeRep p)
-funArgTy (NewTcApp tc tys) = funArgTy (newTypeRep tc tys)
funArgTy ty = pprPanic "funArgTy" (ppr ty)
\end{code}
| isFunTyCon tycon, [ty1,ty2] <- tys
= FunTy ty1 ty2
- | isNewTyCon tycon
- = NewTcApp tycon tys
-
| otherwise
= ASSERT(not (isSynTyCon tycon))
TyConApp tycon tys
Nothing -> pprPanic "splitTyConApp" (ppr ty)
splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
+splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
splitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
-splitTyConApp_maybe (NoteTy _ ty) = splitTyConApp_maybe ty
-splitTyConApp_maybe (PredTy p) = splitTyConApp_maybe (predTypeRep p)
-splitTyConApp_maybe (NewTcApp tc tys) = splitTyConApp_maybe (newTypeRep tc tys)
splitTyConApp_maybe other = Nothing
\end{code}
(b) synonyms
(c) predicates
(d) usage annotations
- (e) [recursive] newtypes
+ (e) all newtypes, including recursive ones
It's useful in the back end.
\begin{code}
repType (ForAllTy _ ty) = repType ty
repType (NoteTy _ ty) = repType ty
repType (PredTy p) = repType (predTypeRep p)
-repType (NewTcApp tc tys) = ASSERT( tys `lengthIs` tyConArity tc )
+repType (TyConApp tc tys)
+ | isNewTyCon tc = ASSERT( tys `lengthIs` tyConArity tc )
repType (new_type_rep tc tys)
repType ty = ty
-
-- ToDo: this could be moved to the code generator, using splitTyConApp instead
-- of inspecting the type directly.
typePrimRep :: Type -> PrimRep
splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
splitForAllTy_maybe ty = splitFAT_m ty
where
- splitFAT_m (NoteTy _ ty) = splitFAT_m ty
- splitFAT_m (PredTy p) = splitFAT_m (predTypeRep p)
- splitFAT_m (NewTcApp tc tys) = splitFAT_m (newTypeRep tc tys)
- splitFAT_m (ForAllTy tyvar ty) = Just(tyvar, ty)
- splitFAT_m _ = Nothing
+ splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
+ splitFAT_m (ForAllTy tyvar ty) = Just(tyvar, ty)
+ splitFAT_m _ = Nothing
splitForAllTys :: Type -> ([TyVar], Type)
splitForAllTys ty = split ty ty []
where
+ split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
- split orig_ty (NoteTy _ ty) tvs = split orig_ty ty tvs
- split orig_ty (PredTy p) tvs = split orig_ty (predTypeRep p) tvs
- split orig_ty (NewTcApp tc tys) tvs = split orig_ty (newTypeRep tc tys) tvs
split orig_ty t tvs = (reverse tvs, orig_ty)
dropForAlls :: Type -> Type
\begin{code}
applyTy :: Type -> Type -> Type
-applyTy (PredTy p) arg = applyTy (predTypeRep p) arg
-applyTy (NewTcApp tc tys) arg = applyTy (newTypeRep tc tys) arg
-applyTy (NoteTy _ fun) arg = applyTy fun arg
-applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
-applyTy other arg = panic "applyTy"
+applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
+applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
+applyTy other arg = panic "applyTy"
applyTys :: Type -> [Type] -> Type
-- This function is interesting because
-- Convert a PredType to its "representation type";
-- the post-type-checking type used by all the Core passes of GHC.
-- Unwraps only the outermost level; for example, the result might
--- be a NewTcApp; c.f. newTypeRep
+-- be a newtype application
predTypeRep (IParam _ ty) = ty
predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
- -- Result might be a NewTcApp, but the consumer will
+ -- Result might be a newtype application, but the consumer will
-- look through that too if necessary
\end{code}
\begin{code}
splitRecNewType_maybe :: Type -> Maybe Type
--- Newtypes are always represented by a NewTcApp
-- Sometimes we want to look through a recursive newtype, and that's what happens here
-- It only strips *one layer* off, so the caller will usually call itself recursively
-- Only applied to types of kind *, hence the newtype is always saturated
-splitRecNewType_maybe (NoteTy _ ty) = splitRecNewType_maybe ty
-splitRecNewType_maybe (PredTy p) = splitRecNewType_maybe (predTypeRep p)
-splitRecNewType_maybe (NewTcApp tc tys)
- | isRecursiveTyCon tc
- = ASSERT( tys `lengthIs` tyConArity tc && isNewTyCon tc )
- -- The assert should hold because splitRecNewType_maybe
- -- should only be applied to *types* (of kind *)
- Just (new_type_rhs tc tys)
+splitRecNewType_maybe ty | Just ty' <- coreView ty = splitRecNewType_maybe ty'
+splitRecNewType_maybe (TyConApp tc tys)
+ | isNewTyCon tc
+ = ASSERT( tys `lengthIs` tyConArity tc ) -- splitRecNewType_maybe only be applied
+ -- to *types* (of kind *)
+ ASSERT( isRecursiveTyCon tc ) -- Guaranteed by coreView
+ case newTyConRhs tc of
+ (tvs, rep_ty) -> Just (substTyWith tvs tys rep_ty)
+
splitRecNewType_maybe other = Nothing
-
------------------------------
-newTypeRep :: TyCon -> [Type] -> Type
--- A local helper function (not exported)
--- Expands *the outermoset level of* a newtype application to
--- *either* a vanilla TyConApp (recursive newtype, or non-saturated)
--- *or* the newtype representation (otherwise), meaning the
--- type written in the RHS of the newtype decl,
--- which may itself be a newtype
---
--- Example: newtype R = MkR S
--- newtype S = MkS T
--- newtype T = MkT (T -> T)
--- newTypeRep on R gives NewTcApp S
--- on S gives NewTcApp T
--- on T gives TyConApp T
---
--- NB: the returned TyConApp is always deconstructed immediately by the
--- caller... a TyConApp with a newtype type constructor never lives
--- in an ordinary type
-newTypeRep tc tys
- | not (isRecursiveTyCon tc), -- Not recursive and saturated
- tys `lengthIs` tyConArity tc -- treat as equivalent to expansion
- = new_type_rhs tc tys
- | otherwise
- = TyConApp tc tys
- -- ToDo: Consider caching this substitution in a NType
-
--- new_type_rhs doesn't ask any questions:
--- it just expands newtype one level, whether recursive or not
-new_type_rhs tc tys
- = case newTyConRhs tc of
- (tvs, rep_ty) -> substTyWith tvs tys rep_ty
\end{code}
typeKind (TyVarTy tyvar) = tyVarKind tyvar
typeKind (TyConApp tycon tys) = foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys
-typeKind (NewTcApp tycon tys) = foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys
typeKind (NoteTy _ ty) = typeKind ty
typeKind (PredTy _) = liftedTypeKind -- Predicates are always
-- represented by lifted types
tyVarsOfType :: Type -> TyVarSet
tyVarsOfType (TyVarTy tv) = unitVarSet tv
tyVarsOfType (TyConApp tycon tys) = tyVarsOfTypes tys
-tyVarsOfType (NewTcApp tycon tys) = tyVarsOfTypes tys
tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs
tyVarsOfType (NoteTy (SynNote ty1) ty2) = tyVarsOfType ty2 -- See note [Syn] below
tyVarsOfType (PredTy sty) = tyVarsOfPred sty
Just tv' -> TyVarTy tv'
go (TyConApp tycon tys) = let args = map go tys
in args `seqList` TyConApp tycon args
- go (NewTcApp tycon tys) = let args = map go tys
- in args `seqList` NewTcApp tycon args
go (NoteTy note ty) = (NoteTy $! (go_note note)) $! (go ty)
go (PredTy sty) = PredTy (tidyPred env sty)
go (AppTy fun arg) = (AppTy $! (go fun)) $! (go arg)
-- They are pretty bogus types, mind you. It would be better never to
-- construct them
+isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
isUnLiftedType (ForAllTy tv ty) = isUnLiftedType ty
-isUnLiftedType (NoteTy _ ty) = isUnLiftedType ty
isUnLiftedType (TyConApp tc _) = isUnLiftedTyCon tc
-isUnLiftedType (PredTy _) = False -- All source types are lifted
-isUnLiftedType (NewTcApp tc tys) = isUnLiftedType (newTypeRep tc tys)
isUnLiftedType other = False
isUnboxedTupleType :: Type -> Bool
which is below TcType in the hierarchy, so it's convenient to put it here.
\begin{code}
+isStrictType (PredTy pred) = isStrictPred pred
+isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
isStrictType (ForAllTy tv ty) = isStrictType ty
-isStrictType (NoteTy _ ty) = isStrictType ty
isStrictType (TyConApp tc _) = isUnLiftedTyCon tc
-isStrictType (NewTcApp tc tys) = isStrictType (newTypeRep tc tys)
-isStrictType (PredTy pred) = isStrictPred pred
isStrictType other = False
isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
seqType (NoteTy note t2) = seqNote note `seq` seqType t2
seqType (PredTy p) = seqPred p
seqType (TyConApp tc tys) = tc `seq` seqTypes tys
-seqType (NewTcApp tc tys) = tc `seq` seqTypes tys
seqType (ForAllTy tv ty) = tv `seq` seqType ty
seqTypes :: [Type] -> ()
%************************************************************************
%* *
-\subsection{Equality on types}
+ Comparison of types
+ (We don't use instances so that we know where it happens)
%* *
%************************************************************************
-Comparison; don't use instances so that we know where it happens.
-Look through newtypes but not usage types.
+Two flavours:
+
+* tcEqType, tcCmpType do *not* look through newtypes, PredTypes
+* coreEqType *does* look through them
Note that eqType can respond 'False' for partial applications of newtypes.
Consider
newtype Parser m a = MkParser (Foogle m a)
-
Does
Monad (Parser m) `eqType` Monad (Foogle m)
-
Well, yes, but eqType won't see that they are the same.
I don't think this is harmful, but it's soemthing to watch out for.
+First, the external interface
+
+\begin{code}
+coreEqType :: Type -> Type -> Bool
+coreEqType t1 t2 = isEqual $ cmpType (deepCoreView t1) (deepCoreView t2)
+
+tcEqType :: Type -> Type -> Bool
+tcEqType t1 t2 = isEqual $ cmpType t1 t2
+
+tcEqTypes :: [Type] -> [Type] -> Bool
+tcEqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
+
+tcCmpType :: Type -> Type -> Ordering
+tcCmpType t1 t2 = cmpType t1 t2
+
+tcCmpTypes :: [Type] -> [Type] -> Ordering
+tcCmpTypes tys1 tys2 = cmpTypes tys1 tys2
+
+tcEqPred :: PredType -> PredType -> Bool
+tcEqPred p1 p2 = isEqual $ cmpPred p1 p2
+
+tcCmpPred :: PredType -> PredType -> Ordering
+tcCmpPred p1 p2 = cmpPred p1 p2
+
+tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool
+tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
+\end{code}
+
+Now here comes the real worker
+
\begin{code}
-eqType t1 t2 = eq_ty emptyVarEnv t1 t2
+cmpType :: Type -> Type -> Ordering
+cmpType t1 t2 = cmpTypeX rn_env t1 t2
+ where
+ rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
--- Look through Notes
-eq_ty env (NoteTy _ t1) t2 = eq_ty env t1 t2
-eq_ty env t1 (NoteTy _ t2) = eq_ty env t1 t2
+cmpTypes :: [Type] -> [Type] -> Ordering
+cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
+ where
+ rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
--- Look through PredTy and NewTcApp. This is where the looping danger comes from.
--- We don't bother to check for the PredType/PredType case, no good reason
--- Hmm: maybe there is a good reason: see the notes below about newtypes
-eq_ty env (PredTy sty1) t2 = eq_ty env (predTypeRep sty1) t2
-eq_ty env t1 (PredTy sty2) = eq_ty env t1 (predTypeRep sty2)
+cmpPred :: PredType -> PredType -> Ordering
+cmpPred p1 p2 = cmpPredX rn_env p1 p2
+ where
+ rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
+
+cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse
-- NB: we *cannot* short-cut the newtype comparison thus:
--- eq_ty env (NewTcApp tc1 tys1) (NewTcApp tc2 tys2)
--- | (tc1 == tc2) = (eq_tys env tys1 tys2)
+-- eqTypeX env (NewTcApp tc1 tys1) (NewTcApp tc2 tys2)
+-- | (tc1 == tc2) = (eqTypeXs env tys1 tys2)
--
-- Consider:
-- newtype T a = MkT [a]
-- but we can only expand saturated newtypes, so just comparing
-- T with [] won't do.
-eq_ty env (NewTcApp tc1 tys1) t2 = eq_ty env (newTypeRep tc1 tys1) t2
-eq_ty env t1 (NewTcApp tc2 tys2) = eq_ty env t1 (newTypeRep tc2 tys2)
-
--- The rest is plain sailing
-eq_ty env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
- Just tv1a -> tv1a == tv2
- Nothing -> tv1 == tv2
-eq_ty env (ForAllTy tv1 t1) (ForAllTy tv2 t2)
- | tv1 == tv2 = eq_ty (delVarEnv env tv1) t1 t2
- | otherwise = eq_ty (extendVarEnv env tv1 tv2) t1 t2
-eq_ty env (AppTy s1 t1) (AppTy s2 t2) = (eq_ty env s1 s2) && (eq_ty env t1 t2)
-eq_ty env (FunTy s1 t1) (FunTy s2 t2) = (eq_ty env s1 s2) && (eq_ty env t1 t2)
-eq_ty env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 == tc2) && (eq_tys env tys1 tys2)
-eq_ty env t1 t2 = False
-
-eq_tys env [] [] = True
-eq_tys env (t1:tys1) (t2:tys2) = (eq_ty env t1 t2) && (eq_tys env tys1 tys2)
-eq_tys env tys1 tys2 = False
+cmpTypeX env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 `compare` rnOccR env tv2
+cmpTypeX env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
+cmpTypeX env (AppTy s1 t1) (AppTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
+cmpTypeX env (FunTy s1 t1) (FunTy s2 t2) = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
+cmpTypeX env (PredTy p1) (PredTy p2) = cmpPredX env p1 p2
+cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
+cmpTypeX env (NoteTy _ t1) t2 = cmpTypeX env t1 t2
+cmpTypeX env t1 (NoteTy _ t2) = cmpTypeX env t1 t2
+
+ -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
+cmpTypeX env (AppTy _ _) (TyVarTy _) = GT
+
+cmpTypeX env (FunTy _ _) (TyVarTy _) = GT
+cmpTypeX env (FunTy _ _) (AppTy _ _) = GT
+
+cmpTypeX env (TyConApp _ _) (TyVarTy _) = GT
+cmpTypeX env (TyConApp _ _) (AppTy _ _) = GT
+cmpTypeX env (TyConApp _ _) (FunTy _ _) = GT
+
+cmpTypeX env (ForAllTy _ _) (TyVarTy _) = GT
+cmpTypeX env (ForAllTy _ _) (AppTy _ _) = GT
+cmpTypeX env (ForAllTy _ _) (FunTy _ _) = GT
+cmpTypeX env (ForAllTy _ _) (TyConApp _ _) = GT
+
+cmpTypeX env (PredTy _) t2 = GT
+
+cmpTypeX env _ _ = LT
+
+-------------
+cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
+cmpTypesX env [] [] = EQ
+cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
+cmpTypesX env [] tys = LT
+cmpTypesX env ty [] = GT
+
+-------------
+cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering
+cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2
+ -- Compare types as well as names for implicit parameters
+ -- This comparison is used exclusively (I think) for the
+ -- finite map built in TcSimplify
+cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` cmpTypesX env tys1 tys2
+cmpPredX env (IParam _ _) (ClassP _ _) = LT
+cmpPredX env (ClassP _ _) (IParam _ _) = GT
+\end{code}
+
+PredTypes are used as a FM key in TcSimplify,
+so we take the easy path and make them an instance of Ord
+
+\begin{code}
+instance Eq PredType where { (==) = tcEqPred }
+instance Ord PredType where { compare = tcCmpPred }
+\end{code}
+
+
+%************************************************************************
+%* *
+ Type substitutions
+%* *
+%************************************************************************
+
+\begin{code}
+data TvSubst
+ = TvSubst InScopeSet -- The in-scope type variables
+ TvSubstEnv -- The substitution itself; guaranteed idempotent
+ -- See Note [Apply Once]
+
+{- ----------------------------------------------------------
+ Note [Apply Once]
+
+We use TvSubsts to instantiate things, and we might instantiate
+ forall a b. ty
+\with the types
+ [a, b], or [b, a].
+So the substition might go [a->b, b->a]. A similar situation arises in Core
+when we find a beta redex like
+ (/\ a /\ b -> e) b a
+Then we also end up with a substition that permutes type variables. Other
+variations happen to; for example [a -> (a, b)].
+
+ ***************************************************
+ *** So a TvSubst must be applied precisely once ***
+ ***************************************************
+
+A TvSubst is not idempotent, but, unlike the non-idempotent substitution
+we use during unifications, it must not be repeatedly applied.
+-------------------------------------------------------------- -}
+
+
+type TvSubstEnv = TyVarEnv Type
+ -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
+ -- invariant discussed in Note [Apply Once]), and also independently
+ -- in the middle of matching, and unification (see Types.Unify)
+ -- So you have to look at the context to know if it's idempotent or
+ -- apply-once or whatever
+
+emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
+isEmptyTvSubst :: TvSubst -> Bool
+isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env
+
+getTvSubstEnv :: TvSubst -> TvSubstEnv
+getTvSubstEnv (TvSubst _ env) = env
+
+getTvInScope :: TvSubst -> InScopeSet
+getTvInScope (TvSubst in_scope _) = in_scope
+
+isInScope :: Var -> TvSubst -> Bool
+isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
+
+setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
+setTvSubstEnv (TvSubst in_scope _) env = TvSubst in_scope env
+
+extendTvInScope :: TvSubst -> [Var] -> TvSubst
+extendTvInScope (TvSubst in_scope env) vars = TvSubst (extendInScopeSetList in_scope vars) env
+
+extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
+extendTvSubst (TvSubst in_scope env) tv ty = TvSubst in_scope (extendVarEnv env tv ty)
+
+extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
+extendTvSubstList (TvSubst in_scope env) tvs tys
+ = TvSubst in_scope (extendVarEnvList env (tvs `zip` tys))
+
+-- mkTvSubst and zipTvSubst generate the in-scope set from
+-- the types given; but it's just a thunk so with a bit of luck
+-- it'll never be evaluated
+
+mkTvSubst :: TvSubstEnv -> TvSubst
+mkTvSubst env
+ = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts env))) env
+
+zipTvSubst :: [TyVar] -> [Type] -> TvSubst
+zipTvSubst tyvars tys
+ = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
+
+-- mkTopTvSubst is called when doing top-level substitutions.
+-- Here we expect that the free vars of the range of the
+-- substitution will be empty.
+mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
+mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
+
+zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
+zipTopTvSubst tyvars tys = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
+
+zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
+zipTyEnv tyvars tys
+#ifdef DEBUG
+ | length tyvars /= length tys
+ = pprTrace "mkTopTvSubst" (ppr tyvars $$ ppr tys) emptyVarEnv
+ | otherwise
+#endif
+ = zip_ty_env tyvars tys emptyVarEnv
+
+-- Later substitutions in the list over-ride earlier ones,
+-- but there should be no loops
+zip_ty_env [] [] env = env
+zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
+ -- There used to be a special case for when
+ -- ty == TyVarTy tv
+ -- (a not-uncommon case) in which case the substitution was dropped.
+ -- But the type-tidier changes the print-name of a type variable without
+ -- changing the unique, and that led to a bug. Why? Pre-tidying, we had
+ -- a type {Foo t}, where Foo is a one-method class. So Foo is really a newtype.
+ -- And it happened that t was the type variable of the class. Post-tiding,
+ -- it got turned into {Foo t2}. The ext-core printer expanded this using
+ -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
+ -- and so generated a rep type mentioning t not t2.
+ --
+ -- Simplest fix is to nuke the "optimisation"
+
+instance Outputable TvSubst where
+ ppr (TvSubst ins env)
+ = sep[ ptext SLIT("<TvSubst"),
+ nest 2 (ptext SLIT("In scope:") <+> ppr ins),
+ nest 2 (ptext SLIT("Env:") <+> ppr env) ]
\end{code}
+%************************************************************************
+%* *
+ Performing type substitutions
+%* *
+%************************************************************************
+
+\begin{code}
+substTyWith :: [TyVar] -> [Type] -> Type -> Type
+substTyWith tvs tys = substTy (zipTvSubst tvs tys)
+
+substTy :: TvSubst -> Type -> Type
+substTy subst ty | isEmptyTvSubst subst = ty
+ | otherwise = subst_ty subst ty
+
+substTys :: TvSubst -> [Type] -> [Type]
+substTys subst tys | isEmptyTvSubst subst = tys
+ | otherwise = map (subst_ty subst) tys
+
+deShadowTy :: Type -> Type -- Remove any shadowing from the type
+deShadowTy ty = subst_ty emptyTvSubst ty
+
+substTheta :: TvSubst -> ThetaType -> ThetaType
+substTheta subst theta
+ | isEmptyTvSubst subst = theta
+ | otherwise = map (substPred subst) theta
+
+substPred :: TvSubst -> PredType -> PredType
+substPred subst (IParam n ty) = IParam n (subst_ty subst ty)
+substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
+
+-- Note that the in_scope set is poked only if we hit a forall
+-- so it may often never be fully computed
+subst_ty subst@(TvSubst in_scope env) ty
+ = go ty
+ where
+ go ty@(TyVarTy tv) = case (lookupVarEnv env tv) of
+ Nothing -> ty
+ Just ty' -> ty' -- See Note [Apply Once]
+
+ go (TyConApp tc tys) = let args = map go tys
+ in args `seqList` TyConApp tc args
+
+ go (PredTy p) = PredTy $! (substPred subst p)
+
+ go (NoteTy (SynNote ty1) ty2) = NoteTy (SynNote $! (go ty1)) $! (go ty2)
+ go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard the free tyvar note
+
+ go (FunTy arg res) = (FunTy $! (go arg)) $! (go res)
+ go (AppTy fun arg) = mkAppTy (go fun) $! (go arg)
+ -- The mkAppTy smart constructor is important
+ -- we might be replacing (a Int), represented with App
+ -- by [Int], represented with TyConApp
+ go (ForAllTy tv ty) = case substTyVar subst tv of
+ (subst', tv') -> ForAllTy tv' $! (subst_ty subst' ty)
+
+substTyVar :: TvSubst -> TyVar -> (TvSubst, TyVar)
+substTyVar subst@(TvSubst in_scope env) old_var
+ | old_var == new_var -- No need to clone
+ -- But we *must* zap any current substitution for the variable.
+ -- For example:
+ -- (\x.e) with id_subst = [x |-> e']
+ -- Here we must simply zap the substitution for x
+ --
+ -- The new_id isn't cloned, but it may have a different type
+ -- etc, so we must return it, not the old id
+ = (TvSubst (in_scope `extendInScopeSet` new_var) (delVarEnv env old_var),
+ new_var)
+
+ | otherwise -- The new binder is in scope so
+ -- we'd better rename it away from the in-scope variables
+ -- Extending the substitution to do this renaming also
+ -- has the (correct) effect of discarding any existing
+ -- substitution for that variable
+ = (TvSubst (in_scope `extendInScopeSet` new_var) (extendVarEnv env old_var (TyVarTy new_var)),
+ new_var)
+ where
+ new_var = uniqAway in_scope old_var
+ -- The uniqAway part makes sure the new variable is not already in scope
+\end{code}
+
+