Recently I’ve been working on a project where scoping is key to safety; the majority of functions in the library either require or provide a subscoping proof.

```
type role (~<) nominal nominal
data p ~< q = UnsafeSubscopeProof
```

The *direct* subscope relation is provided as a skeleton of proof elements, but in general the full reflexive transitive closure is required.

```
instance Category (~<) where
id = UnsafeSubscopeProof
!_ . !_ = UnsafeSubscopeProof
```

Collecting and composing these elements is a burden that need not be born by human hands, however—let’s offload this work onto GHC.

# Constraint Implication

We open with a trick I incidentally mentioned in another post recently.

`QuantifiedConstraints`

allows us to express constraint implication by using `(=>)`

at `Constraint -> Constraint -> Constraint`

. This relation is reflexive and transitive, and GHC knows it. As such, if we make our typeclass synonymous with such an implication, it will inherit these properties!

```
class SubscopeEndo s
class (SubscopeEndo p => SubscopeEndo q) => p <| q where
auto :: p ~< q
instance (SubscopeEndo p => SubscopeEndo q) => p <| q where
auto = UnsafeSubscopeProof
```

All that’s needed is to `reflect`

each proof element. Sadly, the superclass constraint prevents the use of `withDict`

, so we have to settle for `unsafeCoerce`

.

```
reflect :: forall p q r. p ~< q -> (p <| q => r) -> r
reflect !_ r = case magic of
Dict -> r
where
magic :: Dict (p <| q)
magic = unsafeCoerce (Dict @(p <| p))
```

In addition to the main library, there are a few sublibraries doing dual service as usage examples and tests of the interface. In writing them, I found the inference provided by this approach to be excellent—never needing annotations or type applications when proving truths. The only flaw in the UX was that the type errors were somewhat cryptic when mistakenly asked to prove falsehoods.

There are deep flaws in the *implementation*, however. On top of the unsafe `reflect`

ion, the key instance can only be written by abusing access to internals (or `unsafeCoerce`

) to provide an evil all-proof: `forall p q. p ~< q`

. It would also fail completely were the method to actually contain any data that could be distinguished at runtime.

# The Direct Approach

I came face to face with the flaws above when I was refactoring to separate conveniences from the minimal complete public interface—proof tokens fell on one side while inference fell on the other.

Now, I could have just made an exception and shifted the declaration of `~<`

into an internal module, but it didn’t feel right to do so—*I should be able to express my conveniences in terms of the public interface.*

And what was wrong with the direct approach anyway? Perhaps we can write this safely. Let’s see.

```
class p <| q where
auto :: p ~< q
instance p <| p where
auto = id
instance (p <| q, q <| r) => p <| r where
auto = auto @q @r . auto @p @q
```

Rather than *direct*, the above is really the *naïve* approach. Firstly, those instances overlap, but that can be resolved. More problematic is that the linking `q`

in the second instance is entirely ambiguous, and we really have no way to help GHC choose.

We need more structure to work with. Let’s start by distinguishing the direct subscoping proofs we reflect from the indirect ones we infer.

```
class Direct p q where
direct :: p ~< q
reflect :: p ~< q -> (Direct p q => r) -> r
reflect = withDict
```

Morally, this should have a `p <| q`

superclass, but that won’t do `reflect`

any favours so let’s not.

Intuitively, we now have our recursive structure: every `auto`

is either `id`

, or a `direct`

composed with a “smaller” `auto`

. But the matter of ambiguity remains.

We need either `p`

or `r`

to determine `q`

in that second instance. This isn’t possible with `<|`

, but *direct subscope* is functional! A scope may have many direct subscopes, but only one direct superscope.

Advising GHC of this fact by amending the declaration of `class Direct`

with the functional dependency `p -> q`

, we can finally write an instance that makes sense.

```
instance (Direct p q, q <| r) => p <| r where
auto = auto . direct
```

I expect that—with `OVERLAPPING`

and `OVERLAPPABLE`

pragmata in place—this approach would actually work out. For someone else, that is. I, on the other hand, am possessed of an unslakeable lust for `RankNTypes`

.

You see, all the scopes in question are skolems introduced by polymorphic continuations. This complicates the resolution of overlap, because while GHC knows that the instance head `p <| q`

matches, it cannot rule out the possibility that `p <| p`

does too. The way to pull it out of this sticky situation and allow it to select `p <| q`

is to slap `INCOHERENT`

on instance `p <| p`

.

… Or so I’d thought, anyway, but the behaviour of this direct approach is a little wild. At this point in time I don’t care to return for further meditations on the mysteries of Section 6.8.8.5, but it probably explains why I still can’t banish these overlap errors.

More interestingly, when not complaining about overlap, GHC instead throws this rare gem at me:

```
• Reduction stack overflow; size = 201
When simplifying the following type: q0 <| q1
• In the expression: auto
```

Oh dear. *More* mysteries I don’t wish to contemplate. In any case, I won’t fight this battle—let’s just run away.

# Return to the Origin

Let’s start over; reduce the issue to our precise cards and goals—eliminating all else—*then* seek the way between.

## Cards

We have, (we assume) some binary class `C`

for which we can *coherently* implement:

```
refl :: forall x . Dict (C x x)
trans :: forall x y z. Dict (C x y) -> Dict (C y z) -> Dict (C x z)
```

Coherence means the dictionaries are singletons, so it follows trivially that `refl`

is the identity to `trans`

and that `trans`

itself is associative—`C`

is a reflected `Category`

not just in my case, but more generally. Let’s call it `>->`

. Without loss of generality:

```
class C x y where
reify :: x >-> y
```

There’s one last piece of structure that was hiding before the previous section unearthed it: functionality. The possibility exists that the constraint implication approach was always depending upon this additional structure while I was blissfully unaware.

But that’s not the case—the truth is *worse*. Upon further investigation, I found that the way GHC solves quantified constraints is painfully limited! It can solve `c => e`

from `(c => d, c => d', d => e)`

, but not from `(c => d, c' => d, d => e)`

. In short: *the implications in scope must be reverse functional*.

That means my original approach was secretly broken, and should actually have used

```
class (SubscopeEndo q => SubscopeEndo p) => p <| q
```

but my testing either wasn’t extensive enough to uncover issues or my interface just happened to prevent them.

In any case, we don’t have a better approach to transitivity than constraint implication, so we must accept this restriction. Doing so gives us our last card: again w.l.o.g, `class C x y | x -> y`

.

## Goals

We want a `class Transitive c x y`

such that `Transitive C`

is indeed transitive (and reflexive), can be granted any instance that `C`

has:

```
grant :: C x y => Dict (Transitive C x y)
```

and any generated instance can be retrieved in reified form:

```
retrieve :: Transitive C x y => x >-> y
```

## The Way?

The best hint at a way forward is the type signature of `trans`

, or equivalently, `(.)`

:

```
(.) :: forall x y z. y >-> z -> x >-> y -> x >-> z
```

With a little rearranging, that says we have mappings:

```
yoneda1 :: forall y z. y >-> z -> forall x. x >-> y -> x >-> z
yoneda1 yz = (yz .)
yoneda2 :: forall x y. x >-> y -> forall z. y >-> z -> x >-> z
yoneda2 xy = (. xy)
```

`refl`

/`id`

then provides the inverses, showing that these types are equivalent.

```
unYoneda1 :: forall y z. (forall x. x >-> y -> x >-> z) -> y >-> z
unYoneda1 f = f id
unYoneda2 :: forall x y. (forall z. y >-> z -> x >-> z) -> x >-> y
unYoneda2 f = f id
```

These Yoneda embeddings give us alternate representations for any `Category`

, directly analogous to the Cayley transform on group-like structures (e.g. difference lists) and the `Codensity`

of a `Monad`

, down to the uniform re-association.

Translating the transformations onto `C`

, we obtain excellent candidates for our implication constraint:

```
C y z ~= forall x. C x y => C x z
C x y ~= forall z. C y z => C x z
```

Of the two, only the latter is reverse functional, so that’s our best choice.

```
class (forall z. c y z => c x z) => Transitive c x y
instance (forall z. c y z => c x z) => Transitive c x y
```

Having achieved the first of our three goals, the third is easy.

```
retrieve :: forall x y. Transitive C x y => x >-> y
retrieve = case refl @y of Dict -> reify
```

The second isn’t. We *can* write one half:

```
ant :: C x y => forall z. Dict (C y z) -> Dict (C x z)
ant = trans Dict
```

The other half, on the other hand, doesn’t even seem to be possible!

```
gr :: (forall z. Dict (C y z) -> Dict (C x z)) -> Dict (Transitive C x y)
gr f = ???
```

In the particular case where `(>->)`

carries no runtime-distinguishable data, `gr`

can be “written” by ignoring the argument and cooking up a dictionary with `unsafeCoerce`

, but that’s not exactly satisfactory.

# Afterword

Having been taken on such a long ride only to face defeat at every turn, you must be very disappointed. I know I am. Perhaps somewhere out there, there’s a hero who can `grant`

this tale the good ending it deserves.