Various improvements

2 files changed, 111 insertions, 78 deletions

diff --git a/src/Data/Dependent/EnumMap/Strict.hs b/src/Data/Dependent/EnumMap/Strict.hs
index 8a2edd1..2e7066c 100644
--- a/src/Data/Dependent/EnumMap/Strict.hs
+++ b/src/Data/Dependent/EnumMap/Strict.hs
@@ -73,6 +73,7 @@ module Data.Dependent.EnumMap.Strict (
   (\\),
   differenceWith,
   differenceWithKey,
+  differenceWithKey',
 
   -- ** Intersection
 
diff --git a/src/Data/Dependent/EnumMap/Strict/Internal.hs b/src/Data/Dependent/EnumMap/Strict/Internal.hs
index bb1ee29..4e4c566 100644
--- a/src/Data/Dependent/EnumMap/Strict/Internal.hs
+++ b/src/Data/Dependent/EnumMap/Strict/Internal.hs
@@ -1,14 +1,17 @@
+{-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 module Data.Dependent.EnumMap.Strict.Internal where
 
 import Control.Exception
 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
@@ -21,12 +24,17 @@ import Unsafe.Coerce (unsafeCoerce)
 
 import Prelude hiding (lookup, map)
 
+type KV :: forall kind. (kind -> Type) -> (kind -> Type) -> Type
 data KV k v = forall a. KV !(Enum1Info k) !(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.
 newtype DEnumMap k v = DEnumMap (IM.IntMap (KV k v))
 
 instance (Enum1 k, forall a. Show (k a), forall a. Show (v a))
-      => Show (DEnumMap (k :: kind -> Type) (v :: kind -> Type)) where
+      => Show (DEnumMap k v) where
   showsPrec d mp = showParen (d > 10) $
     showString "fromList " . showListWith (\(k :=> v) -> showsPrec 2 k . showString " :=> " . showsPrec 1 v) (toList mp)
 
@@ -77,7 +85,7 @@ singleton k v =
   let (i, inf) = fromEnum1 k
   in DEnumMap (IM.singleton i (KV inf v))
 
--- TODO: probably doesn't make much sense until we have DEnumSet? Or should we ust lists instead?
+-- TODO: Wait for DEnumSet.
 -- fromSet
 
 -- ** From Unordered Lists
@@ -159,11 +167,17 @@ insertLookupWithKey :: (Enum1 k, TestEquality k)
                     -> k a -> v a -> DEnumMap k v -> (Maybe (v a), DEnumMap k v)
 insertLookupWithKey f k v (DEnumMap m) =
   let (i, inf) = fromEnum1 k
-      (mx, dmap) =
+      (!mx, !m') =
         IM.insertLookupWithKey
           (\_ _ (KV inf' v2) -> typeCheck1 k i inf' $ KV inf (f k v (coe1 v2)))
           i (KV inf v) m
-  in ((\(KV inf' v2) -> typeCheck1 k i inf' $ coe1 v2) <$> mx, DEnumMap dmap)
+     -- Note: type checking unnecessary here, because by the BangPatterns,
+     -- evaluating mx evaluates dmap, and the IntMap is strict, so the lambda
+     -- will have run and typechecked the old value already.
+     -- 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')
 
 -- * Deletion\/Update
 
@@ -181,19 +195,22 @@ adjustWithKey f k (DEnumMap m) =
 update :: (Enum1 k, TestEquality k) => (v a -> Maybe (v a)) -> k a -> DEnumMap k v -> DEnumMap k v
 update = updateWithKey . const
 
-updateWithKey :: (Enum1 k, TestEquality k) => (k a -> v a -> Maybe (v a)) -> k a -> DEnumMap k v -> DEnumMap k v
+updateWithKey :: (Enum1 k, TestEquality k)
+              => (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) -> typeCheck1 k i inf $ KV inf <$> f k (coe1 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)
+updateLookupWithKey :: (Enum1 k, TestEquality k)
+                    => (k a -> v a -> Maybe (v a)) -> k a -> DEnumMap k v -> (Maybe (v a), DEnumMap k v)
 updateLookupWithKey f k (DEnumMap m) =
   let (i, _) = fromEnum1 k
-      (mx, dmap) =
+      (!mx, !m') =
         IM.updateLookupWithKey
-          (\_ (KV inf v) -> typeCheck1 k i inf . KV inf <$> f k (coe1 v))
+          (\_ (KV inf v) -> typeCheck1 k i inf $ KV inf <$> f k (coe1 v))
           i m
-  in ((\(KV inf' v2) -> typeCheck1 k i inf' $ coe1 v2) <$> mx, DEnumMap dmap)
+     -- Note: type checking unnecessary here for the same reason as insertLookupWithKey
+  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
@@ -233,7 +250,7 @@ findWithDefault def k (DEnumMap m) =
        KV inf' v -> typeCheck1 k i inf' $ coe1 v
 
 find :: (Enum1 k, TestEquality k) => k a -> DEnumMap k v -> v a
-find k = findWithDefault (error ("Dependent.EnumMap.!: key " ++ show (fst $ fromEnum1 k) ++ " is not an element of the map")) k
+find k = findWithDefault (error ("Data.Dependent.EnumMap.!: key " ++ show (fst (fromEnum1 k)) ++ " is not an element of the map")) k
 
 (!) :: (Enum1 k, TestEquality k) => DEnumMap k v -> k a -> v a
 (!) m k = find k m
@@ -244,25 +261,12 @@ member k (DEnumMap m) = IM.member (fst (fromEnum1 k)) m
 notMember :: Enum1 k => k a -> DEnumMap k v -> Bool
 notMember k m = not $ member k m
 
-lookupLT :: (Enum1 k, TestEquality 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 :: (Enum1 k, TestEquality k) => k a -> DEnumMap k v -> Maybe (DSum k v)
-lookupGT k (DEnumMap m) =
-  let (i, _) = fromEnum1 k
-  in kVToDSum <$> IM.lookupGT i m
-
-lookupLE :: (Enum1 k, TestEquality k) => k a -> DEnumMap k v -> Maybe (DSum k v)
-lookupLE k (DEnumMap m) =
-  let (i, _) = fromEnum1 k
-  in kVToDSum <$> IM.lookupLE i m
-
-lookupGE :: (Enum1 k, TestEquality k) => k a -> DEnumMap k v -> Maybe (DSum k v)
-lookupGE k (DEnumMap m) =
-  let (i, _) = fromEnum1 k
-  in kVToDSum <$> IM.lookupGE i m
+lookupLT, lookupGT, lookupLE, lookupGE
+  :: (Enum1 k, TestEquality 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
 
 -- ** Size
 
@@ -293,44 +297,59 @@ unionWithKey f (DEnumMap m1 :: DEnumMap k v) (DEnumMap m2) = DEnumMap (IM.unionW
     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))
-        -- TODO: are the coe1 correct? is the typeCheck1 needed?
 
 unions :: (Foldable f, Enum1 k, TestEquality k) => f (DEnumMap k v) -> DEnumMap k v
 unions xs = Foldable.foldl' union empty xs
 
-unionsWith :: (Foldable f, Enum1 k, TestEquality k) => (forall a. v a -> v a -> v a) -> f (DEnumMap k v) -> DEnumMap k v
+unionsWith :: (Foldable f, Enum1 k, TestEquality k)
+           => (forall a. v a -> v a -> v a) -> f (DEnumMap k v) -> DEnumMap k v
 unionsWith f xs = Foldable.foldl' (unionWith f) empty xs
 
 -- ** Difference
 
--- TODO: should this be v1, v2 or both v? what about k1 and k2?
-difference :: DEnumMap k1 v1 -> DEnumMap k2 v2 -> DEnumMap k1 v1
+difference :: DEnumMap k v1 -> DEnumMap k v2 -> DEnumMap k v1
 difference (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.difference m1 m2)
 
-(\\) :: DEnumMap k1 v1 -> DEnumMap k2 v2 -> DEnumMap k1 v1
+(\\) :: DEnumMap k v1 -> DEnumMap k v2 -> DEnumMap k v1
 m1 \\ m2 = difference m1 m2
 
--- TODO: what about k1 and k2 here?
 differenceWith :: forall k v1 v2. (Enum1 k, TestEquality k)
                => (forall a. v1 a -> v2 a -> Maybe (v1 a)) -> DEnumMap k v1 -> DEnumMap k v2 -> DEnumMap k v1
 differenceWith 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) =
-      typeCheck2 (Proxy @k) i inf1 inf2 . KV inf1 <$> f (coe1 v1) (coe1 v2)
+      typeCheck2 (Proxy @k) i inf1 inf2 $ KV inf1 <$> f (coe1 v1) (coe1 v2)
 
--- TODO: what about k1 and k2 here?
 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)
+      Some k1 -> typeCheck1 k1 i inf2 $ KV inf1 <$> f k1 (coe1 v1) (coe1 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
+-- assumes that the @Int@ identifiers of @k1@ and @k2@ are compatible, i.e.
+-- that "2" in @k1@ somehow means the same thing as "2" in @k2@.
+--
+-- Because the key types are different, there is no guarantee whatsoever (even
+-- not by 'Enum1' laws) that equal key IDs in @k1@ and @k2@ actually have the
+-- same type index (@a@). Hence, the combining function gets key-value pairs
+-- with potentially distinct type indices.
+differenceWithKey' :: forall k1 k2 v1 v2. (Enum1 k1, Enum1 k2)
+                   => (forall a b. k1 a -> v1 a -> k2 b -> v2 b -> Maybe (v1 a))
+                   -> DEnumMap k1 v1 -> DEnumMap k2 v2 -> DEnumMap k1 v1
+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)
 
 -- ** Intersection
 
-intersection :: DEnumMap k1 v1 -> DEnumMap k2 v2 -> DEnumMap k1 v1
+intersection :: DEnumMap k v1 -> DEnumMap k v2 -> DEnumMap k v1
 intersection (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.intersection m1 m2)
 
 intersectionWith :: forall k v1 v2 v3. (Enum1 k, TestEquality k)
@@ -349,6 +368,17 @@ intersectionWithKey f (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.intersectionWit
     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)
 
+-- | Generalises 'intersectionWithKey' in the same way as 'differenceWithKey''
+-- generalises 'differenceWithKey'.
+intersectionWithKey' :: forall k1 k2 v1 v2 v3. (Enum1 k1, Enum1 k2)
+                     => (forall a b. k1 a -> v1 a -> k2 b -> v2 b -> v3 a)
+                     -> DEnumMap k1 v1 -> DEnumMap k2 v2 -> DEnumMap k1 v3
+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)
+
 -- ** Disjoint
 
 disjoint :: DEnumMap k v1 -> DEnumMap k v2 -> Bool
@@ -356,43 +386,45 @@ disjoint (DEnumMap m1) (DEnumMap m2) = IM.disjoint m1 m2
 
 -- ** Compose
 
-compose :: Enum1 k => DEnumMap k v -> DEnumMap k k -> DEnumMap k v
-compose (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.compose m1 (IM.map (\(KV _ v) -> fst $ fromEnum1 v) m2))
+compose :: (Enum1 k1, Enum1 k2, TestEquality k2) => DEnumMap k2 v -> DEnumMap k1 k2 -> DEnumMap k1 v
+compose m2v (DEnumMap m12) =
+  DEnumMap (IM.mapMaybe (\(KV inf1 k2) -> KV inf1 <$> m2v !? k2) m12)
 
 -- ** Universal combining function
 
 mergeWithKey :: forall k v1 v2 v3. (Enum1 k, TestEquality k)
-             => (forall a. k a -> v1 a -> v2 a -> Maybe (v3 a)) -> (DEnumMap k v1 -> DEnumMap k v3) -> (DEnumMap k v2 -> DEnumMap k v3) -> DEnumMap k v1 -> DEnumMap k v2 -> DEnumMap k v3
-mergeWithKey f g1 g2 (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.mergeWithKey f' g1' g2' m1 m2)
+             => (forall a. k a -> v1 a -> v2 a -> Maybe (v3 a))
+             -> (DEnumMap k v1 -> DEnumMap k v3)
+             -> (DEnumMap k v2 -> DEnumMap k v3)
+             -> DEnumMap k v1 -> DEnumMap k v2 -> DEnumMap k v3
+mergeWithKey f g1 g2 (DEnumMap m1) (DEnumMap m2) =
+  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)
-    g1' m = let DEnumMap m' = g1 (DEnumMap m) in m'
-    g2' m = let DEnumMap m' = g2 (DEnumMap m) in m'
+      Some k1 -> typeCheck1 k1 i inf2 $ KV inf1 <$> f k1 (coe1 v1) (coe1 v2)
 
 -- * Traversal
 -- ** Map
 
--- TODO: can the kind in the typing be avoided? Or moved to DEnumMap or Enum1 definition or somewhere?
-map :: forall c (k :: c -> Type) (v1 :: c -> Type) v2. (Enum1 k, TestEquality k) => (forall a. v1 a -> v2 a) -> DEnumMap k v1 -> DEnumMap k v2
-map f = mapWithKey (\_ x -> f x)
+map :: (Enum1 k, TestEquality k) => (forall a. v1 a -> v2 a) -> DEnumMap k v1 -> DEnumMap k v2
+map f = mapWithKey (const f)
 
 mapWithKey :: (Enum1 k, TestEquality 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)
 
-traverseWithKey :: (Applicative t, Enum1 k, TestEquality k)
-                => (forall a. k a -> v1 a -> t (v2 a)) -> DEnumMap k v1 -> t (DEnumMap k v2)
+traverseWithKey :: (Applicative f, Enum1 k, TestEquality 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
 
-traverseMaybeWithKey :: (Applicative t, Enum1 k, TestEquality k)
-                     => (forall a. k a -> v1 a -> t (Maybe (v2 a))) -> DEnumMap k v1 -> t (DEnumMap k v2)
+traverseMaybeWithKey :: (Applicative f, Enum1 k, TestEquality 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
 
-mapAccum :: forall c (k :: c -> Type) (v1 :: c -> Type) v2 acc. (Enum1 k, TestEquality k) => (forall a. acc -> v1 a -> (acc, v2 a)) -> acc -> DEnumMap k v1 -> (acc, DEnumMap k v2)
+mapAccum :: (Enum1 k, TestEquality 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, TestEquality k) => (forall a. acc -> k a -> v1 a -> (acc, v2 a)) -> acc -> DEnumMap k v1 -> (acc, DEnumMap k v2)
@@ -410,7 +442,6 @@ mapAccumRWithKey f acc0 (DEnumMap m) =
 
 -- * Folds
 
--- TODO: did I miss any typeCheck1 or typeCheck2 here or anywhere else? Or are any checks spurious?
 foldr :: (forall a. v a -> acc -> acc) -> acc -> DEnumMap k v -> acc
 foldr f acc0 (DEnumMap m) = IM.foldr (\(KV _ v) acc -> f v acc) acc0 m
 
@@ -456,7 +487,7 @@ keys (DEnumMap m) = (\(k, KV inf _) -> toEnum1 k inf) <$> IM.assocs m
 assocs :: Enum1 k => DEnumMap k v -> [DSum k v]
 assocs (DEnumMap m) = kVToDSum <$> IM.assocs m
 
--- TODO: probably doesn't make much sense until we have DEnumSet?
+-- TODO: Wait for DEnumSet.
 -- keysSet
 
 -- ** Lists
@@ -481,7 +512,7 @@ filterWithKey :: Enum1 k => (forall a. k a -> v a -> Bool) -> DEnumMap k v -> DE
 filterWithKey f (DEnumMap m) =
   DEnumMap (IM.filterWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> f k (coe1 v)) m)
 
--- TODO: these use IntSet. Do we use a list instead of wait for DEnumSet?
+-- TODO: Wait for DEnumSet.
 -- restrictKeys
 -- withoutKeys
 
@@ -493,44 +524,48 @@ partitionWithKey :: Enum1 k => (forall a. k a -> v a -> Bool) -> 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)
 
--- To make this more efficient, we'd need to define takeWhileAntitoneWithValue
--- for IntMap and use it here.
+-- | \(O(\min(n,W)^2)\). Because of the lack of a @takeWhileAntitoneWithValue@
+-- operation on 'IntMap', this function has performs additional lookups to
+-- reconstruct the full keys to pass to the predicate, resulting in a somewhat
+-- worse complexity than 'IM.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)
 
+-- | \(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)
 
+-- | \(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)
 
--- TODO: can the kind in the typing be avoided? Or moved to DEnumMap or Enum1 definition or somewhere?
-mapMaybe :: forall c (k :: c -> Type) (v1 :: c -> Type) v2. (Enum1 k, TestEquality k) => (forall a. v1 a -> Maybe (v2 a)) -> DEnumMap k v1 -> DEnumMap k v2
-mapMaybe f = mapMaybeWithKey (\_ x -> f x)
+mapMaybe :: (Enum1 k, TestEquality k) => (forall a. v1 a -> Maybe (v2 a)) -> DEnumMap k v1 -> DEnumMap k v2
+mapMaybe f = mapMaybeWithKey (const f)
 
-mapMaybeWithKey :: (Enum1 k, TestEquality k) => (forall a. k a -> v1 a -> Maybe (v2 a)) -> DEnumMap k v1 -> DEnumMap k v2
+mapMaybeWithKey :: (Enum1 k, TestEquality 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)
 
-mapEither :: forall c (k :: c -> Type) (v1 :: c -> Type) v2 v3. (Enum1 k, TestEquality k) => (forall a. v1 a -> Either (v2 a) (v3 a)) -> DEnumMap k v1 -> (DEnumMap k v2, DEnumMap k v3)
-mapEither f = mapEitherWithKey (\_ x -> f x)
+mapEither :: (Enum1 k, TestEquality k)
+          => (forall a. v1 a -> Either (v2 a) (v3 a)) -> DEnumMap k v1 -> (DEnumMap k v2, DEnumMap k v3)
+mapEither f = mapEitherWithKey (const f)
 
-mapEitherWithKey :: (Enum1 k, TestEquality k) => (forall a. k a -> v1 a -> Either (v2 a) (v3 a)) -> DEnumMap k v1 -> (DEnumMap k v2, DEnumMap k v3)
+mapEitherWithKey :: (Enum1 k, TestEquality 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)
 
 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)
 
--- TODO: is this coe1 fine or can we readably check that IM doesn't cheat
--- and give us a value with a wrong type?
--- Or Maybe we should return @Some v@ instead of @v a@? But it has to match @k a@, right?
 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
+     -- Note: this coe1 is fine because of the invariant on DEnumMap.
   in (DEnumMap m1, (\(KV _ v) -> coe1 v) <$> mkv, DEnumMap m2)
 
 splitRoot :: DEnumMap k v -> [DEnumMap k v]
@@ -538,20 +573,17 @@ splitRoot (DEnumMap m) = DEnumMap <$> IM.splitRoot m
 
 -- * Submap
 
--- TODO: can this coe1 be avoided?
+-- TODO: the submap operations can't check any laws because there is no IM.isSubmapOfByKey.
 isSubmapOf :: (forall a. Eq (v a)) => DEnumMap k v -> DEnumMap k v -> Bool
 isSubmapOf (DEnumMap m1) (DEnumMap m2) = IM.isSubmapOfBy (\(KV _ v1) (KV _ v2) -> v1 == coe1 v2) m1 m2
 
--- TODO: can this coe1 be avoided?
 isSubmapOfBy :: (forall a. v1 a -> v2 a -> Bool) -> DEnumMap k v1 -> DEnumMap k v2 -> Bool
 isSubmapOfBy f (DEnumMap m1) (DEnumMap m2) =
   IM.isSubmapOfBy (\(KV _ v1) (KV _ v2) -> f v1 (coe1 v2)) m1 m2
 
--- TODO: can this coe1 be avoided?
 isProperSubmapOf :: (forall a. Eq (v a)) => DEnumMap k v -> DEnumMap k v -> Bool
 isProperSubmapOf (DEnumMap m1) (DEnumMap m2) = IM.isProperSubmapOfBy (\(KV _ v1) (KV _ v2) -> v1 == coe1 v2) m1 m2
 
--- TODO: can this coe1 be avoided?
 isProperSubmapOfBy :: (forall a. v1 a -> v2 a -> Bool) -> DEnumMap k v1 -> DEnumMap k v2 -> Bool
 isProperSubmapOfBy f (DEnumMap m1) (DEnumMap m2) =
   IM.isProperSubmapOfBy (\(KV _ v1) (KV _ v2) -> f v1 (coe1 v2)) m1 m2
@@ -582,15 +614,15 @@ 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
 
-updateMin :: forall c (k :: c -> Type) (v :: c -> Type). Enum1 k => (forall a. v a -> Maybe (v a)) -> DEnumMap k v -> DEnumMap k v
-updateMin f = updateMinWithKey (\_ x -> f x)
+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)
 
-updateMax :: forall c (k :: c -> Type) (v :: c -> Type). Enum1 k => (forall a. v a -> Maybe (v a)) -> DEnumMap k v -> DEnumMap k v
-updateMax f = updateMaxWithKey (\_ x -> f x)
+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) =