Can I statically reject different instantiations of an existential type?

Question

First attempt

It's difficult to make this question pithy, but to provide a minimal example, suppose I have this type:

{-# LANGUAGE GADTs #-}
data Val where
  Val :: Eq a => a -> Val

This type lets me happily construct the following heterogeneous-looking list:

l = [Val 5, Val True, Val "Hello!"]

But, alas, when I write down an Eq instance, things go wrong:

instance Eq Val where
  (Val x) == (Val y) = x == y -- type error

Ah, so we Could not deduce (a1 ~ a). Quite right; there's nothing in the definition that says x and y must be the same type. In fact, the whole point was to allow the possibility that they differ.

Second attempt

Let's bring Data.Typeable into the mix, and only try comparing the two if they happen to be the same type:

data Val2 where
  Val2 :: (Eq a, Typeable a) => a -> Val2

instance Eq Val2 where
  (Val2 x) == (Val2 y) = fromMaybe False $ (==) x <$> cast y

This is pretty nice. If x and y are the same type, it uses the underlying Eq instance. If they differ, it just returns False. However, this check is delayed until runtime, allowing nonsense = Val2 True == Val2 "Hello" to typecheck without complaint.

Question

I realize I'm flirting with dependent types here, but is it possible for the Haskell type system to statically reject something like the above nonsense, while allowing something like sensible = Val2 True == Val2 False to hand back False at runtime?

The more I work with this problem, the more it seems I need to adopt some of the techniques of HList to implement the operations I need as type-level functions. However, I am relatively new to using existentials and GADTs, and I am curious to know whether there's a solution to be found just with these. So, if the answer is no, I'd very much appreciate a discussion of exactly where this problem hits the limit of those features, as well as a nudge toward appropriate techniques, HList or otherwise.

Answer 1

In order to make type-checking decisions based on the contained types, we need to "remember" the contained type by exposing it as a type parameter.

data Val a where
  Val :: Eq a => a -> Val a

Now Val Int and Val Bool are different types, so we can easily enforce that only same-type comparisons are allowed.

instance Eq (Val a) where
  (Val x) == (Val y) = x == y

However, since Val Int and Val Bool are different types, we cannot mix them together in a list without an additional layer which "forgets" the contained type again.

data AnyVal where
  AnyVal :: Val a -> AnyVal

-- For convenience
val :: Eq a => a -> AnyVal
val = AnyVal . Val

Now, we can write

[val 5, val True, val "Hello!"] :: [AnyVal]

It should hopefully be clear by now that you cannot meet both requirements with a single data type, as doing so would require both "forgetting" and "remembering" the contained type at the same time.

Answer 2

So you want a constructor that allows you to use heterogeneous types, but you want comparisons between heterogeneous types that are knowable at compile time to be rejected. As in:

Val True == Val "bar"  --> type error

allSame [] = True
allSame (x:xs) = all (== x) xs

allSame [Val True, Val "bar"]  --> False

But surely:

(x == y) = allSame [x,y]

So I'm pretty sure a function with satisfies these constraints would violate some desirable property of a type system. Doesn't it look like that to you? I am strongly guessing "no, you can't do that".