Better error messages when we know the expected kind in tcHsSigType
authorJose Pedro Magalhaes <jpm@cs.uu.nl>
Mon, 14 Nov 2011 09:50:01 +0000 (09:50 +0000)
committerJose Pedro Magalhaes <jpm@cs.uu.nl>
Wed, 16 Nov 2011 19:47:09 +0000 (20:47 +0100)
compiler/typecheck/TcHsType.lhs
compiler/typecheck/TcMType.lhs
compiler/types/Kind.lhs

index 8f1fb54..3d916d3 100644 (file)
@@ -171,12 +171,15 @@ tcHsSigType ctxt 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 }
+  = do  { -- (kinded_ty, _kind) <- kc_lhs_type hs_ty
+          kinded_ty <- case expectedKindInCtxt ctxt of
+                         Nothing -> fmap fst (kc_lhs_type hs_ty)
+                         Just k  -> kc_check_lhs_type hs_ty (EK k EkUnk) -- JPM fix this
+          -- 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 }
 
 -- Like tcHsType, but takes an expected kind
 tcCheckHsType :: LHsType Name -> Kind -> TcM Type
@@ -1351,9 +1354,9 @@ sc_ds_var_app name arg_kis
 
 -- General case
 sc_ds_var_app name arg_kis = do
-  thing <- tcLookup name
-  case thing of
-    AGlobal (ATyCon tc)
+  (_errs, mb_thing) <- tryTc (tcLookup name)
+  case mb_thing of
+    Just (AGlobal (ATyCon tc))
       | isAlgTyCon tc || isTupleTyCon tc -> do
       poly_kinds <- xoptM Opt_PolyKinds
       unless poly_kinds $ addErr (polyKindsErr name)
@@ -1363,8 +1366,13 @@ sc_ds_var_app name arg_kis = do
           return (mkTyConApp (mkPromotedTypeTyCon tc) arg_kis)
         Just _  -> err tc_kind "is not fully applied"
         Nothing -> err tc_kind "is not promotable"
-
-    _ -> wrongThingErr "promoted type" thing name
+    -- It is in scope, but not what we expected
+    Just thing -> wrongThingErr "promoted type" thing name
+    -- It is not in scope, but it passed the renamer: staging error
+    Nothing    -> ASSERT2 ( isTyConName name, ppr name )
+                  failWithTc (ptext (sLit "Promoted kind") <+> 
+                              quotes (ppr name) <+>
+                              ptext (sLit "used in a mutually recursive group"))
 
   where err k m = failWithTc (    quotes (ppr name) <+> ptext (sLit "of kind")
                               <+> quotes (ppr k)    <+> ptext (sLit m))
index 6ae5be7..19bf384 100644 (file)
@@ -50,6 +50,7 @@ module TcMType (
   --------------------------------
   -- Checking type validity
   Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
+  expectedKindInCtxt, 
   checkValidTheta, 
   checkValidInstHead, checkValidInstance, validDerivPred,
   checkInstTermination, checkValidFamInst, checkTyFamFreeness, 
@@ -892,6 +893,17 @@ This might not necessarily show up in kind checking.
 
        
 \begin{code}
+-- Depending on the context, we might accept any kind (for instance, in a TH
+-- splice), or only certain kinds (like in type signatures).
+expectedKindInCtxt :: UserTypeCtxt -> Maybe Kind
+expectedKindInCtxt (TySynCtxt _)  = Nothing -- Any kind will do
+expectedKindInCtxt ThBrackCtxt    = Nothing
+expectedKindInCtxt GhciCtxt       = Nothing
+expectedKindInCtxt ResSigCtxt     = Just openTypeKind
+expectedKindInCtxt ExprSigCtxt    = Just openTypeKind
+expectedKindInCtxt (ForSigCtxt _) = Just liftedTypeKind
+expectedKindInCtxt _              = Just argTypeKind
+
 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 -- Checks that the type is valid for the given context
 checkValidType ctxt ty = do
@@ -929,14 +941,9 @@ checkValidType ctxt ty = do
 
        actual_kind = typeKind ty
 
-       kind_ok = case ctxt of
-                       TySynCtxt _  -> True -- Any kind will do
-                       ThBrackCtxt  -> True -- ditto
-                        GhciCtxt     -> True -- ditto
-                       ResSigCtxt   -> tcIsSubOpenTypeKind actual_kind
-                       ExprSigCtxt  -> tcIsSubOpenTypeKind actual_kind
-                       ForSigCtxt _ -> isLiftedTypeKind actual_kind
-                       _            -> tcIsSubArgTypeKind actual_kind
+        kind_ok = case expectedKindInCtxt ctxt of
+                    Nothing -> True
+                    Just k  -> tcIsSubKind actual_kind k
        
        ubx_tup 
          | not unboxed = UT_NotOk
index 1358578..31a567d 100644 (file)
@@ -42,7 +42,7 @@ module Kind (
 
         isSubArgTypeKind, tcIsSubArgTypeKind, 
         isSubOpenTypeKind, tcIsSubOpenTypeKind,
-        isSubKind, defaultKind,
+        isSubKind, tcIsSubKind, defaultKind,
         isSubKindCon, tcIsSubKindCon, isSubOpenTypeKindCon,
 
         -- ** Functions on variables
@@ -229,13 +229,18 @@ isSuperKind _                   = False
 isKind :: Kind -> Bool
 isKind k = isSuperKind (typeKind k)
 
-isSubKind :: Kind -> Kind -> Bool
+isSubKind, tcIsSubKind :: Kind -> Kind -> Bool
+isSubKind   = isSubKind' False
+tcIsSubKind = isSubKind' True
+
+-- The first argument denotes whether we are in the type-checking phase or not
+isSubKind' :: Bool -> Kind -> Kind -> Bool
 -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
 
-isSubKind (FunTy a1 r1) (FunTy a2 r2)
-  = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
+isSubKind' duringTc (FunTy a1 r1) (FunTy a2 r2)
+  = (isSubKind' duringTc a2 a1) && (isSubKind' duringTc r1 r2)
 
-isSubKind k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s)
+isSubKind' duringTc k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s)
   | isPromotedTypeTyCon kc1 || isPromotedTypeTyCon kc2
     -- handles promoted kinds (List *, Nat, etc.)
     = eqKind k1 k2
@@ -247,10 +252,10 @@ isSubKind k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s)
 
   | otherwise = -- handles usual kinds (*, #, (#), etc.)
                 ASSERT2( null k1s && null k2s, ppr k1 <+> ppr k2 )
-                kc1 `isSubKindCon` kc2
-
+                if duringTc then kc1 `tcIsSubKindCon` kc2
+                else kc1 `isSubKindCon` kc2
 
-isSubKind k1 k2 = eqKind k1 k2
+isSubKind' _duringTc k1 k2 = eqKind k1 k2
 
 isSubKindCon :: TyCon -> TyCon -> Bool
 -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@