Type variable introduction for existential types

Question

Is there any binder in haskell to introduce a type variable (and constraints) quantified in a type ?

I can add an extra argument, but it defeats the purpose.

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}


data Exists x = forall m. Monad m => Exists (m x)

convBad ::  x -> Exists x  
convBad  x = Exists @m (return @m x, undefined) --Not in scope: type variable ‘m’typecheck


data Proxy (m:: * -> *) where Proxy :: Proxy m

convOk ::  Monad m => x -> Proxy m -> Exists x 
convOk  x (_ :: Proxy m) = Exists (return @m x)

Answer 1

To bring type variables into scope, use forall (enabled by ExplicitForall, which is implied by ScopedTypeVariables):

convWorksNow :: forall m x. Monad m => x -> Exists x  
convWorksNow x = Exists (return @m x)

-- Usage:
ex :: Exists Int
ex = convWorksNow @Maybe 42

But whether you do it like this or via Proxy, keep in mind that m must be chosen at the point of creating Exists. So whoever calls the Exists constructor must know what m is.

If you wanted it to be the other way around - i.e. whoever unwraps an Exists value chooses m, - then your forall should be on the inside:

newtype Exists x = Exists (forall m. Monad m => m x)

convInside :: x -> Exists x
convInside x = Exists (return x)

-- Usage:
ex :: Exists Int
ex = convInside 42

main = do
  case ex of
    Exists mx -> mx >>= print  -- Here I choose m ~ IO

  case ex of
    Exists mx -> print (fromMaybe 0 mx)  -- Here I choose m ~ Maybe

---

Also, as @dfeuer points out in the comments, note that your original type definition (the one with forall on the outside) is pretty much useless beyond just signifying the type of x (same as Proxy does). This is because whoever consumes such value must be able to work with any monad m, and you can do anything with a monad unless you know what it is. You can't bind it inside IO, because it's not necessarily IO, you can't pattern match it with Just or Nothing because it's not necessarily Maybe, and so on. The only thing you can do with it is bind it with >>=, but then you'll just get another instance of it, and you're back to square one.