Thanks Richard, indeed that proposal would not help.  The snippet I posted is a valid GADT syntax.  When it is compiled with `DataKinds`, `PolyKinds` and `KindSignatures` ghc is is quite explicit why it refuses it: Expected a type, but `x` has a kind `a`, which is exactly what you said. However, I think it would be quite reasonable to accept it. In general ghc would only need to generate code for the case `a ~ Type`, all other use cases at term level must be refused. It might be enough to add a type inference rule which injects `a ~ Type` for any such term. Another missing puzzle is that there's no way to specify that one only wants the promoted types / kinds without the term level part. This could be done by specifying an explicit kind signature: ``` type K0 :: a -> K a data K a where   K0 :: forall a (x :: a) -> K a ``` Now this is refused with `The standalone kind signature for 'K0' lacks an accompynying binding`. It's not the first time I stumbled upon this.  The latest incarnation is a gist in which I worked out how to encode pipelining using a type level queue / list in a session type framework which we use at work for developing protocols: https://gist.github.com/coot/b568ebc7bac2e4e31cb54bf3939419d8#file-pipelined... Richard, does it sound reasonable to you? If so, what would be the right process to propose / implement such a feature? I don't think it would require a new extension, rather modify how `DataKind` works in presence of `PolyKinds` and `StandaloneKindSignatures`. Maybe this is in scope of the dependent type Haskell workstream that you're doing? Best regards, Marcin ‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐ On Monday, May 3rd, 2021 at 16:11, Richard Eisenberg wrote:

Perhaps Marcin is looking for https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0402-ga..., but that proposal would not accept the code in the original post, for the reasons Kai describes -- you just cannot have (x :: a) on one side of an arrow.

Richard

...

On May 3, 2021, at 9:10 AM, Kai-Oliver Prott wrote:

...

Hi,

...

I think I don't quite understand the question.

...

The code you propose seems wrong to me for a different reason:

...

The type constructor (->) for function values has Kind: * -> * -> *

...

In fact, GHC will print this error when compiling the snippet with the corresponding extensions.

...

Promoting a data type is done differently.

...

Can you elaborate on what exactly it is you are proposing?

...

Sincerely

...

Kai Prott

...

On 03.05.21 14:04, coot@coot.me wrote:

...

...

Hello,

...

...

Currently with `DataKind` extension, Haskell allows to promote terms / types to types / kinds. Currently, one cannot write:

...

...

``` data K a where K0 :: forall (x :: a). x -> K a ```

...

...

Because `K0` is both a term and a type constructor, and as a term and one cannot represent `x` of kind `a`. Is there a proposal or an issue to allow such declaration and error at use sites of `K0` as a term, rather than at declaration site?

...

...

Best regards, Marcin Szamotulski

...

...

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

...

_______________________________________________

...

Haskell-Cafe mailing list

...

To (un)subscribe, modify options or view archives go to:

...

http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

...

Only members subscribed via the mailman list are allowed to post.

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 wrote:

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

Hi David, My workaround is to use:

data K a where

   K0 :: forall a b. b -> K a

The kind `K Bool` contains things like:

:kind! K0 'True

(K0 'True) :: K Bool

:kind! K0 'False

(K0 'True) :: K Bool But also

:kind! (K0 Int :: K Bool)

(K0 Int :: K Bool) :: K Bool and I'd like to have a way to not allow to construct such a type. Oh!, what I just realised is that I can actually achieve what I want by simply declaring:

data K a where

   K0 :: forall a. a -> K a

Now the type constructor of a type of kind `K Bool`, must is `K0 'True`, `K0 'False`, or `K0` of some exotic type of kind `Bool`. Thanks for making me realise that! Regards, Marcin ‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐ On Monday, May 3rd, 2021 at 22:44, David Feuer wrote:

On Mon, May 3, 2021, 8:04 AM wrote:

...

Currently with `DataKind` extension, Haskell allows to promote terms / types to types / kinds.  Currently, one cannot write:

...

```

...

data K a where

...

  K0 :: forall (x :: a). x -> K a

...

```

I feel like I'm missing something. Suppose `a` is not Type but rather, say, Bool. Then `x` has kind Bool. That is, x is 'True, 'False, or something exotic. K0 @Bool is then a function that takes anything of type 'True or type 'False and gives you something of type K Bool. What I think Richard is getting at is that there isn't anything of type 'True or type 'False, whether at the term level or the type level. These things only exist when `a` is Type (or TYPE rep for some rep :: RuntimeRep). So it's pretty hard to see what you're trying to do.

Thank you Richard, everything clear now. Sent from ProtonMail mobile \-------- Original Message -------- On 3 May 2021, 23:57, Richard Eisenberg < rae@richarde.dev> wrote:

Sounds like you've figured this out, so I won't write a long response to your previous email -- but let me know if there are still outstanding questions there.

Thanks,

Richard

...

On May 3, 2021, at 5:26 PM, [coot@coot.me][coot_coot.me] wrote:

Now the type constructor of a type of kind \`K Bool\`, must is \`K0 'True\`, \`K0 'False\`, or \`K0\` of some exotic type of kind \`Bool\`.

Thanks for making me realise that!

[coot_coot.me]: mailto:coot@coot.me