Opened 2 years ago

Closed 20 months ago

Last modified 20 months ago

#6093 closed bug (fixed)

Kind polymorphism fails with recursive type definition using different kind

Reported by: Ashley Yakeley Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.6.1
Keywords: Cc: dimitris@…, sweirich@…, goldfire, dreixel
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Difficulty: Unknown
Test Case: polykinds/T6093 Blocked By:
Blocking: Related Tickets:

Description

{-# LANGUAGE GADTs, PolyKinds #-}
module Bug where
    data R t where
        MkR :: R f -> R (f ())

results in

Bug.hs:4:26:
    Kind mis-match
    The first argument of `R' should have kind `* -> k0',
    but `f ()' has kind `k0'
    In the type `R (f ())'
    In the definition of data constructor `MkR'
    In the data type declaration for `R'

Change History (16)

comment:1 Changed 2 years ago by simonpj

  • Cc dimitris@… sweirich@… added
  • Difficulty set to Unknown

To be clear, you are hoping for this, where I have made kind quantification and kind arguments explicit:

data R :: k -> * where
  MkR :: forall k. forall (f :: * -> k). R (*->k) f -> R k (f ())

However, just as Hindley-Milner only allows monomorphic recursion for inferred types, so GHC only allows kind-monomorphic recursion for inferred kinds. So your example is behaving just as expected.

At the value level, a type signature is enought to allow polymorphic recursion. So you might hope that this would work:

 data R :: k -> * where
    MkR :: R f -> R (f ())

But it doesn't yet work, because there isn't a clear notion of when a type constructor has a type signature (yet anyway), whereas it's totally clear at the value level. So currently there is no equivalent of "you can get polymorphic recursion if you give a type signature".

Do you have a real application in mind or were you just playing?

Simon

comment:2 Changed 2 years ago by Ashley Yakeley

This is from a real example and potentially quite a useful one. I want to reify types, so I'm doing something a bit like this:

data Type t where
  SimpleType :: IOWitness a -> Type a
  ConstructedType :: Type f -> Type a -> Type (f a)

(There's more to it than that, I'm storing instance witnesses as well, but you get the idea.)

comment:3 Changed 2 years ago by Ashley Yakeley

I also noticed I couldn't get around it with

data R1 t = MkR1 (R2 t)

data R2 t where
        MkR2 :: R1 f -> R2 (f ())

...but perhaps that's to be expected?

comment:4 Changed 2 years ago by simonpj

  • Cc goldfire dreixel added

Hmm. So you want to get the following type and kind signatures (where I put in all kind abstractions and applications):

  Type :: forall k. k -> *
  SimpleType :: forall (a:*). IOWitness a -> Type * a
  ConstructedType :: forall k k2. forall (f:k2->k) (a:k2). 
                     Type (k2->k) g -> Type k2 a -> Type k (f a)

But there's a difficulty with SimpleType because data constructors must have competely parameteric result types. I think you really want

  SimpleType :: forall k. (k ~ *) => forall (a:k). IOWitness a -> Type k a

I'm a bit out of my depth here, but Stephanie and Richard have been working on this kind of stuff so I'm ccing them.

comment:5 Changed 2 years ago by sweirich

As Simon has elaborated, your example requires *kind* equalities (or GADKs) which aren't yet supported. We're working on the theory that would allow us to add such kind equalities to FC now, but its not yet done (or implemented).

comment:6 Changed 2 years ago by Ashley Yakeley

Just to be clear, IOWitness is also polykinded. (It has to be, so I can for instance represent "Maybe Bool".)

IOWitness : k -> *

So I think it should be this:

Type :: forall k. k -> *
  SimpleType :: forall k. forall (a:k). IOWitness k a -> Type k a
  ConstructedType :: forall k k2. forall (f:k2->k) (a:k2). 
                     Type (k2->k) g -> Type k2 a -> Type k (f a)

This should be possible, should it not?

comment:7 Changed 2 years ago by goldfire

With that clarification, this may be a manifestation of the issues discussed in #6049. As I understand it, GHC doesn't currently allow recursive uses of a type to have different kind parameters than in the outer definition.

comment:8 Changed 2 years ago by simonpj

Yes I think Richard (= goldfire) is right. #6049 is on my list but it's a bit messy, so I won't get to it till after the Haskell Symposium deadline.

comment:9 Changed 23 months ago by simonpj@…

commit c91172004f2a5a6bf201b418c32c2d640ee34049

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Thu Jun 7 12:09:22 2012 +0100

    Support polymorphic kind recursion
    
    This is (I hope) the last major patch for kind polymorphism.
    The big new feature is polymorphic kind recursion when you
    supply a complete kind signature for a type constructor.
    (I've documented it in the user manual too.)
    
    This fixes Trac #6137, #6093, #6049.
    
    The patch also makes type/data families less polymorphic by default.
       data family T a
    now defaults to T :: * -> *
    If you want T :: forall k. k -> *, use
       data family T (a :: k)
    
    This defaulting to * is done whenever there is a
    "complete, user-specified kind signature", something that is
    carefully defined in the user manual.
    
    Hurrah!

 compiler/typecheck/TcBinds.lhs      |    3 +-
 compiler/typecheck/TcClassDcl.lhs   |   49 --------
 compiler/typecheck/TcHsType.lhs     |   50 ++++++--
 compiler/typecheck/TcInstDcls.lhs   |  106 +++++------------
 compiler/typecheck/TcRnDriver.lhs   |   66 ++++++++---
 compiler/typecheck/TcRnTypes.lhs    |   31 ++----
 compiler/typecheck/TcSplice.lhs     |    3 +-
 compiler/typecheck/TcTyClsDecls.lhs |  204 ++++++++++++++++++-------------
 docs/users_guide/flags.xml          |    5 +-
 docs/users_guide/glasgow_exts.xml   |  228 ++++++++++++++++++++++-------------
 10 files changed, 400 insertions(+), 345 deletions(-)

comment:10 Changed 23 months ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to polykinds/T6093

comment:11 Changed 20 months ago by Ashley Yakeley

  • Resolution fixed deleted
  • Status changed from closed to new
  • Version changed from 7.4.1 to 7.6.1

This is still present in 7.6.1.

comment:12 Changed 20 months ago by Ashley Yakeley

  • Resolution set to fixed
  • Status changed from new to closed

OK, I see the problem. This compiles:

data R :: k -> * where
    MkR :: R f -> R (f ())

But this doesn't:

data R (t :: k) where
    MkR :: R f -> R (f ())

This is a different bug, and not so serious if you know the work-around.

comment:13 Changed 20 months ago by goldfire

I would argue that the failure of the second of Ashley's recent examples is not a bug, according to the manual. See this section. Polymorphic recursion is only enabled for a datatype with a "complete user-supplied kind signature". According to the manual, such a datatype must be defined with GADT syntax and with a top-level ::. The second example above does not have a top-level (i.e. outside of any parentheses) ::, so it does not have a "complete user-supplied kind signature" and thus cannot use polymorphic recursion.

As I understand it, Simon struggled a bit with the design around this issue, trying to balance kind inference with polymorphic recursion. The final result is something of a compromise, and is admittedly a little fiddly and can be unexpected behavior. However, it is well defined in the manual.

comment:14 Changed 20 months ago by Ashley Yakeley

It's an infelicity, albeit a documented one.

comment:15 Changed 20 months ago by simonpj

It's documented quite carefully; read the bit about a "complete kind signatures" in 7.8.3. If you have a better design, do put it forward.

comment:16 Changed 20 months ago by Ashley Yakeley

Oh, I see. Yes, that makes sense. Sorry.

Note: See TracTickets for help on using tickets.