[Haskell-cafe] Promoted data types

[Richard Eisenberg]

Hi Marcin,

To understand your intent better, what do you think of this:

> type K :: Bool -> Type
> data K b where
>   MkK :: forall a (b :: a). K b

Here, the issue isn't whether `a` is `Type`, but whether `a` is `Bool`. Do you think that should be accepted?

And why restrict this only to GADT type signatures? What about

> f :: forall a (b :: a). b -> b

My personal opinion is that we should reject all of these, including your initial suggestion. You're right in that we could infer an extra equality constraint, but I think that would lead to a worse user experience: a definition is accepted only to be rejected at usage sites. It's almost like accepting

> g x = not x : "hello"

which could be accepted with an equality constraint (Bool ~ Char). I recognize this last one goes a step further into absurdity, but there is a balance between inferring equality constraints and issuing helpful errors.

Put another way: Why not write your original datatype as
> data K a where
>   K0 :: forall (x :: Type). x -> K Type

? That would be accepted and may have your intended meaning.

> On May 3, 2021, at 12:44 PM, coot at coot.me wrote:
> 
> Another missing puzzle is that there's no way to specify that one only wants the promoted types / kinds without the term level part.

Aha. This one really has been proposed (and accepted!): https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0106-type-data.rst

There is no one working on an implementation of it yet, though. I'd be happy to advise someone who wanted to dive in!

Richard