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
)
-- others:
import TcRnMonad -- TcType, amongst others
import FunDeps ( grow )
-import Name ( Name, setNameUnique, mkSysTvName, mkSystemName, getOccName )
+import Name ( Name, setNameUnique, mkSysTvName )
import VarSet
import VarEnv
-import CmdLineOpts ( dopt, DynFlag(..) )
+import DynFlags ( dopt, DynFlag(..) )
import UniqSupply ( uniqsFromSupply )
-import Util ( nOfThem, isSingleton, equalLength, notNull )
-import ListSetOps ( removeDups )
+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 -- Use the OccName of the tyvar we are instantiating
- -- but make a System Name, so that it's updated in
- -- preference to a tcInstSigTyVar
+tcInstTyVar tyvar -- Freshen the Name of the tyvar
= do { uniq <- newUnique
- ; newMetaTyVar (mkSystemName uniq (getOccName tyvar))
+ ; newMetaTyVar (setNameUnique (tyVarName tyvar) uniq)
(tyVarKind tyvar) Flexi }
tcInstType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
---------------------------------------------
-tcInstSigType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
--- Instantiate a type with fresh meta type variables, but
--- ones which have the same Name as the original type
--- variable. This is used for type signatures, where we must
--- instantiate with meta type variables, but we'd like to avoid
--- instantiating them were possible; and the unifier unifies
--- tyvars with System Names by preference
+tcInstSigType :: Name -> [Name] -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type with fresh SigSkol variables
+-- See Note [Signature skolems] in TcType.
--
--- We don't need a fresh unique, because the renamer has made them
+-- 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
-tcInstSigType ty = tc_inst_type tcInstSigTyVars ty
+--
+-- 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!!
+
+tcInstSigType id_name scoped_names ty = tc_inst_type (tcInstSigTyVars id_name scoped_names) ty
-tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
-tcInstSigTyVars tyvars
+tcInstSigTyVars :: Name -> [Name] -> [TyVar] -> TcM [TcTyVar]
+tcInstSigTyVars id_name scoped_names tyvars
= mapM new_tv tyvars
where
- new_tv tv = newMetaTyVar (tyVarName tv) (tyVarKind tv) Flexi
+ 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)) }
---------------------------------------------
\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
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')
-- 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 (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")
projects / ghc-hetmet.git / blobdiff