[commit: ghc] master: Tighten up on the kind checking for foralls (d3149f6)

[Simon Peyton Jones]

Repository : http://darcs.haskell.org/ghc.git/

On branch  : master

https://github.com/ghc/ghc/commit/d3149f6096a987e94d4989e537c1a133bcbb9a6f

>---------------------------------------------------------------

commit d3149f6096a987e94d4989e537c1a133bcbb9a6f
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Mon Apr 29 17:26:17 2013 +0100

    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

>---------------------------------------------------------------

 compiler/typecheck/TcHsType.lhs   | 31 ++++++++++++++++++++++++-------
 compiler/typecheck/TcValidity.lhs | 16 +++++++++-------
 2 files changed, 33 insertions(+), 14 deletions(-)

diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs
index 9ec0d36..d559f99 100644
--- a/compiler/typecheck/TcHsType.lhs
+++ b/compiler/typecheck/TcHsType.lhs
@@ -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
diff --git a/compiler/typecheck/TcValidity.lhs b/compiler/typecheck/TcValidity.lhs
index ee0d9ec..3a828da 100644
--- a/compiler/typecheck/TcValidity.lhs
+++ b/compiler/typecheck/TcValidity.lhs
@@ -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])