[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 goldfire):

 Replying to [comment:16 alexvieth]:

 > 1. Do SCC analysis on all declarations except for open type family
 instances, to give ordered `TyClGroup`s and the set of those instances (in
 source file order).
 > 2. Before checking the `TyClGroup`s, put all equalities arising from the
 open type family instances into the environment (assume for now that
 they're well-kinded).
 > 3. Check the `TyClGroup`s in order as usual.
 > 4. Check the open type family instances (verifying or falsifying the
 assumption in 2).
 >
 > Maybe this is nonsense. Would it be possible to make and use a coercion
 axiom without kind checking the lhs and rhs types?

 I'm not sure I understand. Currently, kind-checking an instance and
 desugaring it are all done at the same time, so step (2) is hard to
 implement. Let's say we get around that barrier, though. This would then
 put ill-kinded equalities into the context. I think it would be awfully
 hard to avoid getting GHC to loop or do other silly things with a bad
 context. Perhaps you could squeeze this through, but I'm very skeptical.

 Or am I misunderstanding something?

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