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

[Richard Eisenberg]

I retract my statement.

My mistake was that I looked at the definition for consistency in FC -- which correctly is agnostic to non-base-kind coercions -- and applied it only to the set of coercion assumptions, not to any coercion derivable from the assumptions. As Andrea's example shows, by assuming an eta coercion, it is possible to derive an inconsistent coercion.

Examining the definition for FC consistency more closely, an eta coercion does not match to the form allowed for coercion assumptions used to prove consistency. The proof, in [1], requires all assumptions to have a type family application on the left-hand side. An eta coercion does not have a type family application on either side, and so the consistency proof in [1] does not apply.

In light of this, it would seem that allowing eta coercions while retaining consistency would require some more work.

Thanks for pointing out my mistake.
Richard

[1] S. Weirich et al. "Generative Type Abstraction and Type-level Computation."
(http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf)

On Sep 3, 2012, at 10:28 PM, Andrea Vezzosi wrote:

> On Mon, Sep 3, 2012 at 9:26 PM, Richard Eisenberg <eir at cis.upenn.edu> wrote:
>> [...]
>> 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.
>> 
> 
> A recent snapshot of ghc HEAD doesn't seem to agree:
> 
> {-# LANGUAGE GADTs, KindSignatures, PolyKinds, DataKinds,
> TypeFamilies, ScopedTypeVariables, TypeOperators #-}
> 
> import GHC.Exts
> import Unsafe.Coerce
> 
> data (:=:) :: k -> k -> * where
>  Refl :: a :=: a
> 
> trans :: a :=: b -> b :=: c -> a :=: c
> trans Refl Refl = Refl
> 
> type family Fst (x :: (a,b)) :: a
> type family Snd (x :: (a,b)) :: b
> 
> type instance Fst '(a,b) = a
> type instance Snd '(a,b) = b
> 
> eta :: x :=: '(Fst x, Snd x)
> eta = unsafeCoerce Refl
> -- ^^^ this is an acceptable way to simulate new coercions, i hope
> 
> type family Bad s t  (x :: (a,b)) :: *
> type instance Bad s t '(a,b) = s
> type instance Bad s t Any = t
> 
> refl_Any :: Any :=: Any
> refl_Any = Refl
> 
> cong_Bad :: x :=: y -> Bad s t x :=: Bad s t y
> cong_Bad Refl = Refl
> 
> s_eq_t :: forall (s :: *) (t :: *). s :=: t
> s_eq_t = cong_Bad (trans refl_Any eta)
> 
> subst :: x :=: y -> x -> y
> subst Refl x = x
> 
> coerce :: s -> t
> coerce = subst s_eq_t
> 
> {-
> GHCi, version 7.7.20120830: http://www.haskell.org/ghc/  :? for help
> *Main> coerce (4.0 :: Double) :: (Int,Int)
> (Segmentation fault
> -}
> 
> -- Andrea Vezzosi
>