Skip to content

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
Edited by Las Safin
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information