Suppose we have a type constructor f that takes two types, by means of a DataKinds-promoted pair.

```
forall (f :: (ka, kb) -> *)
```

I can then implement a function `forward`

, which is like `curry`

for the `forall`

quantifier:

```
forward :: forall (f :: (ka, kb) -> *).
(forall (ab :: (ka, kb)). f ab) ->
(forall (a :: ka) (b :: kb). f '(a, b))
forward x = x
```

However, the reverse function is problematic:

```
backward :: forall (f :: (*, *) -> *).
(forall (a :: *) (b :: *). f '(a, b)) ->
(forall (ab :: (*, *)). f ab)
backward x = x
```

GHC 8.0.1 gives the error message:

• Couldn't match type ‘ab’ with ‘'(a0, b0)’ ‘ab’ is a rigid type variable bound by the type signature for: backward :: forall (ab :: (*, *)). (forall a b. f '(a, b)) -> f ab at :6:116 Expected type: f ab Actual type: f '(a0, b0) • In the expression: x In an equation for ‘backward’: backward x = x

Conceptually, it seems like a valid program. Is there another way to implement this function? Or is this a known limitation of GHC?

`ab ~ '(Fst ab, Snd ab)`

, where`Fst`

and`Snd`

are the type-level projections. – pigworker`Any`

strikes again. (`Any :: (*, *)`

but it is not the case that`Any ~ (a, b)`

for any`a`

and`b`

.) – Daniel Wagner`forward`

and`backward`

functions? When would you want to use them? They just look like complicated`id`

functions to me. – Alexis King