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

[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: <http://hackage.haskell.org/trac/ghc/ticket/7347#comment:11>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler