[GHC] #9211: Untouchable type variable (regression from 7.6)

[GHC]

#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