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 <co...@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 <simo...@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@haskell.org >> *Cc:* Nikolaos S. Papaspyrou (nic...@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@haskell.org >> *Cc:* Dimitrios Vytiniotis; Nikolaos S. Papaspyrou ( >> nic...@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-boun...@haskell.org >> <ghc-devs-boun...@haskell.org>] *On Behalf Of *Conal Elliott >> *Sent:* 20 June 2014 18:59 >> *To:* ghc-devs@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 >> >> >> > >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
