Opened 2 months ago

Closed 8 weeks ago

Last modified 7 weeks ago

#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 8 weeks ago by RyanGlScott

Another workaround is to explicitly quantify the kind like so:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module Works2 where

import Data.Kind

data T :: forall (k :: Type). k -> Type where
  MkT :: T Int

comment:2 Changed 8 weeks ago by 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.

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 in reply to:  2 Changed 8 weeks ago by RyanGlScott

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 8 weeks ago by goldfire

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 8 weeks ago by RyanGlScott

Resolution: invalid
Status: newclosed

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 7 weeks ago by simonpj

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 7 weeks ago by goldfire

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 Changed 7 weeks ago by simonpj

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 in reply to:  8 Changed 7 weeks ago by goldfire

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.