Skip to content

Inconsistent treatment of type family arities in TLKSs

Consider this program:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TopLevelKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

import Data.Kind

type T1 :: forall k (a :: k). Type
type family T1

-- type T2 :: forall {k} (a :: k). Type
type T2 :: forall a. Type
type family T2

T1 and T2 look the same, but they actually get assigned very different arities, as GHCi reveals when -fprint-explicit-kinds is enabled:

λ> :set -fprint-explicit-kinds -fprint-explicit-foralls
λ> :info T1
type family T1 @k @(a :: k) :: *        -- Defined at ../Bug.hs:10:1
λ> :info T2
type family T2 :: forall {k} (a :: k). *
        -- Defined at ../Bug.hs:14:1

T1 has arity two, whereas T2 has arity zero! I find this rather surprising given that there are no syntactic differences in the declarations for T1 and T2—the only differences lie in the visibility of the k in their kinds. I would expect T1 and T2 to have the same arity here.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information