The problem is that GHC doesn't do eta expansion for product types. See #7259, which won't be fixed by 7.10, as I would imagine a fair amount of theory needs to be done for this to be valid. Luckily, you can do eta expansion manually yourself: either by requiring that the caller know the eta-expanded form (1) or by storing that knowledge in a GADT (2): (1): Change the type signature of doubleEq to

doubleEq :: (forall a b. f a -> f b -> Maybe (a :~: b)) -> Dbl f (TwiceVal a1 a2) -> Dbl f (TwiceVal b1 b2) -> Maybe (TwiceVal a1 a2 :~: TwiceVal b1 b2)

Here, I've dumped the unnecessary `forall`s (for my own sanity) and simply eta-expanded `a` and `b`. With this type, the original implementation of `doubleEq` type checks. (2): Learn about the eta-expansion via a GADT pattern-match by changing `Dbl` to this:

data Dbl (f :: k -> *) (tv :: Twice k) where Dbl :: f a -> f b -> Dbl f (TwiceVal a b)

With this definition, when you pattern-match on the constructor `Dbl`, you also learn that `tv` really must be a `TwiceVal`. Then, the original type and definition for `doubleEq` type-check. The trade-off between (1) and (2) is where the caller needs to know about the eta-expansions: in (1), it's the caller of `doubleEq` that must know it's passing in a real `TwiceVal`. In (2), it's the caller of the `Dbl` constructor that must know. I rather favor (2), as it allows you to pass the expansion knowledge around quite easily, and you don't need the `TwiceLeft` and `TwiceRight` type families. Note that you need only solution (1) or (2), not both. (Though both works, too.) I hope this helps! Richard On Nov 8, 2014, at 7:26 PM, Rob wrote:

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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe