diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2,6 +2,10 @@
 
 This package intends to follow the [Package Versioning Policy (PVP)](https://pvp.haskell.org/).
 
+## 0.2.0.0 March 2026
+
+- Simpler but more restrictive Enum1 class definition (one can always set `type Enum1Info f = f`, however, perhaps with a performance cost compared to the old definition).
+
 ## 0.1.0.0 May 2025
 
 - Initial release.
diff --git a/dependent-enummap.cabal b/dependent-enummap.cabal
--- a/dependent-enummap.cabal
+++ b/dependent-enummap.cabal
@@ -1,6 +1,6 @@
 cabal-version:   3.0
 name:            dependent-enummap
-version:         0.1.0.0
+version:         0.2.0.0
 synopsis:        A generalisation of EnumMap to dependent types
 description:
   A generalisation of EnumMap to dependent key and value types. The key type
@@ -9,7 +9,7 @@
   operations in coercions accompanied by some runtime type-consistency
   assertions.
 license:         BSD-3-Clause
-copyright:       (c) 2025 Tom Smeding, Mikolaj Konarski
+copyright:       (c) 2025-2026 Tom Smeding, Mikolaj Konarski
 author:          Tom Smeding, Mikolaj Konarski
 maintainer:      Tom Smeding <xhackage@tomsmeding.com>
 category:        Data, Dependent Types
@@ -22,13 +22,13 @@
     Data.Dependent.EnumMap.Strict.Internal
     -- Data.Dependent.EnumMap.Strict.Unsafe
   build-depends:
-    base >= 4.15 && < 4.22,
+    base >= 4.15 && < 4.23,
     containers >= 0.6 && < 0.9,
     dependent-sum >= 0.7 && < 0.8,
     some >= 1 && < 2,
   hs-source-dirs: src
   default-language: Haskell2010
-  ghc-options: -Wall -Wcompat -Widentities -Wredundant-constraints -Wunused-packages
+  ghc-options: -Wall -Wcompat -Widentities -Wredundant-constraints -Wunused-packages -Wpartial-fields -Wredundant-bang-patterns -Woperator-whitespace -Wredundant-strictness-flags
 
 
 test-suite test
diff --git a/src/Data/Dependent/EnumMap/Strict/Internal.hs b/src/Data/Dependent/EnumMap/Strict/Internal.hs
--- a/src/Data/Dependent/EnumMap/Strict/Internal.hs
+++ b/src/Data/Dependent/EnumMap/Strict/Internal.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE ImportQualifiedPost #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
@@ -7,16 +8,18 @@
 {-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 module Data.Dependent.EnumMap.Strict.Internal where
 
 import Prelude hiding (lookup, map)
 
 import Control.Exception
+import Control.Monad ((<$!>))
 import Data.Bifunctor (bimap, second)
 import Data.Coerce
 import Data.Dependent.Sum
-import qualified Data.Foldable as Foldable
-import qualified Data.IntMap.Strict as IM
+import Data.Foldable qualified as Foldable
+import Data.IntMap.Strict qualified as IM
 import Data.Kind (Type)
 import Data.Proxy
 import Data.Some
@@ -25,12 +28,13 @@
 import Unsafe.Coerce (unsafeCoerce)
 
 type KV :: forall kind. (kind -> Type) -> (kind -> Type) -> Type
-data KV k v = forall a. KV !(Enum1Info k) !(v a)
+data KV k v = forall a. KV !(Enum1Info k a) !(v a)
 
--- Invariant: the key-value pairs in a DEnumMap are type-consistent. That is to
--- say: they have the same type-index. Any other type equalities, like between
--- the key argument to 'lookup' and the key-value pairs in the map argument to
--- 'lookup', may /not/ hold, and should be type-checked as much as we're able.
+-- Invariant ensured by types: the key-value pairs in a DEnumMap
+-- are type-consistent. That is to say: they have the same type-index.
+-- Any other type equalities, like between the key argument to 'lookup'
+-- and the key-value pairs in the map argument to 'lookup',
+-- may /not/ hold, and should be runtime-type-checked as much as we're able.
 newtype DEnumMap k v = DEnumMap (IM.IntMap (KV k v))
 
 instance (Enum1 k, forall a. Show (k a), forall a. Show (v a))
@@ -59,21 +63,27 @@
 --
 -- __Note__: The methods on 'DEnumMap' attempt to check these laws using
 -- 'assert' assertions (which are by default __disabled__ when optimisations
--- are on!), but full consistency cannot always be checked; if you break these
--- laws in a sufficiently clever way, the internals of 'DEnumMap' may
--- 'unsafeCoerce' unequal things and engage nasal demons, including crashes and
--- worse.
+-- are on!), but full consistency cannot always be checked;
+-- __if you break these laws in a sufficiently clever way, the internals of 'DEnumMap' may 'unsafeCoerce' unequal things and engage nasal demons, including crashes and worse.__
+--
+-- To enable assertions in optimized builds, e.g., for test runs
+-- using optimized code, add the following to the cabal.project.local
+-- file of your project:
+--
+-- > package dependent-enummap
+-- >   ghc-options: -fno-ignore-asserts
+
 class Enum1 f where
-  type Enum1Info f
-  fromEnum1 :: f a -> (Int, Enum1Info f)
-  toEnum1 :: Int -> Enum1Info f -> Some f
+  type Enum1Info f :: kind -> Type
+  fromEnum1 :: f a -> (Int, Enum1Info f a)
+  toEnum1 :: Int -> Enum1Info f a -> f a
 
 dSumToKV :: Enum1 k => DSum k v -> (Int, KV k v)
 dSumToKV (k :=> v) = let (i, inf) = fromEnum1 k in (i, KV inf v)
 
 -- | Assumes that the input was obtained via 'fromEnum1'.
 kVToDSum :: Enum1 k => (Int, KV k v) -> DSum k v
-kVToDSum (i, KV inf v) = case toEnum1 i inf of Some k -> k :=> coe1 v
+kVToDSum (i, KV inf v) = toEnum1 i inf :=> v
 
 -- * Construction
 
@@ -99,18 +109,19 @@
 fromListWith f (l :: [DSum k v]) =
   DEnumMap (IM.fromListWithKey
              (\i (KV inf1 v1) (KV inf2 v2) ->
-                typeCheck2 (Proxy @k) i inf1 inf2 $
-                  KV inf1 (f v1 (coe1 v2)))
+                case typeCheck2 (Proxy @k) i inf1 inf2 of
+                  Refl -> KV inf1 (f v1 v2))
              (dSumToKV <$> l))
 
-fromListWithKey :: (Enum1 k, TestEquality k)
+fromListWithKey :: forall k v. (Enum1 k, TestEquality k)
                 => (forall a. k a -> v a -> v a -> v a)
                 -> [DSum k v] -> DEnumMap k v
 fromListWithKey f l =
   DEnumMap (IM.fromListWithKey
              (\i (KV inf1 v1) (KV inf2 v2) ->
-                case toEnum1 i inf1 of
-                  Some k1 -> typeCheck1 k1 i inf2 $ KV inf1 (f k1 (coe1 v1) (coe1 v2)))
+                let k1 = toEnum1 @k i inf1
+                in case typeCheck1 k1 i inf2 of
+                     Refl -> KV inf1 (f k1 v1 v2))
              (dSumToKV <$> l))
 
 -- ** From Ascending Lists
@@ -124,18 +135,19 @@
 fromAscListWith f (l :: [DSum k v]) =
   DEnumMap (IM.fromAscListWithKey
              (\i (KV inf1 v1) (KV inf2 v2) ->
-               typeCheck2 (Proxy @k) i inf1 inf2 $
-                 KV inf1 (f v1 (coe1 v2)))
+               case typeCheck2 (Proxy @k) i inf1 inf2 of
+                 Refl -> KV inf1 (f v1 v2))
              (dSumToKV <$> l))
 
-fromAscListWithKey :: (Enum1 k, TestEquality k)
+fromAscListWithKey :: forall k v. (Enum1 k, TestEquality k)
                    => (forall a. k a -> v a -> v a -> v a)
                    -> [DSum k v] -> DEnumMap k v
 fromAscListWithKey f l =
   DEnumMap (IM.fromAscListWithKey
              (\i (KV inf1 v1) (KV inf2 v2) ->
-               case toEnum1 i inf1 of
-                 Some k1 -> typeCheck1 k1 i inf2 $ KV inf1 (f k1 (coe1 v1) (coe1 v2)))
+               let k1 = toEnum1 @k i inf1
+               in case typeCheck1 k1 i inf2 of
+                    Refl -> KV inf1 (f k1 v1 v2))
              (dSumToKV <$> l))
 
 fromDistinctAscList :: Enum1 k => [DSum k v] -> DEnumMap k v
@@ -159,7 +171,8 @@
 insertWithKey f k v (DEnumMap m) =
   let (i, inf) = fromEnum1 k
   in DEnumMap (IM.insertWith
-                (\_ (KV inf' v2) -> typeCheck1 k i inf' $ KV inf (f k v (coe1 v2)))
+                (\_ (KV inf' v2) -> case typeCheck1 k i inf' of
+                                      Refl -> KV inf (f k v v2))
                 i (KV inf v) m)
 
 insertLookupWithKey :: (Enum1 k, TestEquality k)
@@ -169,7 +182,8 @@
   let (i, inf) = fromEnum1 k
       (!mx, !m') =
         IM.insertLookupWithKey
-          (\_ _ (KV inf' v2) -> typeCheck1 k i inf' $ KV inf (f k v (coe1 v2)))
+          (\_ _ (KV inf' v2) -> case typeCheck1 k i inf' of
+                                  Refl -> KV inf (f k v v2))
           i (KV inf v) m
      -- Note: type checking unnecessary here, because by the BangPatterns,
      -- evaluating mx evaluates dmap, and the IntMap is strict, so the lambda
@@ -177,7 +191,7 @@
      -- Second note: the BangPatterns don't do anything operationally because
      -- with the current implementation of IM.insertLookupWithKey, the pair
      -- components are already strict.
-  in ((\(KV _ v2) -> coe1 v2) <$> mx, DEnumMap m')
+  in ((\(KV _ v2) -> coe1 v2) <$!> mx, DEnumMap m')
 
 -- * Deletion\/Update
 
@@ -190,7 +204,9 @@
 adjustWithKey :: (Enum1 k, TestEquality k) => (k a -> v a -> v a) -> k a -> DEnumMap k v -> DEnumMap k v
 adjustWithKey f k (DEnumMap m) =
   let (i, _) = fromEnum1 k
-  in DEnumMap (IM.adjust (\(KV inf v) -> typeCheck1 k i inf $ KV inf (f k (coe1 v))) i m)
+  in DEnumMap (IM.adjust (\(KV inf v) -> case typeCheck1 k i inf of
+                                           Refl -> KV inf (f k v))
+                         i m)
 
 update :: (Enum1 k, TestEquality k) => (v a -> Maybe (v a)) -> k a -> DEnumMap k v -> DEnumMap k v
 update = updateWithKey . const
@@ -199,7 +215,9 @@
               => (k a -> v a -> Maybe (v a)) -> k a -> DEnumMap k v -> DEnumMap k v
 updateWithKey f k (DEnumMap m) =
   let (i, _) = fromEnum1 k
-  in DEnumMap (IM.update (\(KV inf v) -> typeCheck1 k i inf $ KV inf <$> f k (coe1 v)) i m)
+  in DEnumMap (IM.update (\(KV inf v) -> case typeCheck1 k i inf of
+                                           Refl -> KV inf <$> f k v)
+                         i m)
 
 updateLookupWithKey :: (Enum1 k, TestEquality k)
                     => (k a -> v a -> Maybe (v a)) -> k a -> DEnumMap k v -> (Maybe (v a), DEnumMap k v)
@@ -207,10 +225,11 @@
   let (i, _) = fromEnum1 k
       (!mx, !m') =
         IM.updateLookupWithKey
-          (\_ (KV inf v) -> typeCheck1 k i inf $ KV inf <$> f k (coe1 v))
+          (\_ (KV inf v) -> case typeCheck1 k i inf of
+                              Refl -> KV inf <$> f k v)
           i m
      -- Note: type checking unnecessary here for the same reason as insertLookupWithKey
-  in ((\(KV _ v2) -> coe1 v2) <$> mx, DEnumMap m')
+  in ((\(KV _ v2) -> coe1 v2) <$!> mx, DEnumMap m')
 
 alter :: forall k v a. (Enum1 k, TestEquality k)
       => (Maybe (v a) -> Maybe (v a)) -> k a -> DEnumMap k v -> DEnumMap k v
@@ -220,7 +239,8 @@
 
     f' :: Maybe (KV k v) -> Maybe (KV k v)
     f' Nothing = KV inf <$> f Nothing
-    f' (Just (KV inf' v)) = typeCheck1 k i inf' $ KV inf <$> f (Just (coe1 v))
+    f' (Just (KV inf' v)) = case typeCheck1 k i inf' of
+                              Refl -> KV inf <$> f (Just v)
 
 alterF :: forall k v a f. (Functor f, Enum1 k, TestEquality k)
        => (Maybe (v a) -> f (Maybe (v a))) -> k a -> DEnumMap k v -> f (DEnumMap k v)
@@ -230,15 +250,19 @@
 
     f' :: Maybe (KV k v) -> f (Maybe (KV k v))
     f' Nothing = fmap (KV inf) <$> f Nothing
-    f' (Just (KV inf' v)) = typeCheck1 k i inf' $ fmap (KV inf) <$> f (Just (coe1 v))
+    f' (Just (KV inf' v)) = case typeCheck1 k i inf' of
+                              Refl -> fmap (KV inf) <$> f (Just v)
 
 -- * Query
 -- ** Lookup
 
 lookup :: (Enum1 k, TestEquality k) => k a -> DEnumMap k v -> Maybe (v a)
+{-# INLINEABLE lookup #-}
 lookup k (DEnumMap m) =
   let (i, _) = fromEnum1 k
-  in (\(KV inf v) -> typeCheck1 k i inf $ coe1 v) <$> IM.lookup i m
+  in (\(KV inf v) -> case typeCheck1 k i inf of
+                       Refl -> v)
+     <$!> IM.lookup i m
 
 (!?) :: (Enum1 k, TestEquality k) => DEnumMap k v -> k a -> Maybe (v a)
 (!?) m k = lookup k m
@@ -247,7 +271,8 @@
 findWithDefault def k (DEnumMap m) =
   let (i, _) = fromEnum1 k
   in case IM.findWithDefault (KV undefined def) i m of
-       KV inf' v -> typeCheck1 k i inf' $ coe1 v
+       KV inf' v -> case typeCheck1 k i inf' of
+                      Refl -> v
 
 find :: (Enum1 k, TestEquality k) => k a -> DEnumMap k v -> v a
 find k = findWithDefault (error ("Data.Dependent.EnumMap.!: key " ++ show (fst (fromEnum1 k)) ++ " is not an element of the map")) k
@@ -262,10 +287,10 @@
 notMember k m = not $ member k m
 
 lookupLT, lookupGT, lookupLE, lookupGE :: Enum1 k => k a -> DEnumMap k v -> Maybe (DSum k v)
-lookupLT k (DEnumMap m) = let (i, _) = fromEnum1 k in kVToDSum <$> IM.lookupLT i m
-lookupGT k (DEnumMap m) = let (i, _) = fromEnum1 k in kVToDSum <$> IM.lookupGT i m
-lookupLE k (DEnumMap m) = let (i, _) = fromEnum1 k in kVToDSum <$> IM.lookupLE i m
-lookupGE k (DEnumMap m) = let (i, _) = fromEnum1 k in kVToDSum <$> IM.lookupGE i m
+lookupLT k (DEnumMap m) = let (i, _) = fromEnum1 k in kVToDSum <$!> IM.lookupLT i m
+lookupGT k (DEnumMap m) = let (i, _) = fromEnum1 k in kVToDSum <$!> IM.lookupGT i m
+lookupLE k (DEnumMap m) = let (i, _) = fromEnum1 k in kVToDSum <$!> IM.lookupLE i m
+lookupGE k (DEnumMap m) = let (i, _) = fromEnum1 k in kVToDSum <$!> IM.lookupGE i m
 
 -- ** Size
 
@@ -287,15 +312,18 @@
 unionWith f (DEnumMap m1 :: DEnumMap k v) (DEnumMap m2) = DEnumMap (IM.unionWithKey f' m1 m2)
   where
     f' :: Int -> KV k v -> KV k v -> KV k v
-    f' i (KV inf1 v1) (KV inf2 v2) = typeCheck2 (Proxy @k) i inf1 inf2 $ KV inf1 (f v1 (coe1 v2))
+    f' i (KV inf1 v1) (KV inf2 v2) = case typeCheck2 (Proxy @k) i inf1 inf2 of
+                                       Refl -> KV inf1 (f v1 v2)
 
-unionWithKey :: (Enum1 k, TestEquality k)
+unionWithKey :: forall k v. (Enum1 k, TestEquality k)
              => (forall a. k a -> v a -> v a -> v a) -> DEnumMap k v -> DEnumMap k v -> DEnumMap k v
 unionWithKey f (DEnumMap m1 :: DEnumMap k v) (DEnumMap m2) = DEnumMap (IM.unionWithKey f' m1 m2)
   where
     f' :: Int -> KV k v -> KV k v -> KV k v
-    f' i (KV inf1 v1) (KV inf2 v2) = case toEnum1 i inf1 of
-      Some k1 -> typeCheck1 k1 i inf2 $ KV inf1 (f k1 (coe1 v1) (coe1 v2))
+    f' i (KV inf1 v1) (KV inf2 v2) =
+      let k1 = toEnum1 @k i inf1
+      in case typeCheck1 k1 i inf2 of
+           Refl -> KV inf1 (f k1 v1 v2)
 
 unions :: (Foldable f, Enum1 k, TestEquality k) => f (DEnumMap k v) -> DEnumMap k v
 unions = Foldable.foldl' union empty
@@ -318,15 +346,18 @@
   where
     f' :: Int -> KV k v1 -> KV k v2 -> Maybe (KV k v1)
     f' i (KV inf1 v1) (KV inf2 v2) =
-      typeCheck2 (Proxy @k) i inf1 inf2 $ KV inf1 <$> f (coe1 v1) (coe1 v2)
+      case typeCheck2 (Proxy @k) i inf1 inf2 of
+        Refl -> KV inf1 <$> f v1 v2
 
 differenceWithKey :: forall k v1 v2. (Enum1 k, TestEquality k)
                   => (forall a. k a -> v1 a -> v2 a -> Maybe (v1 a)) -> DEnumMap k v1 -> DEnumMap k v2 -> DEnumMap k v1
 differenceWithKey f (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.differenceWithKey f' m1 m2)
   where
     f' :: Int -> KV k v1 -> KV k v2 -> Maybe (KV k v1)
-    f' i (KV inf1 v1) (KV inf2 v2) = case toEnum1 i inf1 of
-      Some k1 -> typeCheck1 k1 i inf2 $ KV inf1 <$> f k1 (coe1 v1) (coe1 v2)
+    f' i (KV inf1 v1) (KV inf2 v2) =
+      let k1 = toEnum1 @k i inf1
+      in case typeCheck1 k1 i inf2 of
+           Refl -> KV inf1 <$> f k1 v1 v2
 
 -- | Because the underlying maps are keyed on integers, it is possible to
 -- subtract a map from another even if the key types differ. This function
@@ -343,8 +374,10 @@
 differenceWithKey' f (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.differenceWithKey f' m1 m2)
   where
     f' :: Int -> KV k1 v1 -> KV k2 v2 -> Maybe (KV k1 v1)
-    f' i (KV inf1 v1) (KV inf2 v2) = case (toEnum1 i inf1, toEnum1 i inf2) of
-      (Some k1, Some k2) -> KV inf1 <$> f k1 (coe1 v1) k2 (coe1 v2)
+    f' i (KV inf1 v1) (KV inf2 v2) =
+      let k1 = toEnum1 i inf1
+          k2 = toEnum1 i inf2
+      in KV inf1 <$> f k1 v1 k2 v2
 
 -- ** Intersection
 
@@ -357,15 +390,18 @@
   where
     f' :: Int -> KV k v1 -> KV k v2 -> KV k v3
     f' i (KV inf1 v1) (KV inf2 v2) =
-      typeCheck2 (Proxy @k) i inf1 inf2 $ KV inf1 $ f (coe1 v1) (coe1 v2)
+      case typeCheck2 (Proxy @k) i inf1 inf2 of
+        Refl -> KV inf1 $ f v1 v2
 
 intersectionWithKey :: forall k v1 v2 v3. (Enum1 k, TestEquality k)
                     => (forall a. k a -> v1 a -> v2 a -> v3 a) -> DEnumMap k v1 -> DEnumMap k v2 -> DEnumMap k v3
 intersectionWithKey f (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.intersectionWithKey f' m1 m2)
   where
     f' :: Int -> KV k v1 -> KV k v2 -> KV k v3
-    f' i (KV inf1 v1) (KV inf2 v2) = case toEnum1 i inf1 of
-      Some k1 -> typeCheck1 k1 i inf2 $ KV inf1 $ f k1 (coe1 v1) (coe1 v2)
+    f' i (KV inf1 v1) (KV inf2 v2) =
+      let k1 = toEnum1 @k i inf1
+      in case typeCheck1 k1 i inf2 of
+           Refl -> KV inf1 $ f k1 v1 v2
 
 -- | Generalises 'intersectionWithKey' in the same way as 'differenceWithKey''
 -- generalises 'differenceWithKey'.
@@ -375,8 +411,10 @@
 intersectionWithKey' f (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.intersectionWithKey f' m1 m2)
   where
     f' :: Int -> KV k1 v1 -> KV k2 v2 -> KV k1 v3
-    f' i (KV inf1 v1) (KV inf2 v2) = case (toEnum1 i inf1, toEnum1 i inf2) of
-      (Some k1, Some k2) -> KV inf1 $ f k1 (coe1 v1) k2 (coe1 v2)
+    f' i (KV inf1 v1) (KV inf2 v2) =
+      let k1 = toEnum1 i inf1
+          k2 = toEnum1 i inf2
+      in KV inf1 $ f k1 v1 k2 v2
 
 -- ** Disjoint
 
@@ -400,8 +438,10 @@
   DEnumMap (IM.mergeWithKey f' (coerce g1) (coerce g2) m1 m2)
   where
     f' :: Int -> KV k v1 -> KV k v2 -> Maybe (KV k v3)
-    f' i (KV inf1 v1) (KV inf2 v2) = case toEnum1 i inf1 of
-      Some k1 -> typeCheck1 k1 i inf2 $ KV inf1 <$> f k1 (coe1 v1) (coe1 v2)
+    f' i (KV inf1 v1) (KV inf2 v2) =
+      let k1 = toEnum1 @k i inf1
+      in case typeCheck1 k1 i inf2 of
+           Refl -> KV inf1 <$> f k1 v1 v2
 
 -- * Traversal
 -- ** Map
@@ -411,28 +451,43 @@
 
 mapWithKey :: Enum1 k => (forall a. k a -> v1 a -> v2 a) -> DEnumMap k v1 -> DEnumMap k v2
 mapWithKey f (DEnumMap m) =
-  DEnumMap (IM.mapWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> KV inf $ f k (coe1 v)) m)
+  DEnumMap (IM.mapWithKey (\i (KV inf v) ->
+                             let k = toEnum1 i inf
+                             in KV inf $ f k v)
+                          m)
 
 traverseWithKey :: (Applicative f, Enum1 k)
                 => (forall a. k a -> v1 a -> f (v2 a)) -> DEnumMap k v1 -> f (DEnumMap k v2)
 traverseWithKey f (DEnumMap m) =
-  DEnumMap <$> IM.traverseWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> KV inf <$> f k (coe1 v)) m
+  DEnumMap <$> IM.traverseWithKey (\i (KV inf v) ->
+                                     let k = toEnum1 i inf
+                                     in KV inf <$> f k v)
+                                  m
 
 traverseMaybeWithKey :: (Applicative f, Enum1 k)
                      => (forall a. k a -> v1 a -> f (Maybe (v2 a))) -> DEnumMap k v1 -> f (DEnumMap k v2)
 traverseMaybeWithKey f (DEnumMap m) =
-  DEnumMap <$> IM.traverseMaybeWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> fmap (KV inf) <$> f k (coe1 v)) m
+  DEnumMap <$> IM.traverseMaybeWithKey (\i (KV inf v) ->
+                                          let k = toEnum1 i inf
+                                          in fmap (KV inf) <$> f k v)
+                                       m
 
 mapAccum :: Enum1 k => (forall a. acc -> v1 a -> (acc, v2 a)) -> acc -> DEnumMap k v1 -> (acc, DEnumMap k v2)
 mapAccum f = mapAccumWithKey (\x _ y -> f x y)
 
 mapAccumWithKey :: Enum1 k => (forall a. acc -> k a -> v1 a -> (acc, v2 a)) -> acc -> DEnumMap k v1 -> (acc, DEnumMap k v2)
 mapAccumWithKey f acc0 (DEnumMap m) =
-  second DEnumMap $ IM.mapAccumWithKey (\acc i (KV inf v) -> case toEnum1 i inf of Some k -> second (KV inf) $ f acc k (coe1 v)) acc0 m
+  second DEnumMap $ IM.mapAccumWithKey (\acc i (KV inf v) ->
+                                          let k = toEnum1 i inf
+                                          in second (KV inf) $ f acc k v)
+                                       acc0 m
 
 mapAccumRWithKey :: Enum1 k => (forall a. acc -> k a -> v1 a -> (acc, v2 a)) -> acc -> DEnumMap k v1 -> (acc, DEnumMap k v2)
 mapAccumRWithKey f acc0 (DEnumMap m) =
-  second DEnumMap $ IM.mapAccumRWithKey (\acc i (KV inf v) -> case toEnum1 i inf of Some k -> second (KV inf) $ f acc k (coe1 v)) acc0 m
+  second DEnumMap $ IM.mapAccumRWithKey (\acc i (KV inf v) ->
+                                           let k = toEnum1 i inf
+                                           in second (KV inf) $ f acc k v)
+                                        acc0 m
 
 -- TODO: These are hard. Probably we can't avoid using a fold, analogously as in IntMap.
 -- mapKeys
@@ -449,15 +504,24 @@
 
 foldrWithKey :: Enum1 k => (forall a. k a -> v a -> acc -> acc) -> acc -> DEnumMap k v -> acc
 foldrWithKey f acc0 (DEnumMap m) =
-  IM.foldrWithKey (\i (KV inf v) acc -> case toEnum1 i inf of Some k -> f k (coe1 v) acc) acc0 m
+  IM.foldrWithKey (\i (KV inf v) acc ->
+                     let k = toEnum1 i inf
+                     in f k v acc)
+                  acc0 m
 
 foldlWithKey :: Enum1 k => (forall a. acc -> k a -> v a -> acc) -> acc -> DEnumMap k v -> acc
 foldlWithKey f acc0 (DEnumMap m) =
-  IM.foldlWithKey (\acc i (KV inf v) -> case toEnum1 i inf of Some k -> f acc k (coe1 v)) acc0 m
+  IM.foldlWithKey (\acc i (KV inf v) ->
+                     let k = toEnum1 i inf
+                     in f acc k v)
+                  acc0 m
 
 foldMapWithKey :: (Monoid m, Enum1 k) => (forall a. k a -> v a -> m) -> DEnumMap k v -> m
 foldMapWithKey f (DEnumMap m) =
-  IM.foldMapWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> f k (coe1 v)) m
+  IM.foldMapWithKey (\i (KV inf v) ->
+                       let k = toEnum1 i inf
+                       in f k v)
+                    m
 
 -- ** Strict folds
 
@@ -469,11 +533,17 @@
 
 foldrWithKey' :: Enum1 k => (forall a. k a -> v a -> acc -> acc) -> acc -> DEnumMap k v -> acc
 foldrWithKey' f acc0 (DEnumMap m) =
-  IM.foldrWithKey' (\i (KV inf v) acc -> case toEnum1 i inf of Some k -> f k (coe1 v) acc) acc0 m
+  IM.foldrWithKey' (\i (KV inf v) acc ->
+                      let k = toEnum1 i inf
+                      in f k v acc)
+                   acc0 m
 
 foldlWithKey' :: Enum1 k => (forall a. acc -> k a -> v a -> acc) -> acc -> DEnumMap k v -> acc
 foldlWithKey' f acc0 (DEnumMap m) =
-  IM.foldlWithKey' (\acc i (KV inf v) -> case toEnum1 i inf of Some k -> f acc k (coe1 v)) acc0 m
+  IM.foldlWithKey' (\acc i (KV inf v) ->
+                      let k = toEnum1 i inf
+                      in f acc k v)
+                   acc0 m
 
 -- * Conversion
 
@@ -481,7 +551,7 @@
 elems (DEnumMap m) = (\(KV _ v) -> Some v) <$> IM.elems m
 
 keys :: Enum1 k => DEnumMap k v -> [Some k]
-keys (DEnumMap m) = (\(k, KV inf _) -> toEnum1 k inf) <$> IM.assocs m
+keys (DEnumMap m) = (\(k, KV inf _) -> Some (toEnum1 k inf)) <$> IM.assocs m
 
 assocs :: Enum1 k => DEnumMap k v -> [DSum k v]
 assocs (DEnumMap m) = kVToDSum <$> IM.assocs m
@@ -509,7 +579,10 @@
 
 filterWithKey :: Enum1 k => (forall a. k a -> v a -> Bool) -> DEnumMap k v -> DEnumMap k v
 filterWithKey f (DEnumMap m) =
-  DEnumMap (IM.filterWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> f k (coe1 v)) m)
+  DEnumMap (IM.filterWithKey (\i (KV inf v) ->
+                                let k = toEnum1 i inf
+                                in f k v)
+                             m)
 
 -- TODO: Wait for DEnumSet.
 -- restrictKeys
@@ -521,25 +594,38 @@
 
 partitionWithKey :: Enum1 k => (forall a. k a -> v a -> Bool) -> DEnumMap k v -> (DEnumMap k v, DEnumMap k v)
 partitionWithKey f (DEnumMap m) =
-  bimap DEnumMap DEnumMap (IM.partitionWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> f k (coe1 v)) m)
+  bimap DEnumMap DEnumMap (IM.partitionWithKey (\i (KV inf v) ->
+                                                  let k = toEnum1 i inf
+                                                  in f k v)
+                                               m)
 
 -- | \(O(\min(n,W)^2)\). Because of the lack of a @takeWhileAntitoneWithValue@
--- operation on 'IntMap', this function performs additional lookups to
+-- operation on 'Data.IntMap.Strict.IntMap', this function performs additional lookups to
 -- reconstruct the full keys to pass to the predicate, resulting in a somewhat
--- worse complexity than 'IM.takeWhileAntitone'.
+-- worse complexity than 'Data.IntMap.Strict.takeWhileAntitone'.
 takeWhileAntitone :: Enum1 k => (forall a. k a -> Bool) -> DEnumMap k v -> DEnumMap k v
 takeWhileAntitone f (DEnumMap m) =
-  DEnumMap (IM.takeWhileAntitone (\i -> case m IM.! i of KV inf _ -> case toEnum1 i inf of Some k -> f k) m)
+  DEnumMap (IM.takeWhileAntitone (\i -> case m IM.! i of
+                                          KV inf _ -> let k = toEnum1 i inf
+                                                      in f k)
+                                 m)
 
 -- | \(O(\min(n,W)^2)\). See 'takeWhileAntitone'.
 dropWhileAntitone :: Enum1 k => (forall a. k a -> Bool) -> DEnumMap k v -> DEnumMap k v
 dropWhileAntitone f (DEnumMap m) =
-  DEnumMap (IM.dropWhileAntitone (\i -> case m IM.! i of KV inf _ -> case toEnum1 i inf of Some k -> f k) m)
+  DEnumMap (IM.dropWhileAntitone (\i -> case m IM.! i of
+                                          KV inf _ -> let k = toEnum1 i inf
+                                                      in f k)
+                                 m)
 
 -- | \(O(\min(n,W)^2)\). See 'takeWhileAntitone'.
 spanAntitone :: Enum1 k => (forall a. k a -> Bool) -> DEnumMap k v -> (DEnumMap k v, DEnumMap k v)
 spanAntitone f (DEnumMap m) =
-  bimap DEnumMap DEnumMap (IM.spanAntitone (\i -> case m IM.! i of KV inf _ -> case toEnum1 i inf of Some k -> f k) m)
+  bimap DEnumMap DEnumMap
+        (IM.spanAntitone (\i -> case m IM.! i of
+                                  KV inf _ -> let k = toEnum1 i inf
+                                              in f k)
+                         m)
 
 mapMaybe :: Enum1 k => (forall a. v1 a -> Maybe (v2 a)) -> DEnumMap k v1 -> DEnumMap k v2
 mapMaybe f = mapMaybeWithKey (const f)
@@ -547,7 +633,10 @@
 mapMaybeWithKey :: Enum1 k
                 => (forall a. k a -> v1 a -> Maybe (v2 a)) -> DEnumMap k v1 -> DEnumMap k v2
 mapMaybeWithKey f (DEnumMap m) =
-  DEnumMap (IM.mapMaybeWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> KV inf <$> f k (coe1 v)) m)
+  DEnumMap (IM.mapMaybeWithKey (\i (KV inf v) ->
+                                  let k = toEnum1 i inf
+                                  in KV inf <$> f k v)
+                               m)
 
 mapEither :: Enum1 k
           => (forall a. v1 a -> Either (v2 a) (v3 a)) -> DEnumMap k v1 -> (DEnumMap k v2, DEnumMap k v3)
@@ -556,16 +645,19 @@
 mapEitherWithKey :: Enum1 k
                  => (forall a. k a -> v1 a -> Either (v2 a) (v3 a)) -> DEnumMap k v1 -> (DEnumMap k v2, DEnumMap k v3)
 mapEitherWithKey f (DEnumMap m) =
-  bimap DEnumMap DEnumMap (IM.mapEitherWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> bimap (KV inf) (KV inf) $ f k (coe1 v)) m)
+  bimap DEnumMap DEnumMap (IM.mapEitherWithKey (\i (KV inf v) ->
+                                                  let k = toEnum1 i inf
+                                                  in bimap (KV inf) (KV inf) $ f k v)
+                                               m)
 
 split :: Enum1 k => k a -> DEnumMap k v -> (DEnumMap k v, DEnumMap k v)
 split k (DEnumMap m) = bimap DEnumMap DEnumMap (IM.split (fst $ fromEnum1 k) m)
 
 splitLookup :: Enum1 k => k a -> DEnumMap k v -> (DEnumMap k v, Maybe (v a), DEnumMap k v)
 splitLookup k (DEnumMap m) =
-  let (m1, mkv, m2) = IM.splitLookup (fst $ fromEnum1 k) m
+  let (!m1, !mkv, !m2) = IM.splitLookup (fst $ fromEnum1 k) m
      -- Note: this coe1 is fine because of the invariant on DEnumMap.
-  in (DEnumMap m1, (\(KV _ v) -> coe1 v) <$> mkv, DEnumMap m2)
+  in (DEnumMap m1, (\(KV _ v) -> coe1 v) <$!> mkv, DEnumMap m2)
 
 splitRoot :: DEnumMap k v -> [DEnumMap k v]
 splitRoot (DEnumMap m) = DEnumMap <$> IM.splitRoot m
@@ -590,10 +682,10 @@
 -- * Min\/Max
 
 lookupMin :: Enum1 k => DEnumMap k v -> Maybe (DSum k v)
-lookupMin (DEnumMap m) = kVToDSum <$> IM.lookupMin m
+lookupMin (DEnumMap m) = kVToDSum <$!> IM.lookupMin m
 
 lookupMax :: Enum1 k => DEnumMap k v -> Maybe (DSum k v)
-lookupMax (DEnumMap m) = kVToDSum <$> IM.lookupMax m
+lookupMax (DEnumMap m) = kVToDSum <$!> IM.lookupMax m
 
 findMin :: Enum1 k => DEnumMap k v -> DSum k v
 findMin (DEnumMap m) = kVToDSum $ IM.findMin m
@@ -608,36 +700,42 @@
 deleteMax (DEnumMap m) = DEnumMap $ IM.deleteMax m
 
 deleteFindMin :: Enum1 k => DEnumMap k v -> (DSum k v, DEnumMap k v)
-deleteFindMin (DEnumMap m) = bimap kVToDSum DEnumMap $ IM.deleteFindMin m
+deleteFindMin (DEnumMap m) = bimap' kVToDSum DEnumMap $ IM.deleteFindMin m
 
 deleteFindMax :: Enum1 k => DEnumMap k v -> (DSum k v, DEnumMap k v)
-deleteFindMax (DEnumMap m) = bimap kVToDSum DEnumMap $ IM.deleteFindMax m
+deleteFindMax (DEnumMap m) = bimap' kVToDSum DEnumMap $ IM.deleteFindMax m
 
 updateMin :: Enum1 k => (forall a. v a -> Maybe (v a)) -> DEnumMap k v -> DEnumMap k v
 updateMin f = updateMinWithKey (const f)
 
 updateMinWithKey :: Enum1 k => (forall a. k a -> v a -> Maybe (v a)) -> DEnumMap k v -> DEnumMap k v
 updateMinWithKey f (DEnumMap m) =
-  DEnumMap (IM.updateMinWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> KV inf <$> f k (coe1 v)) m)
+  DEnumMap (IM.updateMinWithKey (\i (KV inf v) ->
+                                   let k = toEnum1 i inf
+                                   in KV inf <$> f k v)
+                                m)
 
 updateMax :: Enum1 k => (forall a. v a -> Maybe (v a)) -> DEnumMap k v -> DEnumMap k v
 updateMax f = updateMaxWithKey (const f)
 
 updateMaxWithKey :: Enum1 k => (forall a. k a -> v a -> Maybe (v a)) -> DEnumMap k v -> DEnumMap k v
 updateMaxWithKey f (DEnumMap m) =
-  DEnumMap (IM.updateMaxWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> KV inf <$> f k (coe1 v)) m)
+  DEnumMap (IM.updateMaxWithKey (\i (KV inf v) ->
+                                   let k = toEnum1 i inf
+                                   in KV inf <$> f k v)
+                                m)
 
 minView :: DEnumMap k v -> Maybe (v a, DEnumMap k v)
-minView (DEnumMap m) = bimap (\(KV _ v) -> coe1 v) DEnumMap <$> IM.minView m
+minView (DEnumMap m) = bimap' (\(KV _ v) -> coe1 v) DEnumMap <$!> IM.minView m
 
 maxView :: DEnumMap k v -> Maybe (v a, DEnumMap k v)
-maxView (DEnumMap m) = bimap (\(KV _ v) -> coe1 v) DEnumMap <$> IM.maxView m
+maxView (DEnumMap m) = bimap' (\(KV _ v) -> coe1 v) DEnumMap <$!> IM.maxView m
 
 minViewWithKey :: Enum1 k => DEnumMap k v -> Maybe (DSum k v, DEnumMap k v)
-minViewWithKey (DEnumMap m) = bimap kVToDSum DEnumMap <$> IM.minViewWithKey m
+minViewWithKey (DEnumMap m) = bimap' kVToDSum DEnumMap <$!> IM.minViewWithKey m
 
 maxViewWithKey :: Enum1 k => DEnumMap k v -> Maybe (DSum k v, DEnumMap k v)
-maxViewWithKey (DEnumMap m) = bimap kVToDSum DEnumMap <$> IM.maxViewWithKey m
+maxViewWithKey (DEnumMap m) = bimap' kVToDSum DEnumMap <$!> IM.maxViewWithKey m
 
 
 -- * Helpers
@@ -645,21 +743,37 @@
 coe1 :: v a -> v b
 coe1 = unsafeCoerce
 
-typeCheck1 :: (Enum1 k, TestEquality k)
-           => k a -> Int -> Enum1Info k -> r -> r
-typeCheck1 k1 i inf2 x =
-  assert (case toEnum1 i inf2 of { Some k2 ->
-          case testEquality k1 k2 of
-            Just Refl -> True
-            Nothing -> False })
-         x
+typeCheck1 :: forall k a b. (Enum1 k, TestEquality k)
+           => k a -> Int -> Enum1Info k b -> k a :~: k b
+typeCheck1 k1 i inf2 =
+  let ret :: k a :~: k b
+      ret = unsafeCoerce Refl
+  in assert (let k2 = toEnum1 i inf2
+             in case testEquality k1 k2 of
+                  Just r -> justifies r ret True
+                  Nothing -> False)
+            ret
+  where
+    justifies :: a :~: b -> k a :~: k b -> r -> r
+    justifies Refl _ x = x
 
-typeCheck2 :: forall k proxy r. (Enum1 k, TestEquality k)
-           => proxy k -> Int -> Enum1Info k -> Enum1Info k -> r -> r
-typeCheck2 _ i inf1 inf2 x =
-  assert (case toEnum1 @k i inf1 of { Some k1 ->
-          case toEnum1 i inf2 of { Some k2 ->
-          case testEquality k1 k2 of
-            Just Refl -> True
-            Nothing -> False }})
-         x
+typeCheck2 :: forall k proxy a b. (Enum1 k, TestEquality k)
+           => proxy k -> Int -> Enum1Info k a -> Enum1Info k b -> k a :~: k b
+typeCheck2 _ i inf1 inf2 =
+  let ret :: k a :~: k b
+      ret = unsafeCoerce Refl
+  in assert (let k1 = toEnum1 @k i inf1
+                 k2 = toEnum1 i inf2
+             in case testEquality k1 k2 of
+                  Just r -> justifies r ret True
+                  Nothing -> False)
+            ret
+  where
+    justifies :: a :~: b -> k a :~: k b -> r -> r
+    justifies Refl _ x = x
+
+bimap' :: (a -> b) -> (c -> d) -> (a, c) -> (b, d)
+bimap' f g (a, c) =
+  let !b = f a
+      !d = g c
+  in (b, d)
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -1,15 +1,16 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImportQualifiedPost #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 module Main where
 
-import qualified Data.Dependent.EnumMap.Strict as DE
+import Data.Dependent.EnumMap.Strict qualified as DE
+import Data.Dependent.EnumMap.Strict.Internal (coe1)
 import Data.Dependent.Sum
-import Data.Some
-
+import Data.Functor.Const
 
 data Tag = A | B | C
   deriving (Show)
@@ -21,9 +22,16 @@
 deriving instance Show (STag tag)
 
 instance DE.Enum1 STag where
-  type Enum1Info STag = ()
-  fromEnum1 = \case { SA -> (0, ()); SB -> (1, ()); SC -> (2, ()) }
-  toEnum1 n () = case n of { 0 -> Some SA; 1 -> Some SB; 2 -> Some SC; _ -> error "invalid tag" }
+  type Enum1Info STag = Const ()
+  fromEnum1 = \case
+                SA -> (0, Const ())
+                SB -> (1, Const ())
+                SC -> (2, Const ())
+  toEnum1 n _ = case n of
+                  0 -> coe1 SA
+                  1 -> coe1 SB
+                  2 -> coe1 SC
+                  _ -> error "invalid tag"
 
 data Value tag where
   VA :: Int -> Value A