How to check higher-kinded types with constrained element types

[sjakobi]

I'm currently trying to add some tests to the multiset package. In particular, I want to test MultiSet's Foldable instance.

It turns out that I can't currently use foldableLaws for this, as I can't define an Arbitrary1 instance for MultiSet. The problem is the Ord constraint on the elements.

Can you recommend a workaround or maybe offer a version of foldableLaws that doesn't require Arbitrary1?

[chessai]

When compiling with GHC 8.5+, quickcheck-classes exposes all laws'
constraints in terms of QuantifiedConstraints. So

foldableLaws :: forall proxy f.
  (Foldable f, Eq1 f, Show1 f, Arbitrary1 f)
  => proxy f
  -> Laws

Becomes

foldableLaws :: forall proxy f.
  (Foldable f, forall a. Eq a => Eq (f a), forall a. Show a => Show (f a),
forall a. Arbitrary a => Arbitrary (f a))
  => proxy f
  -> Laws

[chessai]

This reminds me that we should do a release so the haddocks reflect this.

[chessai]

ie as long as a and MultiSet a can have Arbitrary instances, then something like foldableLaws (Proxy @(MultiSet Int)) with GHC 8.5+ should work fine

[sjakobi]

Ah, that explains the funny type error.

I think forall a. Arbitrary a => Arbitrary (f a) is the problem then, as it doesn't allow the additional Ord constraint.

something like foldableLaws (Proxy @(MultiSet Int))

Accepting a Proxy for a specific Type might actually be a solution, but currently foldableLaws requires the higher-kinded Proxy MultiSet.

[chessai]

Ah, yeah, Imessed up writing that proxy.

The following typechecks for me with GHC 8.6.2:

newtype Foo a = Foo a
  deriving (Eq, Show, Foldable)

instance (Arbitrary a, Ord a) => Arbitrary (Foo a) where
  arbitrary = fmap Foo arbitrary

foo :: Laws
foo = foldableLaws (Proxy @Foo)

[sjakobi]

Not sure what I'm doing wrong then. For

module ArbitraryMultiSet where

import Data.MultiSet
import Data.Proxy
import Test.QuickCheck
import Test.QuickCheck.Classes

instance (Arbitrary a, Ord a) => Arbitrary (MultiSet a) where
  arbitrary = fromList <$> arbitrary

laws :: Laws
laws = foldableLaws (Proxy :: Proxy MultiSet)

I get

ArbitraryMultiSet.hs:12:8: error:
    • Could not deduce (Ord a) arising from a use of ‘foldableLaws’
      from the context: Arbitrary a
        bound by a quantified context at ArbitraryMultiSet.hs:1:1
      Possible fix: add (Ord a) to the context of a quantified context
    • In the expression: foldableLaws (Proxy :: Proxy MultiSet)
      In an equation for ‘laws’:
          laws = foldableLaws (Proxy :: Proxy MultiSet)
   |
12 | laws = foldableLaws (Proxy :: Proxy MultiSet)
   |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

[chessai]

Oh, I guess it doesn't compile for me either. Something must've gone wrong with ghcid.

[chessai]

I think the best we could do is allow users to plug in constraints, not sure if this works though:

foldableLaws :: (Foldable f, forall x. (Eq x => Eq (f x), Show x => Show (f x)), forall x. (ctx x, Arbitrary x) => Arbitrary (f x))
  => Proxy ctx
  -> Proxy f
  -> Laws

[chessai]

So, this seems to work in spirit, (it compiles and constraint resolution works as expected, if foldableLawsInternal doesn't test anything) but a problem arises internally.

foldableLawsInternal :: forall proxy f ctx.
  (Foldable f, forall a. Eq a => Eq (f a), forall a. Show a => Show (f a), forall a. (ctx a, Arbitrary a) => (ctx a, Arbitrary (f a)))
  => Proxy ctx
  -> proxy f
  -> Laws
foldableLawsInternal pc p = Laws "Foldable"
  [ (,) "fold" $ property $ \(Apply (a :: f (Sum Integer))) ->
      F.fold a == F.foldMap id a
  , ...
  ]

We get a bunch of type errors like so:

src/Test/QuickCheck/Classes/Foldable.hs:115:18: error:
    • Could not deduce: ctx x arising from a use of ‘property’
      from the context: (Foldable f, forall a. Eq a => Eq (f a),
                         forall a. Show a => Show (f a),
                         forall a. (ctx a, Arbitrary a) => Arbitrary (f a))
        bound by the type signature for:
                   foldableLawsInternal :: forall (proxy :: (* -> *) -> *) (f :: *
                                                                                 -> *) (ctx 
:: *
                                                                                             
  -> Constraint).
                                           (Foldable f, forall a. Eq a => Eq (f a),
                                            forall a. Show a => Show (f a),
                                            forall a. (ctx a, Arbitrary a) => Arbitrary (f 
a)) =>
                                           Proxy ctx -> proxy f -> Laws
        at src/Test/QuickCheck/Classes/Foldable.hs:(107,1)-(113,33)
      or from: Arbitrary x
        bound by a quantified context
        at src/Test/QuickCheck/Classes/Foldable.hs:1:1
    • In the second argument of ‘($)’, namely
        ‘property
           $ \ (Apply (a :: f (Sum Integer))) -> fold a == foldMap id a’
      In the expression:
        (,) "fold"
          $ property
              $ \ (Apply (a :: f (Sum Integer))) -> fold a == foldMap id a
      In the second argument of ‘Laws’, namely
        ‘[(,) "fold"
            $ property
                $ \ (Apply (a :: f (Sum Integer))) -> fold a == foldMap id a,
          (,) "foldMap"
            $ property
                $ \ (Apply (a :: f Integer)) (e :: QuadraticEquation)
                    -> let ... in foldMap f a == foldr (mappend . f) mempty a,
          (,) "foldr"
            $ property
                $ \ (e :: LinearEquationTwo)
                    (z :: Integer)
                    (Apply (t :: f Integer))
                    -> let ... in foldr f z t == SG.appEndo (foldMap (Endo . f) t) z,
          (,) "foldr'" (foldableFoldr' p), ....]’
    • Relevant bindings include
        pc :: Proxy ctx
          (bound at src/Test/QuickCheck/Classes/Foldable.hs:114:22)
        foldableLawsInternal :: Proxy ctx -> proxy f -> Laws
          (bound at src/Test/QuickCheck/Classes/Foldable.hs:114:1)
    |
115 |   [ (,) "fold" $ property $ \(Apply (a :: f (SG.Sum Integer))) ->

[chessai]

That type error is a little confusing, since it refers to some type variable 'x' which doesn't exist, (might the renamer go from 'a' -> 'x'?), also the srcLoc of 1:1 is totally wrong.

[chessai]

Since we're using the following instance of 'Testable':

instance (Arbitrary a, Show a, Testable prop) => Testable (a -> prop)

the quantified constraint seems to be interfering with the Sum Integer, demanding that it satisifies ctx. which makes sense, since we told it the Arbitrary instance for f a demands that a satisfy ctx and Arbitrary.

[sjakobi]

I think the best we could do is allow users to plug in constraints

That looks like a nice idea. No idea about how to implement it though. This is the first time I've seen QuantifiedConstraints in practice.

[chessai]

@andrewthad is there anything here we could do with Dict from constraints? i guess we can't unify a with whatever we want if we allow supplied contexts

[chessai]

@sjakobi, this doesn't solve your issue, but will make your error messages make more sense when referencing the docs: quickcheck-classes 0.6.0.0 was just released to hackage.