[GHC] #12534: GHC 8.0 accepts recursive kind signature that GHC 7.10 rejects

24 Aug 2016

      #12534: GHC 8.0 accepts recursive kind signature that GHC 7.10 rejects
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC accepts
  Unknown/Multiple                   |  invalid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 GHC 7.10 rejects this datatype:

 {{{#!hs
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE PolyKinds #-}
 module Bug where

 data T (a :: a)
 }}}

 {{{
 $ /opt/ghc/7.10.3/bin/ghc Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:5:1:
     Kind variable also used as type variable: ‘a’
     In the data type declaration for ‘T’
 }}}

 But GHC 8.0 accepts the above code! It appears that GHC implicitly
 freshens the kind-level `a` so as to have a different name, since the
 following modification to `T`:

 {{{#!hs
 data T a (a :: a)
 }}}

 Results in this error:

 {{{
 $ /opt/ghc/8.0.1/bin/ghc Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:5:8: error:
     Conflicting definitions for ‘a’
     Bound at: Bug.hs:5:8
               Bug.hs:5:11

 Bug.hs:5:16: error:
     Type variable ‘a’ used in a kind.
     Did you mean to use TypeInType?
     the data type declaration for ‘T’
 }}}

 But with this modification:

 {{{#!hs
 data T (a :: a) a
 }}}

 You won't get an error message about `a` being used as both a kind and
 type:

 {{{
 $ /opt/ghc/8.0.1/bin/ghc Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:5:9: error:
     Conflicting definitions for ‘a’
     Bound at: Bug.hs:5:9
               Bug.hs:5:17
 }}}

 To make things even more confusing, this behavior doesn't seem to carry
 over to typeclass instances. For example: GHC 8.0 will (rightfully) reject
 this code:

 {{{#!hs
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE PolyKinds #-}
 module Bug where

 data T (a :: a)

 class C x
 instance C (T (a :: a))
 }}}

 {{{
 $ /opt/ghc/8.0.1/bin/ghc Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:8:16: error:
     Variable ‘a’ used as both a kind and a type
     Did you intend to use TypeInType?
 }}}

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12534
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler