--------------------------------
-- MetaDetails
- TcTyVarDetails(..),
- MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolemTyVar,
- isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, skolemTvInfo, metaTvRef,
- isFlexi, isIndirect,
+ Expected(..), TcRef, TcTyVarDetails(..),
+ MetaDetails(Flexi, Indirect), SkolemInfo(..), pprTcTyVar, pprSkolInfo,
+ isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, metaTvRef,
+ isFlexi, isIndirect,
--------------------------------
-- Builders
- mkPhiTy, mkSigmaTy,
+ mkPhiTy, mkSigmaTy, hoistForAllTys,
--------------------------------
-- Splitters
-- These are important because they do not look through newtypes
+ tcView,
tcSplitForAllTys, tcSplitPhiTy,
tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcSplitSigmaTy,
- tcGetTyVar_maybe, tcGetTyVar,
+ tcValidInstHeadTy, tcGetTyVar_maybe, tcGetTyVar,
---------------------------------
-- Predicates.
-- Again, newtypes are opaque
- tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
+ tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX,
isSigmaTy, isOverloadedTy,
- isDoubleTy, isFloatTy, isIntTy,
+ isDoubleTy, isFloatTy, isIntTy, isStringTy,
isIntegerTy, isAddrTy, isBoolTy, isUnitTy,
isTauTy, tcIsTyVarTy, tcIsForAllTy,
getClassPredTys_maybe, getClassPredTys,
isClassPred, isTyVarClassPred,
mkDictTy, tcSplitPredTy_maybe,
- isPredTy, isDictTy, tcSplitDFunTy, predTyUnique,
+ isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique,
mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName,
+ dataConsStupidTheta,
---------------------------------
-- Foreign import and export
-- Type substitutions
TvSubst(..), -- Representation visible to a few friends
TvSubstEnv, emptyTvSubst,
- mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst,
+ mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
extendTvSubst, extendTvSubstList, isInScope,
- substTy, substTys, substTyWith, substTheta, substTyVar,
+ substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
isUnLiftedType, -- Source types are always lifted
isUnboxedTupleType, -- Ditto
isPrimitiveType,
tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
- tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
- typeKind,
+ tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
+ typeKind, tidyKind,
tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
#include "HsVersions.h"
-- friends:
-import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
+import TypeRep ( Type(..), funTyCon ) -- friend
import Type ( -- Re-exports
tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
tidyTopType, tidyType, tidyPred, tidyTypes,
tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
tidyTyVarBndr, tidyOpenTyVar,
- tidyOpenTyVars,
- isSubKind,
+ tidyOpenTyVars, tidyKind,
+ isSubKind, deShadowTy, tcView,
+
+ tcEqType, tcEqTypes, tcCmpType, tcCmpTypes,
+ tcEqPred, tcCmpPred, tcEqTypeX,
+
TvSubst(..),
TvSubstEnv, emptyTvSubst,
- mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst,
+ mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
extendTvSubst, extendTvSubstList, isInScope,
- substTy, substTys, substTyWith, substTheta, substTyVar,
+ substTy, substTys, substTyWith, substTheta,
+ substTyVar, substTyVarBndr, substPred,
typeKind, repType,
pprKind, pprParendKind,
pprType, pprParendType, pprTyThingCategory,
pprPred, pprTheta, pprThetaArrow, pprClassPred
)
-import TyCon ( TyCon, isUnLiftedTyCon, tyConUnique )
-import DataCon ( DataCon )
+import TyCon ( TyCon, isUnLiftedTyCon, isSynTyCon, tyConUnique )
+import DataCon ( DataCon, dataConStupidTheta, dataConResTys )
import Class ( Class )
-import Var ( TyVar, Id, isTcTyVar, tcTyVarDetails )
+import Var ( TyVar, Id, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )
import ForeignCall ( Safety, playSafe, DNType(..) )
-import VarEnv
+import Unify ( tcMatchTys )
import VarSet
-- others:
-import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
+import DynFlags ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc )
import NameSet
+import VarEnv ( TidyEnv )
import OccName ( OccName, mkDictOcc )
import PrelNames -- Lots (e.g. in isFFIArgumentTy)
import TysWiredIn ( unitTyCon, charTyCon, listTyCon )
import BasicTypes ( IPName(..), ipNameName )
import SrcLoc ( SrcLoc, SrcSpan )
-import Util ( cmpList, thenCmp, snocView )
-import Maybes ( maybeToBool, expectJust )
+import Util ( snocView, equalLength )
+import Maybes ( maybeToBool, expectJust, mapCatMaybes )
+import ListSetOps ( hasNoDups )
+import List ( nubBy )
import Outputable
import DATA_IOREF
\end{code}
type TcTauType = TcType
type TcKind = Kind
type TcTyVarSet = TyVarSet
+
+type TcRef a = IORef a
+data Expected ty = Infer (TcRef ty) -- The hole to fill in for type inference
+ | Check ty -- The type to check during type checking
\end{code}
It's knot-tied back to Var.lhs. There is no reason in principle
why Var.lhs shouldn't actually have the definition, but it "belongs" here.
+Note [Signature skolems]
+~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this
+
+ x :: [a]
+ y :: b
+ (x,y,z) = ([y,z], z, head x)
+
+Here, x and y have type sigs, which go into the environment. We used to
+instantiate their types with skolem constants, and push those types into
+the RHS, so we'd typecheck the RHS with type
+ ( [a*], b*, c )
+where a*, b* are skolem constants, and c is an ordinary meta type varible.
+
+The trouble is that the occurrences of z in the RHS force a* and b* to
+be the *same*, so we can't make them into skolem constants that don't unify
+with each other. Alas.
+
+On the other hand, we *must* use skolems for signature type variables,
+becuase GADT type refinement refines skolems only.
+
+One solution woudl be insist that in the above defn the programmer uses
+the same type variable in both type signatures. But that takes explanation.
+
+The alternative (currently implemented) is to have a special kind of skolem
+constant, SigSkokTv, which can unify with other SigSkolTvs.
+
+
\begin{code}
type TcTyVar = TyVar -- Used only during type inference
-- A TyVarDetails is inside a TyVar
data TcTyVarDetails
- = SkolemTv SkolemInfo -- A skolem constant
- | MetaTv (IORef MetaDetails) -- A meta type variable stands for a tau-type
+ = MetaTv (IORef MetaDetails) -- A meta type variable stands for a tau-type
+ | SkolemTv SkolemInfo -- A skolem constant
+ | SigSkolTv Name (IORef MetaDetails) -- Ditto, but from a type signature;
+ -- see Note [Signature skolems]
+ -- The MetaDetails, if filled in, will
+ -- always be another SigSkolTv
data SkolemInfo
= SigSkol Name -- Bound at a type signature
-- variable for 'a'.
| ArrowSkol SrcSpan -- An arrow form (see TcArrows)
- | GenSkol TcType -- Bound when doing a subsumption check for this type
+ | GenSkol [TcTyVar] -- Bound when doing a subsumption check for
+ TcType -- (forall tvs. ty)
SrcSpan
data MetaDetails
| Indirect TcType -- Type indirections, treated as wobbly
-- for the purpose of GADT unification.
-pprSkolemTyVar :: TcTyVar -> SDoc
-pprSkolemTyVar tv
+tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar)
+-- Tidy the type inside a GenSkol, preparatory to printing it
+tidySkolemTyVar env tv
= ASSERT( isSkolemTyVar tv )
- quotes (ppr tv) <+> ptext SLIT("is bound by") <+> ppr (skolemTvInfo tv)
-
-instance Outputable SkolemInfo where
- ppr (SigSkol id) = ptext SLIT("the type signature for") <+> quotes (ppr id)
- ppr (ClsSkol cls) = ptext SLIT("the class declaration for") <+> quotes (ppr cls)
- ppr (InstSkol df) = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df)
- ppr (ArrowSkol loc) = ptext SLIT("the arrow form at") <+> ppr loc
- ppr (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc),
- nest 2 (ptext SLIT("at") <+> ppr loc)]
- ppr (GenSkol ty loc) = sep [ptext SLIT("the polymorphic type") <+> quotes (ppr ty),
- nest 2 (ptext SLIT("at") <+> ppr loc)]
+ (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)
+ where
+ (env1, info1) = case tcTyVarDetails tv of
+ SkolemTv (GenSkol tvs ty loc) -> (env2, SkolemTv (GenSkol tvs1 ty1 loc))
+ where
+ (env1, tvs1) = tidyOpenTyVars env tvs
+ (env2, ty1) = tidyOpenType env1 ty
+ info -> (env, info)
+
+pprTcTyVar :: TcTyVar -> SDoc
+-- Print tyvar with info about its binding
+pprTcTyVar tv
+ = quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv)
+ where
+ ppr_details (MetaTv _) = ptext SLIT("is a meta type variable")
+ ppr_details (SigSkolTv id _) = ptext SLIT("is bound by") <+> pprSkolInfo (SigSkol id)
+ ppr_details (SkolemTv info) = ptext SLIT("is bound by") <+> pprSkolInfo info
+
+pprSkolInfo :: SkolemInfo -> SDoc
+pprSkolInfo (SigSkol id) = ptext SLIT("the type signature for") <+> quotes (ppr id)
+pprSkolInfo (ClsSkol cls) = ptext SLIT("the class declaration for") <+> quotes (ppr cls)
+pprSkolInfo (InstSkol df) = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df)
+pprSkolInfo (ArrowSkol loc) = ptext SLIT("the arrow form at") <+> ppr loc
+pprSkolInfo (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc),
+ nest 2 (ptext SLIT("at") <+> ppr loc)]
+pprSkolInfo (GenSkol tvs ty loc) = sep [ptext SLIT("the polymorphic type")
+ <+> quotes (ppr (mkForAllTys tvs ty)),
+ nest 2 (ptext SLIT("at") <+> ppr loc)]
instance Outputable MetaDetails where
ppr Flexi = ptext SLIT("Flexi")
isSkolemTyVar tv
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
- SkolemTv _ -> True
- MetaTv _ -> False
+ SkolemTv _ -> True
+ SigSkolTv _ _ -> True
+ MetaTv _ -> False
isExistentialTyVar tv -- Existential type variable, bound by a pattern
= ASSERT( isTcTyVar tv )
isMetaTyVar tv
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
- SkolemTv _ -> False
MetaTv _ -> True
-
-skolemTvInfo :: TyVar -> SkolemInfo
-skolemTvInfo tv
- = ASSERT( isTcTyVar tv )
- case tcTyVarDetails tv of
- SkolemTv info -> info
+ other -> False
metaTvRef :: TyVar -> IORef MetaDetails
metaTvRef tv
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
- MetaTv ref -> ref
+ MetaTv ref -> ref
+ other -> pprPanic "metaTvRef" (ppr tv)
isFlexi, isIndirect :: MetaDetails -> Bool
isFlexi Flexi = True
\begin{code}
isTauTy :: Type -> Bool
+isTauTy ty | Just ty' <- tcView ty = isTauTy ty'
isTauTy (TyVarTy v) = True
isTauTy (TyConApp _ tys) = all isTauTy tys
isTauTy (AppTy a b) = isTauTy a && isTauTy b
isTauTy (FunTy a b) = isTauTy a && isTauTy b
isTauTy (PredTy p) = True -- Don't look through source types
-isTauTy (NoteTy _ ty) = isTauTy ty
isTauTy other = False
\end{code}
\begin{code}
getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
-- construct a dictionary function name
+getDFunTyKey ty | Just ty' <- tcView ty = getDFunTyKey ty'
getDFunTyKey (TyVarTy tv) = getOccName tv
getDFunTyKey (TyConApp tc _) = getOccName tc
getDFunTyKey (AppTy fun _) = getDFunTyKey fun
-getDFunTyKey (NoteTy _ t) = getDFunTyKey t
getDFunTyKey (FunTy arg _) = getOccName funTyCon
getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
tcSplitForAllTys :: Type -> ([TyVar], Type)
tcSplitForAllTys ty = split ty ty []
where
+ split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
- split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
split orig_ty t tvs = (reverse tvs, orig_ty)
+tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
tcIsForAllTy (ForAllTy tv ty) = True
-tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
tcIsForAllTy t = False
tcSplitPhiTy :: Type -> ([PredType], Type)
tcSplitPhiTy ty = split ty ty []
where
+ split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
Just p -> split res res (p:ts)
Nothing -> (reverse ts, orig_ty)
- split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
split orig_ty ty ts = (reverse ts, orig_ty)
tcSplitSigmaTy ty = case tcSplitForAllTys ty of
Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
+tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
-tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
-- Newtypes are opaque, so they may be split
-- However, predicates are not treated
-- as tycon applications by the type checker
-tcSplitTyConApp_maybe other = Nothing
+tcSplitTyConApp_maybe other = Nothing
+
+tcValidInstHeadTy :: Type -> Bool
+-- Used in Haskell-98 mode, for the argument types of an instance head
+-- These must not be type synonyms, but everywhere else type synonyms
+-- are transparent, so we need a special function here
+tcValidInstHeadTy ty
+ = case ty of
+ NoteTy _ ty -> tcValidInstHeadTy ty
+ TyConApp tc tys -> not (isSynTyCon tc) && ok tys
+ FunTy arg res -> ok [arg, res]
+ other -> False
+ where
+ -- Check that all the types are type variables,
+ -- and that each is distinct
+ ok tys = equalLength tvs tys && hasNoDups tvs
+ where
+ tvs = mapCatMaybes get_tv tys
+
+ get_tv (NoteTy _ ty) = get_tv ty -- through synonyms
+ get_tv (TyVarTy tv) = Just tv -- Again, do not look
+ get_tv other = Nothing
tcSplitFunTys :: Type -> ([Type], Type)
tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
(args,res') = tcSplitFunTys res
tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
+tcSplitFunTy_maybe ty | Just ty' <- tcView ty = tcSplitFunTy_maybe ty'
tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
-tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
tcSplitFunTy_maybe other = Nothing
tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
+tcSplitAppTy_maybe ty | Just ty' <- tcView ty = tcSplitAppTy_maybe ty'
tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
-tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
tcSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
Just (tys', ty') -> Just (TyConApp tc tys', ty')
Nothing -> Nothing
Nothing -> (ty,args)
tcGetTyVar_maybe :: Type -> Maybe TyVar
+tcGetTyVar_maybe ty | Just ty' <- tcView ty = tcGetTyVar_maybe ty'
tcGetTyVar_maybe (TyVarTy tv) = Just tv
-tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
tcGetTyVar_maybe other = Nothing
tcGetTyVar :: String -> Type -> TyVar
tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])
-- Split the type of a dictionary function
tcSplitDFunTy ty
- = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
- case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
+ = case tcSplitSigmaTy ty of { (tvs, theta, tau) ->
+ case tcSplitDFunHead tau of { (clas, tys) ->
(tvs, theta, clas, tys) }}
+
+tcSplitDFunHead :: Type -> (Class, [Type])
+tcSplitDFunHead tau
+ = case tcSplitPredTy_maybe tau of
+ Just (ClassP clas tys) -> (clas, tys)
\end{code}
\begin{code}
tcSplitPredTy_maybe :: Type -> Maybe PredType
-- Returns Just for predicates only
-tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
+tcSplitPredTy_maybe ty | Just ty' <- tcView ty = tcSplitPredTy_maybe ty'
tcSplitPredTy_maybe (PredTy p) = Just p
tcSplitPredTy_maybe other = Nothing
mkDictTy clas tys = mkPredTy (ClassP clas tys)
isDictTy :: Type -> Bool
+isDictTy ty | Just ty' <- tcView ty = isDictTy ty'
isDictTy (PredTy p) = isClassPred p
-isDictTy (NoteTy _ ty) = isDictTy ty
isDictTy other = False
\end{code}
isLinearPred other = False
\end{code}
-
-%************************************************************************
-%* *
-\subsection{Comparison}
-%* *
-%************************************************************************
-
-Comparison, taking note of newtypes, predicates, etc,
-
-\begin{code}
-tcEqType :: Type -> Type -> Bool
-tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
-
-tcEqTypes :: [Type] -> [Type] -> Bool
-tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
-
-tcEqPred :: PredType -> PredType -> Bool
-tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
-
--------------
-tcCmpType :: Type -> Type -> Ordering
-tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
-
-tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
-
-tcCmpPred p1 p2 = cmpPredTy emptyVarEnv p1 p2
--------------
-cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
-
--------------
-cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
- -- The "env" maps type variables in ty1 to type variables in ty2
- -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
- -- we in effect substitute tv2 for tv1 in t1 before continuing
-
- -- Look through NoteTy
-cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
-cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
-
- -- Deal with equal constructors
-cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
- Just tv1a -> tv1a `compare` tv2
- Nothing -> tv1 `compare` tv2
-
-cmpTy env (PredTy p1) (PredTy p2) = cmpPredTy env p1 p2
-cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
-cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
-cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
-cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2
-
- -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
-cmpTy env (AppTy _ _) (TyVarTy _) = GT
-
-cmpTy env (FunTy _ _) (TyVarTy _) = GT
-cmpTy env (FunTy _ _) (AppTy _ _) = GT
-
-cmpTy env (TyConApp _ _) (TyVarTy _) = GT
-cmpTy env (TyConApp _ _) (AppTy _ _) = GT
-cmpTy env (TyConApp _ _) (FunTy _ _) = GT
-
-cmpTy env (ForAllTy _ _) (TyVarTy _) = GT
-cmpTy env (ForAllTy _ _) (AppTy _ _) = GT
-cmpTy env (ForAllTy _ _) (FunTy _ _) = GT
-cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
-
-cmpTy env (PredTy _) t2 = GT
-
-cmpTy env _ _ = LT
-\end{code}
-
-\begin{code}
-cmpPredTy :: TyVarEnv TyVar -> PredType -> PredType -> Ordering
-cmpPredTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy 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
-cmpPredTy env (IParam _ _) (ClassP _ _) = LT
-cmpPredTy env (ClassP _ _) (IParam _ _) = GT
-cmpPredTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
-\end{code}
-
-PredTypes are used as a FM key in TcSimplify,
-so we take the easy path and make them an instance of Ord
+--------------------- The stupid theta (sigh) ---------------------------------
\begin{code}
-instance Eq PredType where { (==) = tcEqPred }
-instance Ord PredType where { compare = tcCmpPred }
+dataConsStupidTheta :: [DataCon] -> ThetaType
+-- Union the stupid thetas from all the specified constructors (non-empty)
+-- All the constructors should have the same result type, modulo alpha conversion
+-- The resulting ThetaType uses type variables from the *first* constructor in the list
+--
+-- It's here because it's used in MkId.mkRecordSelId, and in TcExpr
+dataConsStupidTheta (con1:cons)
+ = nubBy tcEqPred all_preds
+ where
+ all_preds = dataConStupidTheta con1 ++ other_stupids
+ res_tys1 = dataConResTys con1
+ tvs1 = tyVarsOfTypes res_tys1
+ other_stupids = [ substPred subst pred
+ | con <- cons
+ , let Just subst = tcMatchTys tvs1 res_tys1 (dataConResTys con)
+ , pred <- dataConStupidTheta con ]
\end{code}
\begin{code}
isSigmaTy :: Type -> Bool
+isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty'
isSigmaTy (ForAllTy tyvar ty) = True
isSigmaTy (FunTy a b) = isPredTy a
-isSigmaTy (NoteTy n ty) = isSigmaTy ty
isSigmaTy _ = False
isOverloadedTy :: Type -> Bool
+isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty'
isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
isOverloadedTy (FunTy a b) = isPredTy a
-isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
isOverloadedTy _ = False
isPredTy :: Type -> Bool -- Belongs in TcType because it does
-- not look through newtypes, or predtypes (of course)
-isPredTy (NoteTy _ ty) = isPredTy ty
+isPredTy ty | Just ty' <- tcView ty = isPredTy ty'
isPredTy (PredTy sty) = True
isPredTy _ = False
\end{code}
\end{code}
+
+
+%************************************************************************
+%* *
+ Hoisting for-alls
+%* *
+%************************************************************************
+
+hoistForAllTys is used for user-written type signatures only
+We want to 'look through' type synonyms when doing this
+so it's better done on the Type than the HsType
+
+It moves all the foralls and constraints to the top
+e.g. T -> forall a. a ==> forall a. T -> a
+ T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int
+
+Also: it eliminates duplicate constraints. These can show up
+when hoisting constraints, notably implicit parameters.
+
+It tries hard to retain type synonyms if hoisting does not break one
+up. Not only does this improve error messages, but there's a tricky
+interaction with Haskell 98. H98 requires no unsaturated type
+synonyms, which is checked by checkValidType. This runs after
+hoisting, so we don't want hoisting to remove the SynNotes! (We can't
+run validity checking before hoisting because in mutually-recursive
+type definitions we postpone validity checking until after the knot is
+tied.)
+
+\begin{code}
+hoistForAllTys :: Type -> Type
+hoistForAllTys ty
+ = go ty
+
+ where
+ go :: Type -> Type
+
+ go (TyVarTy tv) = TyVarTy tv
+ go ty@(TyConApp tc tys)
+ | isSynTyCon tc, any isSigmaTy tys'
+ = go (expectJust "hoistForAllTys" (tcView ty))
+ -- Revolting special case. If a type synonym has foralls
+ -- at the top of its argument, then expanding the type synonym
+ -- might lead to more hositing. So we just abandon the synonym
+ -- altogether right here.
+ -- Note that we must go back to hoistForAllTys, because
+ -- expanding the type synonym may expose new binders. Yuk.
+ | otherwise
+ = TyConApp tc tys'
+ where
+ tys' = map go tys
+ go (PredTy pred) = PredTy pred -- No nested foralls
+ go (NoteTy _ ty2) = go ty2 -- Discard the free tyvar note
+ go (FunTy arg res) = mk_fun_ty (go arg) (go res)
+ go (AppTy fun arg) = AppTy (go fun) (go arg)
+ go (ForAllTy tv ty) = ForAllTy tv (go ty)
+
+ -- mk_fun_ty does all the work.
+ -- It's building t1 -> t2:
+ -- if t2 is a for-all type, push t1 inside it
+ -- if t2 is (pred -> t3), check for duplicates
+ mk_fun_ty ty1 ty2
+ | not (isSigmaTy ty2) -- No forall's, or context =>
+ = FunTy ty1 ty2
+ | PredTy p1 <- ty1 -- ty1 is a predicate
+ = if p1 `elem` theta2 then -- so check for duplicates
+ ty2
+ else
+ mkSigmaTy tvs2 (p1:theta2) tau2
+ | otherwise
+ = mkSigmaTy tvs2 theta2 (FunTy ty1 tau2)
+ where
+ (tvs2, theta2, tau2) = tcSplitSigmaTy $
+ deShadowTy (tyVarsOfType ty1) $
+ deNoteType ty2
+
+ -- deShadowTy is important. For example:
+ -- type Foo r = forall a. a -> r
+ -- foo :: Foo (Foo ())
+ -- Here the hoisting should give
+ -- foo :: forall a a1. a -> a1 -> ()
+
+ -- deNoteType is important too, so that the deShadow sees that
+ -- synonym expanded! Sigh
+\end{code}
+
+
%************************************************************************
%* *
\subsection{Misc}
\begin{code}
deNoteType :: Type -> Type
- -- Remove synonyms, but not predicate types
-deNoteType ty@(TyVarTy tyvar) = ty
-deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
-deNoteType (PredTy p) = PredTy (deNotePredType p)
-deNoteType (NoteTy _ ty) = deNoteType ty
-deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
-deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
-deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
-
-deNotePredType :: PredType -> PredType
-deNotePredType (ClassP c tys) = ClassP c (map deNoteType tys)
-deNotePredType (IParam n ty) = IParam n (deNoteType ty)
+-- Remove *outermost* type synonyms and other notes
+deNoteType ty | Just ty' <- tcView ty = deNoteType ty'
+deNoteType ty = ty
\end{code}
Find the free tycons and classes of a type. This is used in the front
tyClsNamesOfType :: Type -> NameSet
tyClsNamesOfType (TyVarTy tv) = emptyNameSet
tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
-tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
-tyClsNamesOfType (NoteTy other_note ty2) = tyClsNamesOfType ty2
-tyClsNamesOfType (PredTy (IParam n ty)) = tyClsNamesOfType ty
-tyClsNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
+tyClsNamesOfType (NoteTy _ ty2) = tyClsNamesOfType ty2
+tyClsNamesOfType (PredTy (IParam n ty)) = tyClsNamesOfType ty
+tyClsNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
tyClsNamesOfType (FunTy arg res) = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
tyClsNamesOfType (AppTy fun arg) = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
tyClsNamesOfType (ForAllTy tyvar ty) = tyClsNamesOfType ty