[GHC] #8388: forall on non-* types

[GHC]

#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