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 argumentk
; because now(Any k1 ~ Any k2)
does not entail(k1~k2)
. See also the moduleGHC.TypeLits
inbase
.
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 |