<p dir="ltr">Given</p>
<p dir="ltr">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</p>
<p dir="ltr">data Selector = One | Two | Three<br>
data Big a = forall (x :: Selector) .<br>
   Big !(BigG x a)<br>
data BigG x a where<br>
  GB1a :: some -> fields -> BigG 'One a<br>
  GB1b :: fields -> BigG 'One a<br>
  GB2a :: whatever -> BigG 'Two a<br>
  GB3a :: yeah -> BigG 'Three a</p>
<p dir="ltr">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.</p>
<div class="gmail_quote">On May 24, 2016 4:16 AM, "Ben Gamari" <<a href="mailto:ben@well-typed.com">ben@well-typed.com</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">David Feuer <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> writes:<br>
<br>
> Data.IntMap could be cleaned up some if single-field, single strict<br>
> constructor GADTs/existentials could be unpacked even when wrapping a sum<br>
> type. We could then have<br>
><br>
> data Status = E | NE<br>
> data IntMap' (s :: Status) a where<br>
>   Bin :: ... -> ... -> !(IntMap' NE a) -> !(IntMap' NE a) -> IntMap' NE a<br>
>   Tip :: ... -> a -> IntMap' NE a<br>
>   Nil :: IntMap' E a<br>
> data IntMap a =<br>
>   forall s . IM {-# UNPACK #-} !(IntMap' s a)<br>
><br>
I'm not sure I understand how the existential helps you unpack this sum.<br>
Surely I'm missing something.<br>
<br>
> The representation would be the same as that of a newtype, but the pattern<br>
> matching semantics would be strict. In the GADT case, this would<br>
> essentially allow any fixed concrete datatype to serve directly as a<br>
> witness for an arbitrary set of type equalities demanded on construction.<br>
><br>
> Is there any hope something like this could happen?<br>
<br>
Ignoring the sum issue for a moment:<br>
<br>
My understanding is that it ought to be possible to unpack at least<br>
single-constructor types in an existentially quantified datacon,<br>
although someone needs to step up to do it. A closely related issue<br>
(existentials in newtypes) was discussed by dons in a Stack Overflow<br>
question [1] quite some time ago.<br>
<br>
As far as I understand as long as the existentially-quantified argument<br>
is unconstrained (therefore there is no need to carry a dictionary) and<br>
of kind * (therefore has a uniform representation) there is no reason<br>
why unpacking shouldn't be possible.<br>
<br>
The case that you cite looks to be even easier since the existential is<br>
a phantom so there is no need to represent it at all. It seems to me<br>
like it might not be so difficult to treat this case in particular.<br>
It's possible all that is necessary would be to adjust the unpackability<br>
criteria in MkId.<br>
<br>
It actually looks like there's a rather closely related ticket already<br>
open, #10016.<br>
<br>
Cheers,<br>
<br>
- Ben<br>
<br>
<br>
[1] <a href="http://stackoverflow.com/questions/5890094/is-there-a-way-to-define-an-existentially-quantified-newtype-in-ghc-haskell" rel="noreferrer" target="_blank">http://stackoverflow.com/questions/5890094/is-there-a-way-to-define-an-existentially-quantified-newtype-in-ghc-haskell</a><br>
</blockquote></div>