Opened 12 months ago

Closed 11 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 12 months ago by

### comment:2 Changed 11 months ago by

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:4 Changed 11 months ago by

Resolution: | → invalid |
---|---|

Status: | new → closed |

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

**Note:**See TracTickets for help on using tickets.

I agree. Let's fix this.