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@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-ty... 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