-- Typechecking kinded types
tcHsKindedContext, tcHsKindedType, tcHsBangType,
- tcTyVarBndrs, dsHsType, tcLHsConResTy,
+ tcTyVarBndrs, dsHsType,
tcDataKindSig, ExpKind(..), EkCtxt(..),
-- Pattern type signatures
import TcType
import {- Kind parts of -} Type
import Var
+import VarSet
import Coercion
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}
tcHsInstHead :: LHsType Name -> TcM ([TyVar], ThetaType, 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 ty)
+ = setSrcSpan loc $ -- No need for an "In the type..." context
+ tc_inst_head ty -- because that comes from the caller
+ where
+ -- tc_inst_head expects HsPredTy, which isn't usually even allowed
+ tc_inst_head (HsPredTy pred)
+ = do { pred' <- kcHsPred pred
+ ; pred'' <- dsHsPred pred'
+ ; return ([], [], mkPredTy pred'') }
+
+ tc_inst_head (HsForAllTy _ tvs ctxt (L _ (HsPredTy pred)))
+ = kcHsTyVars tvs $ \ tvs' ->
+ do { ctxt' <- kcHsContext ctxt
+ ; pred' <- kcHsPred pred
+ ; tcTyVarBndrs tvs' $ \ tvs'' ->
+ do { ctxt'' <- mapM dsHsLPred (unLoc ctxt')
+ ; pred'' <- dsHsPred pred'
+ ; return (tvs'', ctxt'', mkPredTy pred'') } }
+
+ tc_inst_head _ = failWithTc (ptext (sLit "Malformed instance type"))
tcHsQuantifiedType :: [LHsTyVarBndr Name] -> LHsType Name -> TcM ([TyVar], Type)
-- Behave very like type-checking (HsForAllTy sig_tvs hs_ty),
; 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
where
(fun_ty, arg_tys) = splitHsAppTys ty1 ty2
-kc_hs_type (HsPredTy (HsEqualP _ _))
- = wrongEqualityErr
-
-kc_hs_type (HsPredTy pred) = do
- pred' <- kcHsPred pred
- return (HsPredTy pred', liftedTypeKind)
+kc_hs_type (HsPredTy pred)
+ = wrongPredErr pred
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
#ifdef GHCI /* Only if bootstrapped */
-kc_hs_type (HsSpliceTy sp) = kcSpliceType sp
+kc_hs_type (HsSpliceTy sp fvs _) = kcSpliceType sp fvs
#else
-kc_hs_type ty@(HsSpliceTy _) = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty)
+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
kc_hs_type (HsDocTy ty _)
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
+
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
-- Check that pat_ty is rigid
; checkTc (isRigidTy res_ty) (wobblyPatSig sig_tvs)
+ -- 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 match the pattern signature against res_ty
-- For convenience, and uniform-looking error messages
-- we do the matching by allocating meta 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
<+> pprQuotedList sig_tvs)
2 (ptext (sLit "unless the pattern has a rigid type context"))
+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]") ]
+
scopedNonVar :: Name -> Type -> SDoc
scopedNonVar n ty
= vcat [sep [ptext (sLit "The scoped type variable") <+> quotes (ppr 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}