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

[GHC]

#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:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * cc: simonpj (added)
 * status:  closed => new
 * resolution:  fixed =>


Comment:

 Hm... I might have been a little too hasty in closing this ticket. This
 patch was undoubtedly an improvement over the status quo, as we now throw
 a proper error instead of silently accepting the original program.
 However, the error message leaves something to be desired:

 {{{
 T15828.hs:9:3: error:
     • Type indexes must match class instance head
       Expected: T (Maybe a) _
         Actual: T (Maybe a) b -- Defined at T15828.hs:9:20
     • In the type instance declaration for ‘T’
       In the instance declaration for ‘C (Maybe a)’
 }}}

 Why did this fail? It's extremely hard to tell, but it's because the two
 `a` variables aren't the same! I suspect that we're missing some necessary
 tidying here.

 Simon, this behavior appears to be new as of your commit
 2257a86daa72db382eb927df12a718669d5491f8 (`Taming the Kind Inference
 Monster`). In particular, this change looks suspicious:

 {{{#!diff
 +    pp_expected_ty = pprIfaceType (toIfaceType (mkTyConApp fam_tc
 expected_args))
 +                     -- Do /not/ tidy, because that will rename all those
 "_"
 +                     -- variables we have put in.  And (I think) the
 intance type
 +                     --  is already tidy
 }}}

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