+%* *
+ 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}
+-- The ExpKind datatype means "expected kind" and contains
+-- some info about just why that kind is expected, to improve
+-- the error message on a mis-match
+data ExpKind = EK TcKind EkCtxt
+data EkCtxt = EkUnk -- Unknown context
+ | EkEqPred -- Second argument of an equality predicate
+ | EkKindSig -- Kind signature
+ | EkArg SDoc Int -- Function, arg posn, expected kind
+
+
+ekLifted, ekOpen :: ExpKind
+ekLifted = EK liftedTypeKind EkUnk
+ekOpen = EK openTypeKind EkUnk
+
+checkExpectedKind :: Outputable a => a -> TcKind -> ExpKind -> 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 (EK exp_kind ek_ctxt)
+ | 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 [ expected_herald ek_ctxt <+> ptext (sLit "kind")
+ <+> quotes (pprKind tidy_exp_kind) <> comma,
+ ptext (sLit "but") <+> quotes (ppr ty) <+>
+ ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
+
+ expected_herald EkUnk = ptext (sLit "Expected")
+ expected_herald EkKindSig = ptext (sLit "An enclosing kind signature specified")
+ expected_herald EkEqPred = ptext (sLit "The left argument of the equality predicate had")
+ expected_herald (EkArg fun arg_no)
+ = ptext (sLit "The") <+> speakNth arg_no <+> ptext (sLit "argument of")
+ <+> quotes fun <+> ptext (sLit ("should have"))
+
+ failWithTcM (env2, err $$ more_info)
+\end{code}
+
+%************************************************************************