[GHC] #14441: GHC HEAD regression involving type families in kinds

[GHC]

#14441: GHC HEAD regression involving type families in kinds
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.4.1
       Component:  Compiler          |              Version:  8.3
      Resolution:                    |             Keywords:  TypeInType,
                                     |  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #13790            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * cc: goldfire (added)


Comment:

 Gah! This is a nice small test case thank you.

 In `TcFlatten.flatten_exact_fam_app_fully` I see
 {{{
                    -- NB: fsk's kind is already flattend because
                    --     the xis are flattened
                    ; return (mkTyVarTy fsk, maybeSubCo eq_rel (mkSymCo co)
                                             `mkTransCo` ret_co ) }
 }}}
 But the comment is a lie.  With the `DemoteX` above, the `fsk` will have
 type `Demote k` for some kind `k`, which is not flat.  So the flattener's
 invariant (that flattened types have flattened kinds) is not respected).
 And that is ultimately the reason that we don't kick out an inert
 constraint that we should.

 Richard, what do you think?

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