#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 Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs