Opened 7 years ago

Last modified 11 months ago

#7259 new bug

Eta expansion of products in System FC

Reported by: simonpj Owned by: simonpj
Priority: normal Milestone:
Component: Compiler Version: 7.6.1
Keywords: Cc: Conor.McBride@…, nfrisby, eir@…, adamgundry, sweirich@…, ekmett@…, josef.svenningsson@…, wren@…, jstolarek, Iceland_jack, edsko, kcsongor, glaebhoerl
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


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!

Change History (26)

comment:1 Changed 7 years ago by nfrisby

Cc: nfrisby added

comment:2 Changed 7 years ago by goldfire

Cc: eir@… added

Adding some discussion that happened on the email thread:

The axioms that Simon mentioned:

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

The last two axioms are the straightforward compilations of the type families Fst and Snd -- nothing new is needed to create these. The first is the challenge and will require some type inference magic.

When trying to solve

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

(where a is untouchable), Simon suggested simplifying to

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

I don't think that's the right replacement. The next natural step would be decomposition, leading to (Fst a ~ t1) and (Snd a ~ t2), which would then get stuck, because Fst and Snd aren't injective. So, I would say we need

 a1, a2 fresh
 [G] a ~ '(a1, a2)
 [W] '(a1, a2) ~ '(t1, t2)

which would then decompose correctly. As I write this, I'm worried about that freshness condition... what if a appears multiple times in the type? We would either need to guarantee that a1 and a2 are the same each time, or create new [W] constraints that a1 ~ a1', etc. But, maybe this is easier in practice than it seems. Type inference experts?

Simon is a bit concerned about constraints like

 F a ~ e

where a:'(k1,k2), and we have a type instance like F '(a,b) = ... .

It seems to me that the proper eta-expansion (a ~ '(Fst a, Snd a)) would work here.

As for Any, (as Nick pointed out and Iavor elaborated) there is a workaround that Iavor and I can use involving the promoted version of

data KindProxy (a :: *) = KindProxy

to make kind classes and such. So, I think it's OK to relegate Any to a type function. Objections?

comment:3 Changed 7 years ago by igloo

Milestone: 7.8.1
Owner: set to simonpj

comment:4 Changed 7 years ago by adamgundry

Cc: adam.gundry@… added

I agree that Any should be a type function: to pass kinds as arguments, the proxy workaround is the right thing for now, at least until we get explicit type/kind application.

Richard, I think your proposed constraint simplification is sound, but I don't really understand the advantage over Simon's version. You are introducing fresh (untouchable?) variables a1 and a2 instead of Fst a and Snd a, but they don't get you any further. It doesn't matter that Fst and Snd are not injective, because the point of the decomposition into Fst a ~ t1 and Snd a ~ t2 is not to solve for a (which is untouchable anyway), but that we might be able to solve for t1 or t2 if one of them is a variable, or we might have other given constraints on the projections.

In general, adding support for eta to the constraint solver means it should never get stuck because an inhabitant of a pair (or other record) kind is not canonical. Certainly type family axioms F '(a, b) = t should be applicable even if the argument is not a canonical pair, but typeclass instances exhibit the same behaviour. For example, given the definitions

  class Foo (x :: '(a, b))
  instance Foo '(a, b)

we should be able to solve class constraints like Foo t using the existing instance.

comment:5 Changed 7 years ago by diatchki

I updated GHC.TypeLits to avoid using Any as a constructor, so now we should be able to convert it to a type function.

In a previous e-mail I mentioned some "sketchiness" that occurs when using Any (in either form) with empty kinds. Here is an example to illustrate the issue:

data {-kind-} Empty

data T (a :: Empty) = C deriving Show

main = print C -- what is the type of C here?

The issue is that in main: constructor C is of type T Any, with Any of kind Empty. However, kind Empty has no members, so what does Any refer to?

comment:6 Changed 7 years ago by simonpj

Cc: Conor.McBride@… sweirich@… added

Re the sketchiness, is your worry the following?

  • Even though the type Empty has no data constructors, there are terms with type Empty, namely diverging ones, such as undefined :: Empty.
  • But are there any types with kind Empty? You might think "no" since we don't have divergent type terms. But there is one, namely (Any Empty).

So, is that a problem? Adding Conor to the cc list.

comment:7 Changed 6 years ago by simonpj

Just by way of concrete example, here's the smallest example Edward wants to do:

{-# LANGUAGE PolyKinds, DataKinds, GADTs #-}
import Prelude hiding (id, (.))

class Category (k :: x -> x -> *) where
  id :: k a a
  (.) :: k b c -> k a b -> k a c

data P :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where
  P :: m a b -> n c d -> P m n '(a,c) '(b,d)

instance (Category m, Category n) => Category (P m n) where
  -- id = P id id
  P lf rf . P lg rg = P (lf . lg) (rf . rg)

The addition of id there causes it to fail to typecheck, because refining the kind to (x,y) doesn't let it know all types have the form '(a,b). It can't because Any still exists as a distinguishable member of every kind, so such a refinement would (currently) be unsound.

When we try to build indexed monad transformers we wind up wanting to take product over their indices. Similar issues arise when trying to compute with collages of profunctors and other nifty theoretical toys that have proven quite useful in the lens package.

comment:8 Changed 6 years ago by thoughtpolice


Moving to 7.10.1

comment:9 Changed 6 years ago by ekmett

Cc: ekmett@… added

comment:10 Changed 5 years ago by thoughtpolice


Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:11 Changed 5 years ago by adamgundry

Cc: adamgundry added; adam.gundry@… removed

It occurred to me in passing today that this would be a nice application of typechecker plugins. They should let us experiment with the type inference issues fairly easily.

comment:12 Changed 4 years ago by josef

Cc: josef.svenningsson@… added

comment:13 Changed 4 years ago by goldfire

Josef and I chatted about this ticket at HIW today. Now that Any is moved out of the way, it seems quite possible to revisit this. Shouldn't be too hard.

comment:14 Changed 4 years ago by thoughtpolice


Milestone renamed

comment:15 Changed 4 years ago by WrenThornton

Cc: wren@… added

comment:16 Changed 4 years ago by jstolarek

Cc: jstolarek added

comment:17 Changed 4 years ago by thomie

Milestone: 8.0.1

comment:18 Changed 3 years ago by Iceland_jack

Cc: Iceland_jack added

comment:19 Changed 3 years ago by edsko

Cc: edsko added

comment:20 Changed 2 years ago by Iceland_jack

What is the status of this?

comment:21 in reply to:  20 Changed 2 years ago by simonpj

What is the status of this?

It's parked at the moment. No one actually working on it that I know of.

comment:22 Changed 22 months ago by adamgundry

This is currently imperilled by #14420.

comment:23 Changed 22 months ago by kcsongor

Cc: kcsongor added

comment:24 Changed 22 months ago by simonpj

This is currently imperilled by #14420.

How, exactly?

comment:25 in reply to:  24 Changed 22 months ago by kcsongor

Replying to simonpj:

This is currently imperilled by #14420.

How, exactly?

#14420 means that one can define a distinguishable member of any kind, bringing back Any

data family Any :: k

Isn't this what caused the original soundness issue?

comment:26 Changed 11 months ago by glaebhoerl

Cc: glaebhoerl added
Note: See TracTickets for help on using tickets.