Pruning GADT case alternatives with uninhabitable coercion parameters

[Conal Elliott]

My first go is at
https://github.com/conal/hermit-extras/blob/master/src/HERMIT/Extras.hs#L1030
. It type-checks. I haven't tried running it yet. Comments most welcome!

-- Conal


On Tue, Jun 24, 2014 at 4:10 PM, Conal Elliott <conal at conal.net> wrote:

> I'm glad for the interest and help. I can make an initial go of it. My
> current simple plan is to traverse expressions, collecting type equalities
> from bound coercion variables as I descend, combining them progressively
> with successive type unifications. The traversal is thus parametrized by a
> TvSubst and yields a Maybe TvSubst. The coercion variables will come from
> lambdas, let bindings and case alternatives. If an added equality is not
> unifiable given the current TvSubst, we've reached a contradiction. If the
> contradiction arises for one of the variables in a case alternative, then
> remove that alternative.
>
> How does this strategy sound?
>
> Some issues:
>
> *   Nominal vs representational type equalities.
> *   Will I want to normalize the types (with normaliseType) before
> unifying?
> *   How can I unify while carrying along a type substitution environment?
> The Unify module exports tcUnifyTy, which takes no such environment, but
> not unify, which does.
>
> -- Conal
>
>
> On Tue, Jun 24, 2014 at 4:43 AM, Simon Peyton Jones <simonpj at microsoft.com
> > wrote:
>
>>  we need to do a bit more work to re-connect to source pattern locations
>> and nested patterns? I can’t assess very well yet if this is a real problem
>> though
>>
>>
>>
>> That is a very good point.
>>
>>
>>
>> Nevertheless, given
>>
>> ·         the typechecked HsSyn (i.e. still in source form, but with
>> type inference fully completed
>>
>> ·         the independent contradiction-detector described below (which
>> is independent of whether the contradiction problems it is given come from
>> HsSyn or Core)
>>
>> it would be easy to give source-localised error messages
>>
>>
>>
>> Simon
>>
>>
>>
>> *From:* Dimitrios Vytiniotis
>> *Sent:* 24 June 2014 11:58
>> *To:* Simon Peyton Jones; Conal Elliott; ghc-devs at haskell.org
>> *Cc:* Nikolaos S. Papaspyrou (nickie at softlab.ntua.gr); George Karachalias
>>
>> *Subject:* RE: Pruning GADT case alternatives with uninhabitable
>> coercion parameters
>>
>>
>>
>>
>>
>> Yes it would be better in the sense that we don’t really want to be
>> dealing with unification variables and evidence when we simply use the
>> constraint solver to detect inconsistencies in possibly missing patterns,
>> but the concern has been that if we are already desugared and in core maybe
>> we need to do a bit more work to re-connect to source pattern locations and
>> nested patterns? I can’t assess very well yet if this is a real problem
>> though …
>>
>>
>>
>> In general I agree that a simple constraint solver for Core might be an
>> independently useful tool for this kind of optimization. (I think George
>> had thought about this too).
>>
>>
>>
>> Thanks!
>>
>> d-
>>
>>
>>
>>
>>
>>
>>
>> *From:* Simon Peyton Jones
>> *Sent:* Tuesday, June 24, 2014 11:41 AM
>> *To:* Conal Elliott; ghc-devs at haskell.org
>> *Cc:* Dimitrios Vytiniotis; Nikolaos S. Papaspyrou (
>> nickie at softlab.ntua.gr); George Karachalias; Simon Peyton Jones
>> *Subject:* RE: Pruning GADT case alternatives with uninhabitable
>> coercion parameters
>>
>>
>>
>> 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
>> <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/96fcf1fc/attachment-0001.html>