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

GHC ghc-devs at haskell.org
Wed Sep 12 20:46:05 UTC 2018


#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):

 > I don't agree with the details in comment:3.

 Yes, I was abbreviating!  What we get is
 {{{
 -- From 'a'
 [W] fsk1 ~ alpha  (CTyEqCan)
 [W] F Int ~ fsk1  (CFunEqCan)
 [W] fsk1 ~ alpha  (CTyEqCan)

 -- From 'b'
 [W] fsk1 ~ beta    (CTyEqCan)
 [W] fsk2 ~ beta    (CTyEqCan)
 [W] F Bool ~ fsk2  (CFunEqCan)
 }}}
 Then from `[W] fsk1 ~ alpha` and `[W] fsk1 ~ beta` we get `[D] alpha ~
 beta`.
 And that leads to `alpha := beta`.  The `beta := F Bool` comes during
 unflattening.

 The purpose of the Derived constraints is precisely to lead to
 unifications,
 exactly as we do here.  So we probalbly don't want to stop that happening.

 Why do we get `fsk1 ~ alpha` rather than `alpha ~ fsk1` followed by
 unification?
 See `Note [Canonical orientation for tyvar/tyvar equality constraints]` in
 `TcCanonical`, and `Note [Eliminate flat-skols]` in `TcType`.

 I think this ticket is closely related to Trac #14185.  If we put the
 constraints
 from the two definitions into separate implication constraints (with no
 skolems
 and no givens), I think the Right Thing would happen.  You'll see some
 half
 written code, commented out, around `alwaysBuildImplication` in `TcUnify`.
 I think that'd fix this.

 But I didn't have time to review all the error message wibbles -- probably
 many
 are improvements.  Does anyone else want to have a go?  The code is there!

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


More information about the ghc-tickets mailing list