Forall behavior has changed since 0.6

[maoe]

The following snippet used to type check with constraints 0.4.1.3 but now it doesn't as of 0.6:

import Control.Concurrent.Async.Lifted.Safe -- lifted-async >= 0.7
import Control.Monad.Reader
import Control.Monad.Trans.Control -- monad-control >= 1

foo :: (MonadBaseControl IO m, Forall (Pure m)) => ReaderT () m a -> ReaderT () m a
foo act = withAsync act wait

{-
Ideally we could write:

withAsync
  :: forall m a b. (MonadBaseControl IO m, forall a. StM m a ~ a)
  => m a -> (Async a -> m b) -> m b

but GHC doesn't support quantified constraints. So instead we do this in lifted-async:

class StM m a ~ a => Pure m a
withAsync
  :: forall m a b. (MonadBaseControl IO m, Forall (Pure m))
  => m a -> (Async a -> m b) -> m b
-}

With constraints >= 0.6, GHC complains

    Could not deduce (StM
                        m (Data.Constraint.Forall.Skolem (Pure (ReaderT () m)))
                      ~ Data.Constraint.Forall.Skolem (Pure (ReaderT () m)))
    from the context (MonadBaseControl IO m, Forall (Pure m))
      bound by the type signature for
                 bar :: (MonadBaseControl IO m, Forall (Pure m)) =>
                        ReaderT () m a -> ReaderT () m a

This is because

Forall (Pure m)
~ Forall_ (Pure m)
~ Pure m (Skolem (Pure m))
~ (StM m (Skolem (Pure m)) ~ (Skolem (Pure m)))

and if m ~ ReaderT () n, GHC can't deduce the constraints.

In contrast with constraints == 0.4.1.3:

Forall (Pure m)
~ (Pure m A, Pure m B)
~ (StM m A ~ A, StM m B ~ B)

so if m ~ ReaderT () n, the constraints become

(StM (ReaderT n) A ~ A, StM (ReaderT n) B ~ B)

which are true.

In order to work around this issue, I have to change the constraints of foo to contain ReaderT ():

foo :: (MonadBaseControl IO m, Forall (Pure (ReaderT () m)) => ReaderT () m a -> ReaderT () m a

Was this use-site change intentional? Could we somehow restore the previous behavior (in constraints or lifted-async) without sacrificing the better definitions of Forall and Skolem etc?

[oerjan]

Gah. I still don't have a working Haskell environment, but unraveling the definitions a bit more by hand:

Forall (Pure (ReaderT () n)) requires expanding

StM (ReaderT () n) (Skolem (Pure (ReaderT () n)))
~ ComposeSt (ReaderT ()) n (Skolem (Pure (ReaderT () n)))
~ StM n (StT (ReaderT ()) (Skolem (Pure (ReaderT () n))))
~ StM n (Skolem (Pure (ReaderT () n)))

Meanwhile, Forall (Pure n) only provides StM n (Skolem (Pure n)) ~ Skolem (Pure n).

So the problem is that Forall (Pure n) no longer automatically implies Forall (Pure (ReaderT () n)) because they end up testing different Skolem values. Which is alas precisely what the new Forall implementation insists on, to preserve safety.

And now I'm starting to worry whether you can even construct Forall (Pure (ReaderT () n)) explicitly, since you have no way of mentioning the Skolem you actually need to instantiate Forall (Pure n) at. A new constraints export like the following might be needed (untested):

instImpl :: forall p q. (forall a. p a :- q a) -> (Forall p :- Forall q)
instImpl sub = Sub $ Dict \\ (sub :: p (Skolem q) :- q (Skolem q)) \\ inst

[oerjan]

Or perhaps this less complicated function, which was (with a different implementation) in the provisional rewrite after A/B were shown broken and before adding Skolems:

forall :: forall p. (forall a. Dict (p a)) -> Dict (Forall p)
forall d = case d :: Dict (p (Skolem p)) of Dict -> Dict

[maoe]

@oerjan Could you elaborate a bit on how to use those functions?

In general, wouldn't it be too restrictive if Forall (Pure m) doesn't imply Foreall (Pure (ReaderT r m)) given forall m a. StM (ReaderT r m) a ~ StM m a holds?