#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): What, precisely, is the rule you propose? I don't know precisely what "float equalities past equalities if the involved levels are OK" means. I think you mean something like "you can float a wanted equality W past a given equality G iff that G not to be used in any solution of W. But it's hard to come up with an implementation of that rule, other than "don't float past equalities". Whatever we choose must be simple and predictable. I worry about things like this {{{ Implic { TcLevel = 3 , Skolems = [] , Given = (y ~ Bool, F y Int ~ Char) , Wanted = z[tau:2] ~ F Bool t[tau:1] } }}} Can I float that wanted? Well, no. Maybe, later, we'll discover that `t := Int`. Then our `F Bool Int` can be rewritten to `F y Int` (with the local equality), and thence to Char. But if we floated it out we'd get stuck. If you have a better rule, that'd be great. I just don't see it yet. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15009#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler