[GHC] #15621: Error message involving type families points to wrong location

[GHC]

#15621: Error message involving type families points to wrong location
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.4.3
  checker)                           |
      Resolution:                    |             Keywords:  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Poor/confusing    |  Unknown/Multiple
  error message                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 We have `Refl :: forall a. Refl a a`

 So from the defn of `a` we instantiate `Refl` with `a := alpha`, and get
 {{{
 [W] c1 :: alpha ~ F Int   -- Line 12
 [W] c2 :: alpha ~ F Int   -- Line 12
 }}}
 Each constraint carries its birth location, which I show here.
 Same for `b`, instantiating `Refl` with `a := beta`:
 {{{
 [W] c3 :: beta ~ F Int     -- Line 15
 [W] c4 :: beta ~ F Bool    -- Line 15
 }}}
 Then depending on the order in which we try to solve, we might do
 {{{
    alpha := beta
    beta  := F Bool   -- solves c4
 }}}
 Now, substituting for these unified varaiables, we get
 {{{
 [W] c1 :: F Bool ~ F Int   -- Line 12
 [W] c2 :: F Bool ~ F Int   -- Line 12
 [W] C3 :: F Bool ~ F Int   -- Line 15
 }}}
 Since these are identical, we pick one; and alas, it is `c1`.
 So that's why we get a bogus message.

 Richard, I'd be interested in your views.

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