#15009: Float equalities past local equalities -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.4.3 Component: Compiler | Version: 8.2.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Actually GHC already does this, or something very like it. See `Note [When does an implication have given equalities?]` and especially `Note [Let-bound skolems]` in `TcSMonad`. I don't say that it's perfectly implemented (eg I'm a bit worried about whether it's sensitive to whether the constraint looks like `a ~ b` or `b ~ a`) but it does more or less what you way. Your condition (%) doesn't look right. After all, in your example the constraint `a ~ b` has both `a` and `b` free -- and the former is not locally bound. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15009#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler