#7259: Eta expansion of products in System FC
---------------------------------+------------------------------------------
Reporter: simonpj | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.6.1
Keywords: | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
---------------------------------+------------------------------------------
This ticket is to capture the ideas in these GHC-users threads:
[http://www.haskell.org/pipermail/glasgow-haskell-
users/2012-August/022790.html PolyKinds Aug 2012] and
[http://www.haskell.org/pipermail/glasgow-haskell-
users/2012-September/thread.html 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!
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7259>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
