Opened 4 years ago

Closed 18 months ago

#11513 closed bug (fixed)

Work out when GADT parameters should be specified

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


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.
  1. 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.

  1. 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.
  1. 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.
  1. 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.

Change History (10)

comment:1 Changed 4 years ago by simonpj

In the worker, I'm sure we should put the universals first. We always have, and I see no reason to change. Moreover in a pattern we drop the universals, so it must be easy to find them.

In the wrapper can't we just do whatever we do for normal type signatures. Eg

data T a b where
  T1 :: T [x] [x]
  T2 :: T [x] y

Here we just get T1 :: forall x. T [x] [x] and T2 :: forall x y. T [x] y. If those were ordinary functions we'd be done. So why aren't we done?

comment:2 Changed 4 years ago by goldfire

Everything in comment:1 is true. The problem comes up only when we don't have a wrapper. And right now, "the type variables are out of order" is not a reason to make a wrapper. If it were, then we'd be done.

comment:3 Changed 4 years ago by simonpj

So why not put them in the "correct order" whatever that is, in the first place. I'm a bit lost.

comment:4 Changed 4 years ago by goldfire

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

Currently, no wrapper is required here. Note that G is not a GADT. The worker has type forall a b. b -> a -> G a, with universals before existentials. Because we have no wrapper, the user sees the worker type.

I'm proposing making a wrapper in this case.

Does that clarify?

comment:5 Changed 4 years ago by simonpj

Ah, now I see. You mean (unlike the example in the Description) when the user explicitly specifies the "wrong" order.

Then let's make a wrapper! It'll get inlined away, and serves (as always) to interface the type the user wants to see with the one GHC uses internally.

comment:6 Changed 4 years ago by Richard Eisenberg <eir@…>

In 90f35612/ghc:

Existentials should be specified.

This addresses point (2) from #11513.

comment:7 Changed 4 years ago by simonpj

This is a very quiet change

-    rep_ty = mkSpecForAllTys univ_tvs $ mkInvForAllTys ex_tvs $
+    rep_ty = mkSpecForAllTys univ_tvs $ mkSpecForAllTys ex_tvs $

Is it worth a comment and an example? After all, it can't have been obvious to you the first time.

Test case?

comment:8 Changed 4 years ago by goldfire

I'll add a comment, but it was just plain wrong the first time around.

comment:9 Changed 4 years ago by Richard Eisenberg <eir@…>

In 0c420cb6/ghc:

Comments only (#11513)

comment:10 Changed 18 months ago by RyanGlScott

Resolution: fixed
Status: newclosed

This has been subsumed by #11721. After that was fixed, GHC now specifies and orders type variables in a GADT type signature according to the usual conventions of TypeApplications (possibly creating wrappers where needed, as noted in comment:4).

Note: See TracTickets for help on using tickets.