Quantified Constraint Trick does not Work with more than One Constraint

Learn
#1

Why can not more than one constraint cannot be specified with the Quantified Constraint Trick?

class Show (StM m a) => ShowWorks m a

works :: forall m. (forall a. Show a => ShowWorks m a) => ...

class (Show a, Show (StM m a)) => ShowFails m a

fails :: forall m. (forall a. ShowFails m a) => ...

Using ghc 9.2.7

#2

Could you be more precise? What exactly doesn’t work? This works fine, for example:

{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

data StM m a = StM
  deriving Show

class Show (StM m a) => ShowWorks m a

works :: forall m. (forall a. Show a => ShowWorks m a) => ()
works = ()

class (Show a, Show (StM m a)) => ShowFails m a

fails :: forall m. (forall a. ShowFails m a) => ()
fails = ()
#3

Sure thing

StM is the type family from monad-control

I define my class here class Show (StM’ m a) => ShowStM’ m a

And use it here forall u a. Show a => ShowStM’ (p u) a

#4

Could you please provide a self-contained failing example, as small as possible? Something like 10 lines should be sufficient. I tried to build your project, but got

% cabal build --enable-tests -w ghc-9.2 biparsing-tests
Warning: Both /home/tom/.cabal and /home/tom/.config/cabal/config exist -
ignoring the former.
It is advisable to remove one of them. In that case, we will use the remaining
one by default (unless '$CABAL_DIR' is explicitly set).
Warning: The package list for 'hackage.haskell.org' is 26 days old.
Run 'cabal update' to get the latest list of available packages.
Resolving dependencies...
Error: cabal: Could not resolve dependencies:
[__0] trying: examples-0.0.0.1 (user goal)
[__1] trying: examples:*test
[__2] unknown package: biparsing-file (dependency of examples *test)
[__2] fail (backjumping, conflict set: biparsing-file, examples,
examples:test)
After searching the rest of the dependency tree exhaustively, these were the
goals I've had most trouble fulfilling: examples, examples:test,
biparsing-file

and indeed biparsing-file does not seem to be present in your repo.

1 Like
#5

Ok, I boilded it down to this

:set -XQuantifiedConstraints -XUndecidableInstances -XTypeFamilies -XAllowAmbiguousTypes
:{
type BaseResult m a = BaseMonad m (StM m a)
class RunBase m where
  type BaseMonad m :: * -> *
  type StM m a :: *
  runBase :: m a -> BaseResult m a
:}
:{
instance RunBase IO where
  type BaseMonad IO = IO
  type StM IO a = a
  runBase = id
:}
newtype MaybeT m a = MaybeT {runMaybeT :: m (Maybe a)} deriving Functor
instance Applicative m => Applicative (MaybeT m) where pure = MaybeT . pure . Just; MaybeT x <*> MaybeT y = MaybeT $ fmap (<*>) x <*> y
:{
instance RunBase m => RunBase (MaybeT m) where
  type BaseMonad (MaybeT m) = BaseMonad m
  type StM (MaybeT m) a = StM m (Maybe a)
  runBase = runBase . runMaybeT
:}
class Show (StM m a) => ShowWorks m a
instance Show (StM m a) => ShowWorks m a
:{
works :: forall m.
  ( forall a. Show a => ShowWorks m a
  , RunBase m
  , BaseMonad m ~ IO
  , Applicative m
  ) => IO ()
works = do
   print =<< runBase @m (pure ())
   print =<< runBase @m (pure 'a')
:}
works @(MaybeT IO)
class (Show a, Show (StM m a)) => ShowFails m a
instance (Show a, Show (StM m a)) => ShowFails m a
:{
fails :: forall m.
  ( forall a. ShowFails m a
  , RunBase m
  , BaseMonad m ~ IO
  , Applicative m
  ) => IO ()
fails = do
   print =<< runBase @m (pure ())
   print =<< runBase @m (pure 'a')
:}
fails @(MaybeT IO)

For me it produces:

<interactive>:47:4: error:
     Could not deduce (Show (StM m ())) arising from a use of ‘print’
      from the context: (forall a. ShowFails m a, RunBase m,
                         BaseMonad m ~ IO, Applicative m)
        bound by the type signature for:
                   fails :: forall (m :: * -> *).
                            (forall a. ShowFails m a, RunBase m, BaseMonad m ~ IO,
                             Applicative m) =>
                            IO ()
        at <interactive>:(40,1)-(45,12)
     In the first argument of ‘(=<<)’, namely ‘print’
      In a stmt of a 'do' block: print =<< runBase @m (pure ())
      In the expression:
        do print =<< runBase @m (pure ())
           print =<< runBase @m (pure 'a')

<interactive>:48:4: error:
     Could not deduce (Show (StM m Char))
        arising from a use of ‘print’
      from the context: (forall a. ShowFails m a, RunBase m,
                         BaseMonad m ~ IO, Applicative m)
        bound by the type signature for:
                   fails :: forall (m :: * -> *).
                            (forall a. ShowFails m a, RunBase m, BaseMonad m ~ IO,
                             Applicative m) =>
                            IO ()
        at <interactive>:(40,1)-(45,12)
     In the first argument of ‘(=<<)’, namely ‘print’
      In a stmt of a 'do' block: print =<< runBase @m (pure 'a')
      In the expression:
        do print =<< runBase @m (pure ())
           print =<< runBase @m (pure 'a')
#6

It is a surprising error, but it can’t possibly work anyway, since you’re asking for forall a. Show a, which isn’t satisfiable. I would expect the error to appear at the use site, fails, though.

#7

Did you perhaps mean

instance (Show a => Show (StM m a)) => ShowFails m a
#8

I get Illegal type synonym family application when I try that.

#9

I’m not sure what you mean by this. works @(MaybeT IO) does compile and can but run.

#10

Sure, works is fine, but fails is not. It requires forall a. ShowFails m a which can’t be satisfied because it implies forall a. Show a.

#11

Hmm, I see we’re back to the original problem. OK, it looks like you have to use some slightly different technology. This works:

class (Show a |- Show (StM m a)) => ShowFails m a
instance (Show a |- Show (StM m a)) => ShowFails m a

fails :: forall m.
  ( forall a. ShowFails m a
  , RunBase m
  , BaseMonad m ~ IO
  , Applicative m
  ) => IO ()
fails = do
   print =<< runBase @m (pure ())
   print =<< runBase @m (pure 'a')

bar = fails @(MaybeT IO)

using |- from the constraints library.

#12

(Parenthetical remark, which I hope comes across in the constructive spirit intended: whatever you’re trying to achieve, you’re unlikely to achieve it this way (unless it’s “experiment with gnarly corners of GHC constraint resolution”).)

#13

Is your remark referring to |-, ShowWorks, or both?

#14

It’s referring to everything you’re doing with QuantifiedConstraints, here and in other Discourse posts. It’s a very little explored corner of the ecosystem. As I understand it you are valiantly trying to write some functionality that works uniformly over different MTL types and/or transformers. I am highly skeptical that it’s going to work. I would recommend just using an effect system instead, either Bluefin or effectful.

1 Like
#15

Very helpful I will look at both Bluefin and effectful.

1 Like