Hi On 18 Mar 2009, at 15:00, Conal Elliott wrote:
I use these defs:
-- | Lift proof through a unary type constructor liftEq :: a :=: a' -> f a :=: f a' liftEq Refl = Refl
-- | Lift proof through a binary type constructor (including '(,)') liftEq2 :: a :=: a' -> b :=: b' -> f a b :=: f a' b' liftEq2 Refl Refl = Refl
-- | Lift proof through a ternary type constructor (including '(,,)') liftEq3 :: a :=: a' -> b :=: b' -> c :=: c' -> f a b c :=: f a' b' c' liftEq3 Refl Refl Refl = Refl
Makes you want kind polymorphism, doesn't it? Then we could just have (=$=) :: f :=: g -> a :=: b -> f a :=: g b Maybe the liftEq_n's are the way to go (although we called them "resp_n" when I was young), but they don't work for higher kinds. An alternative ghastly hack might be
data PackT2T (f :: * -> *)
(=$=) :: (PackT2T f :=: PackT2T g) -> (a :=: b) -> (f a :=: g b) Refl =$= Refl = Refl
But now you need a packer and an application for each higher kind. Or some bonkers type-level programming. This one will run and run... Cheers Conor