# Bidirectional Type Family Inference

## Problem

Imagine you have a relation, say, `R x y z` such that x and y uniquely determine z, and z uniquely determines x and y. You have to use the relation in a type signature in such a way that x and y can be inferred from z, and vice versa.

We'll use this relation as an example:
```
R True e (e, e)
R False e (e, e, e)
```

## Attempt 1: Fundeps in MPTC

Let's try solving this with functional dependencies in multi-parameter typeclasses!
```
{-# LANGUAGE DataKinds, MultiParamTypeClasses, FunctionalDependencies, KindSignatures, FlexibleInstances #-}
class R (x :: Bool) y z | x y -> z, z -> x y where
xy2z :: Proxy x -> y -> z; xy2z = undefined -- for demonstration purposes
z2x :: z -> Proxy x; z2x = undefined
z2y :: z -> y; z2y = undefined
instance R True e (e, e)
instance R False e (e, e, e)
```

Let's test this out!

`xy2z (Proxy :: Proxy True) ()` has type `((), ())`, nice!

`xy2z (Proxy :: Proxy False) 3` has type `Num t => (t, t, t)`, great, now let's test the reverse:

`z2y ((), ())` has type `()`

`z2y (2, 7)` has type...
```
Could not deduce (R x0 y (t0, t2))
arising from the ambiguity check for ‘it’
from the context (R x y (t1, t3), Num t1, Num t3)
bound by the inferred type for ‘it’: (R x y (t1, t3), Num t1, Num t3) => y
The type variables ‘x0’, ‘t0’, ‘t2’ are ambiguous
When checking that ‘it’
has the inferred type ‘forall (x :: Bool) y t1 t2. (R x y (t1, t2), Num t1, Num t2) => y’
Probable cause: the inferred type is ambiguous
```

No go. The typechecker can't infer `a ~ b` from `R x y (a, b)`

## Attempt 2: Closed Type Families

What if we define`R`as a type family taking x and y and returning z?

```
{-# LANGUAGE DataKinds, TypeFamilies, KindSignatures #-}
type family R (x :: Bool) y where
R True e = (e, e)
R False e = (e, e, e)
xy2z :: Proxy x -> y -> R x y; xy2z = undefined
z2xy :: R x y -> (Proxy x, y); z2xy = undefined
```

`xy2z (Proxy :: Proxy True) 3` has type `Num t => (t, t)`, but if we try to typecheck `z2xy ((), ())`...
```
Couldn't match expected type ‘((), ())’ with actual type ‘R x y’
The type variables ‘x’, ‘y’ are ambiguous
```

Even though it's obvious from the definition of `R` (and the fact that it's closed), the typechecker can't derive `y ~ ()` from `R x y ~ ((), ())`

## Attempt 3: Inverse Families

If z uniquely determines x and y, we can build two type families that turn z into x, and into y:
```
{-# LANGUAGE DataKinds, TypeFamilies, KindSignatures #-}
type family R (x :: Bool) y where
R True e = (e, e)
R False e = (e, e, e)
type family ZToX z where
ZToX (e, e') = True
ZToX (e, e', e'') = False
type family ZToY z where
ZToY (e, e') = e
ZToY (e, e', e'') = e
xy2z :: Proxy x -> y -> R x y; xy2z = undefined
z2xy :: z -> (Proxy (ZToX z), ZToY z); z2xy = undefined
```

Note that `ZToX` and `ZToY` accept types that, strictly speaking, cannot be outputs of `R`, this is a rather important point.

`z2xy` now works as expected, `z2xy (4, 0)` infers the type `Num t => (Proxy True, t)`.

Is this it? No. `xy2z` can infer the type of the result from the types of arguments, but it can't infer the types of the arguments from the type of the result! Even though `z2xy` successfully accomplishes an equivalent task! We have a type family for inferring z from x and y, a type family for inferring x from z, and a type family for inferring y from z; why can't we make a type that can infer in both directions simultaneously?

We can. Just throw the three type families into one type signature in the only way that makes sense:
```
xy2z :: (z ~ R x y, x ~ ZToX z, y ~ ZToY z) => Proxy x -> y -> z; xy2z = undefined
z2xy :: (z ~ R x y, x ~ ZToX z, y ~ ZToY z) => z -> (Proxy x, y); z2xy = undefined
```

Now both `xy2z` and `z2xy` can infer the types of their arguments in all ways implied by the original relation. Bonus points:
```
> z2xy (_, ())
Found hole ‘_’ with type: ()
```

That is, `a ~ b` is inferred from `R x y (a, b)`.