Commit d3149f60 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Tighten up on the kind checking for foralls

In particular,
   (forall a. Num a => ...)
always has kind *, becuase the "=>" really is a function.

It turned out that this was at the bottom of the crash in Trac #7778,
which is now fixed
parent 8a1b7eb6
......@@ -192,11 +192,22 @@ tcHsSigTypeNC ctxt (L loc hs_ty)
-----------------
tcHsInstHead :: UserTypeCtxt -> LHsType Name -> TcM ([TyVar], ThetaType, Class, [Type])
-- Like tcHsSigTypeNC, but for an instance head.
tcHsInstHead ctxt lhs_ty@(L loc hs_ty)
tcHsInstHead user_ctxt lhs_ty@(L loc hs_ty)
= setSrcSpan loc $ -- The "In the type..." context comes from the caller
do { ty <- tcCheckHsTypeAndGen hs_ty constraintKind
; ty <- zonkTcType ty
; checkValidInstance ctxt lhs_ty ty }
do { inst_ty <- tc_inst_head hs_ty
; kvs <- kindGeneralize (tyVarsOfType inst_ty) []
; inst_ty <- zonkTcType (mkForAllTys kvs inst_ty)
; checkValidInstance user_ctxt lhs_ty inst_ty }
tc_inst_head :: HsType Name -> TcM TcType
tc_inst_head (HsForAllTy _ hs_tvs hs_ctxt hs_ty)
= tcHsTyVarBndrs hs_tvs $ \ tvs ->
do { ctxt <- tcHsContext hs_ctxt
; ty <- tc_lhs_type hs_ty ekConstraint -- Body for forall has kind Constraint
; return (mkSigmaTy tvs ctxt ty) }
tc_inst_head hs_ty
= tc_hs_type hs_ty ekConstraint
-----------------
tcHsDeriv :: HsType Name -> TcM ([TyVar], Class, [Type])
......@@ -376,12 +387,18 @@ tc_hs_type hs_ty@(HsAppTy ty1 ty2) exp_kind
(fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
--------- Foralls
tc_hs_type (HsForAllTy _ hs_tvs context ty) exp_kind
tc_hs_type hs_ty@(HsForAllTy _ hs_tvs context ty) exp_kind
= tcHsTyVarBndrs hs_tvs $ \ tvs' ->
-- Do not kind-generalise here! See Note [Kind generalisation]
do { ctxt' <- tcHsContext context
; ty' <- tc_lhs_type ty exp_kind
-- Why exp_kind? See Note [Body kind of forall]
; ty' <- if null (unLoc context) then -- Plain forall, no context
tc_lhs_type ty exp_kind -- Why exp_kind? See Note [Body kind of forall]
else
-- If there is a context, then this forall is really a
-- *function*, so the kind of the result really is *
-- The body kind (result of the function can be * or #, hence ekOpen
do { checkExpectedKind hs_ty liftedTypeKind exp_kind
; tc_lhs_type ty ekOpen }
; return (mkSigmaTy tvs' ctxt' ty') }
--------- Lists, arrays, and tuples
......
......@@ -8,7 +8,7 @@ module TcValidity (
Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
expectedKindInCtxt,
checkValidTheta, checkValidFamPats,
checkValidInstHead, checkValidInstance, validDerivPred,
checkValidInstance, validDerivPred,
checkInstTermination, checkValidTyFamInst, checkTyFamFreeness,
checkConsistentFamInst,
arityErr, badATErr
......@@ -827,11 +827,9 @@ validDerivPred tv_set pred
checkValidInstance :: UserTypeCtxt -> LHsType Name -> Type
-> TcM ([TyVar], ThetaType, Class, [Type])
checkValidInstance ctxt hs_type ty
= do { let (tvs, theta, tau) = tcSplitSigmaTy ty
; case getClassPredTys_maybe tau of {
Nothing -> failWithTc (ptext (sLit "Malformed instance type")) ;
Just (clas,inst_tys) ->
do { setSrcSpan head_loc (checkValidInstHead ctxt clas inst_tys)
| Just (clas,inst_tys) <- getClassPredTys_maybe tau
, inst_tys `lengthIs` classArity clas
= do { setSrcSpan head_loc (checkValidInstHead ctxt clas inst_tys)
; checkValidTheta ctxt theta
-- The Termination and Coverate Conditions
......@@ -853,8 +851,12 @@ checkValidInstance ctxt hs_type ty
; checkTc (checkInstCoverage clas inst_tys)
(instTypeErr clas inst_tys msg) }
; return (tvs, theta, clas, inst_tys) } } }
; return (tvs, theta, clas, inst_tys) }
| otherwise
= failWithTc (ptext (sLit "Malformed instance head:") <+> ppr tau)
where
(tvs, theta, tau) = tcSplitSigmaTy ty
msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
undecidableMsg])
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment