\begin{code}
module TcHsType (
- tcHsSigType, tcHsPred,
+ tcHsSigType, tcHsDeriv,
UserTypeCtxt(..),
-- Kind checking
kcHsTyVars, kcHsSigType, kcHsLiftedSigType,
- kcCheckHsType, kcHsContext,
+ kcCheckHsType, kcHsContext, kcHsType,
-- Typechecking kinded types
- tcHsKindedContext, tcHsKindedType, tcTyVarBndrs, dsHsType,
+ tcHsKindedContext, tcHsKindedType, tcHsBangType,
+ tcTyVarBndrs, dsHsType, tcLHsConResTy,
+ tcDataKindSig,
- tcAddScopedTyVars,
-
- TcSigInfo(..), tcTySig, mkTcSig, maybeSig, tcSigPolyId, tcSigMonoId
+ -- Pattern type signatures
+ tcHsPatSigType, tcPatSig
) where
#include "HsVersions.h"
-import HsSyn ( HsType(..), HsTyVarBndr(..), HsContext, Sig(..), HsPred(..) )
-import RnHsSyn ( RenamedHsType, RenamedContext, RenamedSig, extractHsTyVars )
-import TcHsSyn ( TcId )
-
+import HsSyn ( HsType(..), LHsType, HsTyVarBndr(..), LHsTyVarBndr,
+ LHsContext, HsPred(..), LHsPred, HsExplicitForAll(..) )
+import RnHsSyn ( extractHsTyVars )
import TcRnMonad
-import TcEnv ( tcExtendTyVarEnv, tcExtendTyVarKindEnv,
+import TcEnv ( tcExtendTyVarEnv, tcExtendKindEnvTvs,
tcLookup, tcLookupClass, tcLookupTyCon,
- TyThing(..), TcTyThing(..),
- getInLocalScope
- )
-import TcMType ( newKindVar, tcInstType, newMutTyVar,
- zonkTcType, zonkTcKindToKind,
- checkValidType, UserTypeCtxt(..), pprUserTypeCtxt
+ TyThing(..), getInLocalScope, getScopedTyVarBinds,
+ wrongThingErr
)
-import TcUnify ( unifyKind, unifyFunKind, unifyTypeKind )
-import TcType ( Type, PredType(..), ThetaType, TyVarDetails(..),
- TcTyVar, TcKind, TcThetaType, TcTauType,
- mkTyVarTy, mkTyVarTys, mkFunTy,
- mkForAllTys, mkFunTys, tcEqType, isPredTy,
- mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys,
- liftedTypeKind, unliftedTypeKind, eqKind,
- tcSplitFunTy_maybe, tcSplitForAllTys, tcSplitSigmaTy
+import TcMType ( newKindVar,
+ zonkTcKindToKind,
+ tcInstBoxyTyVar, readFilledBox,
+ checkValidType
)
-import PprType ( pprKind, pprThetaArrow )
-import qualified Type ( splitFunTys )
-import Inst ( Inst, InstOrigin(..), newMethod, instToId )
-
-import Id ( mkLocalId, idName, idType )
-import Var ( TyVar, mkTyVar, tyVarKind )
-import ErrUtils ( Message )
+import TcUnify ( boxyUnify, unifyFunKind, checkExpectedKind )
+import TcIface ( checkWiredInTyCon )
+import TcType ( Type, PredType(..), ThetaType, BoxySigmaType,
+ TcType, TcKind, isRigidTy,
+ UserTypeCtxt(..), pprUserTypeCtxt,
+ substTyWith, mkTyVarTys, tcEqType,
+ tcIsTyVarTy, mkFunTy, mkSigmaTy, mkPredTy,
+ mkTyConApp, mkAppTys, typeKind )
+import Kind ( Kind, isLiftedTypeKind, liftedTypeKind, ubxTupleKind,
+ openTypeKind, argTypeKind, splitKindFunTys )
+import Var ( TyVar, mkTyVar, tyVarName )
import TyCon ( TyCon, tyConKind )
-import Class ( classTyCon )
-import Name ( Name )
+import Class ( Class, classTyCon )
+import Name ( Name, mkInternalName )
+import OccName ( mkOccName, tvName )
import NameSet
import PrelNames ( genUnitTyConName )
-import Subst ( deShadowTy )
-import TysWiredIn ( mkListTy, mkPArrTy, mkTupleTy )
+import TysWiredIn ( mkListTy, listTyCon, mkPArrTy, parrTyCon, tupleTyCon )
import BasicTypes ( Boxity(..) )
-import SrcLoc ( SrcLoc )
+import SrcLoc ( Located(..), unLoc, noLoc, getLoc, srcSpanStart )
+import UniqSupply ( uniqsFromSupply )
import Outputable
-import List ( nubBy )
\end{code}
%************************************************************************
\begin{code}
-tcHsSigType :: UserTypeCtxt -> RenamedHsType -> TcM Type
+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 (checkHsTypeCtxt ctxt hs_ty) $
+ = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
do { kinded_ty <- kcTypeType hs_ty
; ty <- tcHsKindedType kinded_ty
; checkValidType ctxt ty
; returnM ty }
--- tcHsPred is happy with a partial application, e.g. (ST s)
--- Used from TcDeriv
-tcHsPred pred
- = do { (kinded_pred,_) <- kc_pred pred -- kc_pred rather than kcHsPred
- -- to avoid the partial application check
- ; dsHsPred kinded_pred }
-
-
-checkHsTypeCtxt ctxt hs_ty
- = vcat [ptext SLIT("In the type signature:") <+> ppr hs_ty,
- ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
+-- Used for the deriving(...) items
+tcHsDeriv :: LHsType Name -> TcM ([TyVar], Class, [Type])
+tcHsDeriv = addLocM (tc_hs_deriv [])
+
+tc_hs_deriv tv_names (HsPredTy (HsClassP cls_name hs_tys))
+ = kcHsTyVars tv_names $ \ tv_names' ->
+ do { cls_kind <- kcClass cls_name
+ ; (tys, res_kind) <- kcApps cls_kind (ppr cls_name) hs_tys
+ ; tcTyVarBndrs tv_names' $ \ tyvars ->
+ do { arg_tys <- dsHsTypes tys
+ ; cls <- tcLookupClass cls_name
+ ; return (tyvars, cls, arg_tys) }}
+
+tc_hs_deriv tv_names1 (HsForAllTy _ tv_names2 (L _ []) (L _ ty))
+ = -- Funny newtype deriving form
+ -- forall a. C [a]
+ -- where C has arity 2. Hence can't use regular functions
+ tc_hs_deriv (tv_names1 ++ tv_names2) ty
+
+tc_hs_deriv _ other
+ = failWithTc (ptext SLIT("Illegal deriving item") <+> ppr other)
\end{code}
These functions are used during knot-tying in
separate kind-checking, desugaring, and validity checking
\begin{code}
-kcHsSigType, kcHsLiftedSigType :: HsType Name -> TcM (HsType Name)
+kcHsSigType, kcHsLiftedSigType :: LHsType Name -> TcM (LHsType Name)
-- Used for type signatures
kcHsSigType ty = kcTypeType ty
kcHsLiftedSigType ty = kcLiftedType ty
-tcHsKindedType :: RenamedHsType -> TcM Type
+tcHsKindedType :: LHsType Name -> TcM Type
-- Don't do kind checking, nor validity checking,
-- but do hoist for-alls to the top
-- This is used in type and class decls, where kinding is
-- done in advance, and validity checking is done later
-- [Validity checking done later because of knot-tying issues.]
-tcHsKindedType hs_ty
- = do { ty <- dsHsType hs_ty
- ; return (hoistForAllTys ty) }
+tcHsKindedType hs_ty = dsHsType hs_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 :: RenamedContext -> TcM ThetaType
+tcHsKindedContext :: LHsContext Name -> TcM ThetaType
-- Used when we are expecting a ClassContext (i.e. no implicit params)
-- Does not do validity checking, like tcHsKindedType
-tcHsKindedContext hs_theta = mappM dsHsPred hs_theta
+tcHsKindedContext hs_theta = addLocM (mappM dsHsLPred) hs_theta
\end{code}
\begin{code}
---------------------------
-kcLiftedType :: HsType Name -> TcM (HsType Name)
- -- The type ty must be a *lifted* *type*
+kcLiftedType :: LHsType Name -> TcM (LHsType Name)
+-- The type ty must be a *lifted* *type*
kcLiftedType ty = kcCheckHsType ty liftedTypeKind
---------------------------
-kcTypeType :: HsType Name -> TcM (HsType Name)
- -- The type ty must be a *type*, but it can be lifted or unlifted
-kcTypeType ty
- = kcHsType ty `thenM` \ (ty', kind) ->
- unifyTypeKind kind `thenM_`
- returnM ty'
+kcTypeType :: LHsType Name -> TcM (LHsType Name)
+-- The type ty must be a *type*, but it can be lifted or
+-- unlifted or an unboxed tuple.
+kcTypeType ty = kcCheckHsType ty openTypeKind
---------------------------
-kcCheckHsType :: HsType Name -> TcKind -> TcM (HsType Name)
+kcCheckHsType :: LHsType Name -> TcKind -> TcM (LHsType Name)
-- Check that the type has the specified kind
-kcCheckHsType ty exp_kind
- = kcHsType ty `thenM` \ (ty', act_kind) ->
- checkExpectedKind (ppr ty) act_kind exp_kind `thenM_`
- returnM ty'
+-- Be sure to use checkExpectedKind, rather than simply unifying
+-- with OpenTypeKind, because it gives better error messages
+kcCheckHsType (L span ty) exp_kind
+ = setSrcSpan span $
+ do { (ty', act_kind) <- add_ctxt ty (kc_hs_type ty)
+ -- Add the context round the inner check only
+ -- because checkExpectedKind already mentions
+ -- 'ty' by name in any error message
+
+ ; checkExpectedKind ty act_kind exp_kind
+ ; return (L span ty') }
+ where
+ -- Wrap a context around only if we want to
+ -- show that contexts. Omit invisble ones
+ -- and ones user's won't grok (HsPred p).
+ add_ctxt (HsPredTy p) thing = thing
+ add_ctxt (HsForAllTy Implicit tvs (L _ []) ty) thing = thing
+ add_ctxt other_ty thing = addErrCtxt (typeCtxt ty) thing
\end{code}
Here comes the main function
\begin{code}
-kcHsType :: HsType Name -> TcM (HsType Name, TcKind)
+kcHsType :: LHsType Name -> TcM (LHsType Name, TcKind)
+kcHsType ty = wrapLocFstM kc_hs_type ty
-- kcHsType *returns* the kind of the type, rather than taking an expected
-- kind as argument as tcExpr does.
-- Reasons:
--
-- The translated type has explicitly-kinded type-variable binders
-kcHsType (HsParTy ty)
+kc_hs_type (HsParTy ty)
= kcHsType ty `thenM` \ (ty', kind) ->
returnM (HsParTy ty', kind)
-kcHsType (HsTyVar name)
+kc_hs_type (HsTyVar name)
= kcTyVar name `thenM` \ kind ->
returnM (HsTyVar name, kind)
-kcHsType (HsListTy ty)
+kc_hs_type (HsListTy ty)
= kcLiftedType ty `thenM` \ ty' ->
returnM (HsListTy ty', liftedTypeKind)
-kcHsType (HsPArrTy ty)
+kc_hs_type (HsPArrTy ty)
= kcLiftedType ty `thenM` \ ty' ->
returnM (HsPArrTy ty', liftedTypeKind)
-kcHsType (HsNumTy n)
+kc_hs_type (HsNumTy n)
= returnM (HsNumTy n, liftedTypeKind)
-kcHsType (HsKindSig ty k)
+kc_hs_type (HsKindSig ty k)
= kcCheckHsType ty k `thenM` \ ty' ->
returnM (HsKindSig ty' k, k)
-kcHsType (HsTupleTy Boxed tys)
+kc_hs_type (HsTupleTy Boxed tys)
= mappM kcLiftedType tys `thenM` \ tys' ->
returnM (HsTupleTy Boxed tys', liftedTypeKind)
-kcHsType (HsTupleTy Unboxed tys)
+kc_hs_type (HsTupleTy Unboxed tys)
= mappM kcTypeType tys `thenM` \ tys' ->
- returnM (HsTupleTy Unboxed tys', unliftedTypeKind)
+ returnM (HsTupleTy Unboxed tys', ubxTupleKind)
-kcHsType (HsFunTy ty1 ty2)
- = kcTypeType ty1 `thenM` \ ty1' ->
- kcTypeType ty2 `thenM` \ ty2' ->
+kc_hs_type (HsFunTy ty1 ty2)
+ = kcCheckHsType ty1 argTypeKind `thenM` \ ty1' ->
+ kcTypeType ty2 `thenM` \ ty2' ->
returnM (HsFunTy ty1' ty2', liftedTypeKind)
-kcHsType ty@(HsOpTy ty1 op ty2)
- = kcTyVar op `thenM` \ op_kind ->
+kc_hs_type ty@(HsOpTy ty1 op ty2)
+ = addLocM kcTyVar op `thenM` \ op_kind ->
kcApps op_kind (ppr op) [ty1,ty2] `thenM` \ ([ty1',ty2'], res_kind) ->
returnM (HsOpTy ty1' op ty2', res_kind)
-kcHsType ty@(HsAppTy ty1 ty2)
+kc_hs_type ty@(HsAppTy ty1 ty2)
= kcHsType fun_ty `thenM` \ (fun_ty', fun_kind) ->
- kcApps fun_kind (ppr fun_ty) arg_tys `thenM` \ (arg_tys', res_kind) ->
- returnM (foldl HsAppTy fun_ty' arg_tys', res_kind)
+ kcApps fun_kind (ppr fun_ty) arg_tys `thenM` \ ((arg_ty':arg_tys'), res_kind) ->
+ returnM (foldl mk_app (HsAppTy fun_ty' arg_ty') arg_tys', res_kind)
where
(fun_ty, arg_tys) = split ty1 [ty2]
- split (HsAppTy f a) as = split f (a:as)
- split f as = (f,as)
-
-kcHsType (HsPredTy pred)
+ split (L _ (HsAppTy f a)) as = split f (a:as)
+ split f as = (f,as)
+ mk_app fun arg = HsAppTy (noLoc fun) arg -- Add noLocs for inner nodes of
+ -- the application; they are never used
+
+kc_hs_type (HsPredTy pred)
= kcHsPred pred `thenM` \ pred' ->
returnM (HsPredTy pred', liftedTypeKind)
-kcHsType (HsForAllTy (Just tv_names) context ty)
+kc_hs_type (HsForAllTy exp tv_names context ty)
= kcHsTyVars tv_names $ \ tv_names' ->
kcHsContext context `thenM` \ ctxt' ->
kcLiftedType ty `thenM` \ ty' ->
- -- The body of a forall must be of kind *
- -- In principle, I suppose, we could allow unlifted types,
- -- but it seems simpler to stick to lifted types for now.
- returnM (HsForAllTy (Just tv_names') ctxt' ty', liftedTypeKind)
+ -- The body of a forall is usually a type, but in principle
+ -- there's no reason to prohibit *unlifted* types.
+ -- In fact, GHC can itself construct a function with an
+ -- unboxed tuple inside a for-all (via CPR analyis; see
+ -- typecheck/should_compile/tc170)
+ --
+ -- Still, that's only for internal interfaces, which aren't
+ -- 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
- -> [HsType Name] -- Arg types
- -> TcM ([HsType Name], TcKind) -- Kind-checked args
+kcApps :: TcKind -- Function kind
+ -> SDoc -- Function
+ -> [LHsType Name] -- Arg types
+ -> TcM ([LHsType Name], TcKind) -- Kind-checked args
kcApps fun_kind ppr_fun args
= split_fk fun_kind (length args) `thenM` \ (arg_kinds, res_kind) ->
- mappM kc_arg (args `zip` arg_kinds) `thenM` \ args' ->
+ zipWithM kc_arg args arg_kinds `thenM` \ args' ->
returnM (args', res_kind)
where
split_fk fk 0 = returnM ([], fk)
Just (ak,fk') -> split_fk fk' (n-1) `thenM` \ (aks, rk) ->
returnM (ak:aks, rk)
- kc_arg (arg, arg_kind) = kcCheckHsType arg arg_kind
+ kc_arg arg arg_kind = kcCheckHsType arg arg_kind
too_many_args = ptext SLIT("Kind error:") <+> quotes ppr_fun <+>
ptext SLIT("is applied to too many type arguments")
---------------------------
-kcHsContext :: HsContext Name -> TcM (HsContext Name)
-kcHsContext ctxt = mappM kcHsPred ctxt
+kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
+kcHsContext ctxt = wrapLocM (mappM kcHsLPred) ctxt
-kcHsPred pred -- Checks that the result is of kind liftedType
- = kc_pred pred `thenM` \ (pred', kind) ->
- checkExpectedKind (ppr pred) kind liftedTypeKind `thenM_`
+kcHsLPred :: LHsPred Name -> TcM (LHsPred Name)
+kcHsLPred = wrapLocM kcHsPred
+
+kcHsPred :: HsPred Name -> TcM (HsPred Name)
+kcHsPred pred -- Checks that the result is of kind liftedType
+ = kc_pred pred `thenM` \ (pred', kind) ->
+ checkExpectedKind pred kind liftedTypeKind `thenM_`
returnM pred'
---------------------------
---------------------------
kcTyVar :: Name -> TcM TcKind
kcTyVar name -- Could be a tyvar or a tycon
- = tcLookup name `thenM` \ thing ->
+ = traceTc (text "lk1" <+> ppr name) `thenM_`
+ tcLookup name `thenM` \ thing ->
+ traceTc (text "lk2" <+> ppr name <+> ppr thing) `thenM_`
case thing of
- ATyVar tv -> returnM (tyVarKind tv)
- ARecTyCon kind -> returnM kind
+ ATyVar _ ty -> returnM (typeKind ty)
+ AThing kind -> returnM kind
AGlobal (ATyCon tc) -> returnM (tyConKind tc)
- other -> failWithTc (wrongThingErr "type" thing name)
+ other -> wrongThingErr "type" thing name
kcClass :: Name -> TcM TcKind
kcClass cls -- Must be a class
= tcLookup cls `thenM` \ thing ->
case thing of
- ARecClass kind -> returnM kind
+ AThing kind -> returnM kind
AGlobal (AClass cls) -> returnM (tyConKind (classTyCon cls))
- other -> failWithTc (wrongThingErr "class" thing cls)
+ other -> wrongThingErr "class" thing cls
\end{code}
- Helper functions
-
-
-\begin{code}
----------------------------
--- We would like to get a decent error message from
--- (a) Under-applied type constructors
--- f :: (Maybe, Maybe)
--- (b) Over-applied type constructors
--- f :: Int x -> Int x
---
-
-
-checkExpectedKind :: SDoc -> TcKind -> TcKind -> TcM TcKind
--- A fancy wrapper for 'unifyKind', which tries to give
--- decent error messages.
--- Returns the same kind that it is passed, exp_kind
-checkExpectedKind pp_ty act_kind exp_kind
- | act_kind `eqKind` exp_kind -- Short cut for a very common case
- = returnM exp_kind
- | otherwise
- = tryTc (unifyKind exp_kind act_kind) `thenM` \ (errs, mb_r) ->
- case mb_r of {
- Just _ -> returnM exp_kind ; -- Unification succeeded
- Nothing ->
-
- -- So there's definitely an error
- -- Now to find out what sort
- zonkTcType exp_kind `thenM` \ exp_kind ->
- zonkTcType act_kind `thenM` \ act_kind ->
-
- let (exp_as, _) = Type.splitFunTys exp_kind
- (act_as, _) = Type.splitFunTys act_kind
- -- Use the Type versions for kinds
- n_exp_as = length exp_as
- n_act_as = length act_as
-
- err | n_exp_as < n_act_as -- E.g. [Maybe]
- = quotes pp_ty <+> ptext SLIT("is not applied to enough type arguments")
-
- -- Now n_exp_as >= n_act_as. In the next two cases,
- -- n_exp_as == 0, and hence so is n_act_as
- | exp_kind `eqKind` liftedTypeKind && act_kind `eqKind` unliftedTypeKind
- = ptext SLIT("Expecting a lifted type, but") <+> quotes pp_ty
- <+> ptext SLIT("is unlifted")
-
- | exp_kind `eqKind` unliftedTypeKind && act_kind `eqKind` liftedTypeKind
- = ptext SLIT("Expecting an unlifted type, but") <+> quotes pp_ty
- <+> ptext SLIT("is lifted")
-
- | otherwise -- E.g. Monad [Int]
- = sep [ ptext SLIT("Expecting kind") <+> quotes (pprKind exp_kind) <> comma,
- ptext SLIT("but") <+> quotes pp_ty <+>
- ptext SLIT("has kind") <+> quotes (pprKind act_kind)]
- in
- failWithTc (ptext SLIT("Kind error:") <+> err)
- }
-\end{code}
%************************************************************************
%* *
* 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
+ (a) spurious ! annotations.
+ (b) a class used as a type
\begin{code}
-dsHsType :: HsType Name -- All HsTyVarBndrs are kind-annotated
- -> TcM Type
+dsHsType :: LHsType Name -> TcM Type
+-- All HsTyVarBndrs in the intput type are kind-annotated
+dsHsType ty = ds_type (unLoc ty)
-dsHsType ty@(HsTyVar name)
+ds_type ty@(HsTyVar name)
= ds_app ty []
-dsHsType (HsParTy ty) -- Remove the parentheses markers
+ds_type (HsParTy ty) -- Remove the parentheses markers
= dsHsType ty
-dsHsType (HsKindSig ty k)
+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
-dsHsType (HsListTy ty)
- = dsHsType ty `thenM` \ tau_ty ->
+ds_type (HsListTy ty)
+ = dsHsType ty `thenM` \ tau_ty ->
+ checkWiredInTyCon listTyCon `thenM_`
returnM (mkListTy tau_ty)
-dsHsType (HsPArrTy ty)
- = dsHsType ty `thenM` \ tau_ty ->
+ds_type (HsPArrTy ty)
+ = dsHsType ty `thenM` \ tau_ty ->
+ checkWiredInTyCon parrTyCon `thenM_`
returnM (mkPArrTy tau_ty)
-dsHsType (HsTupleTy boxity tys)
- = dsHsTypes tys `thenM` \ tau_tys ->
- returnM (mkTupleTy boxity (length tys) tau_tys)
+ds_type (HsTupleTy boxity tys)
+ = dsHsTypes tys `thenM` \ tau_tys ->
+ checkWiredInTyCon tycon `thenM_`
+ returnM (mkTyConApp tycon tau_tys)
+ where
+ tycon = tupleTyCon boxity (length tys)
-dsHsType (HsFunTy ty1 ty2)
+ds_type (HsFunTy ty1 ty2)
= dsHsType ty1 `thenM` \ tau_ty1 ->
dsHsType ty2 `thenM` \ tau_ty2 ->
returnM (mkFunTy tau_ty1 tau_ty2)
-dsHsType (HsOpTy ty1 op ty2)
- = dsHsType ty1 `thenM` \ tau_ty1 ->
- dsHsType ty2 `thenM` \ tau_ty2 ->
- ds_var_app op [tau_ty1,tau_ty2]
+ds_type (HsOpTy ty1 (L span op) ty2)
+ = dsHsType ty1 `thenM` \ tau_ty1 ->
+ dsHsType ty2 `thenM` \ tau_ty2 ->
+ setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
-dsHsType (HsNumTy n)
+ds_type (HsNumTy n)
= ASSERT(n==1)
tcLookupTyCon genUnitTyConName `thenM` \ tc ->
returnM (mkTyConApp tc [])
-dsHsType ty@(HsAppTy ty1 ty2)
- = ds_app ty1 [ty2]
+ds_type ty@(HsAppTy _ _)
+ = ds_app ty []
-dsHsType (HsPredTy pred)
+ds_type (HsPredTy pred)
= dsHsPred pred `thenM` \ pred' ->
returnM (mkPredTy pred')
-dsHsType full_ty@(HsForAllTy (Just tv_names) ctxt ty)
+ds_type full_ty@(HsForAllTy exp tv_names ctxt ty)
= tcTyVarBndrs tv_names $ \ tyvars ->
- mappM dsHsPred ctxt `thenM` \ theta ->
+ mappM dsHsLPred (unLoc ctxt) `thenM` \ theta ->
dsHsType ty `thenM` \ tau ->
returnM (mkSigmaTy tyvars theta tau)
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\begin{code}
-ds_app :: HsType Name -> [HsType Name] -> TcM Type
+ds_app :: HsType Name -> [LHsType Name] -> TcM Type
ds_app (HsAppTy ty1 ty2) tys
- = ds_app ty1 (ty2:tys)
+ = ds_app (unLoc ty1) (ty2:tys)
ds_app ty tys
= dsHsTypes tys `thenM` \ arg_tys ->
case ty of
HsTyVar fun -> ds_var_app fun arg_tys
- other -> dsHsType ty `thenM` \ fun_ty ->
+ other -> ds_type ty `thenM` \ fun_ty ->
returnM (mkAppTys fun_ty arg_tys)
ds_var_app :: Name -> [Type] -> TcM Type
ds_var_app name arg_tys
= tcLookup name `thenM` \ thing ->
case thing of
- ATyVar tv -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
- AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
- ARecTyCon _ -> tcLookupTyCon name `thenM` \ tc ->
- returnM (mkGenTyConApp tc arg_tys)
- other -> pprPanic "ds_app_type" (ppr name <+> ppr arg_tys)
+ ATyVar _ ty -> returnM (mkAppTys ty arg_tys)
+ AGlobal (ATyCon tc) -> returnM (mkTyConApp tc arg_tys)
+ other -> wrongThingErr "type" thing name
\end{code}
Contexts
~~~~~~~~
+
\begin{code}
-dsHsPred :: HsPred Name -> TcM PredType
+dsHsLPred :: LHsPred Name -> TcM PredType
+dsHsLPred pred = dsHsPred (unLoc pred)
+
dsHsPred pred@(HsClassP class_name tys)
= dsHsTypes tys `thenM` \ arg_tys ->
tcLookupClass class_name `thenM` \ clas ->
returnM (IParam name arg_ty)
\end{code}
+GADT constructor signatures
+
+\begin{code}
+tcLHsConResTy :: LHsType Name -> TcM (TyCon, [TcType])
+tcLHsConResTy ty@(L span _)
+ = setSrcSpan span $
+ addErrCtxt (gadtResCtxt ty) $
+ tc_con_res ty []
+
+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)
+
+gadtResCtxt ty
+ = hang (ptext SLIT("In the result type of a data constructor:"))
+ 2 (ppr ty)
+badGadtDecl ty
+ = hang (ptext SLIT("Malformed constructor result type:"))
+ 2 (ppr ty)
+
+typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
+\end{code}
%************************************************************************
%* *
\begin{code}
-kcHsTyVars :: [HsTyVarBndr Name]
- -> ([HsTyVarBndr Name] -> TcM r) -- These binders are kind-annotated
+kcHsTyVars :: [LHsTyVarBndr Name]
+ -> ([LHsTyVarBndr Name] -> TcM r) -- These binders are kind-annotated
-- They scope over the thing inside
-> TcM r
kcHsTyVars tvs thing_inside
- = mappM kcHsTyVar tvs `thenM` \ bndrs ->
- tcExtendTyVarKindEnv bndrs $
- thing_inside bndrs
+ = mappM (wrapLocM kcHsTyVar) tvs `thenM` \ bndrs ->
+ tcExtendKindEnvTvs bndrs (thing_inside bndrs)
kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
-- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it
kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind)
------------------
-tcTyVarBndrs :: [HsTyVarBndr Name] -- Kind-annotated binders, which need kind-zonking
+tcTyVarBndrs :: [LHsTyVarBndr Name] -- Kind-annotated binders, which need kind-zonking
-> ([TyVar] -> TcM r)
-> TcM r
-- Used when type-checking types/classes/type-decls
-- Brings into scope immutable TyVars, not mutable ones that require later zonking
tcTyVarBndrs bndrs thing_inside
- = mapM zonk bndrs `thenM` \ tyvars ->
+ = mapM (zonk . unLoc) bndrs `thenM` \ tyvars ->
tcExtendTyVarEnv tyvars (thing_inside tyvars)
where
- zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
- returnM (mkTyVar name kind')
- zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
- returnM (mkTyVar name liftedTypeKind)
+ zonk (KindedTyVar name kind) = do { kind' <- zonkTcKindToKind kind
+ ; return (mkTyVar name kind') }
+ zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $
+ return (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 :: [RenamedHsType] -> 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 ->
- let
- sig_tvs = [ 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
- -- 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 ->
-
- -- Zonk the mutable kinds and bring the tyvars into scope
- -- Rather like tcTyVarBndrs, except that it brings *mutable*
- -- tyvars into scope, not immutable ones
- mapM zonk kinded_tvs `thenM` \ tyvars ->
- tcExtendTyVarEnv tyvars thing_inside
-
+tcHsPatSigType :: UserTypeCtxt
+ -> LHsType Name -- The type signature
+ -> TcM ([TyVar], -- Newly in-scope type variables
+ Type) -- The signature
+-- Used for type-checking type signatures in
+-- (a) patterns e.g f (x::Int) = e
+-- (b) result signatures e.g. g x :: Int = e
+-- (c) RULE forall bndrs e.g. forall (x::Int). f x = x
+
+tcHsPatSigType ctxt hs_ty
+ = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
+ do { -- Find the type variables that are mentioned in the type
+ -- but not already in scope. These are the ones that
+ -- should be bound by the pattern signature
+ in_scope <- getInLocalScope
+ ; let span = getLoc hs_ty
+ sig_tvs = [ L span (UserTyVar n)
+ | n <- nameSetToList (extractHsTyVars hs_ty),
+ not (in_scope n) ]
+
+ -- Behave very like type-checking (HsForAllTy sig_tvs hs_ty),
+ -- except that we want to keep the tvs separate
+ ; (kinded_tvs, kinded_ty) <- kcHsTyVars sig_tvs $ \ kinded_tvs -> do
+ { kinded_ty <- kcTypeType hs_ty
+ ; return (kinded_tvs, kinded_ty) }
+ ; tcTyVarBndrs kinded_tvs $ \ tyvars -> do
+ { sig_ty <- dsHsType kinded_ty
+ ; checkValidType ctxt sig_ty
+ ; return (tyvars, sig_ty)
+ } }
+
+tcPatSig :: UserTypeCtxt
+ -> LHsType Name
+ -> BoxySigmaType
+ -> TcM (TcType, -- The type to use for "inside" the signature
+ [(Name,TcType)]) -- The new bit of type environment, binding
+ -- the scoped type variables
+tcPatSig ctxt sig res_ty
+ = do { (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig
+
+ ; if null sig_tvs then do {
+ -- The type signature binds no type variables,
+ -- and hence is rigid, so use it to zap the res_ty
+ boxyUnify sig_ty res_ty
+ ; return (sig_ty, [])
+
+ } else do {
+ -- Type signature binds at least one scoped type variable
+
+ -- A pattern binding cannot bind scoped type variables
+ -- The renamer fails with a name-out-of-scope error
+ -- if a pattern binding tries to bind a type variable,
+ -- So we just have an ASSERT here
+ ; let in_pat_bind = case ctxt of
+ BindPatSigCtxt -> True
+ other -> False
+ ; ASSERT( not in_pat_bind || null sig_tvs ) return ()
+
+ -- Check that pat_ty is rigid
+ ; checkTc (isRigidTy res_ty) (wobblyPatSig sig_tvs)
+
+ -- Now match the pattern signature against res_ty
+ -- For convenience, and uniform-looking error messages
+ -- we do the matching by allocating meta type variables,
+ -- unifying, and reading out the results.
+ -- This is a strictly local operation.
+ ; box_tvs <- mapM tcInstBoxyTyVar sig_tvs
+ ; boxyUnify (substTyWith sig_tvs (mkTyVarTys box_tvs) sig_ty) res_ty
+ ; sig_tv_tys <- mapM readFilledBox box_tvs
+
+ -- Check that each is bound to a distinct type variable,
+ -- and one that is not already in scope
+ ; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys
+ ; binds_in_scope <- getScopedTyVarBinds
+ ; check binds_in_scope tv_binds
+
+ -- Phew!
+ ; return (res_ty, tv_binds)
+ } }
where
- zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
- newMutTyVar name kind' VanillaTv
- zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
- returnM (mkTyVar name liftedTypeKind)
-\end{code}
-
-
-%************************************************************************
-%* *
-\subsection{Signatures}
-%* *
-%************************************************************************
-
-@tcSigs@ checks the signatures for validity, and returns a list of
-{\em freshly-instantiated} signatures. That is, the types are already
-split up, and have fresh type variables installed. All non-type-signature
-"RenamedSigs" are ignored.
-
-The @TcSigInfo@ contains @TcTypes@ because they are unified with
-the variable's type, and after that checked to see whether they've
-been instantiated.
+ check in_scope [] = return ()
+ check in_scope ((n,ty):rest) = do { check_one in_scope n ty
+ ; check ((n,ty):in_scope) rest }
-\begin{code}
-data TcSigInfo
- = TySigInfo
- TcId -- *Polymorphic* binder for this value...
- -- Has name = N
-
- [TcTyVar] -- tyvars
- TcThetaType -- theta
- TcTauType -- tau
-
- TcId -- *Monomorphic* binder for this value
- -- Does *not* have name = N
- -- Has type tau
-
- [Inst] -- Empty if theta is null, or
- -- (method mono_id) otherwise
-
- SrcLoc -- Of the signature
+ check_one in_scope n ty
+ = do { checkTc (tcIsTyVarTy ty) (scopedNonVar n ty)
+ -- Must bind to a type variable
-instance Outputable TcSigInfo where
- ppr (TySigInfo id tyvars theta tau _ inst loc) =
- ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
+ ; checkTc (null dups) (dupInScope n (head dups) ty)
+ -- Must not bind to the same type variable
+ -- as some other in-scope type variable
-tcSigPolyId :: TcSigInfo -> TcId
-tcSigPolyId (TySigInfo id _ _ _ _ _ _) = id
-
-tcSigMonoId :: TcSigInfo -> TcId
-tcSigMonoId (TySigInfo _ _ _ _ id _ _) = id
-
-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 :: RenamedSig -> TcM TcSigInfo
-
-tcTySig (Sig v ty src_loc)
- = addSrcLoc src_loc $
- 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.
-
- getSrcLocM `thenM` \ src_loc ->
- returnM (TySigInfo poly_id tyvars' theta' tau'
- (instToId inst) [inst] src_loc)
+ ; return () }
+ where
+ dups = [n' | (n',ty') <- in_scope, tcEqType ty' ty]
\end{code}
%************************************************************************
%* *
-\subsection{Errors and contexts}
+ Scoped type variables
%* *
%************************************************************************
-
\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
+pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
+pprHsSigCtxt ctxt hs_ty = vcat [ ptext SLIT("In") <+> pprUserTypeCtxt ctxt <> colon,
+ nest 2 (pp_sig ctxt) ]
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)
+ pp_sig (FunSigCtxt n) = pp_n_colon n
+ pp_sig (ConArgCtxt n) = pp_n_colon n
+ pp_sig (ForSigCtxt n) = pp_n_colon n
+ pp_sig (RuleSigCtxt n) = pp_n_colon n
+ pp_sig other = ppr (unLoc hs_ty)
+
+ pp_n_colon n = ppr n <+> dcolon <+> ppr (unLoc hs_ty)
+
+
+wobblyPatSig sig_tvs
+ = hang (ptext SLIT("A pattern type signature cannot bind scoped type variables")
+ <+> pprQuotedList sig_tvs)
+ 2 (ptext SLIT("unless the pattern has a rigid type context"))
+
+scopedNonVar n ty
+ = vcat [sep [ptext SLIT("The scoped type variable") <+> quotes (ppr n),
+ nest 2 (ptext SLIT("is bound to the type") <+> quotes (ppr ty))],
+ nest 2 (ptext SLIT("You can only bind scoped type variables to type variables"))]
+
+dupInScope n n' ty
+ = hang (ptext SLIT("The scoped type variables") <+> quotes (ppr n) <+> ptext SLIT("and") <+> quotes (ppr n'))
+ 2 (vcat [ptext SLIT("are bound to the same type (variable)"),
+ ptext SLIT("Distinct scoped type variables must be distinct")])
\end{code}
-
-%************************************************************************
-%* *
-\subsection{Errors and contexts}
-%* *
-%************************************************************************
-
-\begin{code}
-wrongThingErr expected thing name
- = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
- where
- pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
- pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
- pp_thing (AGlobal (AnId _)) = ptext SLIT("Identifier")
- pp_thing (AGlobal (ADataCon _)) = ptext SLIT("Data constructor")
- pp_thing (ATyVar _) = ptext SLIT("Type variable")
- pp_thing (ATcId _ _ _) = ptext SLIT("Local identifier")
- pp_thing (ARecTyCon _) = ptext SLIT("Rec tycon")
- pp_thing (ARecClass _) = ptext SLIT("Rec class")
-\end{code}
projects / ghc-hetmet.git / blobdiff