Skip to content

Unmatchable arrows and data constructor promotion

This is halfway between a bug report and a design question. The immediate issue is that the following code works on current GHCs:

{-# LANGUAGE DataKinds #-}
module Bug where

import Data.Kind

data T = MkT (Type -> Type)

type S = MkT Maybe

However, it fails on the unsaturated_type_families branch:

[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:8:14: error:
    • Expected kind ‘* ~> *’, but ‘Maybe’ has kind ‘* -> *’
    • In the first argument of ‘MkT’, namely ‘Maybe’
      In the type ‘MkT Maybe’
      In the type declaration for ‘S’
  |
8 | type S = MkT Maybe
  |              ^^^^^

The cause appears to be that the -> arrow in the type of MkT's field gets renamed to ~>, which is not changed back when MkT is promoted to a type. In other words, the type of MkT is (Type ~> Type) ~> T, but the kind of 'MkT is (Type ~> Type) -> T.

Should it be promoted to (Type -> Type) -> Type instead? Granted, this is a bit of a thorny question since there's likely some use cases where you'd want one arrow and other use cases where you'd want the other arrow. As things currently stand, however, there is code that compiles in today's GHC but not with your branch, which is a bit suspicious.

Edited by Ryan Scott