packages feed

witness 0.6 → 0.6.1

raw patch · 14 files changed

+305/−13 lines, 14 filesdep +containers

Dependencies added: containers

Files

changelog.md view
@@ -1,3 +1,12 @@+## [0.6.1] - 2022-09-12+- new ListLength type family and associated functions+- new Greater type family and associated functions+- new FixedList type indexed by PeanoNat+- new ListElement functions+- new OrderedWitnessMapFor and OrderedWitnessMapOf types+- new functions:+  - someForToSome+ ## [0.6] - 2022-05-08 - reorganise modules - rename types and functions
src/Data/PeanoNat.hs view
@@ -40,3 +40,8 @@ type family PeanoToNatural pn where     PeanoToNatural 'Zero = 0     PeanoToNatural ('Succ pn) = PeanoToNatural pn + 1++type ListLength :: forall k. [k] -> PeanoNat+type family ListLength l where+    ListLength '[] = 'Zero+    ListLength (a ': aa) = 'Succ (ListLength aa)
src/Data/Type/Witness.hs view
@@ -21,11 +21,14 @@ import Data.Type.Witness.Specific.Either as I import Data.Type.Witness.Specific.Empty as I import Data.Type.Witness.Specific.FiniteAllFor as I+import Data.Type.Witness.Specific.FixedList as I import Data.Type.Witness.Specific.List.Element as I import Data.Type.Witness.Specific.List.List as I import Data.Type.Witness.Specific.List.Product as I import Data.Type.Witness.Specific.List.Sum as I import Data.Type.Witness.Specific.Natural as I+import Data.Type.Witness.Specific.OrderedWitnessMap.For as I+import Data.Type.Witness.Specific.OrderedWitnessMap.Of as I import Data.Type.Witness.Specific.Pair as I import Data.Type.Witness.Specific.PeanoNat as I import Data.Type.Witness.Specific.Single as I
+ src/Data/Type/Witness/Specific/FixedList.hs view
@@ -0,0 +1,76 @@+module Data.Type.Witness.Specific.FixedList where++import Data.PeanoNat+import Data.Type.Witness.General.Representative+import Data.Type.Witness.Specific.PeanoNat+import Data.Type.Witness.Specific.Some+import Import++type FixedList :: PeanoNat -> Type -> Type+data FixedList n a where+    NilFixedList :: FixedList 'Zero a+    ConsFixedList :: a -> FixedList n a -> FixedList ('Succ n) a++instance Functor (FixedList n) where+    fmap _ NilFixedList = NilFixedList+    fmap ab (ConsFixedList a l) = ConsFixedList (ab a) $ fmap ab l++instance Is PeanoNatType n => Applicative (FixedList n) where+    pure = let+        pure' :: PeanoNatType n' -> a -> FixedList n' a+        pure' ZeroType _ = NilFixedList+        pure' (SuccType n) a = ConsFixedList a $ pure' n a+        in pure' representative+    (<*>) = let+        ap' :: PeanoNatType n' -> FixedList n' (a -> b) -> FixedList n' a -> FixedList n' b+        ap' ZeroType NilFixedList NilFixedList = NilFixedList+        ap' (SuccType n) (ConsFixedList ab lab) (ConsFixedList a la) = ConsFixedList (ab a) $ ap' n lab la+        in ap' representative++instance Foldable (FixedList n) where+    foldMap _ NilFixedList = mempty+    foldMap am (ConsFixedList a l) = am a <> foldMap am l++instance Traversable (FixedList n) where+    sequenceA NilFixedList = pure NilFixedList+    sequenceA (ConsFixedList fa l) = liftA2 ConsFixedList fa $ sequenceA l++fixedFromList :: [a] -> (forall n. PeanoNatType n -> FixedList n a -> r) -> r+fixedFromList [] call = call ZeroType NilFixedList+fixedFromList (a:aa) call = fixedFromList aa $ \n l -> call (SuccType n) $ ConsFixedList a l++fixedListArrowSequence_ ::+       forall arrow n a. Arrow arrow+    => FixedList n (arrow a ())+    -> arrow (FixedList n a) ()+fixedListArrowSequence_ NilFixedList = arr $ \_ -> ()+fixedListArrowSequence_ (ConsFixedList x1 xr) =+    proc a1r -> do+        x1 -<+            case a1r of+                ConsFixedList a1 _ -> a1+        fixedListArrowSequence_ xr -<+            case a1r of+                ConsFixedList _ ar -> ar++fixedListArrowSequence ::+       forall arrow n a b. Arrow arrow+    => FixedList n (arrow a b)+    -> arrow (FixedList n a) (FixedList n b)+fixedListArrowSequence NilFixedList = arr $ \_ -> NilFixedList+fixedListArrowSequence (ConsFixedList x1 xr) =+    proc a1r -> do+        b1 <-+            x1 -<+                case a1r of+                    ConsFixedList a1 _ -> a1+        br <-+            fixedListArrowSequence xr -<+                case a1r of+                    ConsFixedList _ ar -> ar+        returnA -< ConsFixedList b1 br++fixedListElement :: Some (Greater n) -> FixedList n a -> a+fixedListElement (MkSome (MkGreater ZeroGreaterEqual)) (ConsFixedList a _) = a+fixedListElement (MkSome (MkGreater (SuccGreaterEqual n))) (ConsFixedList _ l) =+    fixedListElement (MkSome $ MkGreater n) l
src/Data/Type/Witness/Specific/List/Element.hs view
@@ -1,7 +1,10 @@ module Data.Type.Witness.Specific.List.Element where +import Data.PeanoNat import Data.Type.Witness.General.Order import Data.Type.Witness.Specific.List.List+import Data.Type.Witness.Specific.PeanoNat+import Data.Type.Witness.Specific.Some import Import  type ListElementType :: forall k. [k] -> k -> Type@@ -42,6 +45,10 @@ instance Empty (ListElementType '[] t) where     never lt = case lt of {} +pickListElement :: forall k (w :: k -> Type) (t :: k) (lt :: [k]). ListElementType lt t -> ListType w lt -> w t+pickListElement FirstElementType (ConsListType wt _) = wt+pickListElement (RestElementType n) (ConsListType _ l) = pickListElement n l+ lookUpListElement ::        forall k (w :: k -> Type) (t :: k) (lt :: [k]). TestEquality w     => w t@@ -57,3 +64,16 @@ countListType :: ListType w lt -> ListType (ListElementType lt) lt countListType NilListType = NilListType countListType (ConsListType _ lt) = ConsListType FirstElementType (mapListType RestElementType $ countListType lt)++listElementTypeIndex :: Some (ListElementType lt) -> Some (Greater (ListLength lt))+listElementTypeIndex (MkSome FirstElementType) = MkSome $ MkGreater ZeroGreaterEqual+listElementTypeIndex (MkSome (RestElementType n)) =+    case listElementTypeIndex $ MkSome n of+        MkSome (MkGreater n') -> MkSome $ MkGreater $ SuccGreaterEqual n'++indexListElementType :: ListType w lt -> Some (Greater (ListLength lt)) -> SomeFor w (ListElementType lt)+indexListElementType (ConsListType wa _) (MkSome (MkGreater ZeroGreaterEqual)) = MkSomeFor FirstElementType wa+indexListElementType (ConsListType _ lt) (MkSome (MkGreater (SuccGreaterEqual n))) =+    case indexListElementType lt (MkSome (MkGreater n)) of+        MkSomeFor n' wa -> MkSomeFor (RestElementType n') wa+indexListElementType NilListType (MkSome n) = never n
src/Data/Type/Witness/Specific/List/List.hs view
@@ -1,7 +1,10 @@ module Data.Type.Witness.Specific.List.List where +import Data.PeanoNat import Data.Type.Witness.General.Representative+import Data.Type.Witness.Specific.FixedList import Data.Type.Witness.Specific.Pair+import Data.Type.Witness.Specific.PeanoNat import Data.Type.Witness.Specific.Some import Import @@ -82,3 +85,16 @@ listTypeFor_ :: Applicative m => ListType w t -> (forall a. w a -> m ()) -> m () listTypeFor_ NilListType _ = pure () listTypeFor_ (ConsListType t tt) f = f t *> listTypeFor_ tt f++listTypeLengthType :: ListType w lt -> PeanoNatType (ListLength lt)+listTypeLengthType NilListType = ZeroType+listTypeLengthType (ConsListType _ rest) = SuccType $ listTypeLengthType rest++listTypeToFixedList :: (forall a. w a -> r) -> ListType w t -> FixedList (ListLength t) r+listTypeToFixedList _wr NilListType = NilFixedList+listTypeToFixedList wr (ConsListType wa rest) = ConsFixedList (wr wa) $ listTypeToFixedList wr rest++listTypeFromFixedList :: FixedList n (Some w) -> (forall t. n ~ ListLength t => ListType w t -> r) -> r+listTypeFromFixedList NilFixedList call = call NilListType+listTypeFromFixedList (ConsFixedList (MkSome wa) l) call =+    listTypeFromFixedList l $ \rest -> call $ ConsListType wa rest
+ src/Data/Type/Witness/Specific/OrderedWitnessMap/For.hs view
@@ -0,0 +1,71 @@+module Data.Type.Witness.Specific.OrderedWitnessMap.For where++import qualified Data.Map as Map+import Data.Type.Witness.General.Order+import Data.Type.Witness.Specific.Some+import Import++-- | A dictionary that is heterogenous up to its simple witness type @w@.+-- Witnesses are the keys of the dictionary, and the values they witness are the values of the dictionary.+type OrderedWitnessMapFor :: forall k. (k -> Type) -> (k -> Type) -> Type+newtype OrderedWitnessMapFor f w =+    MkOrderedWitnessMapFor (Map.Map (Some w) (SomeFor f w))+    deriving (Semigroup, Monoid)++-- | An empty dictionary.+emptyOrderedWitnessMapFor :: TestOrder w => OrderedWitnessMapFor f w+emptyOrderedWitnessMapFor = mempty++-- | Look up the value in the dictionary that matches the given witness.+orderedWitnessMapForLookup :: TestOrder w => w a -> OrderedWitnessMapFor f w -> Maybe (f a)+orderedWitnessMapForLookup wit (MkOrderedWitnessMapFor wmap) = do+    MkSomeFor wa fa <- Map.lookup (MkSome wit) wmap+    Refl <- testEquality wa wit -- should always succeed+    return fa++-- | Modify the value in the dictionary that matches a particular witness.+orderedWitnessMapForModify ::+       forall f w a. TestOrder w+    => w a+    -> (f a -> f a)+    -> OrderedWitnessMapFor f w+    -> OrderedWitnessMapFor f w+orderedWitnessMapForModify wit amap (MkOrderedWitnessMapFor wmap) = let+    updater :: SomeFor f w -> Maybe (SomeFor f w)+    updater (MkSomeFor wa fa) = do+        Refl <- testEquality wa wit -- should always succeed+        return $ MkSomeFor wa $ amap fa+    in MkOrderedWitnessMapFor $ Map.update updater (MkSome wit) wmap++-- | Replace the value in the dictionary that matches the witness+orderedWitnessMapForReplace :: TestOrder w => w a -> f a -> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w+orderedWitnessMapForReplace wit newfa = orderedWitnessMapForModify wit (const newfa)++-- | Add a witness and value to the dictionary.+orderedWitnessMapForAdd :: TestOrder w => w a -> f a -> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w+orderedWitnessMapForAdd wit fa (MkOrderedWitnessMapFor wmap) =+    MkOrderedWitnessMapFor $ Map.insert (MkSome wit) (MkSomeFor wit fa) wmap++-- | A dictionary for a single witness and value+orderedWitnessMapForSingle :: w a -> f a -> OrderedWitnessMapFor f w+orderedWitnessMapForSingle wit fa = MkOrderedWitnessMapFor $ Map.singleton (MkSome wit) $ MkSomeFor wit fa++orderedWitnessMapForFold :: Monoid m => OrderedWitnessMapFor f w -> (forall a. w a -> f a -> m) -> m+orderedWitnessMapForFold wmf f = mconcat $ fmap (\(MkSomeFor wa fa) -> f wa fa) $ orderedWitnessMapForToList wmf++-- | Remove the entry in the dictionary that matches the given witness.+orderedWitnessMapForRemove :: TestOrder w => w a -> OrderedWitnessMapFor f w -> OrderedWitnessMapFor f w+orderedWitnessMapForRemove wit (MkOrderedWitnessMapFor wmap) = MkOrderedWitnessMapFor $ Map.delete (MkSome wit) wmap++orderedWitnessMapForToList :: OrderedWitnessMapFor f w -> [SomeFor f w]+orderedWitnessMapForToList (MkOrderedWitnessMapFor wmap) = Map.elems wmap++-- | Create a dictionary from a list of witness\/value pairs+orderedWitnessMapForFromList :: TestOrder w => [SomeFor f w] -> OrderedWitnessMapFor f w+orderedWitnessMapForFromList ee =+    MkOrderedWitnessMapFor $ Map.fromList $ fmap (\swf@(MkSomeFor wa _) -> (MkSome wa, swf)) ee++orderedWitnessMapForMapM ::+       Applicative m => (forall a. f a -> m (g a)) -> OrderedWitnessMapFor f w -> m (OrderedWitnessMapFor g w)+orderedWitnessMapForMapM fmg (MkOrderedWitnessMapFor cells) =+    fmap MkOrderedWitnessMapFor $ for cells $ \(MkSomeFor wit fa) -> fmap (MkSomeFor wit) $ fmg fa
+ src/Data/Type/Witness/Specific/OrderedWitnessMap/Of.hs view
@@ -0,0 +1,48 @@+module Data.Type.Witness.Specific.OrderedWitnessMap.Of where++import Data.Type.Witness.General.Order+import Data.Type.Witness.Specific.OrderedWitnessMap.For+import Data.Type.Witness.Specific.Some+import Import++-- | A dictionary that is heterogenous up to its simple witness type @w@.+-- Witnesses are the keys of the dictionary, and the values they witness are the values of the dictionary.+type OrderedWitnessMapOf :: (Type -> Type) -> Type+type OrderedWitnessMapOf = OrderedWitnessMapFor Identity++-- | An empty dictionary.+emptyOrderedWitnessMapOf :: TestOrder w => OrderedWitnessMapOf w+emptyOrderedWitnessMapOf = emptyOrderedWitnessMapFor++-- | Look up the first value in the dictionary that matches the given witness.+orderedWitnessMapOfLookup :: TestOrder w => w a -> OrderedWitnessMapOf w -> Maybe a+orderedWitnessMapOfLookup wit d = fmap runIdentity $ orderedWitnessMapForLookup wit d++-- | Modify the first value in the dictionary that matches a particular witness.+orderedWitnessMapOfModify :: TestOrder w => w a -> (a -> a) -> OrderedWitnessMapOf w -> OrderedWitnessMapOf w+orderedWitnessMapOfModify wit amap = orderedWitnessMapForModify wit (Identity . amap . runIdentity)++-- | Replace the first value in the dictionary that matches the witness+orderedWitnessMapOfReplace :: TestOrder w => w a -> a -> OrderedWitnessMapOf w -> OrderedWitnessMapOf w+orderedWitnessMapOfReplace wit newa = orderedWitnessMapOfModify wit $ const newa++orderedWitnessMapOfSingle :: w a -> a -> OrderedWitnessMapOf w+orderedWitnessMapOfSingle wit a = orderedWitnessMapForSingle wit $ Identity a++orderedWitnessMapOfFold :: Monoid m => OrderedWitnessMapOf w -> (forall a. w a -> a -> m) -> m+orderedWitnessMapOfFold d f = orderedWitnessMapForFold d $ \wa (Identity a) -> f wa a++-- | Add a witness and value as the first entry in the dictionary.+orderedWitnessMapOfAdd :: TestOrder w => w a -> a -> OrderedWitnessMapOf w -> OrderedWitnessMapOf w+orderedWitnessMapOfAdd wit a = orderedWitnessMapForAdd wit $ Identity a++-- | Remove the first entry in the dictionary that matches the given witness.+orderedWitnessMapOfRemove :: TestOrder w => w a -> OrderedWitnessMapOf w -> OrderedWitnessMapOf w+orderedWitnessMapOfRemove = orderedWitnessMapForRemove++-- | Create a dictionary from a list of witness\/value pairs+orderedWitnessMapOfFromList :: TestOrder w => [SomeOf w] -> OrderedWitnessMapOf w+orderedWitnessMapOfFromList = orderedWitnessMapForFromList++orderedWitnessMapOfToList :: OrderedWitnessMapOf w -> [SomeOf w]+orderedWitnessMapOfToList = orderedWitnessMapForToList
src/Data/Type/Witness/Specific/PeanoNat.hs view
@@ -53,6 +53,10 @@     ZeroGreaterEqual :: GreaterEqual a 'Zero     SuccGreaterEqual :: GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b) +greaterEqualIndex :: GreaterEqual a b -> PeanoNatType b+greaterEqualIndex ZeroGreaterEqual = ZeroType+greaterEqualIndex (SuccGreaterEqual n) = SuccType $ greaterEqualIndex n+ samePeanoGreaterEqual :: PeanoNatType a -> GreaterEqual a a samePeanoGreaterEqual ZeroType = ZeroGreaterEqual samePeanoGreaterEqual (SuccType a) = SuccGreaterEqual $ samePeanoGreaterEqual a@@ -94,3 +98,32 @@ addPeanoNatTypeGE a (SuccType b) =     case succAddPeanoNatTypeEqual a b of         Refl -> diff1GreaterEqual $ addPeanoNatTypeGE a b++type Greater :: PeanoNat -> PeanoNat -> Type+data Greater a b where+    MkGreater :: GreaterEqual a b -> Greater ('Succ a) b++greaterIndex :: Greater a b -> PeanoNatType b+greaterIndex (MkGreater n) = greaterEqualIndex n++peanoGreater :: PeanoNatType a -> PeanoNatType b -> Maybe (Greater a b)+peanoGreater (SuccType a) b = fmap MkGreater $ peanoGreaterEqual a b+peanoGreater ZeroType _ = Nothing++instance Eq (Greater 'Zero b) where+    (==) = never++instance Searchable (Greater 'Zero b) where+    search = finiteSearch++instance Countable (Greater 'Zero b) where+    countPrevious = never+    countMaybeNext Nothing = Nothing+    countMaybeNext (Just n) = never n++instance Finite (Greater 'Zero b) where+    allValues = []+    assemble _ = pure never++instance Empty (Greater 'Zero b) where+    never n = case n of {}
src/Data/Type/Witness/Specific/Some.hs view
@@ -73,3 +73,6 @@  instance forall k (w :: k -> Type). AllConstraint Show w => Show (Some w) where     show (MkSome wa) = allShow wa++someForToSome :: SomeFor f w -> Some w+someForToSome (MkSomeFor wa _) = MkSome wa
src/Data/Type/Witness/Specific/WitnessMap/For.hs view
@@ -6,20 +6,20 @@ -- | A dictionary that is heterogenous up to its simple witness type @w@. -- Witnesses are the keys of the dictionary, and the values they witness are the values of the dictionary. type WitnessMapFor :: forall k. (k -> Type) -> (k -> Type) -> Type-newtype WitnessMapFor f w =-    MkWitnessMapFor [SomeFor f w]-    deriving (Semigroup, Monoid)+newtype WitnessMapFor f w = MkWitnessMapFor+    { witnessMapForToList :: [SomeFor f w]+    } deriving (Semigroup, Monoid)  -- | An empty dictionary. emptyWitnessMapFor :: WitnessMapFor f w emptyWitnessMapFor = mempty  -- | Look up the first value in the dictionary that matches the given witness.-witnessMapForLookup :: (TestEquality w) => w a -> WitnessMapFor f w -> Maybe (f a)+witnessMapForLookup :: TestEquality w => w a -> WitnessMapFor f w -> Maybe (f a) witnessMapForLookup wit (MkWitnessMapFor cells) = listToMaybe (mapMaybe (matchSomeFor wit) cells)  -- | Modify the first value in the dictionary that matches a particular witness.-witnessMapForModify :: (TestEquality w) => w a -> (f a -> f a) -> WitnessMapFor f w -> WitnessMapFor f w+witnessMapForModify :: TestEquality w => w a -> (f a -> f a) -> WitnessMapFor f w -> WitnessMapFor f w witnessMapForModify wit amap (MkWitnessMapFor cells) =     MkWitnessMapFor (replaceFirst ((fmap ((MkSomeFor wit) . amap)) . (matchSomeFor wit)) cells)   where@@ -31,7 +31,7 @@     replaceFirst _ _ = []  -- | Replace the first value in the dictionary that matches the witness-witnessMapForReplace :: (TestEquality w) => w a -> f a -> WitnessMapFor f w -> WitnessMapFor f w+witnessMapForReplace :: TestEquality w => w a -> f a -> WitnessMapFor f w -> WitnessMapFor f w witnessMapForReplace wit newfa = witnessMapForModify wit (const newfa)  -- | Add a witness and value as the first entry in the dictionary.@@ -46,7 +46,7 @@ witnessMapForFold (MkWitnessMapFor cells) f = mconcat $ fmap (\(MkSomeFor wit fa) -> f wit fa) cells  -- | Remove the first entry in the dictionary that matches the given witness.-witnessMapForRemove :: (TestEquality w) => w a -> WitnessMapFor f w -> WitnessMapFor f w+witnessMapForRemove :: TestEquality w => w a -> WitnessMapFor f w -> WitnessMapFor f w witnessMapForRemove wit (MkWitnessMapFor cells) =     MkWitnessMapFor (removeFirst (\(MkSomeFor cwit _) -> isJust (testEquality wit cwit)) cells)   where
src/Data/Type/Witness/Specific/WitnessMap/Of.hs view
@@ -14,15 +14,15 @@ emptyWitnessMapOf = emptyWitnessMapFor  -- | Look up the first value in the dictionary that matches the given witness.-witnessMapOfLookup :: (TestEquality w) => w a -> WitnessMapOf w -> Maybe a+witnessMapOfLookup :: TestEquality w => w a -> WitnessMapOf w -> Maybe a witnessMapOfLookup wit d = fmap runIdentity $ witnessMapForLookup wit d  -- | Modify the first value in the dictionary that matches a particular witness.-witnessMapOfModify :: (TestEquality w) => w a -> (a -> a) -> WitnessMapOf w -> WitnessMapOf w+witnessMapOfModify :: TestEquality w => w a -> (a -> a) -> WitnessMapOf w -> WitnessMapOf w witnessMapOfModify wit amap = witnessMapForModify wit (Identity . amap . runIdentity)  -- | Replace the first value in the dictionary that matches the witness-witnessMapOfReplace :: (TestEquality w) => w a -> a -> WitnessMapOf w -> WitnessMapOf w+witnessMapOfReplace :: TestEquality w => w a -> a -> WitnessMapOf w -> WitnessMapOf w witnessMapOfReplace wit newa = witnessMapOfModify wit $ const newa  witnessMapOfSingle :: w a -> a -> WitnessMapOf w@@ -36,9 +36,12 @@ witnessMapOfAdd wit a = witnessMapForAdd wit $ Identity a  -- | Remove the first entry in the dictionary that matches the given witness.-witnessMapOfRemove :: (TestEquality w) => w a -> WitnessMapOf w -> WitnessMapOf w+witnessMapOfRemove :: TestEquality w => w a -> WitnessMapOf w -> WitnessMapOf w witnessMapOfRemove = witnessMapForRemove  -- | Create a dictionary from a list of witness\/value pairs witnessMapOfFromList :: [SomeOf w] -> WitnessMapOf w witnessMapOfFromList = MkWitnessMapFor++witnessMapOfToList :: WitnessMapOf w -> [SomeOf w]+witnessMapOfToList = witnessMapForToList
src/Import.hs view
@@ -3,6 +3,7 @@     ) where  import Control.Applicative as I+import Control.Arrow as I import Control.Category as I import Data.Constraint as I (Dict(..)) import Data.Countable as I
witness.cabal view
@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: a76cbdba6c2986d516e94b90eb9a51cf636e600c1915604c67d33e50e06f3127+-- hash: aae0fd4e94350169efa7229b1559a55e3b9d2ed3d389f607534a15403307b6b1  name:           witness-version:        0.6+version:        0.6.1 synopsis:       values that witness types description:    A /witness/ is a value that witnesses some sort of constraint on some list of type variables. This library provides support for a wide variety of witness types. It also provides classes for /representatives/, which are values that represent types. category:       Data@@ -74,6 +74,7 @@   build-depends:       base >=4.15 && <5     , constraints >=0.13+    , containers >=0.4     , countable >=1.2   exposed-modules:       Data.Type.Witness.Apply@@ -95,8 +96,11 @@       Data.Type.Witness.Specific.FiniteAllFor       Data.Type.Witness.Specific.WitnessMap.Of       Data.Type.Witness.Specific.WitnessMap.For+      Data.Type.Witness.Specific.OrderedWitnessMap.Of+      Data.Type.Witness.Specific.OrderedWitnessMap.For       Data.Type.Witness.Specific.PeanoNat       Data.Type.Witness.Specific.Natural+      Data.Type.Witness.Specific.FixedList       Data.Type.Witness.Specific.List.Element       Data.Type.Witness.Specific.List.List       Data.Type.Witness.Specific.Concat