#9211: Untouchable type variable (regression from 7.6) -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by simonpj): * cc: dimitris@… (added) Comment: Harumph. Suppose we have an implication constraint of this form: {{{ forall a b c. (b ~ ty, ...) => ...blah... }}} where the equality constraint in the "givens" is of form `b ~ ty`, where `b` is one of the variables quantified by the `forall`. Then, as far as I can see, no loss of principality arises if we float constraints from `...blah...`, outside the implication. (Obviously, only ones that do not mention `a,b,c`.) (NB: floating the constraint out is equivalent to allowing a unification of an untouchable underneath.) Reason: such an equality amounts to a let-binding; indeed that is exactly how Oleg wants to use it. This would amount to an ad-hoc but easily-specified extension of GHC's already-ad-hoc rule for floating constraints out of implications, and hence perhaps no big deal. Certainly it's easy to implement. I'm adding Dimitrios in cc. What do you think? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9211#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler