Hello,

I continue my learning of "not so obvious" Haskell/GHC topics when
encountering problems in the code I write.
Below is a small example of an heterogeneous list, using GADT, inspired
from:
http://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types#Example:_heterogeneous_lists

----------
{-# LANGUAGE GADTs #-}

data Box where
    Box :: Eq s => s -> Box

instance Eq Box where

    (Box s1) == (Box s2) = s1 == s2
----------

This code does not compile, because GHC is not sure that s1 and s2 have the
same type:

----------
Could not deduce (s ~ s1)
    from the context (Eq s)
      bound by a pattern with constructor
                 Box :: forall s. Eq s => s -> Box,
               in an equation for `=='
      at test_eq_GADT_before.hs:8:6-11
[and more lines...]
----------

(Do you confirm that tilde in s~s1 means "s has the same type as s1"? I have
not found this information explicitly in the Haskell stuff I have read).

Is this (Typeable) the right way to go? Is there any other solution?