Partially applied type with kind (* -> Constraint)

Question

Consider the following code:

class Foo f
class Bar b

newtype D d = D

call :: Proxy c -> (forall a . c a => a -> Bool) -> x -> Bool
call g x = g x

-- this function is Testable, and can be used by QuickCheck
f :: (Foo (D d), Bar d) => D d -> Bool
f = error ""

//assume the type FConstraint has kind (* -> Constraint)

main = print $ call (Proxy::Proxy FConstraint) (unsafeCoerce f) (D::D 17)

The intent of such a strange function is to be able to easily test polymorphic functions (such as f) using QuickCheck: call would be iterated over a type list of monomorphic types, and this list could be used for several different properties (all taking a single argument) without explicitly writing out type signatures each time. Since this is only appearing in test code, I'm willing to use unsafeCoerce (though I'm not sure it will do what I want at this point. I need to solve the question below first).

I'm certainly open to better/alternate designs for call, but here's my question about the solution I came up with above: I need a type FConstraint with kind (* -> Constraint) which can be used for the first argument to call.

Here's what I've tried:

type FConstraint x = (Foo x, Bar ??)
type FConstraint (D d) = (Foo (D d), Bar d)

Neither type synonym works, since I need to pattern match on the type to get all of the constraints, and also need to partially apply FConstraint, neither of which type synonyms allow.

I've also tried a type family:

type family FConstraint x
type instance FConstraint (D d) = (Foo (D d), Bar d)

but I still can't partially apply this (nor can I with a closed type family).

Thus I need a type of kind (* -> Constraint) which

• Pattern matches on the type of kind *
• Can be partially applied

---

UPDATE

Here's an almost-compiling example using the idea in the answer below:

{-# LANGUAGE RankNTypes, ScopedTypeVariables, ConstraintKinds, TypeOperators,
             MultiParamTypeClasses, DataKinds, PolyKinds, FlexibleInstances,
             UndecidableInstances, FlexibleContexts, TypeFamilies,
             FunctionalDependencies #-}

import Control.Monad
import Data.Proxy
import GHC.Prim
import GHC.TypeLits
import Test.QuickCheck
import Test.Framework
import Test.Framework.Providers.QuickCheck2
import Unsafe.Coerce

newtype Zq q = Zq Integer deriving (Show, Eq)

instance (KnownNat q) => Arbitrary (Zq q) where
  arbitrary = liftM (\i -> Zq $ (i `mod` (natVal (Proxy::Proxy q)))) arbitrary

instance (KnownNat q) => Num (Zq q) where
  (Zq a) + (Zq b) = Zq $ (a + b) `mod` (natVal (Proxy::Proxy q))
  (Zq a) * (Zq b) = Zq $ (a * b) `mod` (natVal (Proxy::Proxy q))
  negate (Zq 0) = (Zq 0)
  negate (Zq a) = Zq $ (natVal (Proxy::Proxy q)) - a
  fromInteger x = Zq $ x `mod` (natVal (Proxy::Proxy q))

f :: (KnownNat q) => Zq q -> Zq q
f x = x + 1

finv :: (KnownNat q) => Zq q -> Zq q
finv x = x - 1

prop_f :: forall q . (KnownNat q) => Zq q -> Bool
prop_f x = (finv . f) x == x

call :: (c x) => Proxy (c :: * -> Constraint) -> 
        (forall a . c a => a -> Bool) -> 
        x -> 
        Bool
call _ f = f

class UnZq zq q | zq -> q
instance UnZq (Zq q) q

class FConstraint x
instance (KnownNat q, UnZq zq q) => FConstraint zq

main = defaultMain $ [testProperty "zq_f_id" $ property $
         (call (Proxy::Proxy FConstraint) $ unsafeCoerce prop_f :: Zq 3 -> Bool)]

I get the error:

Could not deduce (KnownNat q0) arising from a use of ‘prop_f’
from the context (FConstraint a)

I'm hoping this is a simple scoping issue...

Here's more code for a use case:

type MyTypes = '[ Zq 3, Zq 5, Zq 7, Zq 11 ] 

class TypesToProps xs c where
  tmap :: Proxy xs -> Proxy c -> (forall a . c a => a -> Bool) -> [Property]

instance TypesToProps '[] c where
  tmap _ _ _ = []

instance (c x, TypesToProps xs c, Arbitrary x, Show x)
    => TypesToProps (x ': xs) c where
  tmap _ c f = (property (call c f :: x -> Bool)) : (tmap (Proxy::Proxy xs) c f)

-- results in same error as the `main` above
main = defaultMain $ map (testProperty "zq_f_id") $ 
         tmap (Proxy::Proxy MyTypes) 
              (Proxy::Proxy FConstraint) 
              (unsafeCoerce prop_f)

Answer 1

Firstly, your call function doesn't compile, nor should it: there is no way to infer c x in the type Proxy c -> (forall a . c a => a -> Int) -> x -> Int so you can't pass x to f.

Next, your use of unsafeCoerce is not valid here. If you look at the type of unsafeCoerce where you have used it:

withCall 
  :: (forall d . (Foo (D d), Bar d) => D d -> Bool) 
  -> (forall a . FConstraint a => a -> Int)
withCall = unsafeCoerce

You cast D d to any type and Bool to Int. (Note this requires ImpredictiveTypes). I don't understand your use case so I can't say if there is a better solution than unsafeCoerce, but I can say what you are doing will probably blow up in your face.

Writing the actual FConstraint is fairly easy:

class UnD x (y :: Nat) | x -> y 
instance UnD (D x) x 

class FConstraint x
instance (Foo x, Bar t, UnD x t) => FConstraint x

The complete code:

{-# LANGUAGE 
    UndecidableInstances
  , ImpredicativeTypes
  , MultiParamTypeClasses
  , FunctionalDependencies 
  #-}

import Unsafe.Coerce 
import GHC.Exts (Constraint)
import Data.Proxy 
import GHC.TypeLits 

class Foo f
class Bar (b :: Nat)

data D (d :: Nat) = D

call :: Proxy (c :: * -> Constraint) -> (forall a . c a => a -> Int) -> x -> Int
call = undefined

f :: (Foo (D d), Bar d) => D d -> Bool
f = error ""

withCall :: (forall d . (Foo (D d), Bar d) => D d -> Bool) -> (forall a . FConstraint a => a -> Int)
withCall = unsafeCoerce

class UnD x (y :: Nat) | x -> y 
instance UnD (D x) x 

class FConstraint x
instance (Foo x, Bar t, UnD x t) => FConstraint x

main = print $ call (Proxy :: Proxy FConstraint) (withCall f) (D :: D 17)

---

In response to your update, the immediately obvious thing to do would be to refactor your TypesToProps class:

class TypesToProps xs (c :: k -> Constraint) (t :: k -> *) where
  tmap :: Proxy xs -> Proxy c -> Proxy t -> (forall a . c a => t a -> Bool) -> [Property]

instance TypesToProps '[] c t where
  tmap _ _ _ _ = []

instance (c x, TypesToProps xs c t, Arbitrary (t x), Show (t x)) => TypesToProps (x ': xs) c t where
  tmap _ c t f = property (f :: t x -> Bool) : tmap (Proxy :: Proxy xs) c t f

main = defaultMain $ map (testProperty "zq_f_id") $ 
  tmap (Proxy :: Proxy '[3, 5, 7, 11]) 
       (Proxy :: Proxy KnownNat) 
       (Proxy :: Proxy Zq)
       prop_f

This may not be general enough, but it requires no use of unsafeCoerce.

When you write unsafeCoerce prop_f, the type checker demands that the KnownNat q constraint be satisfied before it can do anything with it. You must either retain the constraint on the result type - which is fundamentally incompatible with what you are doing - or erase the constraint first.

You can store constraints as data (which is how they are stored internally anyways for polymorphic functions):

data Dict p where 
  Dict :: p => Dict p 

We can erase constraints using this datatype:

anyDict :: Dict p 
anyDict = unsafeCoerce (Dict :: Dict (Eq ()))

prop_f' :: forall q . Zq q -> Bool
prop_f' q = case anyDict :: Dict (KnownNat q) of Dict -> prop_f q 

In general this will be unsafe, but in this specific case it is actually safe, since the q in Zq q is a phantom parameter, and to use anything involving Zq you need to pick a concrete q anyways, which would remove the class constraint anyways.

Then you can write

class TypesToProps xs where
  tmap :: Proxy xs -> (forall a . a -> Bool) -> [Property]

instance TypesToProps '[] where
  tmap _ _ = []

instance (TypesToProps xs, Arbitrary x, Show x) => TypesToProps (x ': xs) where
  tmap _ f = property (f :: x -> Bool) : tmap (Proxy :: Proxy xs) f where

Note that the function forall a . a -> Bool is uninhabited, so you can only produce a value of that type using unsafe functions. This means that it is impossible to shoot yourself in the foot using tmap alone; unless you use an unsafe function, you will never even be able to instantiate tmap. Finally:

main = defaultMain $ map (testProperty "zq_f_id") $ 
  tmap (Proxy :: Proxy '[Zq 3, Zq 5, Zq 7, Zq 11]) 
       (unsafeCoerce prop_f' :: forall a . a -> Bool)