GND is subtly broken w.r.t. higher-rank kinds
The following program ought to compile:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Coerce
import Data.Kind
import Data.Type.Equality
class HTestEquality (f :: forall k. k -> Type) where
hTestEquality :: forall k1 k2 (a :: k1) (b :: k2).
f a -> f b -> Maybe (a :~~: b)
newtype T :: (forall k. k -> Type) -> (forall k. k -> Type) where
MkT :: forall (f :: forall k. k -> Type) k (a :: k). f a -> T f a
deriving instance forall (f :: forall k. k -> Type).
HTestEquality f => HTestEquality (T f)
Unfortunately, it doesn't. Here is what happens if you try to compile this with GHC HEAD:
$ ~/Software/ghc5/inplace/bin/ghc-stage2 -ddump-deriv Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
==================== Derived instances ====================
Derived class instances:
instance forall (f :: forall k. k -> *).
Bug.HTestEquality f =>
Bug.HTestEquality (Bug.T f) where
Bug.hTestEquality
= GHC.Prim.coerce
@(f_a12D k1_a11H a_a11J
-> f_a12D k2_a11I b_a11K
-> GHC.Maybe.Maybe ((Data.Type.Equality.:~~:) @k1_a11H @k2_a11I a_a11J b_a11K))
@(Bug.T f_a12D k1_a11H a_a11J
-> Bug.T f_a12D k2_a11I b_a11K
-> GHC.Maybe.Maybe ((Data.Type.Equality.:~~:) @k1_a11H @k2_a11I a_a11J b_a11K))
(Bug.hTestEquality @f_a12D) ::
forall (k1_a11H :: TYPE GHC.Types.LiftedRep)
(k2_a11I :: TYPE GHC.Types.LiftedRep)
(a_a11J :: k1_a11H)
(b_a11K :: k2_a11I).
Bug.T f_a12D k1_a11H a_a11J
-> Bug.T f_a12D k2_a11I b_a11K
-> GHC.Maybe.Maybe ((Data.Type.Equality.:~~:) @k1_a11H @k2_a11I a_a11J b_a11K)
Derived type family instances:
Bug.hs:22:1: error:
• Expected kind ‘k4 -> *’, but ‘T f k1’ has kind ‘*’
• In an expression type signature:
forall (k1 :: TYPE GHC.Types.LiftedRep)
(k2 :: TYPE GHC.Types.LiftedRep)
(a :: k1)
(b :: k2).
T f k1 a -> T f k2 b -> Maybe ((:~~:) @k1 @k2 a b)
In the expression:
coerce
@(f k1 a -> f k2 b -> Maybe ((:~~:) @k1 @k2 a b))
@(T f k1 a -> T f k2 b -> Maybe ((:~~:) @k1 @k2 a b))
(hTestEquality @f) ::
forall (k1 :: TYPE GHC.Types.LiftedRep)
(k2 :: TYPE GHC.Types.LiftedRep)
(a :: k1)
(b :: k2).
T f k1 a -> T f k2 b -> Maybe ((:~~:) @k1 @k2 a b)
In an equation for ‘hTestEquality’:
hTestEquality
= coerce
@(f k1 a -> f k2 b -> Maybe ((:~~:) @k1 @k2 a b))
@(T f k1 a -> T f k2 b -> Maybe ((:~~:) @k1 @k2 a b))
(hTestEquality @f) ::
forall (k1 :: TYPE GHC.Types.LiftedRep)
(k2 :: TYPE GHC.Types.LiftedRep)
(a :: k1)
(b :: k2).
T f k1 a -> T f k2 b -> Maybe ((:~~:) @k1 @k2 a b)
When typechecking the code for ‘hTestEquality’
in a derived instance for ‘HTestEquality (T f)’:
To see the code I am typechecking, use -ddump-deriv
|
22 | deriving instance forall (f :: forall k. k -> Type).
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Yikes! There are actually two different (but related) things going wrong here:
- The first visible type argument to
coerce
isf k1 a -> f k2 b -> Maybe ((:~~:) @k1 @k2 a b)
, but this really ought to bef @k1 a -> f @k2 b -> Maybe ((:~~:) @k1 @k2 a b)
instead. The reason this happens is becauseHsUtils.typeToLHsType
(which powersGeneralizedNewtypeDeriving
's code generation) doesn't take visibility into account properly when dealing withAppTy
s likeAppTy (AppTy f k1) a
. - The second visible type argument to
coerce
isT f k1 a -> T f k2 b -> Maybe ((:~~:) @k1 @k2 a b)
, but this really ought to beT f @k1 a -> T f @k2 b -> Maybe ((:~~:) @k1 @k2 a b)
instead. This one is a bit more perplexing, but some digging has revealed thatType.fun_kind_arg_flags
is the culprit. Namely,fun_kind_arg_flags
simply isn't equipped to deal with kind that have nestedforall
s like(forall k. k -> Type) -> (forall k. k -> Type)
, and if it does encounter such a kind, it bails out and incorrectly claims that all arguments are required.
Both of these buglets are quite straightforward to fix. Patch incoming.