Minimal changes to make it compile without Some in Enum1

This includes three additional `coe1`, all applied to `inf`.

1 files changed, 47 insertions, 46 deletions

diff --git a/src/Data/Dependent/EnumMap/Strict/Internal.hs b/src/Data/Dependent/EnumMap/Strict/Internal.hs
index 2058b6c..c0b47ab 100644
--- a/src/Data/Dependent/EnumMap/Strict/Internal.hs
+++ b/src/Data/Dependent/EnumMap/Strict/Internal.hs
@@ -26,12 +26,13 @@ import Text.Show (showListWith)
 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))
@@ -73,16 +74,16 @@ instance (Enum1 k, forall a. Show (k a), forall a. Show (v a))
 -- >   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) = case toEnum1 i inf of k -> k :=> coe1 v
 
 -- * Construction
 
@@ -119,7 +120,7 @@ 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)))
+                  k1 -> typeCheck1 k1 i inf2 $ KV inf1 (f k1 (coe1 v1) (coe1 v2)))
              (dSumToKV <$> l))
 
 -- ** From Ascending Lists
@@ -144,7 +145,7 @@ 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)))
+                 k1 -> typeCheck1 k1 i inf2 $ KV inf1 (f k1 (coe1 v1) (coe1 v2)))
              (dSumToKV <$> l))
 
 fromDistinctAscList :: Enum1 k => [DSum k v] -> DEnumMap k v
@@ -199,7 +200,7 @@ adjust = adjustWithKey . const
 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) -> typeCheck1 k i inf $ KV (coe1 inf) (f k (coe1 v))) i m)
 
 update :: (Enum1 k, TestEquality k) => (v a -> Maybe (v a)) -> k a -> DEnumMap k v -> DEnumMap k v
 update = updateWithKey . const
@@ -208,7 +209,7 @@ 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 (coe1 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)
@@ -216,7 +217,7 @@ updateLookupWithKey f k (DEnumMap m) =
   let (i, _) = fromEnum1 k
       (!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 (coe1 inf) <$> f k (coe1 v))
           i m
      -- Note: type checking unnecessary here for the same reason as insertLookupWithKey
   in ((\(KV _ v2) -> coe1 v2) <$> mx, DEnumMap m')
@@ -304,7 +305,7 @@ unionWithKey f (DEnumMap m1 :: DEnumMap k v) (DEnumMap m2) = DEnumMap (IM.unionW
   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))
+      k1 -> typeCheck1 k1 i inf2 $ KV inf1 (f k1 (coe1 v1) (coe1 v2))
 
 unions :: (Foldable f, Enum1 k, TestEquality k) => f (DEnumMap k v) -> DEnumMap k v
 unions = Foldable.foldl' union empty
@@ -335,7 +336,7 @@ differenceWithKey f (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.differenceWithKey
   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)
+      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
@@ -353,7 +354,7 @@ differenceWithKey' f (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.differenceWithKe
   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)
+      (k1, k2) -> KV inf1 <$> f k1 (coe1 v1) k2 (coe1 v2)
 
 -- ** Intersection
 
@@ -374,7 +375,7 @@ intersectionWithKey f (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.intersectionWit
   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)
+      k1 -> typeCheck1 k1 i inf2 $ KV inf1 $ f k1 (coe1 v1) (coe1 v2)
 
 -- | Generalises 'intersectionWithKey' in the same way as 'differenceWithKey''
 -- generalises 'differenceWithKey'.
@@ -385,7 +386,7 @@ intersectionWithKey' f (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.intersectionWi
   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)
+      (k1, k2) -> KV inf1 $ f k1 (coe1 v1) k2 (coe1 v2)
 
 -- ** Disjoint
 
@@ -410,7 +411,7 @@ mergeWithKey f g1 g2 (DEnumMap m1) (DEnumMap 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)
+      k1 -> typeCheck1 k1 i inf2 $ KV inf1 <$> f k1 (coe1 v1) (coe1 v2)
 
 -- * Traversal
 -- ** Map
@@ -420,28 +421,28 @@ map f = mapWithKey (const f)
 
 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) -> case toEnum1 i inf of k -> KV inf $ f k (coe1 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) -> case toEnum1 i inf of k -> KV inf <$> f k (coe1 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) -> case toEnum1 i inf of k -> fmap (KV inf) <$> f k (coe1 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) -> case toEnum1 i inf of k -> second (KV inf) $ f acc k (coe1 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) -> case toEnum1 i inf of k -> second (KV inf) $ f acc k (coe1 v)) acc0 m
 
 -- TODO: These are hard. Probably we can't avoid using a fold, analogously as in IntMap.
 -- mapKeys
@@ -458,15 +459,15 @@ foldl f acc0 (DEnumMap m) = IM.foldl (\acc (KV _ v) -> f acc v) acc0 m
 
 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 -> case toEnum1 i inf of k -> f k (coe1 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) -> case toEnum1 i inf of k -> f acc k (coe1 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) -> case toEnum1 i inf of k -> f k (coe1 v)) m
 
 -- ** Strict folds
 
@@ -478,11 +479,11 @@ foldl' f acc0 (DEnumMap m) = IM.foldl' (\acc (KV _ v) -> f acc v) acc0 m
 
 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 -> case toEnum1 i inf of k -> f k (coe1 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) -> case toEnum1 i inf of k -> f acc k (coe1 v)) acc0 m
 
 -- * Conversion
 
@@ -490,7 +491,7 @@ elems :: DEnumMap k v -> [Some v]
 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
@@ -518,7 +519,7 @@ filter f (DEnumMap m) = DEnumMap (IM.filter (\(KV _ v) -> f v) m)
 
 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) -> case toEnum1 i inf of k -> f k (coe1 v)) m)
 
 -- TODO: Wait for DEnumSet.
 -- restrictKeys
@@ -530,7 +531,7 @@ partition f (DEnumMap m) =
 
 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) -> case toEnum1 i inf of k -> f k (coe1 v)) m)
 
 -- | \(O(\min(n,W)^2)\). Because of the lack of a @takeWhileAntitoneWithValue@
 -- operation on 'Data.IntMap.Strict.IntMap', this function performs additional lookups to
@@ -538,17 +539,17 @@ partitionWithKey f (DEnumMap m) =
 -- 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)
+  DEnumMap (IM.takeWhileAntitone (\i -> case m IM.! i of KV inf _ -> case toEnum1 i inf of 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)
+  DEnumMap (IM.dropWhileAntitone (\i -> case m IM.! i of KV inf _ -> case toEnum1 i inf of 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)
+  bimap DEnumMap DEnumMap (IM.spanAntitone (\i -> case m IM.! i of KV inf _ -> case toEnum1 i inf of k -> f k) m)
 
 mapMaybe :: Enum1 k => (forall a. v1 a -> Maybe (v2 a)) -> DEnumMap k v1 -> DEnumMap k v2
 mapMaybe f = mapMaybeWithKey (const f)
@@ -556,7 +557,7 @@ mapMaybe f = mapMaybeWithKey (const f)
 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) -> case toEnum1 i inf of k -> KV inf <$> f k (coe1 v)) m)
 
 mapEither :: Enum1 k
           => (forall a. v1 a -> Either (v2 a) (v3 a)) -> DEnumMap k v1 -> (DEnumMap k v2, DEnumMap k v3)
@@ -565,7 +566,7 @@ mapEither f = mapEitherWithKey (const f)
 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) -> case toEnum1 i inf of 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)
@@ -627,14 +628,14 @@ 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) -> case toEnum1 i inf of k -> KV inf <$> f k (coe1 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) -> case toEnum1 i inf of k -> KV inf <$> f k (coe1 v)) m)
 
 minView :: DEnumMap k v -> Maybe (v a, DEnumMap k v)
 minView (DEnumMap m) = bimap (\(KV _ v) -> coe1 v) DEnumMap <$> IM.minView m
@@ -655,19 +656,19 @@ coe1 :: v a -> v b
 coe1 = unsafeCoerce
 
 typeCheck1 :: (Enum1 k, TestEquality k)
-           => k a -> Int -> Enum1Info k -> r -> r
+           => k a -> Int -> Enum1Info k b -> r -> r
 typeCheck1 k1 i inf2 x =
-  assert (case toEnum1 i inf2 of { Some k2 ->
+  assert (case toEnum1 i inf2 of { k2 ->
           case testEquality k1 k2 of
             Just Refl -> True
             Nothing -> False })
          x
 
-typeCheck2 :: forall k proxy r. (Enum1 k, TestEquality k)
-           => proxy k -> Int -> Enum1Info k -> Enum1Info k -> r -> r
+typeCheck2 :: forall k proxy r a b. (Enum1 k, TestEquality k)
+           => proxy k -> Int -> Enum1Info k a -> Enum1Info k b -> r -> r
 typeCheck2 _ i inf1 inf2 x =
-  assert (case toEnum1 @k i inf1 of { Some k1 ->
-          case toEnum1 i inf2 of { Some k2 ->
+  assert (case toEnum1 @k i inf1 of { k1 ->
+          case toEnum1 i inf2 of { k2 ->
           case testEquality k1 k2 of
             Just Refl -> True
             Nothing -> False }})