#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 simonpj): Hmm. I think you may be suggesting this transformation on constraints: {{{ forall tvs1. blah1 => forall tvs2. blah2 => unsolved-stuff --> forall (tvs1, tvs2). (blah1, blah2) => unsolved-stuff }}} The hope would be that an equality in the inner `blah2` might look like `(a~ty)`, where `a` is bound by the outer `tvs1`. If so, then in the transformed implication, the equality would fall under `Note [Let-bound skolems]`, and we could float things from `unsolved-stuff` out. I think that is plausible, and it's an interesting idea that I had not onsidered.. The side condition is that there are no "wanteds" as a peer to the inner implication, like this {{{ forall tvs1. blah1 => ( forall tvs2. blah2 => unsolved-stuff , alpha ~ Int ) }}} If there was, the argument of comment:11 would apply. But what if there were ''two'' such implications? Floating constraints out of either would disable floating constraints out of the other! This looks complicated and unprincipled to me. I suggest just using a type signature. Extremely complicated type inference is not necessarily a boon to the programmer! Perhaps there is a simple, principled algorithm hiding in there; but I don't yet see it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15009#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler