On Mon, Sep 3, 2012 at 9:26 PM, Richard Eisenberg <e...@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 _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users