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?