Weakening vinyl's RecAll constraint through entailment

Question

In the vinyl library, there is a RecAll type family, which let's us ask that a partially applied constraint is true for every type in a type level list. For example, we can write this:

myShowFunc :: RecAll f rs Show => Rec f rs -> String

And that's all lovely. Now, if we have the constraint RecAll f rs c where c is unknown, and we know the c x entails d x (to borrow language from ekmett's contstraints package), how can we get RecAll f rs d?

The reason I ask is that I'm working with records in some functions that require satisfying several typeclass constraints. To do this, I am using the :&: combinator from the Control.Constraints.Combine module in the exists package. (Note: the package won't build if you have other things installed because it depends on a super-old version of contravariant. You can just copy the one module I mentioned though.) With this, I can get some really beautiful constraints while minimizing typeclass broilerplate. For example:

RecAll f rs (TypeableKey :&: FromJSON :&: TypeableVal) => Rec f rs -> Value

But, inside the body of this function, I call another function that demands a weaker constraint. It might look like this:

RecAll f rs (TypeableKey :&: TypeableVal) => Rec f rs -> Value

GHC can't see that the second statement follows from the first. I assumed that would be the case. What I can't see is how to prove it for reify it and help GHC out. So far, I've got this:

import Data.Constraint

weakenAnd1 :: ((a :&: b) c) :- a c                                                                    
weakenAnd1 = Sub Dict -- not the Dict from vinyl. ekmett's Dict.

weakenAnd2 :: ((a :&: b) c) :- b c                                                                    
weakenAnd2 = Sub Dict

These work fine. But this is where I am stuck:

-- The two Proxy args are to stop GHC from complaining about AmbiguousTypes
weakenRecAll :: Proxy f -> Proxy rs -> (a c :- b c) -> (RecAll f rs a :- RecAll f rs b)
weakenRecAll _ _ (Sub Dict) = Sub Dict

This does not compile. Is anyone aware of a way to get the effect I am looking for. Here are the errors if they are helpful. Also, I have Dict as a qualified import in my actual code, so that's why it mentions Constraint.Dict:

Table.hs:76:23:
    Could not deduce (a c) arising from a pattern
    Relevant bindings include
      weakenRecAll :: Proxy f
                      -> Proxy rs -> (a c :- b c) -> RecAll f rs a :- RecAll f rs b
        (bound at Table.hs:76:1)
    In the pattern: Constraint.Dict
    In the pattern: Sub Constraint.Dict
    In an equation for ‘weakenRecAll’:
        weakenRecAll _ _ (Sub Constraint.Dict) = Sub Constraint.Dict

Table.hs:76:46:
    Could not deduce (RecAll f rs b)
      arising from a use of ‘Constraint.Dict’
    from the context (b c)
      bound by a pattern with constructor
                 Constraint.Dict :: forall (a :: Constraint).
                                    (a) =>
                                    Constraint.Dict a,
               in an equation for ‘weakenRecAll’
      at Table.hs:76:23-37
    or from (RecAll f rs a)
      bound by a type expected by the context:
                 (RecAll f rs a) => Constraint.Dict (RecAll f rs b)
      at Table.hs:76:42-60
    Relevant bindings include
      weakenRecAll :: Proxy f
                      -> Proxy rs -> (a c :- b c) -> RecAll f rs a :- RecAll f rs b
        (bound at Table.hs:76:1)
    In the first argument of ‘Sub’, namely ‘Constraint.Dict’
    In the expression: Sub Constraint.Dict
    In an equation for ‘weakenRecAll’:
        weakenRecAll _ _ (Sub Constraint.Dict) = Sub Constraint.Dict

Answer 1

Let's begin by reviewing how Dict and (:-) are meant to be used.

ordToEq :: Dict (Ord a) -> Dict (Eq a)
ordToEq Dict = Dict

Pattern matching on a value Dict of type Dict (Ord a) brings the constraint Ord a into scope, from which Eq a can be deduced (because Eq is a superclass of Ord), so Dict :: Dict (Eq a) is well-typed.

ordEntailsEq :: Ord a :- Eq a
ordEntailsEq = Sub Dict

Similarly, Sub brings its input constraint into scope for the duration of its argument, allowing this Dict :: Dict (Eq a) to be well-typed as well.

However, whereas pattern-matching on Dict brings a constraint into scope, pattern-matching on Sub Dict does not bring into scope some new constraint conversion rule. In fact, unless the input constraint is already in scope, you can't pattern-match on Sub Dict at all.

-- Could not deduce (Ord a) arising from a pattern
constZero :: Ord a :- Eq a -> Int
constZero (Sub Dict) = 0

-- okay
constZero' :: Ord a => Ord a :- Eq a -> Int
constZero' (Sub Dict) = 0

So that explains your first type error, "Could not deduce (a c) arising from a pattern": you have tried to pattern-match on Sub Dict, but the input constraint a c was not already in scope.

The other type error, of course, is saying that the constraints you did manage to get into scope were not sufficient to satisfy the RecAll f rs b constraint. So, which pieces are needed, and which ones are missing? Let's look at the definition of RecAll.

type family RecAll f rs c :: Constraint where
  RecAll f [] c = ()     
  RecAll f (r : rs) c = (c (f r), RecAll f rs c)

Aha! RecAll is a type family, so unevaluated as it is, with a completely abstract rs, the constraint RecAll f rs c is a black box which could not be satisfied from any set of smaller pieces. Once we specialize rs to [] or (r : rs), it becomes clear which pieces we need:

recAllNil :: Dict (RecAll f '[] c)
recAllNil = Dict

recAllCons :: p rs
           -> Dict (c (f r))
           -> Dict (RecAll f rs c)
           -> Dict (RecAll f (r ': rs) c)
recAllCons _ Dict Dict = Dict

I'm using p rs instead of Proxy rs because it's more flexible: if I had a Rec f rs, for instance I could use that as my proxy with p ~ Rec f.

Next, let's implement a version of the above with (:-) instead of Dict:

weakenNil :: RecAll f '[] c1 :- RecAll f '[] c2
weakenNil = Sub Dict

weakenCons :: p rs
           -> c1 (f r) :- c2 (f r)
           -> RecAll f rs c1 :- RecAll f rs c2
           -> RecAll f (r ': rs) c1 :- RecAll f (r ': rs) c2
weakenCons _ entailsF entailsR = Sub $ case (entailsF, entailsR) of
    (Sub Dict, Sub Dict) -> Dict

Sub brings its input constraint RecAll f (r ': rs) c1 into scope for the duration of its argument, which we've arranged to include the rest of the function's body. The equation for the type family RecAll f (r ': rs) c1 expands to (c1 (f r), RecAll f rs c1), which are thus both brought into scope as well. The fact that they are in scope allows us to pattern-match on the two Sub Dict, and those two Dict bring their respective constraints into scope: c2 (f r), and RecAll f rs c2. Those two are precisely what the target constraint RecAll f (r ': rs) c2 expands to, so our Dict right-hand side is well-typed.

To complete our implementation of weakenAllRec, we will need to pattern-match on rs in order to determine whether to delegate the work to weakenNil or weakenCons. But since rs is at the type level, we cannot pattern-match on it directly. The Hasochism paper explains how in order to pattern-match on a type-level Nat, we need to create a wrapper datatype Natty. The way in which Natty works is that each of its constructors is indexed by a corresponding Nat constructor, so when we pattern-match on a Natty constructor at the value level, the corresponding constructor is implied at the type level as well. We could define such a wrapper for type-level lists such as rs, but it just so happens that Rec f rs already has constructors corresponding to [] and (:), and the callers of weakenAllRec are likely to have one lying around anyway.

weakenRecAll :: Rec f rs
             -> (forall a. c1 a :- c2 a)
             -> RecAll f rs c1 :- RecAll f rs c2
weakenRecAll RNil       entails = weakenNil
weakenRecAll (fx :& rs) entails = weakenCons rs entails
                                $ weakenRecAll rs entails

Note that the type of entails must be forall a. c1 a :- c2 a, not merely c1 a :- c2 a, because we don't want to claim that weakenRecAll will work for any a of the caller's choosing, but rather, we want to require the caller to prove that c1 a entails c2 a for every a.