[GHC] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

6 Oct 2017


      #14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
  (Type checker)                     |
           Keywords:  deriving       |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 GHC rejects this program:

 {{{#!hs
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
 module Bug where

 class C a b

 data D = D deriving (C (a :: k))
 }}}

 {{{
 GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:8:1: error:
     Kind variable ‘k’ is implicitly bound in datatype
     ‘D’, but does not appear as the kind of any
     of its type variables. Perhaps you meant
     to bind it (with TypeInType) explicitly somewhere?
   |
 8 | data D = D deriving (C (a :: k))
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

 But it really shouldn't, since it's quite possible to write the code that
 is should generate:

 {{{#!hs
 instance C (a :: k) D
 }}}

 Curiously, this does not appear to happen for data family instances, as
 this typechecks:

 {{{#!hs
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeFamilies #-}
 module Bug where

 class C a b

 data family D1
 data instance D1 = D1 deriving (C (a :: k))

 class E where
   data D2

 instance E where
   data D2 = D2 deriving (C (a :: k))
 }}}

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