--------------------------------
-- Instantiation
tcInstTyVar, tcInstTyVars, tcInstType,
- tcSkolTyVar, tcSkolTyVars, tcSkolType,
+ tcSkolType, tcSkolTyVars, tcInstSigType,
+ tcSkolSigType, tcSkolSigTyVars,
--------------------------------
-- Checking type validity
Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt,
SourceTyCtxt(..), checkValidTheta, checkFreeness,
checkValidInstHead, instTypeErr, checkAmbiguity,
- arityErr, isRigidType,
+ arityErr,
--------------------------------
-- Zonking
-- friends:
import HsSyn ( LHsType )
-import TypeRep ( Type(..), PredType(..), TyNote(..), -- Friend; can see representation
- Kind, ThetaType
+import TypeRep ( Type(..), PredType(..), -- Friend; can see representation
+ ThetaType
)
import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..),
MetaDetails(..), SkolemInfo(..), isMetaTyVar, metaTvRef,
- tcCmpPred, isClassPred,
+ tcCmpPred, tcEqType, isClassPred,
tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
- tcSplitTyConApp_maybe, tcSplitForAllTys,
- tcIsTyVarTy, tcSplitSigmaTy, tcIsTyVarTy,
+ tcValidInstHeadTy, tcSplitForAllTys,
+ tcIsTyVarTy, tcSplitSigmaTy,
isUnLiftedType, isIPPred, isImmutableTyVar,
typeKind, isFlexi, isSkolemTyVar,
mkAppTy, mkTyVarTy, mkTyVarTys,
tyVarsOfPred, getClassPredTys_maybe,
- tyVarsOfType, tyVarsOfTypes,
+ tyVarsOfType, tyVarsOfTypes, tcView,
pprPred, pprTheta, pprClassPred )
-import Kind ( Kind(..), KindVar(..), mkKindVar, isSubKind,
+import Kind ( Kind(..), KindVar, kindVarRef, mkKindVar, isSubKind,
isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
liftedTypeKind, defaultKind
)
import Name ( Name, setNameUnique, mkSysTvName )
import VarSet
import VarEnv
-import CmdLineOpts ( dopt, DynFlag(..) )
-import Util ( nOfThem, isSingleton, equalLength, notNull )
-import ListSetOps ( removeDups )
+import DynFlags ( dopt, DynFlag(..) )
+import UniqSupply ( uniqsFromSupply )
+import Util ( nOfThem, isSingleton, notNull )
+import ListSetOps ( removeDups, findDupsEq )
import SrcLoc ( unLoc )
import Outputable
\end{code}
newTyFlexiVarTys :: Int -> Kind -> TcM [TcType]
newTyFlexiVarTys n kind = mappM newTyFlexiVarTy (nOfThem n kind)
-isRigidType :: TcType -> TcM Bool
--- Check that the type is rigid, *taking the type refinement into account*
--- In other words if a rigid type variable tv is refined to a wobbly type,
--- the answer should be False
--- ToDo: can this happen?
-isRigidType ty
- = do { rigids <- mapM is_rigid (varSetElems (tyVarsOfType ty))
- ; return (and rigids) }
- where
- is_rigid tv = do { details <- lookupTcTyVar tv
- ; case details of
- RigidTv -> return True
- IndirectTv True ty -> isRigidType ty
- other -> return False
- }
-
newKindVar :: TcM TcKind
newKindVar = do { uniq <- newUnique
; ref <- newMutVar Nothing
-- they cannot possibly be captured by
-- any existing for-alls. Hence zipTopTvSubst
-tcInstTyVar tyvar
+tcInstTyVar tyvar -- Freshen the Name of the tyvar
= do { uniq <- newUnique
- ; let name = setNameUnique (tyVarName tyvar) uniq
- -- See Note [TyVarName]
- ; newMetaTyVar name (tyVarKind tyvar) Flexi }
+ ; newMetaTyVar (setNameUnique (tyVarName tyvar) uniq)
+ (tyVarKind tyvar) Flexi }
tcInstType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
-- tcInstType instantiates the outer-level for-alls of a TcType with
-- fresh (mutable) type variables, splits off the dictionary part,
-- and returns the pieces.
-tcInstType ty
- = case tcSplitForAllTys ty of
- ([], rho) -> -- There may be overloading despite no type variables;
- -- (?x :: Int) => Int -> Int
- let
- (theta, tau) = tcSplitPhiTy rho
- in
- returnM ([], theta, tau)
+tcInstType ty = tc_inst_type (mappM tcInstTyVar) ty
- (tyvars, rho) -> tcInstTyVars tyvars `thenM` \ (tyvars', _, tenv) ->
- let
- (theta, tau) = tcSplitPhiTy (substTy tenv rho)
- in
- returnM (tyvars', theta, tau)
---------------------------------------------
--- Similar functions but for skolem constants
+tcInstSigType :: Name -> [Name] -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type with fresh SigSkol variables
+-- See Note [Signature skolems] in TcType.
+--
+-- Tne new type variables have the sane Name as the original *iff* they are scoped.
+-- For scoped tyvars, we don't need a fresh unique, because the renamer has made them
+-- unique, and it's better not to do so because we extend the envt
+-- with them as scoped type variables, and we'd like to avoid spurious
+-- 's = s' bindings in error messages
+--
+-- For non-scoped ones, we *must* instantiate fresh ones:
+--
+-- type T = forall a. [a] -> [a]
+-- f :: T;
+-- f = g where { g :: T; g = <rhs> }
+--
+-- We must not use the same 'a' from the defn of T at both places!!
-tcSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
-tcSkolTyVars info tyvars = mappM (tcSkolTyVar info) tyvars
-
-tcSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
-tcSkolTyVar info tyvar
- = do { uniq <- newUnique
- ; let name = setNameUnique (tyVarName tyvar) uniq
- -- See Note [TyVarName]
- ; return (mkTcTyVar name (tyVarKind tyvar)
- (SkolemTv info)) }
+tcInstSigType id_name scoped_names ty = tc_inst_type (tcInstSigTyVars id_name scoped_names) ty
+tcInstSigTyVars :: Name -> [Name] -> [TyVar] -> TcM [TcTyVar]
+tcInstSigTyVars id_name scoped_names tyvars
+ = mapM new_tv tyvars
+ where
+ new_tv tv
+ = do { let name = tyVarName tv
+ ; ref <- newMutVar Flexi
+ ; name' <- if name `elem` scoped_names
+ then return name
+ else do { uniq <- newUnique; return (setNameUnique name uniq) }
+ ; return (mkTcTyVar name' (tyVarKind tv)
+ (SigSkolTv id_name ref)) }
+
+
+---------------------------------------------
tcSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
-tcSkolType info ty
+-- Instantiate a type with fresh skolem constants
+tcSkolType info ty = tc_inst_type (tcSkolTyVars info) ty
+
+tcSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
+tcSkolTyVars info tyvars
+ = do { us <- newUniqueSupply
+ ; return (zipWith skol_tv tyvars (uniqsFromSupply us)) }
+ where
+ skol_tv tv uniq = mkTcTyVar (setNameUnique (tyVarName tv) uniq)
+ (tyVarKind tv) (SkolemTv info)
+ -- See Note [TyVarName]
+
+
+---------------------------------------------
+tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type signature with skolem constants, but
+-- do *not* give them fresh names, because we want the name to
+-- be in the type environment -- it is lexically scoped.
+tcSkolSigType info ty
+ = tc_inst_type (\tvs -> return (tcSkolSigTyVars info tvs)) ty
+
+tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
+tcSkolSigTyVars info tyvars = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) (SkolemTv info)
+ | tv <- tyvars ]
+
+-----------------------
+tc_inst_type :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
+ -> TcType -- Type to instantiate
+ -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
+tc_inst_type inst_tyvars ty
= case tcSplitForAllTys ty of
- ([], rho) -> let
+ ([], rho) -> let -- There may be overloading despite no type variables;
+ -- (?x :: Int) => Int -> Int
(theta, tau) = tcSplitPhiTy rho
in
- returnM ([], theta, tau)
+ return ([], theta, tau)
- (tyvars, rho) -> tcSkolTyVars info tyvars `thenM` \ tyvars' ->
- let
- tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
- (theta, tau) = tcSplitPhiTy (substTy tenv rho)
- in
- returnM (tyvars', theta, tau)
+ (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
+
+ ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
+ -- Either the tyvars are freshly made, by inst_tyvars,
+ -- or (in the call from tcSkolSigType) any nested foralls
+ -- have different binders. Either way, zipTopTvSubst is ok
+
+ ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
+ ; return (tyvars', theta, tau) }
\end{code}
\begin{code}
data LookupTyVarResult -- The result of a lookupTcTyVar call
- = FlexiTv
- | RigidTv
+ = DoneTv TcTyVarDetails -- Unrefined SkolemTv or virgin MetaTv/SigSkolTv
| IndirectTv Bool TcType
-- True => This is a non-wobbly type refinement,
-- gotten from GADT match unification
lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
-- This function is the ONLY PLACE that we consult the
-- type refinement carried by the monad
---
--- The boolean returned with Indirect
lookupTcTyVar tyvar
- = case tcTyVarDetails tyvar of
+ = let
+ details = tcTyVarDetails tyvar
+ in
+ case details of
+ MetaTv ref -> lookup_wobbly details ref
+
SkolemTv _ -> do { type_reft <- getTypeRefinement
; case lookupVarEnv type_reft tyvar of
Just ty -> return (IndirectTv True ty)
- Nothing -> return RigidTv
- }
- MetaTv ref -> do { details <- readMutVar ref
- ; case details of
- Indirect ty -> return (IndirectTv False ty)
- Flexi -> return FlexiTv
+ Nothing -> return (DoneTv details)
}
+ -- For SigSkolTvs try the refinement, and, failing that
+ -- see if it's been unified to anything. It's a combination
+ -- of SkolemTv and MetaTv
+ SigSkolTv _ ref -> do { type_reft <- getTypeRefinement
+ ; case lookupVarEnv type_reft tyvar of
+ Just ty -> return (IndirectTv True ty)
+ Nothing -> lookup_wobbly details ref
+ }
+
-- Look up a meta type variable, conditionally consulting
-- the current type refinement
condLookupTcTyVar :: Bool -> TcTyVar -> TcM LookupTyVarResult
condLookupTcTyVar use_refinement tyvar
| use_refinement = lookupTcTyVar tyvar
| otherwise
- = case tcTyVarDetails tyvar of
- SkolemTv _ -> return RigidTv
- MetaTv ref -> do { details <- readMutVar ref
- ; case details of
- Indirect ty -> return (IndirectTv False ty)
- Flexi -> return FlexiTv
- }
+ = case details of
+ MetaTv ref -> lookup_wobbly details ref
+ SkolemTv _ -> return (DoneTv details)
+ SigSkolTv _ ref -> lookup_wobbly details ref
+ where
+ details = tcTyVarDetails tyvar
+
+lookup_wobbly :: TcTyVarDetails -> IORef MetaDetails -> TcM LookupTyVarResult
+lookup_wobbly details ref
+ = do { meta_details <- readMutVar ref
+ ; case meta_details of
+ Indirect ty -> return (IndirectTv False ty)
+ Flexi -> return (DoneTv details)
+ }
{-
-- gaw 2004 We aren't shorting anything out anymore, at least for now
\begin{code}
zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
-- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
--- It might be a meta TyVar, in which case we freeze it inot ano ordinary TyVar.
+-- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
-- When we do this, we also default the kind -- see notes with Kind.defaultKind
-- The meta tyvar is updated to point to the new regular TyVar. Now any
-- bound occurences of the original type variable will get zonked to
-- the immutable version.
--
--- We leave skolem TyVars alone; they are imutable.
+-- We leave skolem TyVars alone; they are immutable.
zonkQuantifiedTyVar tv
| isSkolemTyVar tv = return tv
-- It might be a skolem type variable,
go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' ->
returnM (TyConApp tycon tys')
- go (NoteTy (SynNote ty1) ty2) = go ty1 `thenM` \ ty1' ->
- go ty2 `thenM` \ ty2' ->
- returnM (NoteTy (SynNote ty1') ty2')
-
- go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
+ go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations
go (PredTy p) = go_pred p `thenM` \ p' ->
returnM (PredTy p')
-> TcTyVar -> TcM TcType
zonkTyVar unbound_var_fn rflag tyvar
| not (isTcTyVar tyvar) -- When zonking (forall a. ...a...), the occurrences of
- -- the quantified variable a are TyVars not TcTyVars
+ -- the quantified variable 'a' are TyVars not TcTyVars
= returnM (TyVarTy tyvar)
| otherwise
-- If b is true, the variable was refined, and therefore it is okay
-- to continue refining inside. Otherwise it was wobbly and we should
-- not refine further inside.
- IndirectTv b ty -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
- FlexiTv -> unbound_var_fn tyvar -- Unbound flexi
- RigidTv -> return (TyVarTy tyvar) -- Rigid, no zonking necessary
+ IndirectTv b ty -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
+ DoneTv (MetaTv _) -> unbound_var_fn tyvar -- Unbound meta type variable
+ DoneTv other -> return (TyVarTy tyvar) -- Rigid, no zonking necessary
\end{code}
\begin{code}
readKindVar :: KindVar -> TcM (Maybe TcKind)
writeKindVar :: KindVar -> TcKind -> TcM ()
-readKindVar (KVar _ ref) = readMutVar ref
-writeKindVar (KVar _ ref) val = writeMutVar ref (Just val)
+readKindVar kv = readMutVar (kindVarRef kv)
+writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
-------------
zonkTcKind :: TcKind -> TcM TcKind
\begin{code}
data UserTypeCtxt
= FunSigCtxt Name -- Function type signature
+ -- Also used for types in SPECIALISE pragmas
| ExprSigCtxt -- Expression type signature
| ConArgCtxt Name -- Data constructor argument
| TySynCtxt Name -- RHS of a type synonym decl
| ForSigCtxt Name -- Foreign inport or export signature
| RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
| DefaultDeclCtxt -- Types in a default declaration
+ | SpecInstCtxt -- SPECIALISE instance pragma
-- Notes re TySynCtxt
-- We allow type synonyms that aren't types; e.g. type List = []
pprUserTypeCtxt ty (ForSigCtxt n) = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty]
pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)]
+pprUserTypeCtxt ty SpecInstCtxt = sep [ptext SLIT("In a SPECIALISE instance pragma:"), nest 2 (ppr ty)]
pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
\end{code}
-- constructor, hence rank 1
ForSigCtxt _ -> Rank 1
RuleSigCtxt _ -> Rank 1
+ SpecInstCtxt -> Rank 1
actual_kind = typeKind ty
ExprSigCtxt -> isOpenTypeKind actual_kind
GenPatCtxt -> isLiftedTypeKind actual_kind
ForSigCtxt _ -> isLiftedTypeKind actual_kind
- other -> isArgTypeKind actual_kind
+ other -> isArgTypeKind actual_kind
ubx_tup | not gla_exts = UT_NotOk
| otherwise = case ctxt of
check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
-- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
-check_tau_type rank ubx_tup ty@(PredTy _) = pprPanic "check_tau_type" (ppr ty)
+
+-- Naked PredTys don't usually show up, but they can as a result of
+-- {-# SPECIALISE instance Ord Char #-}
+-- The Right Thing would be to fix the way that SPECIALISE instance pragmas
+-- are handled, but the quick thing is just to permit PredTys here.
+check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
+ check_source_ty dflags TypeCtxt sty
check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
check_tau_type rank ubx_tup (AppTy ty1 ty2)
= check_arg_type ty1 `thenM_` check_arg_type ty2
-check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
- -- Synonym notes are built only when the synonym is
- -- saturated (see Type.mkSynTy)
- = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
- (if gla_exts then
- -- If -fglasgow-exts then don't check the 'note' part.
- -- This allows us to instantiate a synonym defn with a
- -- for-all type, or with a partially-applied type synonym.
- -- e.g. type T a b = a
- -- type S m = m ()
- -- f :: S (T Int)
- -- Here, T is partially applied, so it's illegal in H98.
- -- But if you expand S first, then T we get just
- -- f :: Int
- -- which is fine.
- returnM ()
- else
- -- For H98, do check the un-expanded part
- check_tau_type rank ubx_tup syn
- ) `thenM_`
-
- check_tau_type rank ubx_tup ty
-
check_tau_type rank ubx_tup (NoteTy other_note ty)
= check_tau_type rank ubx_tup ty
= -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
-- synonym application, leaving it to checkValidType (i.e. right here)
-- to find the error
- checkTc syn_arity_ok arity_msg `thenM_`
- mappM_ check_arg_type tys
+ do { -- It's OK to have an *over-applied* type synonym
+ -- data Tree a b = ...
+ -- type Foo a = Tree [a]
+ -- f :: Foo a b -> ...
+ ; case tcView ty of
+ Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
+ Nothing -> failWithTc arity_msg
+
+ ; gla_exts <- doptM Opt_GlasgowExts
+ ; if gla_exts then
+ -- If -fglasgow-exts then don't check the type arguments
+ -- This allows us to instantiate a synonym defn with a
+ -- for-all type, or with a partially-applied type synonym.
+ -- e.g. type T a b = a
+ -- type S m = m ()
+ -- f :: S (T Int)
+ -- Here, T is partially applied, so it's illegal in H98.
+ -- But if you expand S first, then T we get just
+ -- f :: Int
+ -- which is fine.
+ returnM ()
+ else
+ -- For H98, do check the type args
+ mappM_ check_arg_type tys
+ }
| isUnboxedTupleTyCon tc
= doptM Opt_GlasgowExts `thenM` \ gla_exts ->
where
ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
- syn_arity_ok = tc_arity <= n_args
- -- It's OK to have an *over-applied* type synonym
- -- data Tree a b = ...
- -- type Foo a = Tree [a]
- -- f :: Foo a b -> ...
n_args = length tys
tc_arity = tyConArity tc
-------------------------
check_class_pred_tys dflags ctxt tys
= case ctxt of
+ TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
InstHeadCtxt -> True -- We check for instance-head
-- formation in checkValidInstHead
- InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys
+ InstThetaCtxt -> undecidable_ok || distinct_tyvars tys
other -> gla_exts || all tyvar_head tys
where
undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
gla_exts = dopt Opt_GlasgowExts dflags
-------------------------
+distinct_tyvars tys -- Check that the types are all distinct type variables
+ = all tcIsTyVarTy tys && null (findDupsEq tcEqType tys)
+
+-------------------------
tyvar_head ty -- Haskell 98 allows predicates of form
| tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
| otherwise -- where a is a type variable
ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
-predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
+predTyVarErr pred = sep [ptext SLIT("Non-type variables, or repeated type variables,"),
+ nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
arityErr kind name n m
| dopt Opt_GlasgowExts dflags
= check_tyvars dflags clas tys
- -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
+ -- WITH HASKELL 98, MUST HAVE C (T a b c)
| isSingleton tys,
- Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
- not (isSynTyCon tycon), -- ...but not a synonym
- all tcIsTyVarTy arg_tys, -- Applied to type variables
- equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
- -- This last condition checks that all the type variables are distinct
+ tcValidInstHeadTy first_ty
= returnM ()
| otherwise
= failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
where
- (first_ty : _) = tys
+ (first_ty : _) = tys
head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
text "where T is not a synonym, and a,b,c are distinct type variables")