[Haskell-cafe] case, GADTs, Arrows

[Ross Paterson]

On Wed, May 14, 2014 at 02:45:29PM +0400, Miguel Mitrofanov wrote:
> Are there EXACT rules for desugaring "case" construct in Arrow syntax? The documentation says just "The translation is similar to that of if commands". But that can't be right in case of GADTs.
> 
> For example, let's say we have
> 
> data A where A :: Show s => s -> A
> 
> Then the following would work fine:
> 
> proc () ->
>   do a <- arr A -< "test"
>      case a of
>        A s ->
>          returnA -< show s
> 
> But if we abstract part of it:
> 
> b :: (Arrow a, Show s) => a s String
> b =
>   proc(s) ->
>     returnA -< show s
> 
> proc() ->
>   do a <- arr A -< "test"
>      case a of
>        A s ->
>          b -< s
> 
> then it fails.

Actually the first one doesn't work either: it is accepted, but
it generates invalid core -- the arrow translation doesn't handle
existentials (this is bug #344).

The translation goes

	proc p -> case {p1 -> c1; ...; pn -> cn}
	=
	arr (\ p -> case {p1 -> (v1, p); ...; pn -> (vn, p)}) >>>
		((proc (v1, p) -> c1) ||| ... ||| (proc (vn, p) -> c))

where vi is the tuple of variables in pi.  Now if n = 1 there's no need
for (|||) and therefore the ArrowChoice constraint, so that's a bit of
a bug.  When there are existentials we should also include the required
dictionaries in the tuple, but unfortunately that's not working.
(#5777 is another arrows GADT bug.)