This sounds to me like what we're trying to describe here smells like an unboxed existential , which is a hairs breadth out of reach of ghcs type system 

@david have you tried out eds structures package? It may provide the right tooling to simulate this or something close to what you want. 

On Tuesday, May 24, 2016, David Feuer <david.feuer@gmail.com> wrote:

Given

data Big a = B1 !(Small1 a) | B2 !(Small2 a) | B3 !(Small3 a), where the Small types are (possibly recursive) sums, it's generally possible to express that as something like

data Selector = One | Two | Three
data Big a = forall (x :: Selector) .
   Big !(BigG x a)
data BigG x a where
  GB1a :: some -> fields -> BigG 'One a
  GB1b :: fields -> BigG 'One a
  GB2a :: whatever -> BigG 'Two a
  GB3a :: yeah -> BigG 'Three a

Making one big GADT from all the constructors of the "small" types, and then wrapping it up in an existential. That's what I meant about "unpacking". But for efficiency purposes, that wrapper needs the newtype optimization.

On May 24, 2016 4:16 AM, "Ben Gamari" <ben@well-typed.com> wrote:
David Feuer <david.feuer@gmail.com> writes:

> Data.IntMap could be cleaned up some if single-field, single strict
> constructor GADTs/existentials could be unpacked even when wrapping a sum
> type. We could then have
>
> data Status = E | NE
> data IntMap' (s :: Status) a where
>   Bin :: ... -> ... -> !(IntMap' NE a) -> !(IntMap' NE a) -> IntMap' NE a
>   Tip :: ... -> a -> IntMap' NE a
>   Nil :: IntMap' E a
> data IntMap a =
>   forall s . IM {-# UNPACK #-} !(IntMap' s a)
>
I'm not sure I understand how the existential helps you unpack this sum.
Surely I'm missing something.

> The representation would be the same as that of a newtype, but the pattern
> matching semantics would be strict. In the GADT case, this would
> essentially allow any fixed concrete datatype to serve directly as a
> witness for an arbitrary set of type equalities demanded on construction.
>
> Is there any hope something like this could happen?

Ignoring the sum issue for a moment:

My understanding is that it ought to be possible to unpack at least
single-constructor types in an existentially quantified datacon,
although someone needs to step up to do it. A closely related issue
(existentials in newtypes) was discussed by dons in a Stack Overflow
question [1] quite some time ago.

As far as I understand as long as the existentially-quantified argument
is unconstrained (therefore there is no need to carry a dictionary) and
of kind * (therefore has a uniform representation) there is no reason
why unpacking shouldn't be possible.

The case that you cite looks to be even easier since the existential is
a phantom so there is no need to represent it at all. It seems to me
like it might not be so difficult to treat this case in particular.
It's possible all that is necessary would be to adjust the unpackability
criteria in MkId.

It actually looks like there's a rather closely related ticket already
open, #10016.

Cheers,

- Ben


[1] http://stackoverflow.com/questions/5890094/is-there-a-way-to-define-an-existentially-quantified-newtype-in-ghc-haskell