Pruning GADT case alternatives with uninhabitable coercion parameters

[Simon Peyton Jones]

Conal

This also relates to detecting redundant or overlapped patterns in source programs. I know that Dimitrios is looking at this with Tom, Nikolas, George who I’m cc’ing him.

I think their current approach may be to integrate the overlap checking with the constraint solver in the type checker.  But that isn’t going to work for optimising Core.

An alternative approach would be to implement a specialised constraint solver.  It could be MUCH simpler than the one in the inference engine, because (a) there are no unification variables to worry about, (b) there is no need to gather evidence.  More or less it’s task could be to answer the question
            Is    C |- D    definitely a contradiction?
where C are the “given” constraints (from enclosing pattern matches) and D are the “wanted” constraints (from the current pattern match that may be unreachable).

I don’t think it would be hard to implement such a function.  I’d be happy to help advise if someone wants to take it on.

Dimitrios: If we had such a function, then maybe it’d be better to use it for the pattern-matching overlap detection too?

Simon

From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Conal Elliott
Sent: 20 June 2014 18:59
To: ghc-devs at haskell.org
Subject: Pruning GADT case alternatives with uninhabitable coercion parameters

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/20140624/d38b6f9c/attachment.html>