Curious kind-checking failure with GHC 9.2.1 and visible dependent quantification
While porting some code over to GHC 9.2.1 recently, I noticed an unusual quirk in the way kind inference interacts with visible dependent quantification. Consider these two modules:
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
module A where
import Data.Kind
type T1 :: Type -> Type
data T1 a = MkT1
t1FunA :: (forall a. T1 a -> r) -> r
t1FunA g = g MkT1
t1FunB :: T1 a -> T1 a -> ()
t1FunB _ _ = ()
type T2 :: forall (a :: Type) -> Type
data T2 a = MkT2
t2FunA :: (forall a. T2 a -> r) -> r
t2FunA g = g MkT2
t2FunB :: T2 a -> T2 a -> ()
t2FunB _ _ = ()
{-# LANGUAGE NoPolyKinds #-}
module B where
import A
g1 :: ()
g1 = t1FunA $ \x ->
let y = MkT1
in t1FunB x y
g2 :: ()
g2 = t2FunA $ \x ->
let y = MkT2
in t2FunB x y
The A
module defines two data types, T1
and T2
, as well as some functions which use them. The only difference between T1
and T2
is that the latter uses visible dependent quantification while the former does not. The B
module uses these functions in a relatively straightforward way. Note that B
does not enable PolyKinds
(I distilled this from a cabal
project which uses Haskell2010
).
What's curious about this is that while both g1
and g2
will typecheck on GHC 9.0.2, only g1
typechecks on GHC 9.2.1. On the other hand, g2
will fail to typecheck in GHC 9.2.1:
$ ghc-9.2.1 B.hs
[1 of 2] Compiling A ( A.hs, A.o )
[2 of 2] Compiling B ( B.hs, B.o )
B.hs:14:18: error:
• Couldn't match type ‘a’ with ‘*’
Expected: T2 a
Actual: T2 (*)
‘a’ is a rigid type variable bound by
a type expected by the context:
forall a. T2 a -> ()
at B.hs:(12,15)-(14,18)
• In the second argument of ‘t2FunB’, namely ‘y’
In the expression: t2FunB x y
In the expression: let y = MkT2 in t2FunB x y
• Relevant bindings include x :: T2 a (bound at B.hs:12:16)
|
14 | in t2FunB x y
| ^
I'm not confident enough to claim with 100% certainty that this is a regression, since the use of NoPolyKinds
might be throwing a wrench into things. Indeed, enabling PolyKinds
is enough to make the program accepted again. Still, the fact that this only fails if the data type uses visible dependent quantification (and only with GHC 9.2.1) is rather strange, so I wanted to file an issue to ask people more knowledgeable in this space than I am.