--------------------------------
-- 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
import VarSet
import VarEnv
import CmdLineOpts ( dopt, DynFlag(..) )
+import UniqSupply ( uniqsFromSupply )
import Util ( nOfThem, isSingleton, equalLength, notNull )
import ListSetOps ( removeDups )
import SrcLoc ( unLoc )
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
| 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 (NewTcApp tycon tys) = mappM go tys `thenM` \ tys' ->
- returnM (NewTcApp tycon tys')
-
go (NoteTy (SynNote ty1) ty2) = go ty1 `thenM` \ ty1' ->
go ty2 `thenM` \ ty2' ->
returnM (NoteTy (SynNote ty1') ty2')
-> Bool -- Consult the type refinement?
-> TcTyVar -> TcM TcType
zonkTyVar unbound_var_fn rflag tyvar
- | not (isTcTyVar tyvar) -- This can happen when
- -- zonking a forall type, when the bound type variable
- -- needn't be mutable
+ | not (isTcTyVar tyvar) -- When zonking (forall a. ...a...), the occurrences of
+ -- 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}
-- Rank is allowed rank for function args
-- No foralls otherwise
-check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
-check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
- check_source_ty dflags TypeCtxt sty
+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
+
+-- 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_poly_type rank UT_NotOk arg_ty `thenM_`
check_tau_type rank ubx_tup (NoteTy other_note ty)
= check_tau_type rank ubx_tup ty
-check_tau_type rank ubx_tup (NewTcApp tc tys)
- = mappM_ check_arg_type tys
-
check_tau_type rank ubx_tup ty@(TyConApp tc tys)
| isSynTyCon tc
= -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
ubx_tup_msg = ubxArgTyErr ty
----------------------------------------
-forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr ty
+forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
projects / ghc-hetmet.git / blobdiff