Opened 8 months ago

Closed 7 months ago

#14795 closed bug (invalid)

Data type return kinds don't obey the forall-or-nothing rule

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.2.2
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Originally noticed here. GHC accepts this:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}

import Data.Kind

data Foo :: forall a. a -> b -> Type where
  MkFoo :: a -> Foo a b

Despite the fact that Foo's return kind is headed by an explicit forall which does not quantify b.

The users' guide doesn't explicitly indicate that the forall-or-nothing rule should apply to data type return kinds, but goldfirere believes that not doing so is an inconsistent design, so I'm opening this ticket to track this.

Change History (4)

comment:1 Changed 8 months ago by simonpj

I agree. Let's fix this.

comment:2 Changed 7 months ago by RyanGlScott

Hm. After thinking about this some more, I'm not 100% convinced that this is an inconsistent design.

The issue is that the forall-or-nothing rule applies to top-level type signatures. But data type return kinds are not truly top-level, as they can mention type variables bound before it. For instance, in this example:

data Foo2 (x :: b) :: forall a. a -> b -> Type

Here, the explicit return kind is only a small part of Foo2's kind. The full shebang would be (using an explicit kind signature):

type Foo2 :: forall b. b -> forall a. a -> b -> Type

In that sense, data type return kinds don't need to satisfy the forall-or-nothing rule, since they're not actually the thing at the top level.

A similar phenomenon occurs at the term level. GHC accepts this:

{-# LANGUAGE RankNTypes #-}

f :: (forall a. a -> b -> Int)
f _ _ = 42

That's because in some sense, (forall a. a -> b -> Int) isn't the real top-level type signature here. The real top-level type signature is revealed if you query GHCi:

λ> :type +v f
f :: forall b a. a -> b -> Int

comment:3 Changed 7 months ago by simonpj

Very good points.

comment:4 Changed 7 months ago by RyanGlScott

Resolution: invalid
Status: newclosed

I think I'll close this as invalid, then. Feel free to reopen if you disagree.

Note: See TracTickets for help on using tickets.