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
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 = ()
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
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')
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.
Did you perhaps mean
instance (Show a => Show (StM m a)) => ShowFails m a
I get Illegal type synonym family application
when I try that.
Iâm not sure what you mean by this. works @(MaybeT IO)
does compile and can but run.
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
.
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.
(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â).)
Is your remark referring to |-
, ShowWorks
, or both?
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
Very helpful I will look at both Bluefin and effectful.
1 Like