Faulty rigid type variable with standalone deriving-via and PolyKind
Summary
In Ghci (and Ghci only!), a query such as
deriving via
Generically1 (Product f g)
instance
(Applicative f, Applicative g) => Applicative (Product f g)
Can fail to typecheck with the following error (in GHC 9.2 it even produces a NoSkolem anomaly, I assume the anomaly has been fixed as part of !7105 (closed)):
src/Data/Functor/Linear/Internal/Applicative.hs:29:18: error:
• Couldn't match kind ‘k’ with ‘*’
Expected kind ‘* -> *’, but ‘f’ has kind ‘k -> *’
‘k’ is a rigid type variable bound by
the deriving clause for ‘Generically1 (Product f g)’
at src/Data/Functor/Linear/Internal/Applicative.hs:27:3-28
• In the first argument of ‘Applicative’, namely ‘f’
In the stand-alone deriving instance for
‘(Applicative f, Applicative g) => Applicative (Product f g)’
|
29 | (Applicative f, Applicative g) => Applicative (Product f g)
| ^
A key ingredient, here, is that f
is supposed to have Type -> Type
, for a type class with variables of kind Type
, the problem doesn't appear to show up.
It is a regression compared to GHC 9.0 [@monoidal points out that this is do to GHC 9.2 having PolyKinds
enabled by default].
Steps to reproduce
Load a file with the following content in Ghci:
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE NoImplicitPrelude #-}
module Data.Functor.Linear.Internal.Applicative
( Applicative (..),
)
where
import GHC.Types
-- type Product :: (Type -> Type) -> (Type -> Type) -> Type -> Type
data Product f g a = Pair (f a) (g a)
-- type Generically1 :: (Type -> Type) -> Type -> Type
newtype Generically1 f a = Generically1 (f a)
type Functor :: (Type -> Type) -> Constraint
class Functor f where
class Functor f => Applicative f where
deriving instance (Functor f, Functor g) => Functor (Product f g)
deriving via
Generically1 (Product f g)
-- Geneically1 (Product (f :: Type -> Type) g)
instance
(Applicative f, Applicative g) => Applicative (Product f g)
The bug disappears when either signature is uncommented. Or when the Generically1 (Product …)
lines is replaced by the commented out one.
It also disappears when built with [actually the behaviour of ghc
rather than loaded in ghci
. Which makes me think that this bug is a companion to #20169.ghc
and ghci
is identical the difference that I observed was probably due to the fact that stack ghci
doesn't respect the language stanza from the cabal file]
Expected behavior
Evidently, the inferred type for Product
is forall k. (k -> Type) -> (k -> Type) -> k -> Type
. But why this k
would be made rigid in the case at hand, I have no idea. I don't think that it should be.
I expect k
to be a unification variable, and the whole standalone deriving
clause to type check without my help.
Environment
- GHC version used: 9.3.20220406