[GHC] #13333: Typeable regression in GHC HEAD

[GHC]

#13333: Typeable regression in GHC HEAD
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  bgamari
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.2.1
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |
      Resolution:                    |             Keywords:  typeable
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):  Phab:D3424
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 I'm sorry, but I still don't get it.  Why don't we fix the bug that makes
 the Note untrue?  I do not understand why it's bad for an evidence term
 (which the constraint solver never looks at) to be Refl, if it relates two
 types that are equal after zonking.

 Your diagnosis concludes

 > And then, when c2 gets put in the inert set, its kind still mentions
 unzonked variables.

 But you do not say why that matters. I think it should not matter.

 Can you explain more precisely what goes wrong and why?

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