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.