Relaxing RecAll Vinyl Restrictions Through Intro

Question

There is a RecAll type family in the vinyl library that allows us to require that the partially applied constraint be true for each type in the level type. For example, we can write this:

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

And this is all wonderful. Now, if we have the RecAll f rs c restriction, where c unknown, and we know that cx entails dx (borrow the language from the ekmett contstraints package ), how can we get RecAll f rs d ?

I ask that I work with records in some functions that require satisfying several type restrictions. To do this, I use the combinator :&: from the Control.Constraints.Combine module in exists . (Note: the package will not be created if you have other things installed, because it depends on the super-old version of contravariant . You can simply copy one of the modules that I mentioned.) With this I can get really nice restrictions while minimizing broiler. For example:

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

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

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

GHC does not see that the second statement follows from the first. I assumed that it would be so. What I do not see is to prove it, to confirm it and help the GHC. So far I have this:

 import Data.Constraint weakenAnd1 :: ((a :&: b) c) :- ac weakenAnd1 = Sub Dict -- not the Dict from vinyl. ekmett Dict. weakenAnd2 :: ((a :&: b) c) :- bc weakenAnd2 = Sub Dict 

They work fine. But here is where I am stuck:

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

This does not compile. Does anyone know of a way to get the effect I'm looking for. Here are the errors if they are helpful. Also, I have a Dict as a qualified import in my actual code, so why does it mention Constraint.Dict :

 Table.hs:76:23: Could not deduce (ac) arising from a pattern Relevant bindings include weakenRecAll :: Proxy f -> Proxy rs -> (ac :- bc) -> 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 (bc) 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 -> (ac :- bc) -> 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 start by looking at how Dict and (:-) should be used.

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

Matching the pattern with a Dict value of type Dict (Ord a) limits Ord a to the scope from which Eq a can be inferred (since Eq is the superclass of Ord ), so Dict :: Dict (Eq a) well-printed.

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

Similarly, Sub introduces an input constraint to the scope for the duration of its argument, allowing it to correctly enter this Dict :: Dict (Eq a) .

However, while pattern matching on a Dict results in a scope constraint, pattern matching in a Sub Dict does not enforce any new constraint conversion rule. In fact, if the input constraint is no longer in scope, you cannot match patterns 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, this explains your error of the first type, "Could not deduce (ac) arising from a pattern" : you tried to map the image to a Sub Dict , but the input restriction ac was not yet in scope.

Another type of error, of course, suggests that the constraints you were able to get in scope were not enough to satisfy the RecAll f rs b constraint. So which parts are needed and which 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 (fr), RecAll f rs c) 

Yeah! RecAll is a type family that is as invaluable as it is, with fully abstract rs , the RecAll f rs c constraint is a black box that cannot be made from any set of smaller parts. Once we specialize rs to [] or (r : rs) , it becomes clear which fragments we need:

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

I use p rs instead of Proxy rs because it is more flexible: if I had Rec f rs , for example, I could use it as my proxy with p ~ Rec f .

Then, to implement the version above with (:-) instead of Dict :

 weakenNil :: RecAll f '[] c1 :- RecAll f '[] c2 weakenNil = Sub Dict weakenCons :: p rs -> c1 (fr) :- c2 (fr) -> 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 introduces the RecAll f (r ': rs) c1 input restriction into the scope for the duration of its argument, which we organized to include the rest of the function body. The equation for the RecAll f (r ': rs) c1 type family expands to (c1 (fr), RecAll f rs c1) , which thus also enters the scope. The fact that they are in scope allows us to map patterns on two Sub Dict , and those two Dict bring their limitations in scope: c2 (fr) and RecAll f rs c2 . These two are what the RecAll f (r ': rs) c2 target constraint RecAll f (r ': rs) c2 , so our right side of the Dict well-typed.

To complete our implementation of weakenAllRec , we need to map the template to rs to determine if weakenNil or weakenCons should be delegated. But since rs is at the type level, we cannot directly match it to a template. The Hasochism document explains how to map patterns at the Nat level, we need to create a Natty shell data type. The way Natty works is that each of its constructors is indexed by the corresponding Nat constructor, so when we map a pattern to the Natty constructor at the value level, the corresponding constructor is also implied at the type level. We could define such a wrapper for lists of type types such as rs , but it happens that Rec f rs already has constructors corresponding to [] and (:) , and the calling elements weakenAllRec will probably have one of which lies around.

 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 entails type must be forall a. c1 a :- c2 a forall a. c1 a :- c2 a , not just c1 a :- c2 a , because we don’t want to say that weakenRecAll will work for any a choice of the caller, we want the caller to call that c1 a entails c2 a for each a .