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
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.