diff --git a/kind-generics.cabal b/kind-generics.cabal
--- a/kind-generics.cabal
+++ b/kind-generics.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                kind-generics
-version:             0.1.0.0
+version:             0.1.1.0
 synopsis:            Generic programming in GHC style for arbitrary kinds and GADTs.
 description:         This package provides functionality to extend the data type generic programming functionality in GHC to classes of arbitrary kind, and constructors featuring constraints and existentials, as usually gound in GADTs.
 -- bug-reports:
diff --git a/src/Generics/Kind.hs b/src/Generics/Kind.hs
--- a/src/Generics/Kind.hs
+++ b/src/Generics/Kind.hs
@@ -22,7 +22,7 @@
 , module Data.PolyKinded.Atom
   -- * Generic representation types
 , (:+:)(..), (:*:)(..), U1(..), M1(..)
-, F(..), (:=>:)(..), E(..)
+, F(..), (:=>:)(..), E(..), ERefl(..)
   -- * Generic type classes
 , GenericK(..)
 , GenericF, fromF, toF
@@ -37,6 +37,7 @@
 import Data.Kind
 import GHC.Generics.Extra hiding ((:=>:))
 import qualified GHC.Generics.Extra as GG
+import Type.Reflection
 
 -- | Fields: used to represent each of the (visible) arguments to a constructor.
 -- Replaces the 'K1' type from "GHC.Generics". The type of the field is
@@ -69,6 +70,18 @@
 data E (f :: LoT (k -> d) -> *) (x :: LoT d) where
   E :: forall (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d)
      . f (t ':&&: x) -> E f x
+
+-- | Existentials with reflection: similar to 'E',
+--   but in addition we remember the type of the existential variable.
+--
+-- > data Exists where
+-- >  E :: Typeable t => t -> Exists
+-- >
+-- > instance GenericK Exists LoT0 where
+-- >   type RepK Exists = ERefl (F V0)
+data ERefl (f :: LoT (k -> d) -> *) (x :: LoT d) where
+  ERefl :: forall (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d)
+         . Typeable t => f (t ':&&: x) -> ERefl f x
 
 -- THE TYPE CLASS
 
diff --git a/src/Generics/Kind/Derive/Eq.hs b/src/Generics/Kind/Derive/Eq.hs
--- a/src/Generics/Kind/Derive/Eq.hs
+++ b/src/Generics/Kind/Derive/Eq.hs
@@ -14,6 +14,7 @@
 module Generics.Kind.Derive.Eq where
 
 import Generics.Kind
+import Type.Reflection
 
 geq' :: forall t f x. (GenericS t f x, GEq (RepK f) x)
      => t -> t -> Bool
@@ -42,7 +43,14 @@
 instance (Ty c tys => GEq f tys) => GEq (c :=>: f) tys where
   geq (C x) (C y) = geq x y
 
-{- We cannot check whether the two existentials have the same type
-instance (forall t. GEq f (t :&&: tys)) => GEq (E f) tys where
-  geq (E x) (E y) = geq x y
--}
+instance (forall t. (GEq f (t :&&: tys), Typeable t)) => GEq (E f) tys where
+  geq (E (x :: f (t1 :&&: tys))) (E (y :: f (t2 :&&: tys)))
+    = case eqTypeRep (typeRep @t1) (typeRep @t2) of
+        Nothing    -> False
+        Just HRefl -> geq x y
+
+instance (forall t. GEq f (t :&&: tys)) => GEq (ERefl f) tys where
+  geq (ERefl (x :: f (t1 :&&: tys))) (ERefl (y :: f (t2 :&&: tys)))
+    = case eqTypeRep (typeRep @t1) (typeRep @t2) of
+        Nothing    -> False
+        Just HRefl -> geq x y
diff --git a/src/Generics/Kind/Derive/Functor.hs b/src/Generics/Kind/Derive/Functor.hs
--- a/src/Generics/Kind/Derive/Functor.hs
+++ b/src/Generics/Kind/Derive/Functor.hs
@@ -58,6 +58,11 @@
          => GFunctor (E f) v as bs where
   gfmap v (E (x :: f (t ':&&: x))) = E (gfmap ((id :^: v) :: Mappings ('Co ': v) (t ':&&: as) (t ':&&: bs)) x)
 
+instance forall f v as bs.
+         (forall (t :: *). GFunctor f ('Co ': v) (t ':&&: as) (t ':&&: bs))
+         => GFunctor (ERefl f) v as bs where
+  gfmap v (ERefl (x :: f (t ':&&: x))) = ERefl (gfmap ((id :^: v) :: Mappings ('Co ': v) (t ':&&: as) (t ':&&: bs)) x)
+
 class GFunctorArg (t :: Atom d (*))
                   (v :: Variances) (intended :: Variance)
                   (as :: LoT d) (bs :: LoT d) where
diff --git a/src/Generics/Kind/Examples.hs b/src/Generics/Kind/Examples.hs
--- a/src/Generics/Kind/Examples.hs
+++ b/src/Generics/Kind/Examples.hs
@@ -6,10 +6,12 @@
 {-# language FlexibleInstances     #-}
 {-# language GADTs                 #-}
 {-# language DeriveGeneric         #-}
+{-# language QuantifiedConstraints #-}
 module Generics.Kind.Examples where
 
 import Data.PolyKinded.Functor
 import GHC.Generics (Generic)
+import Type.Reflection
 
 import Generics.Kind
 import Generics.Kind.Derive.Eq
@@ -62,3 +64,29 @@
 
 instance Show b => KFunctor WeirdTree '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0) where
   kfmap = kfmapDefault
+
+-- Hand-written instance with reflection
+
+data WeirdTreeR a where
+  WeirdBranchR :: WeirdTreeR a -> WeirdTreeR a -> WeirdTreeR a 
+  WeirdLeafR   :: (Show a, Typeable t, Eq t) => t -> a -> WeirdTreeR a
+
+instance Split (WeirdTreeR a) WeirdTreeR (a ':&&: 'LoT0)
+instance GenericK WeirdTreeR (a ':&&: 'LoT0) where
+  type RepK WeirdTreeR
+    = F (WeirdTreeR :$: V0) :*: F (WeirdTreeR :$: V0)
+      :+: ERefl ((Show :$: V1) :=>: ((Eq :$: V0) :=>: (F V0 :*: F V1)))
+
+  fromK (WeirdBranchR l r) = L1 $                 F l :*: F r
+  fromK (WeirdLeafR   a x) = R1 $ ERefl $ C $ C $ F a :*: F x
+
+  toK (L1 (F l :*: F r)) = WeirdBranchR l r
+  toK (R1 (ERefl (C (C (F a :*: F x))))) = WeirdLeafR a x
+
+instance (Eq a) => Eq (WeirdTreeR a) where
+  (==) = geq'
+
+{-
+instance Show b => KFunctor WeirdTreeR '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0) where
+  kfmap = kfmapDefault
+-}