[Haskell-cafe] Extensionality principles for kinds?

8 Nov 2014

      Haskellers,

I've waded into some pretty deep waters, but I'm hoping there's a GHC 
type system wizard in here who can help me.  The following code fragment 
is extracted from something I've been working on involving some pretty 
fancy type-level programming.  I'm using GHC 7.8.3.

I've run into a problem where the typechecker refuses to believe that 
two types are equal; it seems to lack the necessary extensionality 
principles for lifted data kinds.  Basically (see below for definitions) 
I get into a contex where I know that (TwiceLeft a ~ TwiceLeft b) and 
(TwiceRight a ~ TwiceRight b), but the typechecker will not believe that 
(a ~ b).

Are there any tricks I can employ to make this code typecheck (using 
only safe operations)?  Bonus if it doesn't add any runtime cost.

Thanks,
   Rob Dockins

====== code follows ======

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Type.Equality

-- lifted kind (Twice k) consists of a pair of things of kind k
data Twice k = TwiceVal k k

-- type family accessor functions for the Twice kind
type family TwiceLeft (x::Twice k) :: k where
   TwiceLeft (TwiceVal a b) = a

type family TwiceRight (x::Twice k) :: k where
   TwiceRight (TwiceVal a b) = b

-- Double is already taken, use Dbl instead...
data Dbl (f :: k -> *) (tv :: Twice k) = Dbl (f (TwiceLeft tv)) (f 
(TwiceRight tv))

-- This function doesn't typecheck...
doubleEq :: forall (f:: k -> *)
           . (forall (a::k) (b::k). f a -> f b -> Maybe (a :~: b))
          -> (forall (a::Twice k) (b::Twice k). Dbl f a -> Dbl f b -> 
Maybe (a :~: b))
doubleEq teq (Dbl x y) (Dbl z w) =
    case teq x z of
      Nothing -> Nothing
      Just Refl ->
        case teq y w of
          Nothing -> Nothing
          Just Refl -> Just Refl