Skip to content

Inconsistent matchability inference for open type families

In this program, I would expect Sing1, Sing2, and Sing3 to have the same kind:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

import Data.Kind
import GHC.Exts

type Sing1 :: k -> Type
type family Sing1

type Sing2 :: k -> Type
type family Sing2 :: k -> Type

type family Sing3 :: k -> Type

However, this isn't the case:

λ> :set -fprint-explicit-foralls -fprint-explicit-matchabilities
λ> :kind Sing1
Sing1 :: forall {t :: Matchability} k. k -> @(t) *
λ> :kind Sing2
Sing2 :: forall {t :: Matchability} k. k -> @(t) *
λ> :kind Sing3
Sing3 :: forall k. k -> @('Matchable) *

The extra matchability polymorphism in Sing1 and Sing2 is somewhat bothersome, since it prevents the following from typechecking due to the matchability variable being treated as existential:

newtype WrappedSing1 a = WrapSing1 (Sing1 a)
Bug.hs:17:26: error:
    • A newtype constructor cannot have existential type variables
      WrapSing1 :: forall {k} (a :: k) {t :: Matchability}.
                   Sing1 @{t} @k a -> @('Unmatchable) WrappedSing1 @{k} a
    • In the definition of data constructor ‘WrapSing1’
      In the newtype declaration for ‘WrappedSing1’
   |
17 | newtype WrappedSing1 a = WrapSing1 (Sing1 a)
   |                          ^^^^^^^^^^^^^^^^^^^