Work out when GADT parameters should be specified

Right now, there's not a clear specification of when GADT data constructor parameters should be specified, and what order they appear in. For example:

data G a where
  MkG :: b -> a -> G a

To my eye, we should get MkG :: forall b a. b -> a -> G a. But GHC now gives MkG :: a {b}. b -> a -> G a. At least two things are going on here:

1. GHC puts all universals before existentials.
2. There is an outright bug in mkDataCon that makes existentials act as inferred variables, but only for the representation type, not the wrapper type.

You can witness (2) by noting that the b magically becomes specified if you put a strictness annotation (thereby necessitating the construction of a wrapper) anywhere.

I'm not sure what to do about (1), from a design standpoint. Here are some thoughts.

A. Having universals always come before existentials is convenient in pattern matching. When we have type application in patterns, you'll want to match only on existentials, never universals. So keeping the existentials together makes some sense. The universals will be omitted from the match entirely.

B. FC absolutely requires that the universals come first. So if we allow the user to reorder the variables, that will necessitate creating a wrapper. Are there performance implications? That would be sad.

C. We could tread a middle path, where if the user writes a forall, they get the order requested. Otherwise, they get universals first (whose order is taken from the ordering in the data declaration head) followed by existentials (whose order is taken from left-to-right first occurrence in the constructor type signature). But this is different than for functions, where we always use left-to-right ordering, even when lacking a forall.

I tend to think that we should always just do what the user asks, but I'm worried about performance implications of this decision. It will make wrappers necessary for existential constructors that otherwise don't need them.

Note that this whole debate is about only GADT constructors, not Haskell98 ones. Haskell98 constructors will always have universals before existentials, because that's quite obvious from the way they're declared.

Trac metadata

Trac field	Value
Version	8.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture