PolyKinds: kind information for variables bound in instance heads propagates surprisingly badly
Summary
Here's a a reduction of a program I was writing.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE FlexibleConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
module Repro where
import Data.Kind
data P = L | R
data T (a :: P) where
A :: T a
B :: T R
type TConstraint = forall a . T a -> Constraint
class (forall a . constr @a A) => ForAllA (constr :: TConstraint)
instance (forall a . constr @a A) => ForAllA constr
GHC says:
Repro.hs:18:22: error:
• Cannot apply function of kind ‘k0’
to visible kind argument ‘a’
• In the instance declaration for ‘ForAllA constr’
|
18 | instance (forall a . constr @a A) => ForAllA constr
i.e. it has inferred that constr
in the instance declaration should have kind k
. I already find this suprising: the class declaration states that for this class, constr
always has the given kind, so I'd have expected that to propagate. Anyway, let's try and fix it.
- Kind signature on the instance head
instance (forall a . constr @a A) => ForAllA (constr :: TConstraint)
Same error.
- Standalone kind signatures
type ForAllA :: TConstraint -> Constraint
class (forall a . constr @a A) => ForAllA constr
instance (forall a . constr @a A) => ForAllA constr
Same error.
- Explicit quantification in the instance head
instance forall (constr :: MethodConstraint) . (forall a . constr @a A) => ForAllA constr
That finally works!
I'm not totally surprised that 2 doesn't work, but I am surprised that 1 doesn't work. That's usually how we constrain type variables in the absence of standalone kind signatures (which we can't write for instance declarations).
Steps to reproduce
The file above should be independently compilable.
Environment
- GHC version used: 9.2.3