Existential data constructors should not be promoted

[simonpj]

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

[dreixel]

I thought promotion of existentials was "ok" in the theory, though. So we're just going to forbid it entirely?

[simonpj]

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

[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.

[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.

[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.

[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 *.

[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.

[simonpj@…]

commit 8019bc2cb7b2883bdf0da49ccdc52ecc9e2ad2fc

Author: Simon Peyton Jones <simonpj@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(-)

[simonpj]

Please merge if it's easy to do so.

[simonpj]

Also needs this:

commit 1152f9491517ca22ed796bfacbbfb7413dde1bcf
Author: Simon Peyton Jones <simonpj@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" }

[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.

[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.

[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.

[igloo]

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.

[simonpj@…]

commit c0d846917846d303be48d9dc43fb047863ed14ea

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Wed Dec 5 11:07:38 2012 +0000

    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(-)

[simonpj]

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

[igloo]

Merged as e3dc71de7307d30f6063a8447b93e54f1551a041 and f630eb5122b5d6c16b449451e33adda5341b6775.