Is there a way to define an existentially quantified newtype in GHC Haskell?

Question

Is it possible in (GHC) Haskell to define an existentially-quantified newtype? I understand that if type classes are involved it can't be done in a dictionary-passing implementation, but for my purposes type-classes are not needed. What I'd really like to define is this:

newtype Key t where Key :: t a -> Key t

But GHC does not seem to like it. Currently I'm using data Key t where Key :: !(t a) -> Key t. Is there any way (perhaps just using -funbox-strict-fields?) to define a type with the same semantics and overhead as the newtype version above? My understanding is that even with strict fields unboxed there will still be an extra tag word, though I could be totally wrong there.

This is not something that's causing me any noticeable performance issues. It just surprised me that the newtype was not allowed. I'm a naturally curious person, so I can't help wondering whether the version I have is being compiled to the same representation or whether any equivalent type could be defined which would be.

Answer 1

No, according to GHC:

A newtype constructor cannot have an existential context

However, data is just fine:

{-# LANGUAGE ExistentialQuantification #-}

data E = forall a. Show a => E a

test = [ E "foo"
       , E (7 :: Int)
       , E 'x'
       ]

main = mapM_ (\(E e) -> print e) test

E.g.

*Main> main
"foo"
7
'x'

Logically, you do need the dictionary (or tag) allocated somewhere. And that doesn't make sense if you erase the constructor.

Note: You can't unbox functions though, as you seem to be hinting at, nor polymorphic fields.

---

Is there any way (perhaps just using -funbox-strict-fields?) to define a type with the same semantics and overhead as the newtype version above?

Removing the -XGADTs helps me think about this:

{-# LANGUAGE ExistentialQuantification #-}

data Key t = forall a. Key !(t a)

As in, Key (Just 'x') :: Key Maybe

So you want to guarantee the Key constructor is erased.

Here's the code in GHC for type checking the constraints on newtype:

-- Checks for the data constructor of a newtype
checkNewDataCon con
  = do  { checkTc (isSingleton arg_tys) (newtypeFieldErr con (length arg_tys))
        -- One argument
    ; checkTc (null eq_spec) (newtypePredError con)
        -- Return type is (T a b c)
    ; checkTc (null ex_tvs && null eq_theta && null dict_theta) (newtypeExError con)
        -- No existentials
    ; checkTc (not (any isBanged (dataConStrictMarks con)))
          (newtypeStrictError con)
        -- No strictness

We can see why ! won't have any effect on the representation, since it contains polymorphic components, so needs to use the universal representation. And unlifted newtype doesn't make sense, nor non-singleton constructors.

The only thing I can think of is that, like for record accessors for existentials, the opaque type variable will escape if the newtype is exposed.