## Eta expansion of products in System FC

This ticket is to capture the ideas in these GHC-users threads: PolyKinds Aug 2012 and PolyKinds Sept 2012

- We want to add eta-rules to FC. Sticking to pairs for now, that would amount to adding two new type functions (Fst, Snd), and three new, built-in axioms

```
axPair k1 k2 (a:'(k1,k2)) : a ~ '(Fst a, Snd a)
axFst k1 k2 (a:k1) (b:k2) : Fst '(a,b) ~ a
axSnd k1 k2 (a:k1) (b:k2) : Snd '(a,b) ~ a
```

Generalising to arbitrary products looks feasible.

- Adding these axioms would make FC inconsistent, because

` axPair * * (Any '(*,*) ) : Any '(*,*) ~ (Fst .., Snd ..)`

and that has two different type constructors on each side. However, I think is readily solved: see below under "Fixing Any"

- Even in the absence of Any, it's not 100% obvious that adding the above eta axioms retains consistency of FC. I believe that Richard is volunteering to check this out. Right, Richard?

## Type inference

I'm a little unclear about the implications for inference. One route might be this. Suppose we are trying to solve a constraint

` [W] (a:'(k1,ks)) ~ '( t1, t2 )`

where a is an untouchable type variable. (if it was touchable we'd simply unify it.) Then we can replace it with a constraint

` [W] '(Fst a, Snd a) ~ '( t1, t2)`

Is that it? Or do we need more? I'm a bit concerned about constraints like

` F a ~ e`

where `a:'(k1,k2)`

, and we have a type instance like `F '(a,b) = ...`

Anything else?

I don't really want to eagerly eta-expand every type variable, because (a) we'll bloat the constraints and (b) we might get silly error messages. For (b) consider the insoluble constraint

` [W] a~b`

where `a`

and `b`

are both skolems of kind `'(k1,k2)`

. If we eta-expand both we'll get two insoluble constraints `(Fst a ~ Fst b)`

and `(Snd a ~ Snd b)`

, and we DEFINITELY don't want to report that as a type error!

Someone pointed out that Agda grapples with this problem and we should talk to them.

## Fixing Any

- I think we can fix the Any problem readily by making Any into a type family, that has no instances. We certainly allow equalities with a type
**family**application on the left and a type constructor on the right.

I have implemented this change already... it seems like a good plan.

- Several people have asked why we need Any at all. Consider this source program

` reverse []`

At what type should we instantiate

`reverse`

and the empty list`[]`

? Any type will do, but we must choose one; FC doesn't have unbound type variables. So I instantiate it at`(Any *)`

:

` reverse (Any *) ([] (Any *))`

Why is Any poly-kinded? Because the above ambiguity situation sometimes arises at other kinds.

- I'm betting that making Any into a family will mess up Richard's (entirely separate) use of
`(Any k)`

as a proxy for a kind argument`k`

; because now`(Any k1 ~ Any k2)`

does not entail`(k1~k2)`

. See also the module`GHC.TypeLits`

in`base`

.

We can't solve this by making `Any`

to be an *injective* type family, because the use in `TypeLits`

uses it in a type-class instance, and you can't match on type families!

## Trac metadata

Trac field | Value |
---|---|

Version | 7.6.1 |

Type | Bug |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | |

Architecture |