PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

[Richard Eisenberg]

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