[GHC] #12088: Type/data family instances in kind checking

[GHC]

#12088: Type/data family instances in kind checking
-------------------------------------+-------------------------------------
        Reporter:  alexvieth         |                Owner:
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.2.1
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11348, #12239    |  Differential Rev(s):  Phab:D2272
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by mpickering):

 @Richard, it seems to me the crux of the problem is that type instances
 introduce equalities so they must be interleaved with the other
 declarations. Data instances are just one place where these extra
 equalities can be used, another being kind checking for type equalities as
 in comment:17.

 Here is the wiki page I started. It is not complete but I am too tired to
 carry on tonight. Perhaps you could look Alex and fill in some of the
 details?

 https://ghc.haskell.org/trac/ghc/wiki/InterleavingTypeInstanceChecking

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