Existential quantification of typeclass constraints

Question

I am not sure why ko does not typecheck. Is there a particularly enlightening explanation ?

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE NoMonomorphismRestriction, FlexibleInstances #-}

module Wrap where

class ExpSYM repr where
    lit :: Int -> repr

newtype Wrapped = Wrapped{unWrap :: forall repr. ExpSYM repr => repr}

a = (lit <$> Just 5) :: ExpSYM expr => Maybe expr

ko :: Maybe Wrapped
ko = do v <- a
        return $ Wrapped $ v

ok :: Maybe Wrapped
ok = do v <- Just 5
        let e = lit v
        return $ Wrapped $ e

The compiler mentions

SO.hs:15:14: error:
    • No instance for (ExpSYM a0) arising from a use of ‘a’
    • In a stmt of a 'do' block: v <- a
      In the expression:
        do { v <- a;
             return $ Wrapped $ v }
      In an equation for ‘ko’:
          ko
            = do { v <- a;
                   return $ Wrapped $ v }

SO.hs:16:28: error:
    • Couldn't match expected type ‘repr’ with actual type ‘a0’
        because type variable ‘repr’ would escape its scope
      This (rigid, skolem) type variable is bound by
        a type expected by the context:
          ExpSYM repr => repr
        at SO.hs:16:18-28
    • In the second argument of ‘($)’, namely ‘v’
      In the second argument of ‘($)’, namely ‘Wrapped $ v’
      In a stmt of a 'do' block: return $ Wrapped $ v
    • Relevant bindings include v :: a0 (bound at SO.hs:15:9)
Failed, modules loaded: none.

Edit : Found a nice solution to circumvent this in Oleg's note, which is to specialize the type such that the polymorphism is removed by type application, adding the instance

instance ExpSYM Wrapped where
   lit x = Wrapped $ lit x

we then have

notko :: Maybe Wrapped
notko = do v <- a    
           return $ v -- note the difference. what's the type of a ?

-- and we get all the usual goodies, no silly impredicative error
alsoOk = lit <$> Just 5 :: Maybe Wrapped

Answer 1

ko would only work if the type of a were

a :: Maybe (∀ expr . ExpSYM expr => expr)
a = lit <$> Just 5

...because only then would you be able to do-unwrap it to obtain the polymorphic value v :: ∀ expr . ExpSYM expr => expr. That value must be polymorphic so it can actually be used in Wrapped.

But Maybe (∀ expr . ExpSYM expr => expr) is an impredicative type. GHC Haskell doesn't support impredicative types.

OTOH, in ok, v is just a boring old integer coming from an unspectacular Just 5 :: Maybe Int. Only e introduces the polymorphism, but does so outside of the Maybe monad.