GHC fails to unify kinds when deriving polykinded typeclass instance for polykinded newtype
This is failing:
{-# 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 (closed), 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.
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |