haskell - Using the "constraints" package to make a wrapped function less polymorphic

Question

I have this datatype:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

import Data.Proxy
import Data.Constraint
import Data.Kind

type Foo :: (Type -> Constraint) -> Type
data Foo c = Foo (Proxy c) (forall x. c x => x -> x)

It doesn't look very useful, but it's a reduced version of a datatype that is useful.

I want to use the constraints package to write a mapping function over the constraint, using evidence of entailment:

restrictFoo :: forall less more. (forall v. more v :- less v) -> Foo less -> Foo more 

The idea is that if the more constraint is stronger than the less constraint, it should be possible to convert a less constrained function inside Foo into a more constrained one.

I think the forall v is in the correct place. If it ranged across all of the signature, the caller would be the one who chose v, which seems counterproductive when working with the polymorphic functions.

This naive attempt at implementation doesn't work:

restrictFoo :: forall less more. (forall v. more v :- less v) -> Foo less -> Foo more 
restrictFoo (Sub Dict) (Foo proxy f) = 
     Foo (Proxy @more) f

It fails with

* Could not deduce: more v0 arising from a pattern
* In the pattern: Dict
  In the pattern: Sub Dict
...
* Could not deduce: less x arising from a use of `f'
  from the context: less v0

How to write correctly the body of restrictFoo?

Answer 1

The problem is that, when you're unwrapping Sub Dict, there needs to be some v in scope to which the dictionary is going to apply, but there is none. So the compiler tries to create a fresh var v0 in hopes to unify it with something eventually, but the eventuality never comes.

But let's think: where would that v ultimately come from? Well, what does unwrapping Sub Dict give us? It gives us a less v (for some as of yet unknown v), provided we can give it more v. And what is the place where we just happen to have more v and need less v? Why it's inside of Foo's second argument of course!

So this means that we need to unwrap Sub Dict only when the second argument of Foo is actually called. At that point, whoever called it will have provided an instance of more v, so we'll be able to give it to Sub Dict and get out a less v.

So naively it would look something like this:

restrictFoo e (Foo proxy f) =
     Foo (Proxy @more) x -> case e of Sub Dict -> f x

But this still doesn't work: the compiler doesn't know that the type of x is the same type that it needs to use for Sub Dict. There is no connection between the two!

To create such connection, we need to explicitly quantify over the type of x, and to do that, we need to give the new function a type signature:

restrictFoo e (Foo proxy f) =
     Foo (Proxy @more) f'
     where
        f' :: forall x. more x => x -> x
        f' x = case e of Sub (Dict :: Dict (less x)) -> f x

Now this works: whenever somebody takes f' out of the Foo and calls it, they will have to provide an instance of more x, and having that instance in scope will allow us to give it to Sub and get out a Dict (less x), which gives us an instance of less x, which finally allows us to call the original f.