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