I’m on a train, so can’t look at your code. But I urge you (or whoever) to
split the task into two:
· Traverse the Core tree, gathering given constraints, deleting
unreachable branches
· The Contradiction Checker (CCK)
CCK is independently useful; for example George et al may use it when
traversing HsSyn to report overlapping patterns.
The API of CCK might look something like this:
contradictionCheck :: FamInstEnvs -> [PredType] -> [PredType] ->
Bool
· FamInstEnvs tells it what type-family-instances exist
· The first [PredType] are the enclosing givens
· The second [PredType] are the givens of a new pattern match
· Result is True if the new pattern match is inaccessible
One might also consider a more incremental API, something like
data ContradictionChecker
newCCK :: FamInstEnvs -> ContradictionChecker
check :: ContradictionChecker -> [PredType] -> Maybe
ContradictionChecker
Returns Nothing for a contradiction, (Just cc) if the branch is reachable,
where you should use cc for the body of the branch.
I like the latter API. For example a ContrdictionChecker might carry a
renaming of type variables, to account for shadowing.
Simon
From: [email protected] [mailto:[email protected]] On Behalf Of
Conal Elliott
Sent: 25 June 2014 00:11
To: Simon Peyton Jones
Cc: Dimitrios Vytiniotis; [email protected]; Nikolaos S. Papaspyrou
([email protected]); George Karachalias
Subject: Re: Pruning GADT case alternatives with uninhabitable coercion
parameters
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
<[email protected]<mailto:[email protected]>> 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;
[email protected]<mailto:[email protected]>
Cc: Nikolaos S. Papaspyrou
([email protected]<mailto:[email protected]>); 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; [email protected]<mailto:[email protected]>
Cc: Dimitrios Vytiniotis; Nikolaos S. Papaspyrou
([email protected]<mailto:[email protected]>); 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:[email protected]] On Behalf Of Conal Elliott
Sent: 20 June 2014 18:59
To: [email protected]<mailto:[email protected]>
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
_______________________________________________
ghc-devs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/ghc-devs
