Hi Richard,
type K :: Bool -> Type data K b where MkK :: forall a (b :: a). K b
This requests `b` to be of kind `a` for any `a`, and it constraint `b` to by of kind `Bool`, so this cannot be satisfied.
data K a where K0 :: forall (x :: Type). x -> K Type
There are two levels here: 1. `K a` is a perfectly defined type with a single constructor `K0`. This is not what I am looking for. 2. `K a` is a kind, `K0 x` for any `x :: Type` is a type of kind `K a`. This will work only for `x`-es which are of kind `Type`, am interested in `x`-es which are of other kind. So one can proceed with this:
data K a where K0 :: forall x. x -> K a
The problem here is that the promoted type `K0` is too broad, I'd like to express that I am only interested with `x`-es of kind `a`.
f :: forall a (b :: a). b -> b
Let's get one step back. If I couldn't write this
f :: forall (b :: A). b -> b
I would be forced to write this
f :: forall b. b -> b
And these are very different (e.g. free theorems). The concrete 'A', in my case gets generalised and constraint by some type class. Hence the framework requires
f :: forall a (b :: a). b -> b
though all the instances provide and use a concrete `a`. I see your point on error messages, maybe there's a way around it. Let's say that the author must provide an explicit kind signature, e.g.
type K0 :: a -> K a data K a where K0 :: x -> K a
Such K0 can only be a type; When one would use it at a term level GHC should say: data constructor not in scope (and possibly explain that there is a type of the same name).
Marcin
‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐
On Monday, May 3rd, 2021 at 19:12, 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@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