--------------------------------
-- MetaDetails
Expected(..), TcRef, TcTyVarDetails(..),
- MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolemTyVar,
- isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, skolemTvInfo, metaTvRef,
- isFlexi, isIndirect,
+ MetaDetails(Flexi, Indirect), SkolemInfo(..), pprTcTyVar, pprSkolInfo,
+ isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, metaTvRef,
+ isFlexi, isIndirect,
--------------------------------
-- Builders
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, tcEqTypeX,
isSigmaTy, isOverloadedTy,
- isDoubleTy, isFloatTy, isIntTy,
+ isDoubleTy, isFloatTy, isIntTy, isStringTy,
isIntegerTy, isAddrTy, isBoolTy, isUnitTy,
isTauTy, tcIsTyVarTy, tcIsForAllTy,
mkDictTy, tcSplitPredTy_maybe,
isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique,
mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName,
+ dataConsStupidTheta,
---------------------------------
-- Foreign import and export
tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
- typeKind,
+ typeKind, tidyKind,
tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
tidyTopType, tidyType, tidyPred, tidyTypes,
tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
tidyTyVarBndr, tidyOpenTyVar,
- tidyOpenTyVars,
+ tidyOpenTyVars, tidyKind,
isSubKind, deShadowTy,
tcEqType, tcEqTypes, tcCmpType, tcCmpTypes,
mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
extendTvSubst, extendTvSubstList, isInScope,
- substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
+ 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, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )
import ForeignCall ( Safety, playSafe, DNType(..) )
+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 TysWiredIn ( unitTyCon, charTyCon, listTyCon )
import BasicTypes ( IPName(..), ipNameName )
import SrcLoc ( SrcLoc, SrcSpan )
-import Util ( 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}
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
-- Tidy the type inside a GenSkol, preparatory to printing it
tidySkolemTyVar env tv
= ASSERT( isSkolemTyVar tv )
- (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) (SkolemTv info1))
+ (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)
where
- (env1, info1) = case skolemTvInfo tv of
- GenSkol tvs ty loc -> (env2, GenSkol tvs1 ty1 loc)
+ (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)
-pprSkolemTyVar :: TcTyVar -> SDoc
-pprSkolemTyVar 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 tvs ty loc) = sep [ptext SLIT("the polymorphic type")
- <+> quotes (ppr (mkForAllTys tvs ty)),
- nest 2 (ptext SLIT("at") <+> ppr loc)]
+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
-- as tycon applications by the type checker
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
+ TyConApp tc tys -> ASSERT( not (isSynTyCon tc) ) ok tys
+ -- A synonym would be a NoteTy
+ FunTy arg res -> ok [arg, res]
+ NoteTy (SynNote _) _ -> False
+ NoteTy other_note ty -> tcValidInstHeadTy ty
+ 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 (TyVarTy tv) = Just tv -- Again, do not look
+ get_tv (NoteTy (SynNote _) _) = Nothing -- through synonyms
+ get_tv (NoteTy other_note ty) = get_tv ty
+ get_tv other = Nothing
+
tcSplitFunTys :: Type -> ([Type], Type)
tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
Nothing -> ([], ty)
isLinearPred other = False
\end{code}
+--------------------- The stupid theta (sigh) ---------------------------------
+
+\begin{code}
+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}
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 (NoteTy _ ty) = deNoteType ty
+deNoteType ty = ty
\end{code}
Find the free tycons and classes of a type. This is used in the front
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 (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