#15009: Float equalities past local equalities -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: 8.4.3 Component: Compiler | Version: 8.2.2 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: gadt/T15009 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by nfrisby): I think I'm slowly making progress! I'm doing it at wiki:FloatMoreEqs2018, to avoid polluting this ticket any more. I might open a separate feature request at some point. In particular, I work through an example there {{{ forall[3] y. () => ( (u : <U>) , forall[4]. (g : y ~ <Y>) => (w1 : <W1>) ) }}} showing why floating {{{w1}}} out from under {{{g}}} can be problematic. I think this answers my question from comment:10 more precisely than does comment:11. That example motivates a rule, which I'm now working to broaden and concretize:
We can float {{{w1}}} out from under {{{g}}} if {{{y}}} does not and can never again occur in {{{<W1>}}}.
The destination I have in mind is something like "retiring" {{{g}}} (e.g. discarding it) if we can determine that it has eliminated all possible occurrences of {{{y}}} under it now and forever. I think some relatively simple heuristics are within reach -- will keep working on it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15009#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler