Forgot to include the reference: [1] B. A. Yorgey et al. "Giving Haskell a Promotion" (http://www.seas.upenn.edu/~sweirich/papers/tldi12.pdf) On Sep 3, 2012, at 3:26 PM, Richard Eisenberg wrote:
On Sep 1, 2012, at 4:25 AM, Adam Gundry wrote:
As Edward and others have recognised, the problem here is that FC coercions are not expressive enough to prove eta rules, that is
forall x : (a, b) . x ~ (Fst x, Snd x)
or more generally, that every element of a single-constructor (record) type is equal to the constructor applied to the projections.
It seems like it should be perfectly fine to assert such a thing as an axiom, though, ... unless you have Any (as Richard observed), in which case all bets are off. Why did you want Any again?
I don't necessarily want Any, but Any is already there, in GHC.Exts. (Though, Any has been helpful in other type hackery exploits of mine...) So, any way of introducing eta-coercions will have to respect Any.
Intriguingly, the most recent published formulation of FC [1] leaves room for adding eta rules. The issue is one of consistency: if we have a coercion g : forall k1. forall k2. forall x:(k1,k2). x ~ (Fst x, Snd x) and the existence of Any : forall k.k, can we derive h : Int ~ Bool? In [1], the rules for consistency (from which progress & preservation are proved) apply only to coercions at a base kind, either * or Constraint. So, our eta coercion g is exempt from the consistency check -- it cannot make a system inconsistent. Thus, with or without Any, the coercion g cannot lead to a program that crashes due to a type error.
So, it seems possible to introduce eta coercions into FC for all kinds containing only one type constructor without sacrificing soundness. How the type inference engine/source Haskell triggers the use of these coercions is another matter, but there doesn't seem to be anything fundamentally wrong with the idea.
Richard