-- Typechecking kinded types
tcHsKindedContext, tcHsKindedType, tcHsBangType,
- tcTyVarBndrs, dsHsType, tcLHsConSig, tcDataKindSig,
+ tcTyVarBndrs, dsHsType, tcLHsConResTy,
+ tcDataKindSig,
- tcHsPatSigType, tcAddLetBoundTyVars,
-
- TcSigInfo(..), TcSigFun, lookupSig
+ -- Pattern type signatures
+ tcHsPatSigType, tcPatSig
) where
#include "HsVersions.h"
-import HsSyn ( HsType(..), LHsType, HsTyVarBndr(..), LHsTyVarBndr, HsBang,
- LHsContext, HsPred(..), LHsPred, LHsBinds,
- getBangStrictness, collectSigTysFromHsBinds )
+import HsSyn ( HsType(..), LHsType, HsTyVarBndr(..), LHsTyVarBndr,
+ LHsContext, HsPred(..), LHsPred, HsExplicitForAll(..) )
import RnHsSyn ( extractHsTyVars )
import TcRnMonad
-import TcEnv ( tcExtendTyVarEnv, tcExtendKindEnv,
+import TcEnv ( tcExtendTyVarEnv, tcExtendKindEnvTvs,
tcLookup, tcLookupClass, tcLookupTyCon,
- TyThing(..), getInLocalScope, wrongThingErr
+ TyThing(..), getInLocalScope, getScopedTyVarBinds,
+ wrongThingErr
)
-import TcMType ( newKindVar, newMetaTyVar, zonkTcKindToKind,
- checkValidType, UserTypeCtxt(..), pprHsSigCtxt
+import TcMType ( newKindVar,
+ zonkTcKindToKind,
+ tcInstBoxyTyVar, readFilledBox,
+ checkValidType
)
-import TcUnify ( unifyFunKind, checkExpectedKind )
-import TcType ( Type, PredType(..), ThetaType,
- MetaDetails(Flexi), hoistForAllTys,
- TcType, TcTyVar, TcKind, TcThetaType, TcTauType,
- mkForAllTys, mkFunTys, tcEqType, isPredTy, mkFunTy,
- mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys,
- tcSplitFunTy_maybe, tcSplitForAllTys, typeKind )
+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 Id ( idName )
-import Var ( TyVar, mkTyVar )
+import Var ( TyVar, mkTyVar, tyVarName )
import TyCon ( TyCon, tyConKind )
import Class ( Class, classTyCon )
import Name ( Name, mkInternalName )
import OccName ( mkOccName, tvName )
import NameSet
import PrelNames ( genUnitTyConName )
-import Type ( deShadowTy )
-import TysWiredIn ( mkListTy, mkPArrTy, mkTupleTy )
-import Bag ( bagToList )
+import TysWiredIn ( mkListTy, listTyCon, mkPArrTy, parrTyCon, tupleTyCon )
import BasicTypes ( Boxity(..) )
-import SrcLoc ( Located(..), unLoc, noLoc, srcSpanStart )
+import SrcLoc ( Located(..), unLoc, noLoc, getLoc, srcSpanStart )
import UniqSupply ( uniqsFromSupply )
import Outputable
-import List ( nubBy )
\end{code}
; 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 [])
-- 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
-- with OpenTypeKind, because it gives better error messages
kcCheckHsType (L span ty) exp_kind
= setSrcSpan span $
- kc_hs_type ty `thenM` \ (ty', act_kind) ->
- checkExpectedKind ty act_kind exp_kind `thenM_`
- returnM (L span ty')
+ 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
* Zonks any kinds
It cannot fail, and does no validity checking, except for
-structural matters, such as spurious ! annotations.
+structural matters, such as
+ (a) spurious ! annotations.
+ (b) a class used as a type
\begin{code}
dsHsType :: LHsType Name -> TcM Type
= dsHsType ty -- Kind checking done already
ds_type (HsListTy ty)
- = dsHsType ty `thenM` \ tau_ty ->
+ = dsHsType ty `thenM` \ tau_ty ->
+ checkWiredInTyCon listTyCon `thenM_`
returnM (mkListTy tau_ty)
ds_type (HsPArrTy ty)
- = dsHsType ty `thenM` \ tau_ty ->
+ = dsHsType ty `thenM` \ tau_ty ->
+ checkWiredInTyCon parrTyCon `thenM_`
returnM (mkPArrTy tau_ty)
ds_type (HsTupleTy boxity tys)
- = dsHsTypes tys `thenM` \ tau_tys ->
- returnM (mkTupleTy boxity (length tys) tau_tys)
+ = dsHsTypes tys `thenM` \ tau_tys ->
+ checkWiredInTyCon tycon `thenM_`
+ returnM (mkTyConApp tycon tau_tys)
+ where
+ tycon = tupleTyCon boxity (length tys)
ds_type (HsFunTy ty1 ty2)
= dsHsType ty1 `thenM` \ tau_ty1 ->
ds_var_app name arg_tys
= tcLookup name `thenM` \ thing ->
case thing of
- ATyVar _ ty -> returnM (mkAppTys ty arg_tys)
- AGlobal (ATyCon 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}
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) }
-
---------
+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 _ = failWithTc (badGadtDecl ty)
-gadtSigCtxt ty
- = hang (ptext SLIT("In the signature of a data constructor:"))
+gadtResCtxt ty
+ = hang (ptext SLIT("In the result type of a data constructor:"))
2 (ppr ty)
badGadtDecl ty
- = hang (ptext SLIT("Malformed constructor signature:"))
+ = hang (ptext SLIT("Malformed constructor result type:"))
2 (ppr ty)
+
+typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
\end{code}
%************************************************************************
-> TcM r
kcHsTyVars tvs thing_inside
= mappM (wrapLocM kcHsTyVar) tvs `thenM` \ bndrs ->
- tcExtendKindEnv [(n,k) | L _ (KindedTyVar n k) <- bndrs]
- (thing_inside 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
= 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 (KindedTyVar name kind) = do { kind' <- zonkTcKindToKind kind
+ ; return (mkTyVar name kind') }
zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $
- returnM (mkTyVar name liftedTypeKind)
+ return (mkTyVar name liftedTypeKind)
-----------------------------------
tcDataKindSig :: Maybe Kind -> TcM [TyVar]
it with expected_ty afterwards
\begin{code}
-tcPatSigBndrs :: LHsType Name
- -> TcM ([TcTyVar], -- Brought into scope
- LHsType Name) -- Kinded, but not yet desugared
+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
-tcPatSigBndrs hs_ty
- = do { in_scope <- getInLocalScope
- ; span <- getSrcSpanM
- ; let sig_tvs = [ L span (UserTyVar n)
+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) ]
- -- 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
+ -- 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) }
-
- -- Zonk the mutable kinds and bring the tyvars into scope
- -- 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
- ; tyvars <- mapM (zonk . unLoc) kinded_tvs
- ; return (tyvars, 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' ->
- 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
+ check in_scope [] = return ()
+ check in_scope ((n,ty):rest) = do { check_one in_scope n ty
+ ; check ((n,ty):in_scope) rest }
-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) }
- }
+ check_one in_scope n ty
+ = do { checkTc (tcIsTyVarTy ty) (scopedNonVar n ty)
+ -- Must bind to a type variable
-tcAddLetBoundTyVars :: LHsBinds Name -> TcM a -> TcM a
--- Turgid funciton, used for type variables bound by the patterns of a let binding
+ ; checkTc (null dups) (dupInScope n (head dups) ty)
+ -- Must not bind to the same type variable
+ -- as some other in-scope type variable
-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) }
+ ; return () }
+ where
+ dups = [n' | (n',ty') <- in_scope, tcEqType ty' ty]
\end{code}
%************************************************************************
%* *
-\subsection{Signatures}
+ Scoped type variables
%* *
%************************************************************************
-@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.
-
\begin{code}
-data TcSigInfo
- = TcSigInfo {
- sig_id :: TcId, -- *Polymorphic* binder for this value...
-
- sig_scoped :: [Name], -- Names for any scoped type variables
- -- Invariant: correspond 1-1 with an initial
- -- segment of sig_tvs (see Note [Scoped])
-
- sig_tvs :: [TcTyVar], -- Instantiated type variables
- -- See Note [Instantiate sig]
-
- 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 (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
+pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
+pprHsSigCtxt ctxt hs_ty = vcat [ ptext SLIT("In") <+> pprUserTypeCtxt ctxt <> colon,
+ nest 2 (pp_sig ctxt) ]
+ where
+ 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}