PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
eir at cis.upenn.edu
Tue Sep 4 00:20:58 CEST 2012
Forgot to include the reference:
 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  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 , 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.
More information about the Glasgow-haskell-users