Perhaps this is a stupid question. Here's a quote from the *Hasochism* paper:

One approach to resolving this issue is to encode lemmas, given by parameterised equations, as Haskell functions. In general, such lemmas may be encoded as functions of type:

```
∀ x1 ... xn. Natty x1 → ... → Natty xn → ((l ~ r) ⇒ t) → t
```

I thought I understood `RankNTypes`

, but I can't make sense of the last part of this proposition. I'm reading it informally as "given a term which requires `l ~ r`

, return that term". I'm sure this interpretation is wrong because it seems to lead to a circularity: we don't know `l ~ r`

until the conclusion of the proof itself, so how can I be expected to provide as an assumption of the proof a term which requires that?

I would have expected an equality proof to have a type more like this:

```
Natty x1 → ... → Natty xn → l :~: r
```

Informally, "given a bunch of `Natty`

s, return a proof that the propositions `l`

and `r`

are equal" (using GHC's Data.Type.Equality). This makes far more sense to me, and seems to align with what you'd say in other dependently typed systems. I'm guessing it's equivalent to the version in the paper, but I'm struggling to mentally square away the two versions.

In short, I'm confused. I feel like I'm missing a key insight. How should I read the type `((l ~ r) => t) -> t`

?

# Best How To :

I'm reading it as "given a term which requires `l ~ r`

, return that term"

It's "given a term whose type contains `l`

, return that term with all `l`

s being substituted by `r`

s in the type" (or in the other direction `r -> l`

). It's a very neat trick, that allows you to delegate all `cong`

, `trans`

, `subst`

and similar stuff to GHC.

Here is an example:

```
{-# LANGUAGE GADTs, DataKinds, PolyKinds, TypeFamilies, TypeOperators, RankNTypes #-}
data Nat = Z | S Nat
data Natty n where
Zy :: Natty Z
Sy :: Natty n -> Natty (S n)
data Vec a n where
Nil :: Vec a Z
Cons :: a -> Vec a n -> Vec a (S n)
type family (n :: Nat) :+ (m :: Nat) :: Nat where
Z :+ m = m
(S n) :+ m = S (n :+ m)
assoc :: Natty n -> Natty m -> Natty p -> (((n :+ m) :+ p) ~ (n :+ (m :+ p)) => t) -> t
assoc Zy my py t = t
assoc (Sy ny) my py t = assoc ny my py t
coerce :: Natty n -> Natty m -> Natty p -> Vec a ((n :+ m) :+ p) -> Vec a (n :+ (m :+ p))
coerce ny my py xs = assoc ny my py xs
```

**UPDATE**

It's instructive to specialize `assoc`

:

```
assoc' :: Natty n -> Natty m -> Natty p ->
(((n :+ m) :+ p) ~ (n :+ (m :+ p)) => Vec a (n :+ (m :+ p)))
-> Vec a (n :+ (m :+ p))
assoc' Zy my py t = t
assoc' (Sy ny) my py t = assoc ny my py t
coerce' :: Natty n -> Natty m -> Natty p -> Vec a ((n :+ m) :+ p) -> Vec a (n :+ (m :+ p))
coerce' ny my py xs = assoc' ny my py xs
```

**Daniel Wagner** explained what's going on in comments:

Or, to say it another way, you can read ((l ~ r) => t) -> t as, "given a term that is well typed assuming that l ~ r, return that same term from a context where we have proven l ~ r and discharged that assumption".

Let's elaborate the proving part.

In the `assoc' Zy my py t = t`

case `n`

is equal to `Zy`

and hence we have

```
((Zy :+ m) :+ p) ~ (Zy :+ (m :+ p))
```

which reduces to

```
(m :+ p) ~ (m :+ p)
```

This is clearly identity and hence we can discharge that assumption and return `t`

.

At each recursive step we maintain the

```
((n :+ m) :+ p) ~ (n :+ (m :+ p))
```

equation. So when `assoc' (Sy ny) my py t = assoc ny my py t`

the equation becomes

```
((Sy n :+ m) :+ p) ~ (Sy n :+ (m :+ p))
```

which reduces to

```
Sy ((n :+ m) :+ p) ~ Sy (n :+ (m :+ p))
```

due to the definition of `(:+)`

. And since constructors are injective

```
constructors_are_injective :: S n ~ S m => Vec a n -> Vec a m
constructors_are_injective xs = xs
```

the equation becomes

```
((n :+ m) :+ p) ~ (n :+ (m :+ p))
```

and we can call `assoc'`

recursively.

Finally in the call of `coerce'`

these two terms are unified:

```
1. ((n :+ m) :+ p) ~ (n :+ (m :+ p)) => Vec a (n :+ (m :+ p))
2. Vec a ((n :+ m) :+ p)
```

Clearly `Vec a ((n :+ m) :+ p)`

is `Vec a (n :+ (m :+ p))`

under the assumption that `((n :+ m) :+ p) ~ (n :+ (m :+ p))`

.