#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