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)
| ^^^^^^^^^^^^^^^^^^^