-- Typechecking kinded types
tcHsKindedContext, tcHsKindedType, tcHsBangType,
- tcTyVarBndrs, dsHsType, tcLHsConSig, tcDataKindSig,
+ tcTyVarBndrs, dsHsType, tcLHsConResTy,
+ tcDataKindSig,
tcHsPatSigType, tcAddLetBoundTyVars,
- TcSigInfo(..), mkTcSig,
- TcSigFun, lookupSig
+ TcSigInfo(..), TcSigFun, lookupSig
) 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, LHsBinds, HsExplicitForAll(..),
+ collectSigTysFromHsBinds )
import RnHsSyn ( extractHsTyVars )
import TcRnMonad
-import TcEnv ( tcExtendTyVarEnv, tcExtendKindEnv,
+import TcEnv ( tcExtendTyVarEnv, tcExtendKindEnvTvs,
tcLookup, tcLookupClass, tcLookupTyCon,
TyThing(..), getInLocalScope, wrongThingErr
)
-import TcMType ( newKindVar, tcSkolType, newMetaTyVar,
- zonkTcKindToKind,
+import TcMType ( newKindVar, newMetaTyVar, zonkTcKindToKind,
checkValidType, UserTypeCtxt(..), pprHsSigCtxt
)
import TcUnify ( unifyFunKind, checkExpectedKind )
+import TcIface ( checkWiredInTyCon )
import TcType ( Type, PredType(..), ThetaType,
- SkolemInfo(SigSkol), MetaDetails(Flexi),
+ MetaDetails(Flexi), hoistForAllTys,
TcType, TcTyVar, TcKind, TcThetaType, TcTauType,
- mkTyVarTy, mkFunTy,
- mkForAllTys, mkFunTys, tcEqType, isPredTy,
- mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys,
- tcSplitFunTy_maybe, tcSplitForAllTys )
+ mkFunTy, mkSigmaTy, mkPredTy, mkGenTyConApp,
+ mkTyConApp, mkAppTys, typeKind )
import Kind ( Kind, isLiftedTypeKind, liftedTypeKind, ubxTupleKind,
openTypeKind, argTypeKind, splitKindFunTys )
-import Id ( idName, idType )
-import Var ( TyVar, mkTyVar, tyVarKind )
+import Id ( idName )
+import Var ( TyVar, mkTyVar )
import TyCon ( TyCon, tyConKind )
import Class ( Class, classTyCon )
import Name ( Name, mkInternalName )
import OccName ( mkOccName, tvName )
import NameSet
+import NameEnv
import PrelNames ( genUnitTyConName )
-import Type ( deShadowTy )
-import TysWiredIn ( mkListTy, mkPArrTy, mkTupleTy )
-import Bag ( bagToList )
-import BasicTypes ( Boxity(..) )
+import TysWiredIn ( mkListTy, listTyCon, mkPArrTy, parrTyCon, tupleTyCon )
+import BasicTypes ( Boxity(..), RecFlag )
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 [])
-- 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
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
* 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)
--- AThing _ -> 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 (mkGenTyConApp 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
; return (tyvars, sig_ty) }
}
-tcAddLetBoundTyVars :: LHsBinds Name -> TcM a -> TcM a
+tcAddLetBoundTyVars :: [(RecFlag,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
+ = go (concatMap (collectSigTysFromHsBinds . snd) binds) thing_inside
where
go [] thing_inside = thing_inside
go (hs_ty:hs_tys) thing_inside
\begin{code}
data TcSigInfo
= TcSigInfo {
- sig_id :: TcId, -- *Polymorphic* binder for this value...
- sig_tvs :: [TcTyVar], -- tyvars
- sig_theta :: TcThetaType, -- theta
- sig_tau :: TcTauType, -- tau
- sig_loc :: InstLoc -- The location of the signature
+ 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 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
-
-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
- do { let rigid_info = SigSkol (idName poly_id)
- ; (tyvars', theta', tau') <- tcSkolType rigid_info (idType poly_id)
- ; loc <- getInstLoc (SigOrigin rigid_info)
- ; return (TcSigInfo { sig_id = poly_id, sig_tvs = tyvars',
- sig_theta = theta', sig_tau = tau', sig_loc = 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
+lookupSig sigs = lookupNameEnv env
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)
+ env = mkNameEnv [(idName (sig_id sig), sig) | sig <- sigs]
\end{code}
projects / ghc-hetmet.git / blobdiff