DRY type annotation for QuickCheck properties

With QuickCheck, one can write parametrically polymorphic properties, like this:

associativityLaw :: (Eq a, Show a, Semigroup a) => a -> a -> a -> Property
associativityLaw x y z = (x <> y) <> z === x <> (y <> z)

This is just an example, as my actual properties are more complex, but it illustrates the problem well enough. This property verifies that for a type a, the <> operator is associative.

Imagine that I'd like to exercise this property for more than one type. I could define my test list like this:

tests =
  [
    testGroup "Monoid laws" [
      testProperty "Associativity law, [Int]" (associativityLaw :: [Int] -> [Int] -> [Int] -> Property),
      testProperty "Associativity law, Sum Int" (associativityLaw :: Sum Int -> Sum Int -> Sum Int -> Property)
    ]
  ]

This works, but feels unnecessarily verbose. I'd like to be able to simply state that for a given property, a should be [Int], or a should be Sum Int.

Something like this hypothetical syntax:

testProperty "Associativity law, [Int]" (associativityLaw :: a = [Int]),
testProperty "Associativity law, Sum Int" (associativityLaw :: a = Sum Int)

Is there a way to do this, perhaps with a GHC language extension?

My actual problem involves higher-kinded types, and I'd like to be able to state that e.g. f a is [Int], or f a is Maybe String.

I'm aware of this answer, but both options (Proxy and Tagged) seem, as described there, at least, too awkward to really address the issue.

Solution

You can use TypeApplications to bind type variables like this:

{-# LANGUAGE TypeApplications #-}

associativityLaw @[Int]

In the case you mentioned where you have a higher kinded type and you want to bind f a to [Int], you have to bind the type variables f and a separately:

fmap @[] @Int

For functions with more than one type variable, you can apply the args in order:

f :: a -> b -> Int

-- bind both type vars    
f @Int @String

-- bind just the first type var, and let GHC infer the second one
f @Int

-- bind just the second type var, and let GHC infer the first one
f @_ @String

Sometimes the "order" of the type variables may not be obvious, but you can use :type +v and ask GHCi for more info:

λ> :t +v traverse
traverse
  :: Traversable t =>
     forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b)

In standard haskell, the "order" of the type variables doesn't matter, so GHC just makes one up for you. But in the presence of TypeApplications, the order does matter:

map :: forall b a. (a -> b) -> ([a] -> [b])
-- is not the same as
map :: forall a b. (a -> b) -> ([a] -> [b])

For this reason, when working with highly parametric code, or you expect your users are going to want to use TypeApplications on your functions, you might want to explicitly set the order of your type vars instead of letting GHC define an order for you, with ExplicitForAll:

{-# LANGUAGE ExplicitForAll #-}

map :: forall a b. (a -> b) -> ([a] -> [b])

Which feels a lot like <T1, T2> in java or c#