Typeclass fails to compile with StandaloneKindSignatures; only compiles with conventional kind annotations
Summary
A typeclass compiles correctly with conventional kind annotations, but when the kinds are given with a standalone kind signature it ceases to compile.
Steps to reproduce
Try to compile this module:
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Main where
import Data.Kind
import Data.Proxy
import GHC.TypeLits
data Color
= R
| B
deriving (Show, Eq)
data Map symbol q
= E
| N Color (Map symbol q) symbol q (Map symbol q)
deriving (Show, Eq)
type Record :: (q -> Type) -> Map Symbol q -> Type
data Record f t where
Empty :: Record f E
Node :: Record f left -> f v -> Record f right -> Record f (N color left k v right)
type CanMakeBlack :: Map Symbol q -> Constraint
class CanMakeBlack t where
type MakeBlack t :: Map Symbol q
makeBlackR :: Record f t -> Record f (MakeBlack t)
instance CanMakeBlack (N color left k v right) where
type MakeBlack (N color left k v right) = N B left k v right
makeBlackR (Node left fv right) = Node left fv right
instance CanMakeBlack E where
type MakeBlack E = E
makeBlackR Empty = Empty
type Delable :: Symbol -> q -> Map Symbol q -> Constraint
class Delable k v t where
-- Using conventional kind annotations, it compiles correctly
--class Delable (k :: Symbol) (v :: q) (t :: Map Symbol q) where
type Del k v t :: Map Symbol q
del :: Record f t -> Record f (Del k v t)
type Deletable :: Symbol -> q -> Map Symbol q -> Constraint
class Deletable (k :: Symbol) (v :: q) (t :: Map Symbol q) where
type Delete k v t :: Map Symbol q
_delete :: Record f t -> Record f (Delete k v t)
instance (Delable k v t, Del k v t ~ deleted, CanMakeBlack deleted) => Deletable k v t where
type Delete k v t = MakeBlack (Del k v t)
_delete r = makeBlackR (del @_ @k @v r)
main :: IO ()
main = pure ()
The compilation will fail with the error:
Main.hs:70:15: error:
* Could not deduce: MakeBlack (Del k v t) ~ MakeBlack (Del k v t)
from the context: (Delable k v t, Del k v t ~ deleted,
CanMakeBlack deleted)
bound by the instance declaration at Main.hs:68:10-86
Expected: Record f (Delete k v t)
Actual: Record f (MakeBlack (Del k v t))
NB: `MakeBlack' is a non-injective type family
However, if instead of the line
class Delable k v t where
We use the line
class Delable (k :: Symbol) (v :: q) (t :: Map Symbol q) where
The code compiles correctly, even if the standalone kind signature remains.
Expected behavior
The code should compile correctly with the standalone kind signature, without need of explicit kind annotations on the variables.
Environment
- GHC version used: 9.0.1
Optional:
- Operating System: Windows 10