#8388: forall on non-* types -------------------------------------+------------------------------------ Reporter: monoidal | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): You are quite right about this, but GHC currently doesn't check that the body of a `forall` has kind `*`. Indeed `TcHsType` has this comment {{{ Really we should check that it's a type of value kind {*, Constraint, #}, but I'm not doing that yet Example that should be rejected: f :: (forall (a:*->*). a) Int }}} This is for several reasons, all minor: * The body can also have kind `#`, eg `forall a. (# a, a #)` * If we have explicit `foralls` in kinds (which we don't yet), the body will have kind `BOX` not `*`. * In this generalised-newtype-deriving code (cf #3621) {{{ class C s m where newtype WrappedState a = WS ... deriving (C s) }}} the `(C s)` part is hackily represented as `forall state. C s`. This is a convenient hack that would have to be done some other way. * The error message for `T7019` and `T7019a` changed, not in a good way. None of these are fatal, but I don't think this bug is causing a problem today, so I'm going to leave this for now. Below is the diff to `TcHsTypes` which I tried, as a starting point. Simon {{{ diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs index b7cd841..20a5f99 100644 --- a/compiler/typecheck/TcHsType.lhs +++ b/compiler/typecheck/TcHsType.lhs @@ -393,13 +393,16 @@ tc_hs_type hs_ty@(HsAppTy ty1 ty2) exp_kind (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2] --------- Foralls -tc_hs_type hs_ty@(HsForAllTy _ hs_tvs context ty) exp_kind - = tcHsTyVarBndrs hs_tvs $ \ tvs' -> +tc_hs_type hs_ty@(HsForAllTy _ hs_tvs context ty) exp_kind@(EK exp_k _) + = tcHsTyVarBndrs hs_tvs $ \ tvs' -> -- Do not kind-generalise here! See Note [Kind generalisation] do { ctxt' <- tcHsContext context ; 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 + do { checkExpectedKind hs_ty exp_k ekOpen + -- Check that the expected kind is *, #, or Constraint + -- See Note [Body kind of forall] + ; tc_lhs_type ty exp_kind } + 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 @@ -408,7 +411,7 @@ tc_hs_type hs_ty@(HsForAllTy _ hs_tvs context ty) exp_kind ; return (mkSigmaTy tvs' ctxt' ty') } --------- Lists, arrays, and tuples -tc_hs_type hs_ty@(HsListTy elt_ty) exp_kind +tc_hs_type hs_ty@(HsListTy elt_ty) exp_kind = do { tau_ty <- tc_lhs_type elt_ty ekLifted ; checkExpectedKind hs_ty liftedTypeKind exp_kind ; checkWiredInTyCon listTyCon @@ -779,11 +782,11 @@ Note [Body kind of a forall] The body of a forall is usually a type, but in principle there's no reason to prohibit *unlifted* types. In fact, GHC can itself construct a function with an -unboxed tuple inside a for-all (via CPR analyis; see +unboxed tuple inside a for-all (via CPR analyis; see typecheck/should_compile/tc170). Moreover in instance heads we get forall-types with -kind Constraint. +kind Constraint. Moreover if we have a signature f :: Int# @@ -816,9 +819,9 @@ So we *must* keep the HsForAll on the instance type HsForAll Implicit [] [] (Typeable Apply) so that we do kind generalisation on it. -Really we should check that it's a type of value kind -{*, Constraint, #}, but I'm not doing that yet -Example that should be rejected: +We do check that it's a type of value kind {*, Constraint, #}, via the +call (checkExpectedKind hs_ty exp_k ekOpen) in the null-context case. +(c.f. Trac #8388). Example that should be rejected: f :: (forall (a:*->*). a) Int Note [Inferring tuple kinds] }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8388#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler