#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
