<div dir="ltr"><div>I'm looking for tips on pruning away impossible branches in `case` expressions on GADTs, due to uninhabited coercion parameter types.<br><br>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:<br>

<br>> case ds of wild (Sum Int)<br>>   L (~# :: S (S Z) ~N Z) a1 -> f a1<br>>   B n1 (~# :: S (S Z) ~N S n1) uv -> ...<br><br>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.<br>

<br>The reasoning gets subtler, however.<br>After inlining and simplifying in the second (`B`) alternative, the following turns up:<br><br>>     case ds0 of wild0 (Sum Int)<br>>       L (~# :: n1 ~N Z) a1 -> f0 a1<br>

>       B n2 (~# :: n1 ~N S n2) uv0 -> ...<br><br>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.<br>

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

<br></div>-- Conal<br><div><br></div></div>