Re: [GHC] #7347: Existential data constructors should not be promoted

2012-12-06 Thread GHC
#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: 
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

2012-12-05 Thread GHC
#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: 
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

2012-12-05 Thread GHC
#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 
 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: 
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

2012-11-29 Thread GHC
#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: 
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

2012-11-24 Thread GHC
#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: 
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

2012-11-22 Thread GHC
#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: 
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

2012-11-16 Thread GHC
#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: 
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

2012-10-26 Thread GHC
#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 
 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: 
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

2012-10-26 Thread GHC
#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: 
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

2012-10-26 Thread GHC
#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 
 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: 
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

2012-10-26 Thread GHC
#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: 
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

2012-10-25 Thread GHC
#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: 
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

2012-10-25 Thread GHC
#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: 
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

2012-10-25 Thread GHC
#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: 
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

2012-10-25 Thread GHC
#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: 
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

2012-10-19 Thread GHC
#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: 
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

2012-10-19 Thread GHC
#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: 
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

2012-10-19 Thread GHC
#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: 
GHC 
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs