[GHC] #11837: GHC fails to unify kinds when deriving polykinded typeclass instance for polykinded newtype

14 Apr 2016

      #11837: GHC fails to unify kinds when deriving polykinded typeclass instance for
polykinded newtype
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  RyanGlScott
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #8865, #11833
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This is failing:

 {{{#!hs
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE PolyKinds #-}
 module Example where

 class Category (cat :: k -> k -> *) where
   catId   :: cat a a
   catComp :: cat b c -> cat a b -> cat a c

 newtype T (c :: k -> k -> *) a b = MkT (c a b) deriving Category
 }}}

 with the following error:

 {{{
 $ /opt/ghc/8.0.1/bin/ghc Example.hs -fprint-explicit-kinds -ddump-deriv
 [1 of 1] Compiling Example          ( Example.hs, Example.o )

 ==================== Derived instances ====================
 Derived instances:
   instance forall k_ayw k_ayx (c_ayy :: k_ayx
                                         -> k_ayx -> GHC.Types.*).
            Example.Category k_ayw c_ayy =>
            Example.Category k_ayw (Example.T k_ayx c_ayy) where
     Example.catId
       = GHC.Prim.coerce (Example.catId :: c_apb a_apg a_apg) ::
           forall (a_apg :: k_XxC). Example.T c_apb a_apg a_apg
     Example.catComp
       = GHC.Prim.coerce
           (Example.catComp ::
              c_apb b_aph c_api -> c_apb a_apj b_aph -> c_apb a_apj c_api)
 ::
           forall (b_aph :: k_XxC) (c_api :: k_XxC) (a_apj :: k_XxC).
           Example.T c_apb b_aph c_api
           -> Example.T c_apb a_apj b_aph -> Example.T c_apb a_apj c_api

 GHC.Generics representation types:

 Example.hs:9:57: error:
     • Expected kind ‘k1’, but ‘a1’ has kind ‘k’
     • In the second argument of ‘T’, namely ‘a’
       In an expression type signature: forall (a :: k). T c a a
       In the expression:
           GHC.Prim.coerce (catId :: c a a) :: forall (a :: k). T c a a
       When typechecking the code for ‘catId’
         in a derived instance for ‘Category k (T k c)’:
         To see the code I am typechecking, use -ddump-deriv
     • Relevant bindings include
         catId :: T k1 c a a (bound at Example.hs:9:57)
 }}}

 This is very similar to #11833, but in this scenario, //both// the
 datatype and typeclass are poly-kinded, and I believe the issue here is
 fundamentally different.

 With `-fprint-explicit-kinds`, it becomes apparent what the issue is: for
 some reason, the kind variable of `Category` (`k_ayw`) is not unifying
 with the kind variable of `T` (`k_ayx`), resulting in a kind mismatch.

 I'll fix this - patch incoming.

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