Improve error reporting for kind errors (fix Trac #1633)

[ghc-hetmet.git] / compiler / typecheck / TcUnify.lhs

diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 9f5daeb..e5e16fc 100644 (file)
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -14,7 +14,6 @@ module TcUnify (
         -- Various unifications
   unifyType, unifyTypeList, unifyTheta,
   unifyKind, unifyKinds, unifyFunKind,
-  checkExpectedKind,
   preSubType, boxyMatchTypes,
 
   --------------------------------
@@ -611,7 +610,10 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst
                         Nothing -> orig_boxy_ty
                         Just ty -> ty `boxyLub` orig_boxy_ty
 
-    go _ (TyVarTy tv) | isMetaTyVar tv
+    go _ (TyVarTy tv) | isTcTyVar tv && isMetaTyVar tv
+                               -- NB: A TyVar (not TcTyVar) is possible here, representing
+                               --     a skolem, because in this pure boxy_match function 
+                               --     we don't instantiate foralls to TcTyVars; cf Trac #2714
         = subst         -- Don't fail if the template has more info than the target!
                         -- Otherwise, with tmpl_tvs = [a], matching (a -> Int) ~ (Bool -> beta)
                         -- would fail to instantiate 'a', because the meta-type-variable
@@ -1294,8 +1296,8 @@ Note [TyCon app]
 When we find two TyConApps, the argument lists are guaranteed equal
 length.  Reason: intially the kinds of the two types to be unified is
 the same. The only way it can become not the same is when unifying two
-AppTys (f1 a1):=:(f2 a2).  In that case there can't be a TyConApp in
-the f1,f2 (because it'd absorb the app).  If we unify f1:=:f2 first,
+AppTys (f1 a1)~(f2 a2).  In that case there can't be a TyConApp in
+the f1,f2 (because it'd absorb the app).  If we unify f1~f2 first,
 which we do, that ensures that f1,f2 have the same kind; and that
 means a1,a2 have the same kind.  And now the argument repeats.
 
@@ -1870,7 +1872,7 @@ kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
 -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
 -- If the flag is False, it requires k <: sk
 -- E.g.         kindSimpleKind False ?? = *
--- What about (kv -> *) :=: ?? -> *
+-- What about (kv -> *) ~ ?? -> *
 kindSimpleKind orig_swapped orig_kind
   = go orig_swapped orig_kind
   where
@@ -1918,75 +1920,6 @@ unifyFunKind _                         = return Nothing
 
 %************************************************************************
 %*                                                                      *
-        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}
-checkExpectedKind :: Outputable a => a -> TcKind -> TcKind -> 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 exp_kind
-  | 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 [ ptext (sLit "Expected kind") <+>
-                                     quotes (pprKind tidy_exp_kind) <> comma,
-                                 ptext (sLit "but") <+> quotes (ppr ty) <+>
-                                     ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
-
-           failWithTcM (env2, err $$ more_info)
-\end{code}
-
-%************************************************************************
-%*                                                                      *
 \subsection{Checking signature type variables}
 %*                                                                      *
 %************************************************************************