Re: [GHC] #15828: Type family equation foralls allow strange re-quantification of class-bound type variables

30 Nov 2018

      #15828: Type family equation foralls allow strange re-quantification of class-bound
type variables
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.8.1
       Component:  Compiler          |              Version:  8.7
      Resolution:                    |             Keywords:  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
                                     |  rename/should_fail/T15828
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):  Phab:D5283
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Replying to [comment:10 simonpj]:
...
What is 12eeb9?
...
Quite true.  So what would we ''like'' to show here?  Once we decide
It's referring to commit 512eeb9bb9a81e915bfab25ca16bc87c62252064 (the
 leading "5" was simply dropped by mistake).

 that we can think how to achieve it.

 I was quite fond of the way it was printed at the time that I landed the
 patch:

 {{{
     • Type indexes must match class instance head
       Expected: T (Maybe a1) <tv>
         Actual: T (Maybe a) b
 }}}

 That is, using tidying to emphasize the difference between the two `a`s.

 Unfortunately, I didn't notice that your commit had changed this until I
 `validate`d the whole set of patches I was about to commit, at which point
 I just accepted the new output and moved on. (Upon further thought, I
 realized the new output was rather smelly, which is why I reopened this
 ticket.)
...
I'm quite keen on using "_" for the bits that don't matter
...
but if needs must, instead of printing `(F t1 t2 t3)` with one call, we
 can make separate calls for `t1`, `t2`, `t3` etc, and that would eliminate
Sure. I have no preference as to whether we display other type variables
 as `_`, `<tv>`, or something else.

 the need to fake-up a tyvar "_" which you'll see in the code.

 I'm afraid I have no idea what you are referring to with this sentence.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15828#comment:11
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler