Opened 6 years ago

Last modified 5 years ago

#8388 new bug

forall on non-* types

Reported by: monoidal Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.6.3
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This code

{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}
x = Nothing :: (forall a. Maybe) Int

gives

    Couldn't match type `Maybe' with `forall a. Maybe'
    Expected type: forall a. Maybe Int
      Actual type: Maybe Int

which does not seem correct. There are two options:

Option A: We allow this.

Option B: We reject this as ill-kinded and allow forall a. T only when T has kind *. I prefer this option; in theory this can break existing code, but I am not aware of any code that uses forall on non-* type (please correct me if I'm wrong), and e.g. this means forall a. a inhabits every kind, for example Bool.

Change History (2)

comment:1 Changed 6 years ago 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]

comment:2 Changed 5 years ago by thomie

Component: CompilerCompiler (Type checker)
Note: See TracTickets for help on using tickets.