{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} module Data.Dependent.EnumMap.Strict.Internal where import Control.Exception import Data.Bifunctor (bimap) import Data.Dependent.Sum import qualified Data.Foldable as Foldable import qualified Data.IntMap.Strict as IM import Data.Kind (Type) import Data.Proxy import Data.Some import Data.Type.Equality import Text.Show (showListWith) import Unsafe.Coerce (unsafeCoerce) import Prelude hiding (lookup, map) data KV k v = forall a. KV !(Enum1Info k) !(v a) 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 showsPrec d mp = showParen (d > 10) $ showString "fromList " . showListWith (\(k :=> v) -> showsPrec 2 k . showString " :=> " . showsPrec 1 v) (toList mp) -- | This class attempts to generalise 'Enum' to indexed data types: data types -- with a GADT-like type parameter. Conversion to an 'Int' naturally loses type -- information, and furthermore it is common to actually need some additional -- data alongside the 'Int' to be able to reconstruct the original (in -- 'toEnum1'). This additional data lives in 'Enum1Info'. The laws are: -- -- [Unique IDs] -- If @'fst' ('fromEnum1' x) == 'fst' ('fromEnum1' y)@ then @'testEquality' x y == 'Just' 'Refl' && x '==' y@ -- [Persistent IDs] -- @'fst' ('fromEnum1' ('uncurry' 'toEnum1' ('fromEnum1' x))) == 'fst' ('fromEnum1' x)@ -- -- The "Unique IDs" law states that if the IDs of two values are equal, then -- the values themselves must have the same type index, and furthermore be -- equal. If @f@ does not implement 'TestEquality' or 'Eq', the law should -- morally hold (but most of the API will be unusable). -- -- The "Persistent IDs" law states that reconstructing a value using 'toEnum1' -- does not change its ID. -- -- __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. class Enum1 f where type Enum1Info f fromEnum1 :: f a -> (Int, Enum1Info f) toEnum1 :: Int -> Enum1Info f -> Some f 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 -- * Construction empty :: DEnumMap k v empty = DEnumMap IM.empty singleton :: Enum1 k => k a -> v a -> DEnumMap k v singleton k v = let (i, inf) = fromEnum1 k in DEnumMap (IM.singleton i (KV inf v)) -- fromSet -- ** From Unordered Lists fromList :: Enum1 k => [DSum k v] -> DEnumMap k v fromList l = DEnumMap (IM.fromList (dSumToKV <$> l)) fromListWith :: (Enum1 k, TestEquality k) => (forall a. v a -> v a -> v a) -> [DSum k v] -> DEnumMap k v 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))) (dSumToKV <$> l)) fromListWithKey :: (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))) (dSumToKV <$> l)) -- ** From Ascending Lists fromAscList :: Enum1 k => [DSum k v] -> DEnumMap k v fromAscList l = DEnumMap (IM.fromAscList (dSumToKV <$> l)) fromAscListWith :: (Enum1 k, TestEquality k) => (forall a. v a -> v a -> v a) -> [DSum k v] -> DEnumMap k v 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))) (dSumToKV <$> l)) fromAscListWithKey :: (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))) (dSumToKV <$> l)) fromDistinctAscList :: Enum1 k => [DSum k v] -> DEnumMap k v fromDistinctAscList l = DEnumMap (IM.fromDistinctAscList (dSumToKV <$> l)) -- * Insertion insert :: Enum1 k => k a -> v a -> DEnumMap k v -> DEnumMap k v insert k v (DEnumMap m) = let (i, inf) = fromEnum1 k in DEnumMap (IM.insert i (KV inf v) m) insertWith :: (Enum1 k, TestEquality k) => (v a -> v a -> v a) -> k a -> v a -> DEnumMap k v -> DEnumMap k v insertWith = insertWithKey . const insertWithKey :: (Enum1 k, TestEquality k) => (k a -> v a -> v a -> v a) -> k a -> v a -> DEnumMap k v -> DEnumMap k v 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))) i (KV inf v) m) insertLookupWithKey :: (Enum1 k, TestEquality k) => (k a -> v a -> v a -> v a) -> 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) = 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) -- * Deletion\/Update delete :: Enum1 k => k a -> DEnumMap k v -> DEnumMap k v delete k (DEnumMap m) = DEnumMap (IM.delete (fst (fromEnum1 k)) m) adjust :: (Enum1 k, TestEquality k) => (v a -> v a) -> k a -> DEnumMap k v -> DEnumMap k v 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) 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 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) 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) = IM.updateLookupWithKey (\_ (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) alter :: forall k v a. (Enum1 k, TestEquality k) => (Maybe (v a) -> Maybe (v a)) -> k a -> DEnumMap k v -> DEnumMap k v alter f k (DEnumMap m) = DEnumMap (IM.alter f' i m) where (i, inf) = fromEnum1 k 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)) 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) alterF f k (DEnumMap m) = DEnumMap <$> IM.alterF f' i m where (i, inf) = fromEnum1 k 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)) -- * Query -- ** Lookup lookup :: (Enum1 k, TestEquality k) => k a -> DEnumMap k v -> Maybe (v a) lookup k (DEnumMap m) = let (i, _) = fromEnum1 k in (\(KV inf v) -> typeCheck1 k i inf $ coe1 v) <$> IM.lookup i m (!?) :: (Enum1 k, TestEquality k) => DEnumMap k v -> k a -> Maybe (v a) (!?) m k = lookup k m findWithDefault :: (Enum1 k, TestEquality k) => v a -> k a -> DEnumMap k v -> v a 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 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 (!) :: (Enum1 k, TestEquality k) => DEnumMap k v -> k a -> v a (!) m k = find k m member :: Enum1 k => k a -> DEnumMap k v -> Bool 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 -- ** Size null :: DEnumMap k v -> Bool null (DEnumMap m) = IM.null m size :: DEnumMap k v -> Int size (DEnumMap m) = IM.size m -- * Combine -- ** Union union :: (Enum1 k, TestEquality k) => DEnumMap k v -> DEnumMap k v -> DEnumMap k v union = unionWith const -- if we're type checking, we need unionWith anyway, so might as well just delegate here already unionWith :: (Enum1 k, TestEquality k) => (forall a. v a -> v a -> v a) -> DEnumMap k v -> DEnumMap k v -> DEnumMap k v 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)) unionWithKey :: (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)) -- TODO: are the coe1 correct? is the use of typeCheck1 fine? 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 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 m1) (DEnumMap m2) = DEnumMap (IM.difference m1 m2) (\\) :: DEnumMap k1 v1 -> DEnumMap k2 v2 -> DEnumMap k1 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) -- 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) -- ** Intersection intersection :: DEnumMap k1 v1 -> DEnumMap k2 v2 -> DEnumMap k1 v1 intersection (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.intersection m1 m2) intersectionWith :: forall k v1 v2 v3. (Enum1 k, TestEquality k) => (forall a. v1 a -> v2 a -> v3 a) -> DEnumMap k v1 -> DEnumMap k v2 -> DEnumMap k v3 intersectionWith 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) = typeCheck2 (Proxy @k) i inf1 inf2 $ KV inf1 $ f (coe1 v1) (coe1 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) -- ** Disjoint disjoint :: DEnumMap k v1 -> DEnumMap k v2 -> Bool 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)) -- ** 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) 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' -- * Traversal -- ** Map -- map -- mapWithKey -- traverseWithKey -- traverseMaybeWithKey -- mapAccum -- mapAccumWithKey -- mapAccumRWithKey -- mapKeys -- mapKeysWith -- mapKeysMonotonic -- * Folds -- foldr -- foldl -- foldrWithKey -- foldlWithKey -- foldMapWithKey -- ** Strict folds -- foldr' -- foldl' -- foldrWithKey' -- foldlWithKey' -- * Conversion 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 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? -- keysSet -- ** Lists toList :: Enum1 k => DEnumMap k v -> [DSum k v] toList = toAscList -- ** Ordered lists toAscList :: Enum1 k => DEnumMap k v -> [DSum k v] toAscList (DEnumMap m) = kVToDSum <$> IM.toAscList m toDescList :: Enum1 k => DEnumMap k v -> [DSum k v] toDescList (DEnumMap m) = kVToDSum <$> IM.toDescList m -- * Filter -- filter filter :: (forall a. v a -> Bool) -> DEnumMap k v -> DEnumMap k v 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) -- TODO: these use IntSet. Do we use a list instead of wait for DEnumSet? -- restrictKeys -- withoutKeys partition :: (forall a. v a -> Bool) -> DEnumMap k v -> (DEnumMap k v, DEnumMap k v) partition f (DEnumMap m) = bimap DEnumMap DEnumMap (IM.partition (\(KV _ v) -> f v) 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) -- To make this more efficient, we'd need to define takeWhileAntitoneWithValue -- for IntMap and use it here. 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) 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) 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) -- mapMaybe -- mapMaybeWithKey -- mapEither -- mapEitherWithKey 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? 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 in (DEnumMap m1, (\(KV _ v) -> coe1 v) <$> mkv, DEnumMap m2) splitRoot :: DEnumMap k v -> [DEnumMap k v] splitRoot (DEnumMap m) = DEnumMap <$> IM.splitRoot m -- * Submap -- isSubmapOf, isSubmapOfBy -- isProperSubmapOf, isProperSubmapOfBy -- * Min\/Max -- lookupMin -- lookupMax -- findMin -- findMax -- deleteMin -- deleteMax -- deleteFindMin -- deleteFindMax -- updateMin -- updateMax -- updateMinWithKey -- updateMaxWithKey -- minView -- maxView -- minViewWithKey maxViewWithKey :: Enum1 k => DEnumMap k v -> Maybe (DSum k v, DEnumMap k v) maxViewWithKey (DEnumMap m) = bimap kVToDSum DEnumMap <$> IM.maxViewWithKey m -- * Helpers 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 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