Problem with quantified constraints

#1

Hi, I have a problem with quantified constraints not working as I think they should do. Consider the following typeclass

class Monad m => MonadStoreTrans c k f m | m -> f, m -> k, k -> c where
  type InitialStoreInfo m

  liftTask         :: f a -> m a
  lookupTaskResult :: c a => k a -> m (Maybe a)
  saveTaskResult   :: c a => k a -> a -> m ()
  runStoreTrans    :: InitialStoreInfo m -> m a -> f a

It describes a monad transformer with added ability of looking up keys k a -> a and saving them in store. I have one HashMap-based implementation, which works fine:

instance 
  ( Monad m
  , TaskPipeline k
  , TestEquality k
  , forall a. Hashable (k a)
  , c ~ TaskValueConstraint k
  ) => MonadStoreTrans c k m (NonPersistentStoreT k m) where

Ignoring other constraints, I have a quantified constraint forall a. Hashable (k a), which allows me to call hash on any key k a supplied in functions lookupTaskResult and saveTaskResult.

I wanted to have another instance of MonadStoreTrans, describing a logging transformer on top of other transformer:

instance 
  ( MonadStoreTrans c k f n
  , forall a. Show (k a)
  , forall a. c a => Show a
  ) => MonadStoreTrans c k f (LoggingStoreT n) where

However, this time the quantified constraint forall a. Show (k a) doesn’t work (while the second one forall a. c a => Show a works). When I try to show a key k a supplied to one of the functions, I get an error

• Could not deduce (Show (k a)) arising from a use of ‘show’
  from the context: (MonadStoreTrans c k f n, forall a. Show (k a),
                     forall a. c a => Show a)
    bound by the instance declaration
    at /home/mateusz/testing-framework/src/Testing/Store/LoggingTrans.hs:(27,3)-(30,46)
  or from: c a
    bound by the type signature for:
               lookupTaskResult :: forall a.
                                   c a =>
                                   k a -> LoggingStoreT n (Maybe a)
    at /home/mateusz/testing-framework/src/Testing/Store/LoggingTrans.hs:35:3-18
• In the first argument of ‘(<>)’, namely ‘show key’
  In the second argument of ‘(<>)’, namely
    ‘show key <> " as " <> show val’
  In the second argument of ‘($)’, namely
    ‘"Found cached key: " <> show key <> " as " <> show val’typecheck(-Wdeferred-type-errors)

My gut tells me there is something in play with instance resolution, as adding the same constraint to the previous declaration (without “basic” constraint MonadStoreTrans c k f n) works just fine. Any ideas how to make it work?

#2

I tested some things, and it seems that the presence of the constraint forall a. c a => Show a is preventing inference somehow.

Deleting forall a from this line, as shown below, got rid of the error.

instance 
  ( MonadStoreTrans c k f n
  , forall a. Show (k a) 
--, forall a. c a => Show a -- old
  , c a => Show a           -- new
  ) => MonadStoreTrans c k f (LoggingStoreT n) where

However, I don’t know why this happens, whether it will work for you, or whether it’s an acceptable solution overall.

1 Like
#3

Hi Gregory,

thanks for help and trying it out. Now I’m even more confused, as I have an instance with quantified constraint on a which works:

instance 
  ( MonadIO m
  , TaskPipeline k
  , TestEquality k
  , ShouldPersist k
  , forall a. Hashable (k a)
  , forall a. TaskValueConstraint k a => ToJSON a
  , forall a. TaskValueConstraint k a => FromJSON a
  , c ~ TaskValueConstraint k
  ) => MonadStoreTrans c k m (PersistentStoreT k m) where

(this is similar store but also persists values on filesystem via aeson instances). So here Hashable works along with constraints.

A workaround I went for was to use Show (Some k) instead of forall a. Show (k a), which is a bit annoying and ad-hoc, but at least works. I’ll try to extract some minimal example and maybe file GHC bug.

#4 
forall a. Hashable (k a)

That says that k a should be Hashable even if a isn’t. Is a meant to be some kind of phantom type parameter?

#5

Your new instance has qualified constraints, but all of them involve different classes Hashable, ToJSON and FromJSON. So perhaps the problem is having two qualified constraints with the same class, potentially overlapping?

I’ve already written cut-down test code, so here it is (declarations of language extensions omitted). Only the instance for BadInstance gives an error.

class Foo a where
  doFoo :: a -> ()

class Test k m where
  test :: k a -> ()

data BadInstance = BadInstance
instance
  ( forall a. Foo (k a)
  , forall a. c a => Foo a
  ) => Test k BadInstance where
    test x = doFoo x

data GoodInstance = GoodInstance
instance
  ( forall a. Foo (k a)
  ) => Test k GoodInstance where
    test x = doFoo x

data GoodInstance2 = GoodInstance2
instance
  ( forall a. Foo (k a)
  , c a => Foo a
  ) => Test k GoodInstance2 where
    test x = doFoo x

data GoodInstance3 = OtherInstance3
instance
  ( forall a. Foo (k a)
  , forall a. c a => Show a -- different class
  ) => Test k GoodInstance3 where
    test x = doFoo x
#6

k is a GADT, here describing a result of a computation

data Task a where
  ReadFile :: FilePath -> Task ByteString
  GetCurrentTime :: Task UTCTime

and so on. You see that a being Hashable has nothing to do with Task a being Hashable.

#7

Wow, you are spot on. If I change it to

class S a where
  sh :: a -> Text

instance 
  ( forall a. S (k a)
  , forall a. c a => Show a
  , MonadStoreTrans c k f n
  ) => MonadStoreTrans c k f (LoggingStoreT n) where

It doesn’t give any errors anymore. Not sure why, the constraints concern different types (a and k).

I guess I can use Show for keys and ToJSON for values, as I use them in base transformer anyway…

#8

But if the constraints use forall a, doesn’t that mean that a in the constraint can stand for any type? And in forall a. c a => Show a, if you choose a to be k a, you get forall a. c (k a) => Show (k a).

So, in the instance which gives an error, when the compiler is working out whether a type of the form k a has Show, it has to consider two constraints. I don’t know the details, but I can imagine that this could make inference more difficult.

Edit to add: This looks like a lot like the situation in the section on overlap of quantified constraints in the GHC user’s guide. It says that at the moment, GHC conservatively rejects these overlapping constraints if in doubt. So probably that is what’s happening.

1 Like