[GHC] #9161: Pattern synonyms interact badly with data kinds

[GHC]

#9161: Pattern synonyms interact badly with data kinds
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |            Owner:  cactus
            Type:  bug               |           Status:  new
        Priority:  lowest            |        Milestone:
       Component:  Compiler (Type    |          Version:  7.8.2
  checker)                           |         Keywords:  renamer, pattern
      Resolution:                    |  synonyms, data kinds
Operating System:  Unknown/Multiple  |     Architecture:  Unknown/Multiple
 Type of failure:  Compile-time      |       Difficulty:  Unknown
  crash                              |       Blocked By:
       Test Case:                    |  Related Tickets:
        Blocking:                    |
-------------------------------------+-------------------------------------
Changes (by cactus):

 * failure:  None/Unknown => Compile-time crash
 * component:  Compiler => Compiler (Type checker)
 * os:  Linux => Unknown/Multiple


Comment:

 This one is tricky...

 One would expect in this scenario roughly the same code path as if you
 write

 {{{
 {-# LANGUAGE DataKinds #-}
 data TYPE = CON

 wrongLift :: CON
 wrongLift = undefined
 }}}

 which BTW results in a reasonable error message:

 {{{
 Expected a type, but ‘CON’ has kind ‘TYPE’
 In the type signature for ‘wrongLift’: wrongLift :: CON
 }}}

 However, since pattern synonyms are internally handled as binds, not
 `TyClDecl`s, they are not yet in scope during kind checking (which is done
 by `tcTyClsInstDecls`) - hence the crash.

 How do we even get to trying to kindcheck them? `OccName.demoteOccName`
 handles data constructor names and type constructor names the same way,
 since we don't differentiate between the two there.

 So I think our best bet would be to have a bespoke internal kind for
 pattern synonyms,  inject pattern synonyms at that kind before doing kind
 checking, and then barf on types of that kind with a meaningful error
 message.

 Simon, does that sound like a good plan of action?

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