\begin{code}
module TcHsType (
- tcHsSigType, tcHsDeriv,
+ tcHsSigType, tcHsSigTypeNC, tcHsDeriv,
tcHsInstHead, tcHsQuantifiedType,
UserTypeCtxt(..),
-- Typechecking kinded types
tcHsKindedContext, tcHsKindedType, tcHsBangType,
- tcTyVarBndrs, dsHsType, tcLHsConResTy,
- tcDataKindSig,
+ tcTyVarBndrs, dsHsType, kcHsLPred, dsHsLPred,
+ tcDataKindSig, ExpKind(..), EkCtxt(..),
-- Pattern type signatures
tcHsPatSigType, tcPatSig
#include "HsVersions.h"
+#ifdef GHCI /* Only if bootstrapped */
+import {-# SOURCE #-} TcSplice( kcSpliceType )
+#endif
+
import HsSyn
import RnHsSyn
import TcRnMonad
import TcType
import {- Kind parts of -} Type
import Var
-import Coercion
+import VarSet
import TyCon
import Class
import Name
-import OccName
import NameSet
import PrelNames
import TysWiredIn
import BasicTypes
import SrcLoc
+import Util
import UniqSupply
import Outputable
import FastString
-
-import Control.Monad
\end{code}
%************************************************************************
\begin{code}
-tcHsSigType :: UserTypeCtxt -> LHsType Name -> TcM Type
+tcHsSigType, tcHsSigTypeNC :: 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
+ tcHsSigTypeNC ctxt hs_ty
+
+tcHsSigTypeNC ctxt hs_ty
+ = do { (kinded_ty, _kind) <- kc_lhs_type hs_ty
+ -- The kind is checked by checkValidType, and isn't necessarily
+ -- of kind * in a Template Haskell quote eg [t| Maybe |]
; ty <- tcHsKindedType kinded_ty
; checkValidType ctxt ty
; return ty }
-tcHsInstHead :: LHsType Name -> TcM ([TyVar], ThetaType, Type)
+tcHsInstHead :: LHsType Name -> TcM ([TyVar], ThetaType, Class, [Type])
-- Typecheck an instance head. We can't use
-- tcHsSigType, because it's not a valid user type.
-tcHsInstHead hs_ty
- = do { kinded_ty <- kcHsSigType hs_ty
- ; poly_ty <- tcHsKindedType kinded_ty
- ; return (tcSplitSigmaTy poly_ty) }
+tcHsInstHead (L loc hs_ty)
+ = setSrcSpan loc $ -- No need for an "In the type..." context
+ -- because that comes from the caller
+ do { kinded_ty <- kc_inst_head hs_ty
+ ; ds_inst_head kinded_ty }
+ where
+ kc_inst_head ty@(HsPredTy pred@(HsClassP {}))
+ = do { (pred', kind) <- kc_pred pred
+ ; checkExpectedKind ty kind ekLifted
+ ; return (HsPredTy pred') }
+ kc_inst_head (HsForAllTy exp tv_names context (L loc ty))
+ = kcHsTyVars tv_names $ \ tv_names' ->
+ do { ctxt' <- kcHsContext context
+ ; ty' <- kc_inst_head ty
+ ; return (HsForAllTy exp tv_names' ctxt' (L loc ty')) }
+ kc_inst_head _ = failWithTc (ptext (sLit "Malformed instance type"))
+
+ ds_inst_head (HsPredTy (HsClassP cls_name tys))
+ = do { clas <- tcLookupClass cls_name
+ ; arg_tys <- dsHsTypes tys
+ ; return ([], [], clas, arg_tys) }
+ ds_inst_head (HsForAllTy _ tvs ctxt (L _ tau))
+ = tcTyVarBndrs tvs $ \ tvs' ->
+ do { ctxt' <- mapM dsHsLPred (unLoc ctxt)
+ ; (tvs_r, ctxt_r, cls, tys) <- ds_inst_head tau
+ ; return (tvs' ++ tvs_r, ctxt' ++ ctxt_r , cls, tys) }
+ ds_inst_head _ = panic "ds_inst_head"
tcHsQuantifiedType :: [LHsTyVarBndr Name] -> LHsType Name -> TcM ([TyVar], Type)
-- Behave very like type-checking (HsForAllTy sig_tvs hs_ty),
---------------------------
kcLiftedType :: LHsType Name -> TcM (LHsType Name)
-- The type ty must be a *lifted* *type*
-kcLiftedType ty = kc_check_lhs_type ty liftedTypeKind
+kcLiftedType ty = kc_check_lhs_type ty ekLifted
---------------------------
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 = kc_check_lhs_type ty openTypeKind
+kcTypeType ty = kc_check_lhs_type ty ekOpen
---------------------------
-kcCheckLHsType :: LHsType Name -> TcKind -> TcM (LHsType Name)
+kcCheckLHsType :: LHsType Name -> ExpKind -> TcM (LHsType Name)
kcCheckLHsType ty kind = addKcTypeCtxt ty $ kc_check_lhs_type ty kind
-kc_check_lhs_type :: LHsType Name -> TcKind -> TcM (LHsType Name)
+kc_check_lhs_type :: LHsType Name -> ExpKind -> TcM (LHsType Name)
-- Check that the type has the specified kind
-- Be sure to use checkExpectedKind, rather than simply unifying
-- with OpenTypeKind, because it gives better error messages
do { ty' <- kc_check_hs_type ty exp_kind
; return (L span ty') }
-kc_check_lhs_types :: [(LHsType Name,TcKind)] -> TcM [LHsType Name]
+kc_check_lhs_types :: [(LHsType Name, ExpKind)] -> TcM [LHsType Name]
kc_check_lhs_types tys_w_kinds
= mapM kc_arg tys_w_kinds
where
---------------------------
-kc_check_hs_type :: HsType Name -> TcKind -> TcM (HsType Name)
+kc_check_hs_type :: HsType Name -> ExpKind -> TcM (HsType Name)
-- First some special cases for better error messages
-- when we know the expected kind
; arg_tys' <- kcCheckApps fun_ty fun_kind arg_tys ty exp_kind
; return (mkHsAppTys fun_ty' arg_tys') }
-kc_check_hs_type ty@(HsPredTy (HsClassP cls tys)) exp_kind
- = do { cls_kind <- kcClass cls
- ; tys' <- kcCheckApps cls cls_kind tys ty exp_kind
- ; return (HsPredTy (HsClassP cls tys')) }
-
-- This is the general case: infer the kind and compare
kc_check_hs_type ty exp_kind
= do { (ty', act_kind) <- kc_hs_type ty
strip (HsBangTy _ (L _ ty)) = strip ty
strip (HsForAllTy _ _ _ (L _ ty)) = strip ty
strip ty = ty
-
\end{code}
Here comes the main function
= return (HsNumTy n, liftedTypeKind)
kc_hs_type (HsKindSig ty k) = do
- ty' <- kc_check_lhs_type ty k
+ ty' <- kc_check_lhs_type ty (EK k EkKindSig)
return (HsKindSig ty' k, k)
kc_hs_type (HsTupleTy Boxed tys) = do
return (HsTupleTy Unboxed tys', ubxTupleKind)
kc_hs_type (HsFunTy ty1 ty2) = do
- ty1' <- kc_check_lhs_type ty1 argTypeKind
+ ty1' <- kc_check_lhs_type ty1 (EK argTypeKind EkUnk)
ty2' <- kcTypeType ty2
return (HsFunTy ty1' ty2', liftedTypeKind)
where
(fun_ty, arg_tys) = splitHsAppTys ty1 ty2
-kc_hs_type (HsPredTy (HsEqualP _ _))
- = wrongEqualityErr
+kc_hs_type (HsPredTy pred)
+ = wrongPredErr pred
-kc_hs_type (HsPredTy pred) = do
- pred' <- kcHsPred pred
- return (HsPredTy pred', liftedTypeKind)
+kc_hs_type (HsCoreTy ty)
+ = return (HsCoreTy ty, typeKind ty)
kc_hs_type (HsForAllTy exp tv_names context ty)
= kcHsTyVars tv_names $ \ tv_names' ->
; return (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind) }
-kc_hs_type (HsBangTy b ty) = do
- (ty', kind) <- kc_lhs_type ty
- return (HsBangTy b ty', kind)
+kc_hs_type (HsBangTy b ty)
+ = do { (ty', kind) <- kc_lhs_type ty
+ ; return (HsBangTy b ty', kind) }
+
+kc_hs_type ty@(HsRecTy _)
+ = failWithTc (ptext (sLit "Unexpected record type") <+> ppr ty)
+ -- Record types (which only show up temporarily in constructor signatures)
+ -- should have been removed by now
-kc_hs_type ty@(HsSpliceTy _)
- = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty)
+#ifdef GHCI /* Only if bootstrapped */
+kc_hs_type (HsSpliceTy sp fvs _) = kcSpliceType sp fvs
+#else
+kc_hs_type ty@(HsSpliceTy {}) = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty)
+#endif
+
+kc_hs_type (HsQuasiQuoteTy {}) = panic "kc_hs_type" -- Eliminated by renamer
-- remove the doc nodes here, no need to worry about the location since
-- its the same for a doc node and it's child type node
-> [LHsType Name] -- Arg types
-> TcM ([LHsType Name], TcKind) -- Kind-checked args
kcApps the_fun fun_kind args
- = do { (args_w_kinds, res_kind) <- splitFunKind the_fun fun_kind args
+ = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
; args' <- kc_check_lhs_types args_w_kinds
; return (args', res_kind) }
kcCheckApps :: Outputable a => a -> TcKind -> [LHsType Name]
-> HsType Name -- The type being checked (for err messages only)
- -> TcKind -- Expected kind
+ -> ExpKind -- Expected kind
-> TcM [LHsType Name]
kcCheckApps the_fun fun_kind args ty exp_kind
- = do { (args_w_kinds, res_kind) <- splitFunKind the_fun fun_kind args
+ = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
; checkExpectedKind ty res_kind exp_kind
-- Check the result kind *before* checking argument kinds
-- This improves error message; Trac #2994
-- never used
---------------------------
-splitFunKind :: Outputable a => a -> TcKind -> [b] -> TcM ([(b,TcKind)], TcKind)
-splitFunKind _ fk [] = return ([], fk)
-splitFunKind the_fun fk (arg:args)
- = do { mb_fk <- unifyFunKind fk
+splitFunKind :: SDoc -> Int -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind)
+splitFunKind _ _ fk [] = return ([], fk)
+splitFunKind the_fun arg_no fk (arg:args)
+ = do { mb_fk <- matchExpectedFunKind fk
; case mb_fk of
Nothing -> failWithTc too_many_args
- Just (ak,fk') -> do { (aks, rk) <- splitFunKind the_fun fk' args
- ; return ((arg,ak):aks, rk) } }
+ Just (ak,fk') -> do { (aks, rk) <- splitFunKind the_fun (arg_no+1) fk' args
+ ; return ((arg, EK ak (EkArg the_fun arg_no)):aks, rk) } }
where
- too_many_args = quotes (ppr the_fun) <+>
+ too_many_args = quotes the_fun <+>
ptext (sLit "is applied to too many type arguments")
---------------------------
kcHsLPred = wrapLocM kcHsPred
kcHsPred :: HsPred Name -> TcM (HsPred Name)
-kcHsPred pred = do -- Checks that the result is of kind liftedType
+kcHsPred pred = do -- Checks that the result is a type kind
(pred', kind) <- kc_pred pred
- checkExpectedKind pred kind liftedTypeKind
+ checkExpectedKind pred kind ekOpen
return pred'
---------------------------
-- application (reason: used from TcDeriv)
kc_pred (HsIParam name ty)
= do { (ty', kind) <- kc_lhs_type ty
- ; return (HsIParam name ty', kind)
- }
+ ; return (HsIParam name ty', kind) }
kc_pred (HsClassP cls tys)
= do { kind <- kcClass cls
; (tys', res_kind) <- kcApps cls kind tys
- ; return (HsClassP cls tys', res_kind)
- }
+ ; return (HsClassP cls tys', res_kind) }
kc_pred (HsEqualP ty1 ty2)
= do { (ty1', kind1) <- kc_lhs_type ty1
--- ; checkExpectedKind ty1 kind1 liftedTypeKind
; (ty2', kind2) <- kc_lhs_type ty2
--- ; checkExpectedKind ty2 kind2 liftedTypeKind
- ; checkExpectedKind ty2 kind2 kind1
- ; return (HsEqualP ty1' ty2', liftedTypeKind)
- }
+ ; checkExpectedKind ty2 kind2 (EK kind1 EkEqPred)
+ ; return (HsEqualP ty1' ty2', unliftedTypeKind) }
---------------------------
kcTyVar :: Name -> TcM TcKind
kcTyVar name = do -- Could be a tyvar or a tycon
- traceTc (text "lk1" <+> ppr name)
+ traceTc "lk1" (ppr name)
thing <- tcLookup name
- traceTc (text "lk2" <+> ppr name <+> ppr thing)
+ traceTc "lk2" (ppr name <+> ppr thing)
case thing of
ATyVar _ ty -> return (typeKind ty)
AThing kind -> return kind
ds_type (HsParTy ty) -- Remove the parentheses markers
= dsHsType ty
-ds_type ty@(HsBangTy _ _) -- No bangs should be here
+ds_type ty@(HsBangTy {}) -- No bangs should be here
= failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty)
+ds_type ty@(HsRecTy {}) -- No bangs should be here
+ = failWithTc (ptext (sLit "Unexpected record type:") <+> ppr ty)
+
ds_type (HsKindSig ty _)
= dsHsType ty -- Kind checking done already
tau <- dsHsType ty
return (mkSigmaTy tyvars theta tau)
-ds_type (HsSpliceTy {}) = panic "ds_type: HsSpliceTy"
-
ds_type (HsDocTy ty _) -- Remove the doc comment
= dsHsType ty
+ds_type (HsSpliceTy _ _ kind)
+ = do { kind' <- zonkTcKindToKind kind
+ ; newFlexiTyVarTy kind' }
+
+ds_type (HsQuasiQuoteTy {}) = panic "ds_type" -- Eliminated by renamer
+ds_type (HsCoreTy ty) = return ty
+
dsHsTypes :: [LHsType Name] -> TcM [Type]
dsHsTypes arg_tys = mapM dsHsType arg_tys
\end{code}
}
\end{code}
-GADT constructor signatures
-
\begin{code}
-tcLHsConResTy :: LHsType Name -> TcM (TyCon, [TcType])
-tcLHsConResTy (L span res_ty)
- = setSrcSpan span $
- case get_args res_ty [] of
- (HsTyVar tc_name, args)
- -> do { args' <- mapM dsHsType args
- ; thing <- tcLookup tc_name
- ; case thing of
- AGlobal (ATyCon tc) -> return (tc, args')
- _ -> failWithTc (badGadtDecl res_ty) }
- _ -> failWithTc (badGadtDecl res_ty)
- where
- -- We can't call dsHsType on res_ty, and then do tcSplitTyConApp_maybe
- -- because that causes a black hole, and for good reason. Building
- -- the type means expanding type synonyms, and we can't do that
- -- inside the "knot". So we have to work by steam.
- get_args (HsAppTy (L _ fun) arg) args = get_args fun (arg:args)
- get_args (HsParTy (L _ ty)) args = get_args ty args
- get_args (HsOpTy ty1 (L _ tc) ty2) args = (HsTyVar tc, ty1:ty2:args)
- get_args ty args = (ty, args)
-
-badGadtDecl :: HsType Name -> SDoc
-badGadtDecl ty
- = hang (ptext (sLit "Malformed constructor result type:"))
- 2 (ppr ty)
-
addKcTypeCtxt :: LHsType Name -> TcM a -> TcM a
-- Wrap a context around only if we want to show that contexts.
addKcTypeCtxt (L _ (HsPredTy _)) thing = thing
-> ([LHsTyVarBndr Name] -> TcM r) -- These binders are kind-annotated
-- They scope over the thing inside
-> TcM r
-kcHsTyVars tvs thing_inside = do
- bndrs <- mapM (wrapLocM kcHsTyVar) tvs
- tcExtendKindEnvTvs bndrs (thing_inside bndrs)
+kcHsTyVars tvs thing_inside
+ = do { kinded_tvs <- mapM (wrapLocM kcHsTyVar) tvs
+ ; tcExtendKindEnvTvs kinded_tvs thing_inside }
kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
-- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it
-kcHsTyVar (UserTyVar name) = KindedTyVar name <$> newKindVar
-kcHsTyVar (KindedTyVar name kind) = return (KindedTyVar name kind)
+kcHsTyVar (UserTyVar name _) = UserTyVar name <$> newKindVar
+kcHsTyVar tv@(KindedTyVar {}) = return tv
------------------
tcTyVarBndrs :: [LHsTyVarBndr Name] -- Kind-annotated binders, which need kind-zonking
tyvars <- mapM (zonk . unLoc) bndrs
tcExtendTyVarEnv tyvars (thing_inside tyvars)
where
- zonk (KindedTyVar name kind) = do { kind' <- zonkTcKindToKind kind
- ; return (mkTyVar name kind') }
- zonk (UserTyVar name) = WARN( True, ptext (sLit "Un-kinded tyvar") <+> ppr name )
- return (mkTyVar name liftedTypeKind)
+ zonk (UserTyVar name kind) = do { kind' <- zonkTcKindToKind kind
+ ; return (mkTyVar name kind') }
+ zonk (KindedTyVar name kind) = return (mkTyVar name kind)
-----------------------------------
tcDataKindSig :: Maybe Kind -> TcM [TyVar]
-- 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) ]
+ sig_tvs = userHsTyVarBndrs $ map (L span) $
+ filterOut in_scope $
+ nameSetToList (extractHsTyVars hs_ty)
; (tyvars, sig_ty) <- tcHsQuantifiedType sig_tvs hs_ty
; checkValidType ctxt sig_ty
tcPatSig :: UserTypeCtxt
-> LHsType Name
- -> BoxySigmaType
+ -> TcSigmaType
-> TcM (TcType, -- The type to use for "inside" the signature
[(Name, TcType)], -- The new bit of type environment, binding
-- the scoped type variables
- CoercionI) -- Coercion due to unification with actual ty
+ HsWrapper) -- Coercion due to unification with actual ty
+ -- Of shape: res_ty ~ sig_ty
tcPatSig ctxt sig res_ty
= do { (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig
+ -- sig_tvs are the type variables free in 'sig',
+ -- and not already in scope. These are the ones
+ -- that should be brought into scope
; 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
- coi <- boxyUnify sig_ty res_ty
- ; return (sig_ty, [], coi)
+ wrap <- tcSubType PatSigOrigin (SigSkol ctxt) res_ty sig_ty
+ ; return (sig_ty, [], wrap)
} else do {
-- Type signature binds at least one scoped type variable
_ -> 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
- ; coi <- 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
+ -- Check that all newly-in-scope tyvars are in fact
+ -- constrained by the pattern. This catches tiresome
+ -- cases like
+ -- type T a = Int
+ -- f :: Int -> Int
+ -- f (x :: T a) = ...
+ -- Here 'a' doesn't get a binding. Sigh
+ ; let bad_tvs = filterOut (`elemVarSet` exactTyVarsOfType sig_ty) sig_tvs
+ ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
+
+ -- Now do a subsumption check of the pattern signature against res_ty
+ ; sig_tvs' <- tcInstSigTyVars sig_tvs
+ ; let sig_ty' = substTyWith sig_tvs sig_tv_tys' sig_ty
+ sig_tv_tys' = mkTyVarTys sig_tvs'
+ ; wrap <- tcSubType PatSigOrigin (SigSkol ctxt) res_ty sig_ty'
+
+ -- Check that each is bound to a distinct type variable,
+ -- and one that is not already in scope
; binds_in_scope <- getScopedTyVarBinds
+ ; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys'
; check binds_in_scope tv_binds
- -- Phew!
- ; return (res_ty, tv_binds, coi)
+ -- Phew!
+ ; return (sig_ty', tv_binds, wrap)
} }
where
check _ [] = return ()
; check ((n,ty):in_scope) rest }
check_one in_scope n ty
- = do { checkTc (tcIsTyVarTy ty) (scopedNonVar n ty)
- -- Must bind to a type variable
-
- ; checkTc (null dups) (dupInScope n (head dups) ty)
+ = checkTc (null dups) (dupInScope n (head dups) ty)
-- Must not bind to the same type variable
-- as some other in-scope type variable
-
- ; return () }
where
dups = [n' | (n',ty') <- in_scope, tcEqType ty' ty]
\end{code}
%************************************************************************
+%* *
+ Checking kinds
+%* *
+%************************************************************************
+
+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
+
+\begin{code}
+-- The ExpKind datatype means "expected kind" and contains
+-- some info about just why that kind is expected, to improve
+-- the error message on a mis-match
+data ExpKind = EK TcKind EkCtxt
+data EkCtxt = EkUnk -- Unknown context
+ | EkEqPred -- Second argument of an equality predicate
+ | EkKindSig -- Kind signature
+ | EkArg SDoc Int -- Function, arg posn, expected kind
+
+
+ekLifted, ekOpen :: ExpKind
+ekLifted = EK liftedTypeKind EkUnk
+ekOpen = EK openTypeKind EkUnk
+
+checkExpectedKind :: Outputable a => a -> TcKind -> ExpKind -> TcM ()
+-- A fancy wrapper for 'unifyKind', which tries
+-- to give decent error messages.
+-- (checkExpectedKind ty act_kind exp_kind)
+-- checks that the actual kind act_kind is compatible
+-- with the expected kind exp_kind
+-- The first argument, ty, is used only in the error message generation
+checkExpectedKind ty act_kind (EK exp_kind ek_ctxt)
+ | act_kind `isSubKind` exp_kind -- Short cut for a very common case
+ = return ()
+ | otherwise = do
+ (_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind)
+ case mb_r of
+ Just _ -> return () -- Unification succeeded
+ Nothing -> do
+
+ -- So there's definitely an error
+ -- Now to find out what sort
+ exp_kind <- zonkTcKind exp_kind
+ act_kind <- zonkTcKind act_kind
+
+ env0 <- tcInitTidyEnv
+ let (exp_as, _) = splitKindFunTys exp_kind
+ (act_as, _) = splitKindFunTys act_kind
+ n_exp_as = length exp_as
+ n_act_as = length act_as
+
+ (env1, tidy_exp_kind) = tidyKind env0 exp_kind
+ (env2, tidy_act_kind) = tidyKind env1 act_kind
+
+ err | n_exp_as < n_act_as -- E.g. [Maybe]
+ = quotes (ppr 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
+ | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
+ = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
+ <+> ptext (sLit "is unlifted")
+
+ | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
+ = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
+ <+> ptext (sLit "is lifted")
+
+ | otherwise -- E.g. Monad [Int]
+ = ptext (sLit "Kind mis-match")
+
+ more_info = sep [ expected_herald ek_ctxt <+> ptext (sLit "kind")
+ <+> quotes (pprKind tidy_exp_kind) <> comma,
+ ptext (sLit "but") <+> quotes (ppr ty) <+>
+ ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
+
+ expected_herald EkUnk = ptext (sLit "Expected")
+ expected_herald EkKindSig = ptext (sLit "An enclosing kind signature specified")
+ expected_herald EkEqPred = ptext (sLit "The left argument of the equality predicate had")
+ expected_herald (EkArg fun arg_no)
+ = ptext (sLit "The") <+> speakNth arg_no <+> ptext (sLit "argument of")
+ <+> quotes fun <+> ptext (sLit ("should have"))
+
+ failWithTcM (env2, err $$ more_info)
+\end{code}
+
+%************************************************************************
%* *
Scoped type variables
%* *
\begin{code}
pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
-pprHsSigCtxt ctxt hs_ty = vcat [ ptext (sLit "In") <+> pprUserTypeCtxt ctxt <> colon,
+pprHsSigCtxt ctxt hs_ty = sep [ ptext (sLit "In") <+> pprUserTypeCtxt ctxt <> colon,
nest 2 (pp_sig ctxt) ]
where
pp_sig (FunSigCtxt n) = pp_n_colon n
pp_n_colon n = ppr n <+> dcolon <+> ppr (unLoc hs_ty)
-wobblyPatSig :: [Var] -> SDoc
-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 :: Name -> Type -> SDoc
-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"))]
+badPatSigTvs :: TcType -> [TyVar] -> SDoc
+badPatSigTvs sig_ty bad_tvs
+ = vcat [ fsep [ptext (sLit "The type variable") <> plural bad_tvs,
+ quotes (pprWithCommas ppr bad_tvs),
+ ptext (sLit "should be bound by the pattern signature") <+> quotes (ppr sig_ty),
+ ptext (sLit "but are actually discarded by a type synonym") ]
+ , ptext (sLit "To fix this, expand the type synonym")
+ , ptext (sLit "[Note: I hope to lift this restriction in due course]") ]
dupInScope :: Name -> Name -> Type -> SDoc
dupInScope n n' _
2 (vcat [ptext (sLit "are bound to the same type (variable)"),
ptext (sLit "Distinct scoped type variables must be distinct")])
-wrongEqualityErr :: TcM (HsType Name, TcKind)
-wrongEqualityErr
- = failWithTc (text "Equality predicate used as a type")
+wrongPredErr :: HsPred Name -> TcM (HsType Name, TcKind)
+wrongPredErr pred = failWithTc (text "Predicate used as a type:" <+> ppr pred)
\end{code}