Impredicative kinds & type synonyms seemingly don't work together
Steps to reproduce
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
import Data.Proxy (Proxy)
import Data.Functor.Identity (Identity (Identity))
import Data.Kind (Type)
-- Changing this to a type family doesn't work either (EDIT: see new comment)
type P :: forall a. a -> Type
type P = Proxy
type Good :: Identity (forall a. a -> Type)
type Good = 'Identity @(forall a. a -> Type) Proxy
type Bad :: Identity (forall a. a -> Type)
type Bad = 'Identity @(forall a. a -> Type) P
{-
Example.hs:17:45: error:
• Expected kind ‘forall a. a -> Type’,
but ‘P’ has kind ‘a0 -> Type’
• In the second argument of ‘'Identity’, namely ‘P’
In the type ‘'Identity @(forall a. a -> Type) P’
In the type declaration for ‘Bad’
|
17 | type Bad = 'Identity @(forall a. a -> Type) P
-}
Expected behavior
Bad
should seemingly also work, but I would be satisfied with a work-around if there is one.
Environment
- GHC version used: 9.4.2