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

[Richard Eisenberg]

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