Pruning GADT case alternatives with uninhabitable coercion parameters

[Conal Elliott]

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