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

[Andrea Vezzosi]

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