Pruning GADT case alternatives with uninhabitable coercion parameters

[Conal Elliott]

I'm looking for tips on pruning away impossible branches in `case`
expressions on GADTs, due to uninhabited coercion parameter types.

Here's a simple example (rendered by HERMIT) from a type-specializion of
the Foldable instance a GADT for perfect leaf trees in which the tree depth
is part of the type:

> case ds of wild (Sum Int)
>   L (~# :: S (S Z) ~N Z) a1 -> f a1
>   B n1 (~# :: S (S Z) ~N S n1) uv -> ...

Note the kind of the coercion parameter to the leaf constructor (`L`): `S
(S Z) ~N Z`, i.e., 2 == 0. I think we can safely remove this branch as
impossible.

The reasoning gets subtler, however.
After inlining and simplifying in the second (`B`) alternative, the
following turns up:

>     case ds0 of wild0 (Sum Int)
>       L (~# :: n1 ~N Z) a1 -> f0 a1
>       B n2 (~# :: n1 ~N S n2) uv0 -> ...

Now I want to remove the first `L` alternative with `n1 ~ Z`, given that
the kind `S (S Z) ~N S n1` is inhabited (since we're in the first `B`
alternative), so that `n1 ~ S Z`. With more inlining, more such equalities
pile up. Soon we get to an impossible `B` alternative, whose removal would
then eliminate the rest of the recursive unfolding.

My questions:

*   Does this sort of transformation already live in GHC somewhere, and if
so, where?
*   Are there gotchas / sources of unsoundness in the transformation I'm
suggesting?
*   Is anyone else already working on this sort of transformation?

-- Conal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140620/3aa98d9c/attachment.html>