[GHC] #10204: Odd interaction between rank-2 types and type families

[GHC]

#10204: Odd interaction between rank-2 types and type families
-------------------------------------+-------------------------------------
        Reporter:  diatchki          |                   Owner:
            Type:  feature request   |                  Status:  new
        Priority:  normal            |               Milestone:  ⊥
       Component:  Compiler (Type    |                 Version:  7.10.1
  checker)                           |                Keywords:
      Resolution:                    |            Architecture:
Operating System:  Unknown/Multiple  |  Unknown/Multiple
 Type of failure:  GHC rejects       |               Test Case:
  valid program                      |                Blocking:
      Blocked By:                    |  Differential Revisions:
 Related Tickets:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * type:  bug => feature request
 * milestone:   => ⊥


Comment:

 You could indeed consider this a failure of inference, but it's by-design
 (currently), and it's one I don't know how to fix.

 Consider this constraint that arise from `example`:
 {{{
 forall s. (F s ~ Int) => (s -> beta) ~ (sigma ~ Char)
 }}}
 Here
  * `beta` is a unification variable that arises from instantiating `b` in
 the call to `f`.
  * `sigma` is a unification variable that arises from instantiating `s` in
 the call to `k`.

 We can safely unify `sigma := s`, because the call to `k` is inside the
 polymorphic argument to `f`.  But it is less clear that we can unify `beta
 := Char` because both (a) it affects the inferred type of `(f k)`, and (b)
 the `(beta ~ Char)` is under an equality `F s ~ Int`..

 Suppose that instead of `F s ~ Int` it had been `F s ~ Char`.  Then should
 we unify `beta := Char` or `beta := F s`?  GHC never guesses,so instead it
 refrains from unifying `beta`, saying that it is "untouchable", hoping
 that some other constraint will determine how to unify `beta`.

 You may say that `(F s ~ Int)` can't possibly affect `beta`, but it should
 be clear that it's ''really'' hard to be sure about that.  GHC simply
 treats ''any'' equality in an implication constraint as making all the
 unification variables from an outer scope untouchable.

 This issue is discussed (somewhat) in 5.6.1 of the
 [https://wiki.haskell.org/Simonpj/Talk:OutsideIn OutsideIn paper]

 I'll mark this as a feature request!

 Simon

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10204#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler