Re: [GHC] #6093: Kind polymorphism fails with recursive type definition using different kind
#6093: Kind polymorphism fails with recursive type definition using different kind +--- Reporter: Ashley Yakeley | Owner: Type: bug| Status: closed Priority: normal | Milestone: Component: Compiler (Type checker)|Version: 7.6.1 Resolution: fixed | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Difficulty: Unknown Testcase: polykinds/T6093| Blockedby: Blocking: |Related: +--- Comment(by Ashley Yakeley): It's an infelicity, albeit a documented one. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6093#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6093: Kind polymorphism fails with recursive type definition using different kind
#6093: Kind polymorphism fails with recursive type definition using different kind +--- Reporter: Ashley Yakeley | Owner: Type: bug| Status: closed Priority: normal | Milestone: Component: Compiler (Type checker)|Version: 7.6.1 Resolution: fixed | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Difficulty: Unknown Testcase: polykinds/T6093| Blockedby: Blocking: |Related: +--- Comment(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. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6093#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6093: Kind polymorphism fails with recursive type definition using different kind
#6093: Kind polymorphism fails with recursive type definition using different kind +--- Reporter: Ashley Yakeley | Owner: Type: bug| Status: closed Priority: normal | Milestone: Component: Compiler (Type checker)|Version: 7.6.1 Resolution: fixed | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Difficulty: Unknown Testcase: polykinds/T6093| Blockedby: Blocking: |Related: +--- Comment(by Ashley Yakeley): Oh, I see. Yes, that makes sense. Sorry. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6093#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6093: Kind polymorphism fails with recursive type definition using different kind
#6093: Kind polymorphism fails with recursive type definition using different kind +--- Reporter: Ashley Yakeley | Owner: Type: bug| Status: new Priority: normal | Milestone: Component: Compiler (Type checker)|Version: 7.6.1 Resolution: | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Difficulty: Unknown Testcase: polykinds/T6093| Blockedby: Blocking: |Related: +--- Changes (by Ashley Yakeley): * status: closed = new * version: 7.4.1 = 7.6.1 * resolution: fixed = Comment: This is still present in 7.6.1. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6093#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6093: Kind polymorphism fails with recursive type definition using different kind
#6093: Kind polymorphism fails with recursive type definition using different
kind
+---
Reporter: Ashley Yakeley | Owner:
Type: bug| Status: closed
Priority: normal | Milestone:
Component: Compiler (Type checker)|Version: 7.6.1
Resolution: fixed | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: GHC rejects valid program | Difficulty: Unknown
Testcase: polykinds/T6093| Blockedby:
Blocking: |Related:
+---
Changes (by Ashley Yakeley):
* status: new = closed
* resolution: = fixed
Comment:
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.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6093#comment:12
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6093: Kind polymorphism fails with recursive type definition using different kind
#6093: Kind polymorphism fails with recursive type definition using different
kind
+---
Reporter: Ashley Yakeley | Owner:
Type: bug| Status: closed
Priority: normal | Milestone:
Component: Compiler (Type checker)|Version: 7.6.1
Resolution: fixed | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: GHC rejects valid program | Difficulty: Unknown
Testcase: polykinds/T6093| Blockedby:
Blocking: |Related:
+---
Comment(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
[http://www.haskell.org/ghc/docs/latest/html/users_guide/kind-
polymorphism.html#id620778 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.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6093#comment:13
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6093: Kind polymorphism fails with recursive type definition using different kind
#6093: Kind polymorphism fails with recursive type definition using different
kind
+---
Reporter: Ashley Yakeley | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 7.4.1
Keywords: | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: GHC rejects valid
program
Difficulty: Unknown |Testcase:
Blockedby: |Blocking:
Related: |
+---
Comment(by simonpj@…):
commit c91172004f2a5a6bf201b418c32c2d640ee34049
{{{
Author: Simon Peyton Jones simo...@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(-)
}}}
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6093#comment:9
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6093: Kind polymorphism fails with recursive type definition using different kind
#6093: Kind polymorphism fails with recursive type definition using different kind +--- Reporter: Ashley Yakeley | Owner: Type: bug| Status: closed Priority: normal | Milestone: Component: Compiler (Type checker)|Version: 7.4.1 Resolution: fixed | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Difficulty: Unknown Testcase: polykinds/T6093| Blockedby: Blocking: |Related: +--- Changes (by simonpj): * status: new = closed * testcase: = polykinds/T6093 * resolution: = fixed -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6093#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6093: Kind polymorphism fails with recursive type definition using different kind
#6093: Kind polymorphism fails with recursive type definition using different kind +--- Reporter: Ashley Yakeley | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.4.1 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: GHC rejects valid program Difficulty: Unknown |Testcase: Blockedby: |Blocking: Related: | +--- Comment(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. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6093#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6093: Kind polymorphism fails with recursive type definition using different kind
#6093: Kind polymorphism fails with recursive type definition using different kind +--- Reporter: Ashley Yakeley | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.4.1 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: GHC rejects valid program Difficulty: Unknown |Testcase: Blockedby: |Blocking: Related: | +--- Comment(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. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6093#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6093: Kind polymorphism fails with recursive type definition using different kind
#6093: Kind polymorphism fails with recursive type definition using different
kind
+---
Reporter: Ashley Yakeley | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 7.4.1
Keywords: | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: GHC rejects valid
program
Difficulty: Unknown |Testcase:
Blockedby: |Blocking:
Related: |
+---
Changes (by simonpj):
* cc: goldfire, dreixel (added)
Comment:
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.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6093#comment:4
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6093: Kind polymorphism fails with recursive type definition using different kind
#6093: Kind polymorphism fails with recursive type definition using different kind +--- Reporter: Ashley Yakeley | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.4.1 Keywords: | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: GHC rejects valid program Difficulty: Unknown |Testcase: Blockedby: |Blocking: Related: | +--- Comment(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). -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6093#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6093: Kind polymorphism fails with recursive type definition using different kind
#6093: Kind polymorphism fails with recursive type definition using different
kind
+---
Reporter: Ashley Yakeley | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 7.4.1
Keywords: | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: GHC rejects valid
program
Difficulty: Unknown |Testcase:
Blockedby: |Blocking:
Related: |
+---
Comment(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?
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6093#comment:6
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6093: Kind polymorphism fails with recursive type definition using different kind
#6093: Kind polymorphism fails with recursive type definition using different
kind
+---
Reporter: Ashley Yakeley | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 7.4.1
Keywords: | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: GHC rejects valid
program
Difficulty: Unknown |Testcase:
Blockedby: |Blocking:
Related: |
+---
Changes (by simonpj):
* cc: dimitris@…, sweirich@… (added)
* difficulty: = Unknown
Comment:
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
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6093#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6093: Kind polymorphism fails with recursive type definition using different kind
#6093: Kind polymorphism fails with recursive type definition using different
kind
+---
Reporter: Ashley Yakeley | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 7.4.1
Keywords: | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: GHC rejects valid
program
Difficulty: Unknown |Testcase:
Blockedby: |Blocking:
Related: |
+---
Comment(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.)
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6093#comment:2
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #6093: Kind polymorphism fails with recursive type definition using different kind
#6093: Kind polymorphism fails with recursive type definition using different
kind
+---
Reporter: Ashley Yakeley | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 7.4.1
Keywords: | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: GHC rejects valid
program
Difficulty: Unknown |Testcase:
Blockedby: |Blocking:
Related: |
+---
Comment(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?
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/6093#comment:3
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
