Existential data constructors should not be promoted
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
Trac metadata
| Trac field | Value |
|---|---|
| Version | 7.6.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |
Activity
added Tbug Trac import labels
mentioned in commit 8019bc2c
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
Trac metadata
Trac field Value CC → eir@cis.upenn.edu 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.
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) = StringAnd 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) = 42The point is still that if the kind of the promoted constructor is
MkEx :: * -> Exthen 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 -> ExAFAIK, 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.
Well this
type instance MkEx x = xshould 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 isJust :: forall a. a -> Maybe athen we get poly-kinded type constructor
'Just :: forlal k. k -> 'Maybe kYou 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 havedata Ex = MkEx STARwhere
STARis an uninhabited type whose promotion to the kind level is*.I'm sorry. I was confused by the fact that if I load a file containing
data Ex = forall a. MkEx ainto GHCi, I get this:
*Main> :kind 'MkEx 'MkEx :: * -> ExBut I note now that this is because I didn't say
PolyKindsin GHCi. Indeed, then I get:*Main> :set -XPolyKinds *Main> :kind 'MkEx 'MkEx :: k -> ExSo 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.
mentioned in commit cdb03615
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" }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) = xThis compiles in GHC 7.6.1, and it should.
First off, let's look at the type of
'MkEx, which isforall (k::BOX). k -> Ex. Now, let's look at the elaboration ofUnExin FC:UnEx :: forall (k::BOX). Ex -> k axUnEx :: forall k. forall (x::k). (UnEx k (MkEx k x) ~ x)So, the elaboration of
UnExsimply contains a non-linear pattern ink. But, becausekis a parameter toUnEx, the kind ofxis 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) ~# xOne comment above says that
UnExwould 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.What if I declare
Exlike this?data KEx :: * where MkKEx :: forall (a::k). Proxy a -> KExNow the kind variable
kas well as the type variableais 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 toUnKEx: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.
If you declare
KExas above, something weird happens when you promote (in 7.6.1): the typeKExgets promoted to a kind, but the kind-polymorphic data constructorMkKExdoes not get promoted to a type. So,KExbecomes 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
UnKExtype 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.
mentioned in commit c0d84691
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
'Tis poly-kinded, and that makes its use inDfine. 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
- The type constructor has no kind polymorphism; indeed has kind
added Pnormal label
