-- Kind checking
kcHsTyVars, kcHsSigType, kcHsLiftedSigType,
- kcCheckHsType, kcHsContext, kcHsType,
+ kcCheckHsType, kcHsContext, kcHsType,
-- Typechecking kinded types
- tcHsKindedContext, tcHsKindedType, tcTyVarBndrs, dsHsType,
+ tcHsKindedContext, tcHsKindedType, tcHsBangType,
+ tcTyVarBndrs, dsHsType, tcLHsConSig, tcDataKindSig,
- tcAddScopedTyVars,
+ tcHsPatSigType, tcAddLetBoundTyVars,
- TcSigInfo(..), tcTySig, mkTcSig, maybeSig
+ TcSigInfo(..), TcSigFun, lookupSig
) where
#include "HsVersions.h"
-import HsSyn ( HsType(..), LHsType, HsTyVarBndr(..), LHsTyVarBndr,
- LHsContext, Sig(..), LSig, HsPred(..), LHsPred )
+import HsSyn ( HsType(..), LHsType, HsTyVarBndr(..), LHsTyVarBndr, HsBang,
+ LHsContext, HsPred(..), LHsPred, LHsBinds,
+ getBangStrictness, collectSigTysFromHsBinds )
import RnHsSyn ( extractHsTyVars )
-import TcHsSyn ( TcId )
-
import TcRnMonad
import TcEnv ( tcExtendTyVarEnv, tcExtendKindEnv,
tcLookup, tcLookupClass, tcLookupTyCon,
- TyThing(..), TcTyThing(..),
- getInLocalScope, wrongThingErr
+ TyThing(..), getInLocalScope, wrongThingErr
)
-import TcMType ( newKindVar, tcInstType, newMutTyVar,
- zonkTcKindToKind,
+import TcMType ( newKindVar, newMetaTyVar, zonkTcKindToKind,
checkValidType, UserTypeCtxt(..), pprHsSigCtxt
)
import TcUnify ( unifyFunKind, checkExpectedKind )
-import TcType ( Type, PredType(..), ThetaType, TyVarDetails(..),
- TcTyVar, TcKind, TcThetaType, TcTauType,
- mkTyVarTy, mkTyVarTys, mkFunTy,
- mkForAllTys, mkFunTys, tcEqType, isPredTy,
+import TcType ( Type, PredType(..), ThetaType,
+ MetaDetails(Flexi), hoistForAllTys,
+ TcType, TcTyVar, TcKind, TcThetaType, TcTauType,
+ mkFunTy,
mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys,
- tcSplitFunTy_maybe, tcSplitForAllTys )
-import Kind ( liftedTypeKind, ubxTupleKind, openTypeKind, argTypeKind )
-import Inst ( Inst, InstOrigin(..), newMethod, instToId )
-
-import Id ( mkLocalId, idName, idType )
-import Var ( TyVar, mkTyVar, tyVarKind )
+ typeKind )
+import Kind ( Kind, isLiftedTypeKind, liftedTypeKind, ubxTupleKind,
+ openTypeKind, argTypeKind, splitKindFunTys )
+import Id ( idName )
+import Var ( TyVar, mkTyVar )
import TyCon ( TyCon, tyConKind )
import Class ( Class, classTyCon )
-import Name ( Name )
+import Name ( Name, mkInternalName )
+import OccName ( mkOccName, tvName )
import NameSet
import PrelNames ( genUnitTyConName )
-import Subst ( deShadowTy )
import TysWiredIn ( mkListTy, mkPArrTy, mkTupleTy )
+import Bag ( bagToList )
import BasicTypes ( Boxity(..) )
-import SrcLoc ( SrcSpan, Located(..), unLoc, noLoc )
+import SrcLoc ( Located(..), unLoc, noLoc, srcSpanStart )
+import UniqSupply ( uniqsFromSupply )
import Outputable
-import List ( nubBy )
\end{code}
\begin{code}
tcHsSigType :: UserTypeCtxt -> LHsType Name -> TcM Type
-- Do kind checking, and hoist for-alls to the top
+ -- NB: it's important that the foralls that come from the top-level
+ -- HsForAllTy in hs_ty occur *first* in the returned type.
+ -- See Note [Scoped] with TcSigInfo
tcHsSigType ctxt hs_ty
= addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
do { kinded_ty <- kcTypeType hs_ty
; ty <- tcHsKindedType kinded_ty
; checkValidType ctxt ty
; returnM ty }
+
-- Used for the deriving(...) items
tcHsDeriv :: LHsType Name -> TcM ([TyVar], Class, [Type])
tcHsDeriv = addLocM (tc_hs_deriv [])
= do { ty <- dsHsType hs_ty
; return (hoistForAllTys ty) }
+tcHsBangType :: LHsType Name -> TcM Type
+-- Permit a bang, but discard it
+tcHsBangType (L span (HsBangTy b ty)) = tcHsKindedType ty
+tcHsBangType ty = tcHsKindedType ty
+
tcHsKindedContext :: LHsContext Name -> TcM ThetaType
-- Used when we are expecting a ClassContext (i.e. no implicit params)
-- Does not do validity checking, like tcHsKindedType
-- Be sure to use checkExpectedKind, rather than simply unifying
-- with OpenTypeKind, because it gives better error messages
kcCheckHsType (L span ty) exp_kind
- = addSrcSpan span $
+ = setSrcSpan span $
kc_hs_type ty `thenM` \ (ty', act_kind) ->
checkExpectedKind ty act_kind exp_kind `thenM_`
returnM (L span ty')
= kcHsType ty `thenM` \ (ty', kind) ->
returnM (HsParTy ty', kind)
--- kcHsType (HsSpliceTy s)
--- = kcSpliceType s)
-
kc_hs_type (HsTyVar name)
= kcTyVar name `thenM` \ kind ->
returnM (HsTyVar name, kind)
-- kind-checked, so we only allow liftedTypeKind here
returnM (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind)
+kc_hs_type (HsBangTy b ty)
+ = do { (ty', kind) <- kcHsType ty
+ ; return (HsBangTy b ty', kind) }
+
+kc_hs_type ty@(HsSpliceTy _)
+ = failWithTc (ptext SLIT("Unexpected type splice:") <+> ppr ty)
+
+
---------------------------
kcApps :: TcKind -- Function kind
-> SDoc -- Function
tcLookup name `thenM` \ thing ->
traceTc (text "lk2" <+> ppr name <+> ppr thing) `thenM_`
case thing of
- ATyVar tv -> returnM (tyVarKind tv)
+ ATyVar _ ty -> returnM (typeKind ty)
AThing kind -> returnM kind
AGlobal (ATyCon tc) -> returnM (tyConKind tc)
other -> wrongThingErr "type" thing name
* Transforms from HsType to Type
* Zonks any kinds
-It cannot fail, and does no validity checking
+It cannot fail, and does no validity checking, except for
+structural matters, such as spurious ! annotations.
\begin{code}
dsHsType :: LHsType Name -> TcM Type
ds_type (HsParTy ty) -- Remove the parentheses markers
= dsHsType ty
+ds_type ty@(HsBangTy _ _) -- No bangs should be here
+ = failWithTc (ptext SLIT("Unexpected strictness annotation:") <+> ppr ty)
+
ds_type (HsKindSig ty k)
= dsHsType ty -- Kind checking done already
ds_type (HsOpTy ty1 (L span op) ty2)
= dsHsType ty1 `thenM` \ tau_ty1 ->
dsHsType ty2 `thenM` \ tau_ty2 ->
- addSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
+ setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
ds_type (HsNumTy n)
= ASSERT(n==1)
ds_var_app name arg_tys
= tcLookup name `thenM` \ thing ->
case thing of
- ATyVar tv -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
+ ATyVar _ ty -> returnM (mkAppTys ty arg_tys)
AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
- AThing _ -> tcLookupTyCon name `thenM` \ tc ->
- returnM (mkGenTyConApp tc arg_tys)
other -> pprPanic "ds_app_type" (ppr name <+> ppr arg_tys)
\end{code}
Contexts
~~~~~~~~
+
\begin{code}
dsHsLPred :: LHsPred Name -> TcM PredType
dsHsLPred pred = dsHsPred (unLoc pred)
returnM (IParam name arg_ty)
\end{code}
+GADT constructor signatures
+
+\begin{code}
+tcLHsConSig :: LHsType Name
+ -> TcM ([TcTyVar], TcThetaType,
+ [HsBang], [TcType],
+ TyCon, [TcType])
+-- Take apart the type signature for a data constructor
+-- The difference is that there can be bangs at the top of
+-- the argument types, and kind-checking is the right place to check
+tcLHsConSig sig@(L span (HsForAllTy exp tv_names ctxt ty))
+ = setSrcSpan span $
+ addErrCtxt (gadtSigCtxt sig) $
+ tcTyVarBndrs tv_names $ \ tyvars ->
+ do { theta <- mappM dsHsLPred (unLoc ctxt)
+ ; (bangs, arg_tys, tc, res_tys) <- tc_con_sig_tau ty
+ ; return (tyvars, theta, bangs, arg_tys, tc, res_tys) }
+tcLHsConSig ty
+ = do { (bangs, arg_tys, tc, res_tys) <- tc_con_sig_tau ty
+ ; return ([], [], bangs, arg_tys, tc, res_tys) }
+
+--------
+tc_con_sig_tau (L _ (HsFunTy arg ty))
+ = do { (bangs, arg_tys, tc, res_tys) <- tc_con_sig_tau ty
+ ; arg_ty <- tcHsBangType arg
+ ; return (getBangStrictness arg : bangs,
+ arg_ty : arg_tys, tc, res_tys) }
+
+tc_con_sig_tau ty
+ = do { (tc, res_tys) <- tc_con_res ty []
+ ; return ([], [], tc, res_tys) }
+
+--------
+tc_con_res (L _ (HsAppTy fun res_ty)) res_tys
+ = do { res_ty' <- dsHsType res_ty
+ ; tc_con_res fun (res_ty' : res_tys) }
+
+tc_con_res ty@(L _ (HsTyVar name)) res_tys
+ = do { thing <- tcLookup name
+ ; case thing of
+ AGlobal (ATyCon tc) -> return (tc, res_tys)
+ other -> failWithTc (badGadtDecl ty)
+ }
+
+tc_con_res ty _ = failWithTc (badGadtDecl ty)
+
+gadtSigCtxt ty
+ = hang (ptext SLIT("In the signature of a data constructor:"))
+ 2 (ppr ty)
+badGadtDecl ty
+ = hang (ptext SLIT("Malformed constructor signature:"))
+ 2 (ppr ty)
+\end{code}
%************************************************************************
%* *
where
zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
returnM (mkTyVar name kind')
- zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
+ zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $
returnM (mkTyVar name liftedTypeKind)
+
+-----------------------------------
+tcDataKindSig :: Maybe Kind -> TcM [TyVar]
+-- GADT decls can have a (perhpas partial) kind signature
+-- e.g. data T :: * -> * -> * where ...
+-- This function makes up suitable (kinded) type variables for
+-- the argument kinds, and checks that the result kind is indeed *
+tcDataKindSig Nothing = return []
+tcDataKindSig (Just kind)
+ = do { checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
+ ; span <- getSrcSpanM
+ ; us <- newUniqueSupply
+ ; let loc = srcSpanStart span
+ uniqs = uniqsFromSupply us
+ ; return [ mk_tv loc uniq str kind
+ | ((kind, str), uniq) <- arg_kinds `zip` names `zip` uniqs ] }
+ where
+ (arg_kinds, res_kind) = splitKindFunTys kind
+ mk_tv loc uniq str kind = mkTyVar name kind
+ where
+ name = mkInternalName uniq occ loc
+ occ = mkOccName tvName str
+
+ names :: [String] -- a,b,c...aa,ab,ac etc
+ names = [ c:cs | cs <- "" : names, c <- ['a'..'z'] ]
+
+badKindSig :: Kind -> SDoc
+badKindSig kind
+ = hang (ptext SLIT("Kind signature on data type declaration has non-* return kind"))
+ 2 (ppr kind)
\end{code}
it with expected_ty afterwards
\begin{code}
-tcAddScopedTyVars :: [LHsType Name] -> TcM a -> TcM a
-tcAddScopedTyVars [] thing_inside
- = thing_inside -- Quick get-out for the empty case
-
-tcAddScopedTyVars sig_tys thing_inside
- = getInLocalScope `thenM` \ in_scope ->
- getSrcSpanM `thenM` \ span ->
- let
- sig_tvs = [ L span (UserTyVar n)
- | ty <- sig_tys,
- n <- nameSetToList (extractHsTyVars ty),
- not (in_scope n) ]
- -- The tyvars we want are the free type variables of
- -- the type that are not already in scope
- in
+tcPatSigBndrs :: LHsType Name
+ -> TcM ([TcTyVar], -- Brought into scope
+ LHsType Name) -- Kinded, but not yet desugared
+
+tcPatSigBndrs hs_ty
+ = do { in_scope <- getInLocalScope
+ ; span <- getSrcSpanM
+ ; let sig_tvs = [ L span (UserTyVar n)
+ | n <- nameSetToList (extractHsTyVars hs_ty),
+ not (in_scope n) ]
+ -- The tyvars we want are the free type variables of
+ -- the type that are not already in scope
+
-- Behave like kcHsType on a ForAll type
-- i.e. make kinded tyvars with mutable kinds,
-- and kind-check the enclosed types
- kcHsTyVars sig_tvs (\ kinded_tvs -> do
- { mappM kcTypeType sig_tys
- ; return kinded_tvs }) `thenM` \ kinded_tvs ->
+ ; (kinded_tvs, kinded_ty) <- kcHsTyVars sig_tvs $ \ kinded_tvs -> do
+ { kinded_ty <- kcTypeType hs_ty
+ ; return (kinded_tvs, kinded_ty) }
-- Zonk the mutable kinds and bring the tyvars into scope
- -- Rather like tcTyVarBndrs, except that it brings *mutable*
- -- tyvars into scope, not immutable ones
+ -- Just like the call to tcTyVarBndrs in ds_type (HsForAllTy case),
+ -- except that it brings *meta* tyvars into scope, not regular ones
--
+ -- [Out of date, but perhaps should be resurrected]
-- Furthermore, the tyvars are PatSigTvs, which means that we get better
-- error messages when type variables escape:
-- Inferred type is less polymorphic than expected
-- Quantified type variable `t' escapes
-- It is mentioned in the environment:
-- t is bound by the pattern type signature at tcfail103.hs:6
- mapM (zonk . unLoc) kinded_tvs `thenM` \ tyvars ->
- tcExtendTyVarEnv tyvars thing_inside
-
+ ; tyvars <- mapM (zonk . unLoc) kinded_tvs
+ ; return (tyvars, kinded_ty) }
where
zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
- newMutTyVar name kind' PatSigTv
- zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
+ newMetaTyVar name kind' Flexi
+ -- Scoped type variables are bound to a *type*, hence Flexi
+ zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $
returnM (mkTyVar name liftedTypeKind)
+
+tcHsPatSigType :: UserTypeCtxt
+ -> LHsType Name -- The type signature
+ -> TcM ([TcTyVar], -- Newly in-scope type variables
+ TcType) -- The signature
+
+tcHsPatSigType ctxt hs_ty
+ = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
+ do { (tyvars, kinded_ty) <- tcPatSigBndrs hs_ty
+
+ -- Complete processing of the type, and check its validity
+ ; tcExtendTyVarEnv tyvars $ do
+ { sig_ty <- tcHsKindedType kinded_ty
+ ; checkValidType ctxt sig_ty
+ ; return (tyvars, sig_ty) }
+ }
+
+tcAddLetBoundTyVars :: LHsBinds Name -> TcM a -> TcM a
+-- Turgid funciton, used for type variables bound by the patterns of a let binding
+
+tcAddLetBoundTyVars binds thing_inside
+ = go (collectSigTysFromHsBinds (bagToList binds)) thing_inside
+ where
+ go [] thing_inside = thing_inside
+ go (hs_ty:hs_tys) thing_inside
+ = do { (tyvars, _kinded_ty) <- tcPatSigBndrs hs_ty
+ ; tcExtendTyVarEnv tyvars (go hs_tys thing_inside) }
\end{code}
\begin{code}
data TcSigInfo
- = TySigInfo {
- sig_poly_id :: TcId, -- *Polymorphic* binder for this value...
- -- Has name = N
-
- sig_tvs :: [TcTyVar], -- tyvars
- sig_theta :: TcThetaType, -- theta
- sig_tau :: TcTauType, -- tau
+ = TcSigInfo {
+ sig_id :: TcId, -- *Polymorphic* binder for this value...
- sig_mono_id :: TcId, -- *Monomorphic* binder for this value
- -- Does *not* have name = N
- -- Has type tau
+ sig_scoped :: [Name], -- Names for any scoped type variables
+ -- Invariant: correspond 1-1 with an initial
+ -- segment of sig_tvs (see Note [Scoped])
- sig_insts :: [Inst], -- Empty if theta is null, or
- -- (method mono_id) otherwise
+ sig_tvs :: [TcTyVar], -- Instantiated type variables
+ -- See Note [Instantiate sig]
- sig_loc :: SrcSpan -- The location of the signature
+ sig_theta :: TcThetaType, -- Instantiated theta
+ sig_tau :: TcTauType, -- Instantiated tau
+ sig_loc :: InstLoc -- The location of the signature
}
+-- Note [Scoped]
+-- There may be more instantiated type variables than scoped
+-- ones. For example:
+-- type T a = forall b. b -> (a,b)
+-- f :: forall c. T c
+-- Here, the signature for f will have one scoped type variable, c,
+-- but two instantiated type variables, c' and b'.
+--
+-- We assume that the scoped ones are at the *front* of sig_tvs,
+-- and remember the names from the original HsForAllTy in sig_scoped
+
+-- Note [Instantiate sig]
+-- It's vital to instantiate a type signature with fresh variable.
+-- For example:
+-- type S = forall a. a->a
+-- f,g :: S
+-- f = ...
+-- g = ...
+-- Here, we must use distinct type variables when checking f,g's right hand sides.
+-- (Instantiation is only necessary because of type synonyms. Otherwise,
+-- it's all cool; each signature has distinct type variables from the renamer.)
+
+type TcSigFun = Name -> Maybe TcSigInfo
instance Outputable TcSigInfo where
- ppr (TySigInfo id tyvars theta tau _ inst _) =
- ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
-
-maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
- -- Search for a particular signature
-maybeSig [] name = Nothing
-maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name
- | name == idName sig_id = Just sig
- | otherwise = maybeSig sigs name
-\end{code}
-
-
-\begin{code}
-tcTySig :: LSig Name -> TcM TcSigInfo
-
-tcTySig (L span (Sig (L _ v) ty))
- = addSrcSpan span $
- tcHsSigType (FunSigCtxt v) ty `thenM` \ sigma_tc_ty ->
- mkTcSig (mkLocalId v sigma_tc_ty) `thenM` \ sig ->
- returnM sig
-
-mkTcSig :: TcId -> TcM TcSigInfo
-mkTcSig poly_id
- = -- Instantiate this type
- -- It's important to do this even though in the error-free case
- -- we could just split the sigma_tc_ty (since the tyvars don't
- -- unified with anything). But in the case of an error, when
- -- the tyvars *do* get unified with something, we want to carry on
- -- typechecking the rest of the program with the function bound
- -- to a pristine type, namely sigma_tc_ty
- tcInstType SigTv (idType poly_id) `thenM` \ (tyvars', theta', tau') ->
-
- getInstLoc SignatureOrigin `thenM` \ inst_loc ->
- newMethod inst_loc poly_id
- (mkTyVarTys tyvars')
- theta' tau' `thenM` \ inst ->
- -- We make a Method even if it's not overloaded; no harm
- -- But do not extend the LIE! We're just making an Id.
-
- getSrcSpanM `thenM` \ src_loc ->
- returnM (TySigInfo { sig_poly_id = poly_id, sig_tvs = tyvars',
- sig_theta = theta', sig_tau = tau',
- sig_mono_id = instToId inst,
- sig_insts = [inst], sig_loc = src_loc })
-\end{code}
-
-
-%************************************************************************
-%* *
-\subsection{Errors and contexts}
-%* *
-%************************************************************************
-
-
-\begin{code}
-hoistForAllTys :: Type -> Type
--- Used for user-written type signatures only
--- Move 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: eliminate duplicate constraints. These can show up
--- when hoisting constraints, notably implicit parameters.
---
--- We want to 'look through' type synonyms when doing this
--- so it's better done on the Type than the HsType
-
-hoistForAllTys ty
- = let
- no_shadow_ty = deShadowTy ty
- -- Running over ty with an empty substitution gives it the
- -- no-shadowing property. This 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 -> ()
- --
- -- What about type vars that are lexically in scope in the envt?
- -- We simply rely on them having a different unique to any
- -- binder in 'ty'. Otherwise we'd have to slurp the in-scope-tyvars
- -- out of the envt, which is boring and (I think) not necessary.
- in
- case hoist no_shadow_ty of
- (tvs, theta, body) -> mkForAllTys tvs (mkFunTys (nubBy tcEqType theta) body)
- -- The 'nubBy' eliminates duplicate constraints,
- -- notably implicit parameters
- where
- hoist ty
- | (tvs1, body_ty) <- tcSplitForAllTys ty,
- not (null tvs1)
- = case hoist body_ty of
- (tvs2,theta,tau) -> (tvs1 ++ tvs2, theta, tau)
-
- | Just (arg, res) <- tcSplitFunTy_maybe ty
- = let
- arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively
- in -- to the argument type
- if (isPredTy arg') then
- case hoist res of
- (tvs,theta,tau) -> (tvs, arg':theta, tau)
- else
- case hoist res of
- (tvs,theta,tau) -> (tvs, theta, mkFunTy arg' tau)
-
- | otherwise = ([], [], ty)
+ ppr (TcSigInfo { sig_id = id, sig_tvs = tyvars, sig_theta = theta, sig_tau = tau})
+ = ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
+
+lookupSig :: [TcSigInfo] -> TcSigFun -- Search for a particular signature
+lookupSig [] name = Nothing
+lookupSig (sig : sigs) name
+ | name == idName (sig_id sig) = Just sig
+ | otherwise = lookupSig sigs name
\end{code}