Re: [GHC] #7347: Existential data constructors should not be promoted
#7347: Existential data constructors should not be promoted ---+ Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal| Milestone: Component: Compiler |Version: 7.6.1 Resolution: fixed | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: None/Unknown | Difficulty: Unknown Testcase: polykinds/T7347 | Blockedby: Blocking:|Related: ---+ Changes (by igloo): * status: merge = closed Comment: Merged as e3dc71de7307d30f6063a8447b93e54f1551a041 and f630eb5122b5d6c16b449451e33adda5341b6775. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7347#comment:17 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] #7347: Existential data constructors should not be promoted
#7347: Existential data constructors should not be promoted
---+
Reporter: simonpj | Owner:
Type: bug | Status: closed
Priority: normal| Milestone:
Component: Compiler |Version: 7.6.1
Resolution: fixed | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Difficulty: Unknown
Testcase: polykinds/T7347 | Blockedby:
Blocking:|Related:
---+
Comment(by simonpj@…):
commit c0d846917846d303be48d9dc43fb047863ed14ea
{{{
Author: Simon Peyton Jones simo...@microsoft.com
Date: Wed Dec 5 11:07:38 2012 +
Allow existential data constructors to be promoted
This reverts the change in Trac #7347, which prevented promotion
of existential data constructors. Ones with constraints in
their types, or kind polymorphism, still can't be promoted.
compiler/basicTypes/DataCon.lhs |8 +---
compiler/types/TyCon.lhs|6 --
2 files changed, 9 insertions(+), 5 deletions(-)
}}}
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7347#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] #7347: Existential data constructors should not be promoted
#7347: Existential data constructors should not be promoted
---+
Reporter: simonpj | Owner:
Type: bug | Status: merge
Priority: normal| Milestone:
Component: Compiler |Version: 7.6.1
Resolution: fixed | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Difficulty: Unknown
Testcase: polykinds/T7347 | Blockedby:
Blocking:|Related:
---+
Changes (by simonpj):
* status: closed = merge
Comment:
After further discussion with Richard and Stephanie we decided to promote
data constructors where
* The type constructor has no kind polymorphism; indeed has kind `* -
- *`.
* The data constructor has no constraints (equality or otherwise) in its
type
* The argument types of the data constructor are all promotable
This restores the 7.6.1 behaviour, and that turns out to be useful for
Richard and/or Pedro.
I'm not sure why Stefan's original bug report is a bug. In his example
{{{
data K = forall a. T a -- promotion gives 'T :: forall k. k - K
data G :: K - * where
D :: G (T [])
}}}
the promoted kind of `'T` is poly-kinded, and that makes its use in `D`
fine. So currently it is accepted and I think we agree it should be.
The reminaing open issue concerns data types that have some promotable and
some non-promotable constructors, but I'll open a new ticket for that.
Ian, I this this should merge smoothly onto 7.6.1, along with a doc patch
that I'll commit shortly.
Simon
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7347#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] #7347: Existential data constructors should not be promoted
#7347: Existential data constructors should not be promoted ---+ Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal| Milestone: Component: Compiler |Version: 7.6.1 Resolution: fixed | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: None/Unknown | Difficulty: Unknown Testcase: polykinds/T7347 | Blockedby: Blocking:|Related: ---+ Changes (by igloo): * status: merge = closed * resolution: = fixed Comment: Merged as 4b380f192d1b3f7455e7c2bb9bf3ebe6c6b5e7ca and 29bbb9f538db07ecbc412879f357f16607b2ad65. If another change is desirable, then I think it would be best to open a fresh ticket for it, so people looking at it don't have to trawl through so much history. Hence closing this one. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7347#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] #7347: Existential data constructors should not be promoted
#7347: Existential data constructors should not be promoted
-+--
Reporter: simonpj | Owner:
Type: bug | Status: merge
Priority: normal| Milestone:
Component: Compiler | Version: 7.6.1
Keywords:| Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown |Testcase: polykinds/T7347
Blockedby:|Blocking:
Related:|
-+--
Comment(by goldfire):
If you declare {{{KEx}}} as above, something weird happens when you
promote (in 7.6.1): the type {{{KEx}}} gets promoted to a kind, but the
kind-polymorphic data constructor {{{MkKEx}}} does not get promoted to a
type. So, {{{KEx}}} becomes an uninhabited kind. This behavior is weird,
but it seems not to violate any description of promotion: kind-polymorphic
things are not promoted, and other (suitable) things are.
So, one cannot write an {{{UnKEx}}} type instance, and thus there is no
problem.
I agree that this is far from urgent. But, if the checks you added to fix
this bug added complexity, they could perhaps be removed. I believe the
original implementation of naive promotion of existentials is the right
one.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7347#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] #7347: Existential data constructors should not be promoted
#7347: Existential data constructors should not be promoted
-+--
Reporter: simonpj | Owner:
Type: bug | Status: merge
Priority: normal| Milestone:
Component: Compiler | Version: 7.6.1
Keywords:| Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown |Testcase: polykinds/T7347
Blockedby:|Blocking:
Related:|
-+--
Comment(by simonpj):
What if I declare `Ex` like this?
{{{
data KEx :: * where
MkKEx :: forall (a::k). Proxy a - KEx
}}}
Now the kind variable `k` as well as the type variable `a` is
existentially quantified, and NOW we will have to worry about existential
escape, notwithstanding your comment about no phase separation. Indeed
I can't give a kind to `UnKEx`:
{{{
type family UnKEx :: KEx - ???
}}}
So maybe what saves us here is that type families have user-specified kind
signatures, and that in turn means we don't need to check for existential
escape.
So I think I agree with your point, but I don't know how urgent/important
it is, nor how hard it would be to implement. At its easiest it might
mean just removing a restriction, but I'm not certain.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7347#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] #7347: Existential data constructors should not be promoted
#7347: Existential data constructors should not be promoted
-+--
Reporter: simonpj | Owner:
Type: bug | Status: merge
Priority: normal| Milestone:
Component: Compiler | Version: 7.6.1
Keywords:| Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown |Testcase: polykinds/T7347
Blockedby:|Blocking:
Related:|
-+--
Comment(by goldfire):
Stephanie and I thought about this issue this morning, and we believe that
promoting existentials is sound.
Consider this:
{{{
{-# LANGUAGE ExistentialQuantification, PolyKinds, DataKinds #-}
data Ex = forall a. MkEx a
type family UnEx (ex :: Ex) :: k
type instance UnEx (MkEx x) = x
}}}
This compiles in GHC 7.6.1, and it should.
First off, let's look at the type of {{{'MkEx}}}, which is {{{forall
(k::BOX). k - Ex}}}. Now, let's look at the elaboration of {{{UnEx}}} in
FC:
{{{
UnEx :: forall (k::BOX). Ex - k
axUnEx :: forall k. forall (x::k). (UnEx k (MkEx k x) ~ x)
}}}
So, the elaboration of {{{UnEx}}} simply contains a non-linear pattern in
{{{k}}}. But, because {{{k}}} is a parameter to {{{UnEx}}}, the kind of
{{{x}}} is not really escaping. As proof, here is an excerpt of the output
from {{{-ddump-tc}}}:
{{{
TYPE CONSTRUCTORS
Ex :: *
data Ex
No C type associated
RecFlag NonRecursive
= MkEx :: forall a. a - Ex Stricts: _
FamilyInstance: none
UnEx :: forall (k :: BOX). Ex - k
type family UnEx (k::BOX) (ex::Ex) :: k
COERCION AXIOMS
axiom Scratch.TFCo:R:UnExkMkEx (k :: BOX) (x :: k)
:: UnEx k ('MkEx k x) ~# x
}}}
One comment above says that {{{UnEx}}} would default to a result kind of
{{{*}}}. This would only happen in the absence of an explicit kind
signature for the return kind; all un-annotated types involved in a type
family default to {{{*}}}.
What's different about the type level is that there is no phase separation
between kinds and types. Unpacking a type-level existential happens at
compile time, so the type checker can incorporate what it learns in
simplifying the call to {{{UnEx}}}.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7347#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] #7347: Existential data constructors should not be promoted
#7347: Existential data constructors should not be promoted
-+--
Reporter: simonpj | Owner:
Type: bug | Status: new
Priority: normal| Milestone:
Component: Compiler | Version: 7.6.1
Keywords:| Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown |Testcase:
Blockedby:|Blocking:
Related:|
-+--
Comment(by kosmikus):
I'm sorry. I was confused by the fact that if I load a file containing
{{{
data Ex = forall a. MkEx a
}}}
into GHCi, I get this:
{{{
*Main :kind 'MkEx
'MkEx :: * - Ex
}}}
But I note now that this is because I didn't say `PolyKinds` in GHCi.
Indeed, then I get:
{{{
*Main :set -XPolyKinds
*Main :kind 'MkEx
'MkEx :: k - Ex
}}}
So I thought GHC would not promote to an existential quantification on the
type level, but it actually does. So yes, I was wrong, and this is indeed
problematic.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7347#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] #7347: Existential data constructors should not be promoted
#7347: Existential data constructors should not be promoted
-+--
Reporter: simonpj | Owner:
Type: bug | Status: new
Priority: normal| Milestone:
Component: Compiler | Version: 7.6.1
Keywords:| Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown |Testcase:
Blockedby:|Blocking:
Related:|
-+--
Comment(by simonpj@…):
commit 8019bc2cb7b2883bdf0da49ccdc52ecc9e2ad2fc
{{{
Author: Simon Peyton Jones simo...@microsoft.com
Date: Fri Oct 19 12:53:21 2012 +0100
Only promote *non-existential* data constructors
I don't konw how this was left out before; Trac #7347.
In fixing this I did the usual round of refactoring. In particular, I
cached the fact that a DataCon can be promoted in the DataCon
itself (the dcPromoted field).
compiler/basicTypes/DataCon.lhs | 69
--
compiler/iface/TcIface.lhs |4 +-
compiler/prelude/TysWiredIn.lhs |6 ++--
compiler/types/TyCon.lhs|2 +-
4 files changed, 42 insertions(+), 39 deletions(-)
}}}
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7347#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] #7347: Existential data constructors should not be promoted
#7347: Existential data constructors should not be promoted -+-- Reporter: simonpj | Owner: Type: bug | Status: merge Priority: normal| Milestone: Component: Compiler | Version: 7.6.1 Keywords:| Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown |Testcase: polykinds/T7347 Blockedby:|Blocking: Related:| -+-- Changes (by simonpj): * status: new = merge * testcase: = polykinds/T7347 Comment: Please merge if it's easy to do so. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7347#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] #7347: Existential data constructors should not be promoted
#7347: Existential data constructors should not be promoted
-+--
Reporter: simonpj | Owner:
Type: bug | Status: merge
Priority: normal| Milestone:
Component: Compiler | Version: 7.6.1
Keywords:| Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown |Testcase: polykinds/T7347
Blockedby:|Blocking:
Related:|
-+--
Comment(by simonpj):
Also needs this:
{{{
commit 1152f9491517ca22ed796bfacbbfb7413dde1bcf
Author: Simon Peyton Jones simo...@microsoft.com
Date: Fri Oct 19 20:29:06 2012 +0100
An accidentally-omitted part of commit 8019bc2c, about promoting data
constructors
---
compiler/typecheck/TcHsType.lhs | 14 ++
1 files changed, 6 insertions(+), 8 deletions(-)
diff --git a/compiler/typecheck/TcHsType.lhs
b/compiler/typecheck/TcHsType.lhs index bbfc673..60cf544 100644
--- a/compiler/typecheck/TcHsType.lhs
+++ b/compiler/typecheck/TcHsType.lhs
@@ -427,8 +427,8 @@ tc_hs_type hs_ty@(HsExplicitListTy _k tys) exp_kind
; checkExpectedKind hs_ty (mkPromotedListTy kind) exp_kind
; return (foldr (mk_cons kind) (mk_nil kind) taus) }
where
-mk_cons k a b = mkTyConApp (buildPromotedDataCon consDataCon) [k, a,
b]
-mk_nil k = mkTyConApp (buildPromotedDataCon nilDataCon) [k]
+mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
+mk_nil k = mkTyConApp (promoteDataCon nilDataCon) [k]
tc_hs_type hs_ty@(HsExplicitTupleTy _ tys) exp_kind
= do { tks - mapM tc_infer_lhs_type tys
@@ -607,12 +607,10 @@ tcTyVar name -- Could be a tyvar, a tycon,
or a datacon
AGlobal (ATyCon tc) - inst_tycon (mkTyConApp tc) (tyConKind
tc)
AGlobal (ADataCon dc)
- | isPromotableType ty - inst_tycon (mkTyConApp tc)
(tyConKind tc)
+ | Just tc - promoteDataCon_maybe dc
+ - inst_tycon (mkTyConApp tc) (tyConKind tc)
| otherwise - failWithTc (quotes (ppr dc) + ptext (sLit
of type)
-+ quotes (ppr ty) + ptext (sLit is not
promotable))
- where
- ty = dataConUserType dc
- tc = buildPromotedDataCon dc
++ quotes (ppr (dataConUserType dc)) +
+ ptext (sLit is not promotable))
APromotionErr err - promotionErr name err
@@ -1465,7 +1463,7 @@ tc_kind_var_app name arg_kis
; unless data_kinds $ addErr (dataKindsErr name)
; case isPromotableTyCon tc of
Just n | n == length arg_kis -
-return (mkTyConApp (buildPromotedTyCon tc)
arg_kis)
+return (mkTyConApp (promoteTyCon tc) arg_kis)
Just _ - tycon_err tc is not fully applied
Nothing - tycon_err tc is not promotable }
}}}
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7347#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] #7347: Existential data constructors should not be promoted
#7347: Existential data constructors should not be promoted -+-- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal| Milestone: Component: Compiler | Version: 7.6.1 Keywords:| Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown |Testcase: Blockedby:|Blocking: Related:| -+-- Comment(by kosmikus): It seems that all that GHC 7.6.1 currently allows is to promote existentially quantified variables of kind *. Such constructors, if promoted, lead to simply kinded datatypes. No polymorphism, no existentials on that level. So why not keep allowing them? There's no danger of escaping variables even for type families, afaics. The bug Stefan reports seems to be a missing check whether the type is used according to its inferred kind. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7347#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
Re: [GHC] #7347: Existential data constructors should not be promoted
#7347: Existential data constructors should not be promoted -+-- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal| Milestone: Component: Compiler | Version: 7.6.1 Keywords:| Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown |Testcase: Blockedby:|Blocking: Related:| -+-- Comment(by simonpj): As far as I know, we don't currently have a mechanism for pattern matching on an existential data constructor at the type level. I'm pretty sure that 7.6.1 is broken in this respect. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7347#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] #7347: Existential data constructors should not be promoted
#7347: Existential data constructors should not be promoted
-+--
Reporter: simonpj | Owner:
Type: bug | Status: new
Priority: normal| Milestone:
Component: Compiler | Version: 7.6.1
Keywords:| Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown |Testcase:
Blockedby:|Blocking:
Related:|
-+--
Comment(by kosmikus):
Well, this works in 7.6.1:
{{{
data Ex = forall a. MkEx a
type family F (t :: Ex) :: *
type instance F (MkEx Int) = Int
type instance F (MkEx Bool) = String
}}}
And I don't see how it's dangerous or any different from this:
{{{
data Wrap = MkWrap Int
f :: Wrap - Int
f (MkWrap 0) = 0
f (MkWrap 1) = 42
}}}
The point is still that if the kind of the promoted constructor is
{{{
MkEx :: * - Ex
}}}
then there's no actual existential on the type level. We've just created a
wrapper for values of kind *. I'm ''not'' arguing that we should promote
constructors that would get polymorphic kinds of the form
{{{
MkStrange :: forall k. k - Ex
}}}
AFAIK, Pedro makes use of promoted existentials in at least one of his
generic universe encodings. So it'd be nice if they keep working, unless
there's actually a problem with them.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7347#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] #7347: Existential data constructors should not be promoted
#7347: Existential data constructors should not be promoted
-+--
Reporter: simonpj | Owner:
Type: bug | Status: new
Priority: normal| Milestone:
Component: Compiler | Version: 7.6.1
Keywords:| Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown |Testcase:
Blockedby:|Blocking:
Related:|
-+--
Comment(by simonpj):
Well this
{{{
type instance MkEx x = x
}}}
should give an existential escape error, but it doesn't. Instead it
somehow fixes the kind to *.
You are arguing for this in general. If we promote a data constructor,
such as `Just`, whose type is
{{{
Just :: forall a. a - Maybe a
}}}
then we get poly-kinded type constructor
{{{
'Just :: forlal k. k - 'Maybe k
}}}
You are arguing for some different type-promotion rule for existentials.
Maybe, but I have never thought about that and I don't know what the
details would be.
If you want something that isn't kind-polymorphic, you don't need an
existential at all. Wha you want is something like
{{{
data kind Ex = MkEx *
}}}
a perfectly ordinary non-existential data type with an argument of kind
`*`. Now, as Pedro points out in his ICFP paper we don't have a way to
say that, but that is quite a separate matter; existntials are a total red
herring. Maybe we should have
{{{
data Ex = MkEx STAR
}}}
where `STAR` is an uninhabited type whose promotion to the kind level is
`*`.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7347#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
[GHC] #7347: Existential data constructors should not be promoted
#7347: Existential data constructors should not be promoted
-+--
Reporter: simonpj | Owner:
Type: bug | Status: new
Priority: normal| Milestone:
Component: Compiler | Version: 7.6.1
Keywords:| Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown |Testcase:
Blockedby:|Blocking:
Related:|
-+--
Stefan Holdermans reports: I am almost sure this is a known issue, but I
noticed some erroneous (?) interaction between datatype promotion and
existential quantification. Consider the following program:
{{{
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures#-}
module Test where
data K = forall a. T a -- promotion gives 'T :: * - K
data G :: K - * where
D :: G (T []) -- kind error!
}}}
I would expect the type checker to reject it, but GHC (version 7.6.1)
compiles it happily
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7347
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] #7347: Existential data constructors should not be promoted
#7347: Existential data constructors should not be promoted -+-- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal| Milestone: Component: Compiler | Version: 7.6.1 Keywords:| Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown |Testcase: Blockedby:|Blocking: Related:| -+-- Comment(by dreixel): I thought promotion of existentials was ok in the theory, though. So we're just going to forbid it entirely? -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7347#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] #7347: Existential data constructors should not be promoted
#7347: Existential data constructors should not be promoted -+-- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal| Milestone: Component: Compiler | Version: 7.6.1 Keywords:| Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: None/Unknown Difficulty: Unknown |Testcase: Blockedby:|Blocking: Related:| -+-- Changes (by simonpj): * cc: dimitris@…, sweirich@…, eir@… (added) Comment: If we promote existentials, people will want to pattern match on them to take them apart; we will need to deal with skolem-escape checks; etc. I don't know what the consequences are. I'd be happy to be told they are fine, but for now the implementation definitely isn't up to it, so better to exclude them now and allow them later. Simon -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7347#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
