## #13761 closed bug (invalid)

# Can't create poly-kinded GADT with TypeInType enabled, but can without

Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | |

Component: | Compiler (Type checker) | Version: | 8.0.1 |

Keywords: | TypeInType | Cc: | |

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | GHC rejects valid program | Test Case: | |

Blocked By: | Blocking: | ||

Related Tickets: | Differential Rev(s): | ||

Wiki Page: |

### Description

Surprisingly, this compiles without `TypeInType`

:

{-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} module Works where import Data.Kind data T :: k -> Type where MkT :: T Int

But once you add `TypeInType`

:

{-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind data T :: k -> Type where MkT :: T Int

then it stops working!

GHCi, version 8.3.20170516: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:11:12: error: • Expected kind ‘k’, but ‘Int’ has kind ‘*’ • In the first argument of ‘T’, namely ‘Int’ In the type ‘T Int’ In the definition of data constructor ‘MkT’ | 11 | MkT :: T Int | ^^^

This bug is present in GHC 8.0.1, 8.0.2, 8.2.1, and HEAD.

What's strange about this bug is that is requires that you write `T`

with an explicit kind signature. If you write `T`

like this:

data T (a :: k) where MkT :: T Int

Then it will work with `TypeInType`

enabled.

### Change History (9)

### comment:1 Changed 14 months ago by

### comment:2 follow-up: 3 Changed 14 months ago by

This behavior is all expected... or, in one case, not unexpected.

The very first example in the OP is regrettable, but it is "not unexpected", as `-XNoTypeInType`

rejects such programs on a best-effort basis. That one is hard.

The other examples are all consequences of the CUSK rules.

Proposed solution: allow top-level kind signatures of type-level declarations (just like we have top-level type signatures of term-level declarations) and deprecate CUSKs. One Of These Days, I will write a ghc-proposal for this.

### comment:3 Changed 14 months ago by

Replying to goldfire:

This behavior is all expected... or, in one case, not unexpected.

The very first example in the OP is regrettable, but it is "not unexpected", as

`-XNoTypeInType`

rejects such programs on a best-effort basis. That one is hard.The other examples are all consequences of the CUSK rules.

Thanks for the link. I'm a bit embarrassed to say I didn't think to look in the users' guide to see if CUSKs were documented, but I'm glad they are!

Proposed solution: allow top-level kind signatures of type-level declarations (just like we have top-level type signatures of term-level declarations) and deprecate CUSKs. One Of These Days, I will write a ghc-proposal for this.

If I may ask, what do you mean by "top-level kind signature" here? I thought that

data T :: forall k. k -> Type

*was* a top-level kind signature, but perhaps you meant something different?

### comment:4 Changed 14 months ago by

I mean something like

type T :: k -> Type -- this is the kind signature data T _ where MkT :: T Int

Note that there is no `=`

in the kind signature, distinguishing it from a type synonym declaration. The `_`

in the `data`

line is a recognition that a datatype with a kind signature does not need anything after the `T`

. Not sure what the best concrete syntax around that is. (In my thought about this feature, `data T a where`

and `data T :: ... where`

would also both be acceptable.)

Types with kind signatures will be treated just like types with CUSKs are today. Eventually, I would expect types without kind signatures to be treated just like types without CUSKs today. We would then cease to have a notion of CUSK.

### comment:5 Changed 14 months ago by

Resolution: | → invalid |
---|---|

Status: | new → closed |

Thanks! That proposal sounds like an interesting solution.

Since the original bug is expected behavior (and documented, no less), I'm going to close this ticket.

### comment:6 Changed 14 months ago by

I mean something like

But is that so different from this?

data T :: k -> * where MkT :: T Int

Is a separate kind signature better?

### comment:7 Changed 14 months ago by

A separate kind signature will be understood independent of the type definition -- much like how type signatures on functions are understood (and kind-generalized) independently of the body.

For example, consider

data Proxy (a :: k) = P data S :: Proxy k -> Type where MkS :: S (P :: Proxy Maybe)

What's the type of `k`

? Taking the definition into account, we can see that `k :: Type -> Type`

. But if we must take the definition into account, then we don't have a CUSK, by definition. Currently, the declaration above causes GHC to complain that `Type -> Type`

does not match `k`

, as we're using `S`

at a different instantiation in its body than in its head (i.e. using polymorphic recursion). Change to

data S :: forall k. Proxy k -> Type where ...

and now we get

You have written a *complete user-suppled kind signature*, but the following variable is undetermined: k0 :: * Perhaps add a kind signature.

This is quite correct. The declaration looks like it has a CUSK, but really it doesn't.

Instead, we can write

data S :: forall (k :: Type -> Type). Proxy k -> Type where ...

or

data S :: forall (kk :: Type) (k :: kk). Proxy k -> Type where ...

both of which are accepted. Note that these define *different* types: the second defines a kind-indexed GADT.

The point of all this is that it's incredibly confusing. Much better would be

(*) A definition can use polymorphic recursion if it has a standalone type/kind signature.

Simple! It works for types and terms. And it's exactly what happens for terms today.

Under (*), all the declarations for `S`

would be rejected, as none of them have a standalone kind signature. (The proposal will also describe `-XCUSKs`

, on by default, that retains the current behavior. This extension will be off by default and deprecated in due course.)

### comment:8 follow-up: 9 Changed 14 months ago by

I'm only questioning whether we need new syntax.

Let me re-state what I think you are saying.

- The kind of a type constructor can be
*inferred*from its definition, or*specified*by a CUSK.

- A CUSK
*specifies*the kind of a type constructor, fully. No need to look at any other definitions etc; it all comes from the CUSK.

- In type declarations you can add kind signatures but they merely specify additional constraints that may guide the inference process. For example
data T (a :: k -> *) = ...

constraints`a`

to have a kind of the specified form, but it does no more than that.

The thing you say is "incredibly confusing" is that the switch from inferred to specified is based on some fairly subtle syntactic rules, and you'd like to have a clearer syntactic distinction. It's a software engineering issue, not a technical one.

Separate kind signatures would be one solution.

Simplifying the CUSK rules might be another. The existing rules are not bad, actually, except for the mysterious second bullet which depends on explicit quantification of kind variables. Otherwise the rule is *it has a CUSK if every argument variable, and result kind have explicit signatures*.

### comment:9 Changed 14 months ago by

Replying to simonpj:

The thing you say is "incredibly confusing" is that the switch from inferred to specified is based on some fairly subtle syntactic rules, and you'd like to have a clearer syntactic distinction. It's a software engineering issue, not a technical one.

Yes, precisely. There's no real technical challenge here. I just want an easy way for the user to say what they mean: inference or specification.

The problem with the CUSK rules as they are is that sometimes you've written a CUSK when you don't mean to. For example

data T (a :: Proxy k) where ...

According to the rules, this declaration has a CUSK. But suppose I want `k`

's kind to be inferred. The only way to do so is to write

data T :: Proxy k -> Type where ...

This form is a CUSK with `-XNoTypeInType`

but is *not* a CUSK with `-XTypeInType`

. The reason for the extra rule with `-XTypeInType`

is to support this case, where the user wants inference. (Note that with `-XNoTypeInType`

, `k`

's kind will always by `Type`

, and so the issue of inference doesn't arise.)

This particular problem is worse for closed type families and for classes, where there is no alternate syntax available if the user does not want a CUSK.

The intent of my proposal is to make all of this simpler: the user simply says whether they want inference (no kind sig) or specification (kind sig). No fiddly rules. No exceptions.

**Note:**See TracTickets for help on using tickets.

Another workaround is to explicitly quantify the kind like so: