Pruning GADT case alternatives with uninhabitable coercion parameters
conal at conal.net
Fri Jun 20 17:59:14 UTC 2014
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
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.
* Does this sort of transformation already live in GHC somewhere, and if
* Are there gotchas / sources of unsoundness in the transformation I'm
* Is anyone else already working on this sort of transformation?
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the ghc-devs