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.

[Lysxia]

I just ran into this issue too. Types like Set require more structure to define Arbitrary (another example is HashSet and its Hashable constraint). IMO rather than stacking more abstraction it's much better to expose the underlying type there. Just ask Arbitrary (f Integer) or something similar and let users use whatever operations on Integer are convenient for them to satisfy that constraint. You could also let users choose x in Arbitrary (f x), which may be useful for users who want to control every last bit of performance, but pretty much everyone will be happy with an arbitrary Int or Integer.

[aniketd]

I just ran into this too with foldableLaws

Details

data OSet a = OSet
  { osSeq :: Seq a
  , osSet :: Set a
  }

[Soupstraw]

I think there's no reason to have quantified constraints here whatsoever, because they both overconstrain the functions and confuse the hell out of people 😅. It'd be perfectly fine to have

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

In the end, a gets instantiated as an Integer anyways so it doesn't make sense to have stricter constraints on a than the ones on Integer.