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]> 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] > *Cc:* Nikolaos S. Papaspyrou ([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] > *Cc:* Dimitrios Vytiniotis; Nikolaos S. Papaspyrou ([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] > <[email protected]>] *On Behalf Of *Conal Elliott > *Sent:* 20 June 2014 18:59 > *To:* [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
