packages feed

witness 0.5 → 0.6

raw patch · 61 files changed

+1517/−1446 lines, 61 filesdep −semigroupoidsdep −transformersdep ~basedep ~constraintsdep ~countable

Dependencies removed: semigroupoids, transformers

Dependency ranges changed: base, constraints, countable

Files

LICENSE view
@@ -1,4 +1,4 @@-witness is Copyright (c) Ashley Yakeley, 2007-2008.+witness is Copyright (c) Ashley Yakeley, 2007-2021. All rights reserved.  Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
+ changelog.md view
@@ -0,0 +1,6 @@+## [0.6] - 2022-05-08+- reorganise modules+- rename types and functions+- additional functionality++## [0.5] - 2020-09-22
− src/Control/Category/Tensor.hs 
@@ -1,17 +0,0 @@-module Control.Category.Tensor where--import Data.Semigroupoid.Dual-import Prelude---- could use data-lens:Control.Category.Product(Tensor)-class Tensor cc where-    tensorUnit :: cc () ()-    tensorPair :: cc a1 b1 -> cc a2 b2 -> cc (a1, a2) (b1, b2)--instance Tensor (->) where-    tensorUnit = id-    tensorPair ab1 ab2 (a1, a2) = (ab1 a1, ab2 a2)--instance (Tensor cc) => Tensor (Dual cc) where-    tensorUnit = Dual tensorUnit-    tensorPair (Dual ab1) (Dual ab2) = Dual (tensorPair ab1 ab2)
− src/Data/Nat.hs 
@@ -1,21 +0,0 @@-module Data.Nat where--import Prelude--data Nat-    = Zero-    | Succ Nat--addNat :: Nat -> Nat -> Nat-addNat Zero b = b-addNat (Succ a) b = Succ $ addNat a b---- | subtractFromNat a b = b - a-subtractFromNat :: Nat -> Nat -> Maybe Nat-subtractFromNat Zero b = Just b-subtractFromNat (Succ a) (Succ b) = subtractFromNat a b-subtractFromNat (Succ _) Zero = Nothing--multiplyNat :: Nat -> Nat -> Nat-multiplyNat Zero _ = Zero-multiplyNat (Succ a) b = addNat (multiplyNat a b) b
+ src/Data/PeanoNat.hs view
@@ -0,0 +1,42 @@+module Data.PeanoNat where++import GHC.TypeNats+import Import+import Numeric.Natural++-- | Inductive natural numbers.+data PeanoNat+    = Zero+    | Succ PeanoNat++addPeanoNat :: PeanoNat -> PeanoNat -> PeanoNat+addPeanoNat Zero b = b+addPeanoNat (Succ a) b = Succ $ addPeanoNat a b++type Add :: PeanoNat -> PeanoNat -> PeanoNat+type family Add a b where+    Add 'Zero b = b+    Add ('Succ a) b = 'Succ (Add a b)++-- | subtractFromPeanoNat a b = b - a+subtractFromPeanoNat :: PeanoNat -> PeanoNat -> Maybe PeanoNat+subtractFromPeanoNat Zero b = Just b+subtractFromPeanoNat (Succ a) (Succ b) = subtractFromPeanoNat a b+subtractFromPeanoNat (Succ _) Zero = Nothing++multiplyPeanoNat :: PeanoNat -> PeanoNat -> PeanoNat+multiplyPeanoNat Zero _ = Zero+multiplyPeanoNat (Succ a) b = addPeanoNat (multiplyPeanoNat a b) b++peanoToNatural :: PeanoNat -> Natural+peanoToNatural Zero = 0+peanoToNatural (Succ n) = succ $ peanoToNatural n++naturalToPeano :: Natural -> PeanoNat+naturalToPeano 0 = Zero+naturalToPeano n = Succ $ naturalToPeano $ pred n++type PeanoToNatural :: PeanoNat -> Nat+type family PeanoToNatural pn where+    PeanoToNatural 'Zero = 0+    PeanoToNatural ('Succ pn) = PeanoToNatural pn + 1
− src/Data/Type/Apply.hs 
@@ -1,14 +0,0 @@-module Data.Type.Apply where--import Control.Category-import Data.Kind-import Data.Type.Equality--applyRefl ::-       forall k1 k2 (fa :: k1 -> k2) (fb :: k1 -> k2) (a :: k1) (b :: k1). fa :~: fb -> a :~: b -> (fa a) :~: (fb b)-applyRefl Refl Refl = Refl--reflId ::-       forall k (cat :: k -> k -> Type) (a :: k) (b :: k). Category cat-    => a :~: b -> cat a b-reflId Refl = id
− src/Data/Type/Heterogeneous.hs 
@@ -1,15 +0,0 @@-module Data.Type.Heterogeneous where--import Data.Kind-import Data.Type.Equality-import Prelude--withHRefl :: forall ka (a :: ka) kb (b :: kb) (r :: Type). a :~~: b -> ((a ~~ b) => r) -> r-withHRefl HRefl r = r---- | somewhat awkwardly named-homoHetEq :: forall (k :: Type) (a :: k) (b :: k). a :~~: b -> a :~: b-homoHetEq HRefl = Refl--class TestHetEquality (w :: forall k. k -> Type) where-    testHetEquality :: forall (ka :: Type) (a :: ka) (kb :: Type) (b :: kb). w a -> w b -> Maybe (a :~~: b)
− src/Data/Type/With.hs 
@@ -1,18 +0,0 @@-module Data.Type.With where--import Control.Category-import Data.Kind-import Data.Type.Equality--withRefl :: forall k (a :: k) (b :: k) (r :: Type). a :~: b -> (a ~ b => r) -> r-withRefl Refl r = r--reflCat ::-       forall k (cat :: k -> k -> Type) (a :: k) (b :: k). Category cat-    => a :~: b -> cat a b-reflCat Refl = id--reflWitCat ::-       forall kq (cat :: kq -> kq -> Type) kp (w :: kp -> kq) (a :: kp) (b :: kp). Category cat-    => a :~: b -> cat (w a) (w b)-reflWitCat Refl = id
+ src/Data/Type/Witness.hs view
@@ -0,0 +1,35 @@+module Data.Type.Witness+    ( module I+    ) where++import Data.PeanoNat as I+import Data.Proxy as I+import Data.Type.Equality as I+import Data.Type.Witness.Apply as I+import Data.Type.Witness.General.AllConstraint as I+import Data.Type.Witness.General.Finite as I+import Data.Type.Witness.General.HetConstraint as I+import Data.Type.Witness.General.ListElement as I+import Data.Type.Witness.General.Order as I+import Data.Type.Witness.General.Representative as I+import Data.Type.Witness.General.TestHetEquality as I+import Data.Type.Witness.General.WitnessConstraint as I+import Data.Type.Witness.General.WitnessValue as I+import Data.Type.Witness.Specific.All as I+import Data.Type.Witness.Specific.ApplyStack as I+import Data.Type.Witness.Specific.Concat as I+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.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.Pair as I+import Data.Type.Witness.Specific.PeanoNat as I+import Data.Type.Witness.Specific.Single as I+import Data.Type.Witness.Specific.Some as I+import Data.Type.Witness.Specific.Symbol as I+import Data.Type.Witness.Specific.WitnessMap.For as I+import Data.Type.Witness.Specific.WitnessMap.Of as I
+ src/Data/Type/Witness/Apply.hs view
@@ -0,0 +1,20 @@+module Data.Type.Witness.Apply where++import Import++applyRefl ::+       forall k1 k2 (fa :: k1 -> k2) (fb :: k1 -> k2) (a :: k1) (b :: k1). fa :~: fb -> a :~: b -> (fa a) :~: (fb b)+applyRefl Refl Refl = Refl++withRefl :: forall k (a :: k) (b :: k) (r :: Type). a :~: b -> (a ~ b => r) -> r+withRefl Refl r = r++reflId ::+       forall k (cat :: k -> k -> Type) (a :: k) (b :: k). Category cat+    => a :~: b -> cat a b+reflId Refl = id++reflId1 ::+       forall kq (cat :: kq -> kq -> Type) kp (w :: kp -> kq) (a :: kp) (b :: kp). Category cat+    => a :~: b -> cat (w a) (w b)+reflId1 Refl = id
+ src/Data/Type/Witness/General/AllConstraint.hs view
@@ -0,0 +1,18 @@+module Data.Type.Witness.General.AllConstraint where++import Import++type AllConstraint :: forall kw kt. (kw -> Constraint) -> (kt -> kw) -> Constraint+class AllConstraint c w where+    allConstraint :: forall t. Dict (c (w t))++instance AllConstraint Show ((:~:) t) where+    allConstraint = Dict++allShow ::+       forall k (w :: k -> Type) (t :: k). AllConstraint Show w+    => w t+    -> String+allShow wt =+    case allConstraint @_ @_ @Show @w @t of+        Dict -> show wt
+ src/Data/Type/Witness/General/Finite.hs view
@@ -0,0 +1,54 @@+{-# OPTIONS -fno-warn-orphans #-}++module Data.Type.Witness.General.Finite where++import Data.Type.Witness.General.AllConstraint+import Data.Type.Witness.General.WitnessConstraint+import Data.Type.Witness.Specific.All+import Data.Type.Witness.Specific.Some+import Import++type FiniteWitness :: forall k. (k -> Type) -> Constraint+class FiniteWitness (w :: k -> Type) where+    assembleAllFor ::+           forall (m :: Type -> Type) (f :: k -> Type). Applicative m+        => (forall (t :: k). w t -> m (f t))+        -> m (AllFor f w)++instance FiniteWitness ((:~:) t) where+    assembleAllFor getsel = fmap (\ft -> MkAllFor $ \Refl -> ft) $ getsel Refl++instance (TestEquality w, FiniteWitness w) => Countable (Some w) where+    countPrevious = finiteCountPrevious+    countMaybeNext = finiteCountMaybeNext++instance (TestEquality w, FiniteWitness w) => Searchable (Some w) where+    search = finiteSearch++instance (TestEquality w, FiniteWitness w) => Finite (Some w) where+    assemble ::+           forall b f. Applicative f+        => (Some w -> f b)+        -> f (Some w -> b)+    assemble afb =+        fmap (\(MkAllFor wtcb) (MkSome wt) -> getConst $ wtcb wt) $ assembleAllFor $ \wt -> fmap Const $ afb $ MkSome wt+    allValues = getConst $ assembleAllFor $ \wt -> Const [MkSome wt]++allWitnesses :: FiniteWitness w => [Some w]+allWitnesses = getConst $ assembleAllFor $ \wt -> Const [MkSome wt]++allForCodomain :: FiniteWitness w => AllFor f w -> [Some f]+allForCodomain af = fmap (allMapSome af) allWitnesses++instance (FiniteWitness w, AllConstraint Show w, WitnessConstraint Show w) => Show (AllOf w) where+    show (MkAllOf wtt) = let+        showItem :: Some w -> String+        showItem (MkSome wt) =+            allShow wt +++            " -> " +++            case witnessConstraint @_ @Show wt of+                Dict -> show (wtt wt)+        in "{" ++ intercalate "," (fmap showItem allWitnesses) ++ "}"++assembleAllOf :: (FiniteWitness w, Applicative m) => (forall t. w t -> m t) -> m (AllOf w)+assembleAllOf wtmt = fmap allForToAllOf $ assembleAllFor $ \wt -> fmap Identity $ wtmt wt
+ src/Data/Type/Witness/General/HetConstraint.hs view
@@ -0,0 +1,16 @@+module Data.Type.Witness.General.HetConstraint where++import Import++type HetConstraintWitness :: forall k1. (k1 -> Constraint) -> forall k2. k2 -> Type+data HetConstraintWitness c t where+    MkHetConstraintWitness+        :: forall k (c :: k -> Constraint) (t :: k). c t+        => HetConstraintWitness c t++type HetConstraint :: forall k1. (k1 -> Constraint) -> forall k2. k2 -> Constraint+class HetConstraint c t where+    hetConstraint :: HetConstraintWitness c t++instance forall k (c :: k -> Constraint) (t :: k). c t => HetConstraint c t where+    hetConstraint = MkHetConstraintWitness
+ src/Data/Type/Witness/General/ListElement.hs view
@@ -0,0 +1,17 @@+module Data.Type.Witness.General.ListElement where++import Data.Type.Witness.General.Representative+import Data.Type.Witness.Specific.List.Element+import Data.Type.Witness.Specific.List.List+import Import++type ListElementWitness :: forall k. (k -> Type) -> Constraint+class Is (ListType Proxy) (WitnessTypeList w) => ListElementWitness (w :: k -> Type) where+    type WitnessTypeList w :: [k]+    toListElementWitness :: forall t. w t -> ListElementType (WitnessTypeList w) t+    fromListElementWitness :: forall t. ListElementType (WitnessTypeList w) t -> w t++instance Is (ListType Proxy) tt => ListElementWitness (ListElementType tt) where+    type WitnessTypeList (ListElementType tt) = tt+    toListElementWitness = id+    fromListElementWitness = id
+ src/Data/Type/Witness/General/Order.hs view
@@ -0,0 +1,16 @@+module Data.Type.Witness.General.Order where++import Import++data WOrdering (a :: k) (b :: k) where+    WLT :: forall k (a :: k) (b :: k). WOrdering a b+    WEQ :: forall k (a :: k). WOrdering a a+    WGT :: forall k (a :: k) (b :: k). WOrdering a b++wOrderingToOrdering :: WOrdering a b -> Ordering+wOrderingToOrdering WLT = LT+wOrderingToOrdering WEQ = EQ+wOrderingToOrdering WGT = GT++class TestEquality w => TestOrder (w :: k -> Type) where+    testCompare :: forall (a :: k) (b :: k). w a -> w b -> WOrdering a b
+ src/Data/Type/Witness/General/Representative.hs view
@@ -0,0 +1,77 @@+module Data.Type.Witness.General.Representative where++import Data.Type.Witness.General.WitnessValue+import Data.Type.Witness.Specific.Some+import Import++isWitnessRepresentative :: Dict (Is rep a) -> rep a+isWitnessRepresentative Dict = representative++type Subrepresentative (p :: k -> Type) (q :: k -> Type) = forall (a :: k). p a -> Dict (Is q a)++withSubrepresentative :: Subrepresentative p q -> p a -> (Is q a => r) -> r+withSubrepresentative subrep pa f =+    case subrep pa of+        Dict -> f++type Representative :: forall k. (k -> Type) -> Constraint+class Representative rep where+    -- | Every value is an instance of 'Is'.+    getRepWitness :: Subrepresentative rep rep++instance Representative Proxy where+    getRepWitness Proxy = Dict++withRepresentative :: Representative rep => rep a -> (Is rep a => r) -> r+withRepresentative = withSubrepresentative getRepWitness++-- | If two representatives have the same type, then they have the same value.+type Is :: forall k. (k -> Type) -> k -> Constraint+class Representative rep => Is rep a where+    -- | The representative value for type @a@.+    representative :: rep a++instance Is Proxy a where+    representative = Proxy++getRepresentative :: Is rep a => a -> rep a+getRepresentative _ = representative++rerepresentative :: Is rep a => p a -> rep a+rerepresentative _ = representative++fromRepWitness :: Dict (Is rep a) -> rep a+fromRepWitness Dict = representative++mkSomeOf :: Is rep a => a -> SomeOf rep+mkSomeOf a = MkSomeOf representative a++mkSomeFor :: Is rep a => f a -> SomeFor f rep+mkSomeFor fa = MkSomeFor representative fa++instance Representative ((:~:) (t :: k)) where+    getRepWitness Refl = Dict++instance Is ((:~:) (t :: k)) (t :: k) where+    representative = Refl++instance Representative (Compose Dict c) where+    getRepWitness (Compose Dict) = Dict++instance c t => Is (Compose Dict c) t where+    representative = Compose Dict++typeValue ::+       forall k (rep :: k -> Type) (a :: k). (Is rep a, WitnessValue rep)+    => WitnessValueType rep+typeValue = witnessToValue @k @rep (representative @k @rep @a)++-- | See whether two represented and witnessed types are the same.+matchIs ::+       forall w a b. (TestEquality w, Is w a, Is w b)+    => Maybe (a :~: b)+matchIs = let+    r :: forall t. Is w t+      => w t+    r = representative+    in testEquality (r @a) (r @b)
+ src/Data/Type/Witness/General/TestHetEquality.hs view
@@ -0,0 +1,27 @@+module Data.Type.Witness.General.TestHetEquality+    ( (:~~:)(..)+    , withHRefl+    , hetHomoEq+    , TestHetEquality(..)+    , HetEqual(..)+    ) where++import Import++withHRefl :: forall ka (a :: ka) kb (b :: kb) (r :: Type). a :~~: b -> ((a ~~ b) => r) -> r+withHRefl HRefl r = r++-- | somewhat awkwardly named+hetHomoEq :: forall (k :: Type) (a :: k) (b :: k). a :~~: b -> a :~: b+hetHomoEq HRefl = Refl++class TestHetEquality (w :: forall k. k -> Type) where+    testHetEquality :: forall (ka :: Type) (a :: ka) (kb :: Type) (b :: kb). w a -> w b -> Maybe (a :~~: b)++-- | Equivalent to ':~~:', but can be made an instance of 'TestHetEquality'+type HetEqual :: forall ka. ka -> forall kb. kb -> Type+data HetEqual a b where+    HetRefl :: forall k (a :: k). HetEqual a a++instance forall k (a :: k). TestHetEquality (HetEqual a) where+    testHetEquality HetRefl HetRefl = Just HRefl
+ src/Data/Type/Witness/General/WitnessConstraint.hs view
@@ -0,0 +1,13 @@+module Data.Type.Witness.General.WitnessConstraint where++import Import++type WitnessConstraint :: forall k. (k -> Constraint) -> (k -> Type) -> Constraint+class WitnessConstraint c w where+    witnessConstraint :: forall t. w t -> Dict (c t)++instance WitnessConstraint c (Compose Dict c) where+    witnessConstraint (Compose d) = d++instance c t => WitnessConstraint c ((:~:) t) where+    witnessConstraint Refl = Dict
+ src/Data/Type/Witness/General/WitnessValue.hs view
@@ -0,0 +1,22 @@+module Data.Type.Witness.General.WitnessValue where++import Data.Type.Witness.Specific.Some+import Import++type WitnessValue :: forall k. (k -> Type) -> Constraint+class WitnessValue w where+    type WitnessValueType w :: Type+    witnessToValue :: forall t. w t -> WitnessValueType w+    valueToWitness :: forall r. WitnessValueType w -> (forall t. w t -> r) -> r++someToValue ::+       forall k (w :: k -> Type). WitnessValue w+    => Some w+    -> WitnessValueType w+someToValue (MkSome wt) = witnessToValue wt++valueToSome ::+       forall k (w :: k -> Type). WitnessValue w+    => WitnessValueType w+    -> Some w+valueToSome v = valueToWitness v MkSome
+ src/Data/Type/Witness/Specific/All.hs view
@@ -0,0 +1,56 @@+module Data.Type.Witness.Specific.All where++import Data.Type.Witness.General.WitnessConstraint+import Data.Type.Witness.Specific.Some+import Import++type AllFor :: forall k. (k -> Type) -> (k -> Type) -> Type+newtype AllFor f w = MkAllFor+    { unAllFor :: forall t. w t -> f t+    }++type AllOf :: (Type -> Type) -> Type+newtype AllOf w = MkAllOf+    { unAllOf :: forall t. w t -> t+    }++setAllOf ::+       forall (w :: Type -> Type) (a :: Type). TestEquality w+    => w a+    -> a+    -> AllOf w+    -> AllOf w+setAllOf wa a (MkAllOf wtt) =+    MkAllOf $ \wa' ->+        case testEquality wa wa' of+            Just Refl -> a+            Nothing -> wtt wa'++allForToAllOf :: forall (w :: Type -> Type). AllFor Identity w -> AllOf w+allForToAllOf (MkAllFor wtit) = MkAllOf $ \wt -> runIdentity $ wtit wt++allOfToAllFor :: forall (w :: Type -> Type). AllOf w -> AllFor Identity w+allOfToAllFor (MkAllOf wtt) = MkAllFor $ \wt -> Identity $ wtt wt++allMapSome :: AllFor f w -> SomeFor g w -> SomeFor g f+allMapSome (MkAllFor f) = mapSome f++type UnAllOf :: Type -> Type -> Type+type family UnAllOf aw where+    UnAllOf (AllOf w) = w++splitSomeOfList ::+       forall (w :: Type -> Type). TestEquality w+    => [SomeOf w]+    -> AllFor [] w+splitSomeOfList [] = MkAllFor $ \_ -> []+splitSomeOfList ((MkSomeOf wt t):rr) =+    MkAllFor $ \wt' ->+        case testEquality wt wt' of+            Just Refl -> t : (unAllFor (splitSomeOfList rr) wt')+            Nothing -> unAllFor (splitSomeOfList rr) wt'++allForWitnessConstraint ::+       forall k (c :: k -> Constraint) (w :: k -> Type). WitnessConstraint c w+    => AllFor (Compose Dict c) w+allForWitnessConstraint = MkAllFor $ \wt -> Compose $ witnessConstraint wt
+ src/Data/Type/Witness/Specific/ApplyStack.hs view
@@ -0,0 +1,25 @@+module Data.Type.Witness.Specific.ApplyStack where++import Data.Type.Witness.General.Representative+import Data.Type.Witness.Specific.Concat+import Data.Type.Witness.Specific.List.List+import Import++type ApplyStack :: forall k. [k -> k] -> k -> k+type family ApplyStack f a where+    ApplyStack '[] a = a+    ApplyStack (t ': tt) a = t (ApplyStack tt a)++witApplyConcatRefl ::+       forall k (f1 :: [k -> k]) (f2 :: [k -> k]) (a :: k) w.+       ListType w f1+    -> (ApplyStack (Concat f1 f2) a) :~: (ApplyStack f1 (ApplyStack f2 a))+witApplyConcatRefl NilListType = Refl+witApplyConcatRefl (ConsListType _ lt) =+    case witApplyConcatRefl @k @_ @f2 @a lt of+        Refl -> Refl++applyConcatRefl ::+       forall k (f1 :: [k -> k]) (f2 :: [k -> k]) (a :: k) w. Is (ListType w) f1+    => (ApplyStack (Concat f1 f2) a) :~: (ApplyStack f1 (ApplyStack f2 a))+applyConcatRefl = witApplyConcatRefl @k @f1 @f2 @a $ representative @_ @(ListType w) @f1
+ src/Data/Type/Witness/Specific/Concat.hs view
@@ -0,0 +1,42 @@+module Data.Type.Witness.Specific.Concat where++import Data.Type.Witness.General.Representative+import Data.Type.Witness.Specific.List.List+import Import++type Concat :: forall k. [k] -> [k] -> [k]+type family Concat a b where+    Concat '[] bb = bb+    Concat (a ': aa) bb = a ': (Concat aa bb)++concatEmptyRefl :: ListType w a -> Concat a '[] :~: a+concatEmptyRefl NilListType = Refl+concatEmptyRefl (ConsListType _ la) =+    case concatEmptyRefl la of+        Refl -> Refl++concatIsDict ::+       forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]). (Representative w, Is (ListType w) aa, Is (ListType w) bb)+    => Dict (Is (ListType w) (Concat aa bb))+concatIsDict = let+    build :: forall aa'. ListType w aa' -> Dict (Is (ListType w) (Concat aa' bb))+    build NilListType = Dict+    build (ConsListType wa la) =+        case build la of+            Dict ->+                case getRepWitness wa of+                    Dict -> Dict+    in build $ representative @_ @(ListType w) @aa++withConcatIs ::+       forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r. (Representative w, Is (ListType w) aa, Is (ListType w) bb)+    => (Is (ListType w) (Concat aa bb) => r)+    -> r+withConcatIs call =+    case concatIsDict @k @w @aa @bb of+        Dict -> call++concatListType ::+       forall k (w :: k -> Type) (a :: [k]) (b :: [k]). ListType w a -> ListType w b -> ListType w (Concat a b)+concatListType NilListType lb = lb+concatListType (ConsListType wa la) lb = ConsListType wa $ concatListType la lb
+ src/Data/Type/Witness/Specific/Either.hs view
@@ -0,0 +1,78 @@+module Data.Type.Witness.Specific.Either where++import Data.Type.Witness.General.AllConstraint+import Data.Type.Witness.General.Finite+import Data.Type.Witness.General.ListElement+import Data.Type.Witness.General.WitnessConstraint+import Data.Type.Witness.Specific.All+import Data.Type.Witness.Specific.List.Element+import Data.Type.Witness.Specific.Single+import Import++type EitherType :: forall k. (k -> Type) -> (k -> Type) -> (k -> Type)+data EitherType w1 w2 t+    = LeftType (w1 t)+    | RightType (w2 t)++instance (TestEquality w1, TestEquality w2) => TestEquality (EitherType w1 w2) where+    testEquality (LeftType s1) (LeftType s2) = do+        Refl <- testEquality s1 s2+        return Refl+    testEquality (RightType s1) (RightType s2) = do+        Refl <- testEquality s1 s2+        return Refl+    testEquality _ _ = Nothing++instance (FiniteWitness p, FiniteWitness q) => FiniteWitness (EitherType p q) where+    assembleAllFor getsel =+        (\(MkAllFor p) (MkAllFor q) ->+             MkAllFor $ \wt ->+                 case wt of+                     LeftType rt -> p rt+                     RightType rt -> q rt) <$>+        assembleAllFor (getsel . LeftType) <*>+        assembleAllFor (getsel . RightType)++instance (WitnessConstraint c p, WitnessConstraint c q) => WitnessConstraint c (EitherType p q) where+    witnessConstraint (LeftType rt) =+        case witnessConstraint @_ @c rt of+            Dict -> Dict+    witnessConstraint (RightType rt) =+        case witnessConstraint @_ @c rt of+            Dict -> Dict++instance (Show (p t), Show (q t)) => Show (EitherType p q t) where+    show (LeftType rt) = show rt+    show (RightType rt) = show rt++instance (AllConstraint Show p, AllConstraint Show q) => AllConstraint Show (EitherType p q) where+    allConstraint :: forall t. Dict (Show (EitherType p q t))+    allConstraint =+        case allConstraint @_ @_ @Show @p @t of+            Dict ->+                case allConstraint @_ @_ @Show @q @t of+                    Dict -> Dict++eitherAllOf :: AllOf sel1 -> AllOf sel2 -> AllOf (EitherType sel1 sel2)+eitherAllOf (MkAllOf tup1) (MkAllOf tup2) =+    MkAllOf $ \esel ->+        case esel of+            LeftType sel -> tup1 sel+            RightType sel -> tup2 sel++eitherAllFor :: AllFor f sel1 -> AllFor f sel2 -> AllFor f (EitherType sel1 sel2)+eitherAllFor (MkAllFor tup1) (MkAllFor tup2) =+    MkAllFor $ \esel ->+        case esel of+            LeftType sel -> tup1 sel+            RightType sel -> tup2 sel++type ConsType :: forall k. k -> (k -> Type) -> k -> Type+type ConsType a = EitherType (SingleType a)++instance ListElementWitness lt => ListElementWitness (ConsType a lt) where+    type WitnessTypeList (ConsType a lt) = a : (WitnessTypeList lt)+    toListElementWitness (LeftType Refl) = FirstElementType+    toListElementWitness (RightType sel) = RestElementType $ toListElementWitness sel+    fromListElementWitness FirstElementType = LeftType Refl+    fromListElementWitness (RestElementType lt) = RightType $ fromListElementWitness lt
+ src/Data/Type/Witness/Specific/Empty.hs view
@@ -0,0 +1,44 @@+module Data.Type.Witness.Specific.Empty where++import Data.Type.Witness.General.Finite+import Data.Type.Witness.General.ListElement+import Data.Type.Witness.General.Order+import Data.Type.Witness.General.Representative+import Data.Type.Witness.General.WitnessConstraint+import Data.Type.Witness.Specific.All+import Import++type EmptyType :: forall k. k -> Type+newtype EmptyType t =+    MkEmptyType Void+    deriving (Eq, Countable, Searchable, Empty)++instance Finite (EmptyType t) where+    allValues = []+    assemble _ = pure never++instance TestEquality EmptyType where+    testEquality = never++instance TestOrder EmptyType where+    testCompare = never++instance Representative EmptyType where+    getRepWitness = never++instance FiniteWitness EmptyType where+    assembleAllFor _ = pure emptyAllFor++instance WitnessConstraint c EmptyType where+    witnessConstraint = never++instance ListElementWitness EmptyType where+    type WitnessTypeList EmptyType = '[]+    toListElementWitness wit = never wit+    fromListElementWitness lt = never lt++emptyAllOf :: AllOf EmptyType+emptyAllOf = MkAllOf never++emptyAllFor :: AllFor f EmptyType+emptyAllFor = MkAllFor never
+ src/Data/Type/Witness/Specific/FiniteAllFor.hs view
@@ -0,0 +1,34 @@+module Data.Type.Witness.Specific.FiniteAllFor where++import Data.Type.Witness.General.Finite+import Data.Type.Witness.Specific.All+import Data.Type.Witness.Specific.Either+import Data.Type.Witness.Specific.Some+import Import++type FiniteAllFor :: forall k. (k -> Type) -> (k -> Type) -> Type+data FiniteAllFor f w = MkFiniteAllFor+    { finiteDomain :: [Some w]+    , finiteGetAllFor :: forall t. w t -> f t+    }++finiteAllFor :: FiniteAllFor f w -> AllFor f w+finiteAllFor (MkFiniteAllFor _ f) = MkAllFor f++finiteCodomain :: FiniteAllFor f w -> [Some f]+finiteCodomain sw = fmap (\(MkSome st) -> MkSome $ finiteGetAllFor sw st) $ finiteDomain sw++mapFiniteAllFor :: (forall t. f1 t -> f2 t) -> FiniteAllFor f1 w -> FiniteAllFor f2 w+mapFiniteAllFor ff (MkFiniteAllFor ai i) = MkFiniteAllFor ai $ \s -> ff $ i s++eitherFiniteAllFor :: FiniteAllFor t w1 -> FiniteAllFor t w2 -> FiniteAllFor t (EitherType w1 w2)+eitherFiniteAllFor (MkFiniteAllFor a1 i1) (MkFiniteAllFor a2 i2) =+    MkFiniteAllFor+        ((fmap (mapSome LeftType) a1) ++ (fmap (mapSome RightType) a2))+        (unAllFor $ eitherAllFor (MkAllFor i1) (MkAllFor i2))++mkFiniteAllFor ::+       forall f w. FiniteWitness w+    => (forall t. w t -> f t)+    -> FiniteAllFor f w+mkFiniteAllFor = MkFiniteAllFor allWitnesses
+ src/Data/Type/Witness/Specific/List/Element.hs view
@@ -0,0 +1,59 @@+module Data.Type.Witness.Specific.List.Element where++import Data.Type.Witness.General.Order+import Data.Type.Witness.Specific.List.List+import Import++type ListElementType :: forall k. [k] -> k -> Type+data ListElementType kk t where+    FirstElementType :: ListElementType (t : tt) t+    RestElementType :: ListElementType aa t -> ListElementType (a : aa) t++instance TestEquality (ListElementType tt) where+    testEquality FirstElementType FirstElementType = Just Refl+    testEquality (RestElementType lt1) (RestElementType lt2) = do+        Refl <- testEquality lt1 lt2+        return Refl+    testEquality _ _ = Nothing++instance TestOrder (ListElementType tt) where+    testCompare FirstElementType FirstElementType = WEQ+    testCompare (RestElementType a) (RestElementType b) =+        case testCompare a b of+            WLT -> WLT+            WGT -> WGT+            WEQ -> WEQ+    testCompare (RestElementType _) FirstElementType = WGT+    testCompare FirstElementType (RestElementType _) = WLT++instance Searchable (ListElementType '[] t) where+    search = finiteSearch++instance Eq (ListElementType tt t) where+    lt1 == lt2 = isJust $ testEquality lt1 lt2++instance Countable (ListElementType '[] t) where+    countPrevious = finiteCountPrevious+    countMaybeNext = finiteCountMaybeNext++instance Finite (ListElementType '[] t) where+    allValues = []++instance Empty (ListElementType '[] t) where+    never lt = case lt of {}++lookUpListElement ::+       forall k (w :: k -> Type) (t :: k) (lt :: [k]). TestEquality w+    => w t+    -> ListType w lt+    -> Maybe (ListElementType lt t)+lookUpListElement _ NilListType = Nothing+lookUpListElement wt (ConsListType wt' _)+    | Just Refl <- testEquality wt wt' = Just FirstElementType+lookUpListElement wt (ConsListType _ lt) = do+    et <- lookUpListElement wt lt+    return $ RestElementType et++countListType :: ListType w lt -> ListType (ListElementType lt) lt+countListType NilListType = NilListType+countListType (ConsListType _ lt) = ConsListType FirstElementType (mapListType RestElementType $ countListType lt)
+ src/Data/Type/Witness/Specific/List/List.hs view
@@ -0,0 +1,84 @@+module Data.Type.Witness.Specific.List.List where++import Data.Type.Witness.General.Representative+import Data.Type.Witness.Specific.Pair+import Data.Type.Witness.Specific.Some+import Import++-- | a witness type for lists of types+-- The @w@ parameter is the witness type of the elements.+type ListType :: (k -> Type) -> ([k] -> Type)+data ListType w lt where+    NilListType :: ListType w '[]+    ConsListType :: w a -> ListType w lt -> ListType w (a : lt)++instance Representative w => Representative (ListType w) where+    getRepWitness NilListType = Dict+    getRepWitness (ConsListType w lw) =+        case (getRepWitness w, getRepWitness lw) of+            (Dict, Dict) -> Dict++instance Representative w => Is (ListType w) '[] where+    representative = NilListType++instance (Is w a, Is (ListType w) lt) => Is (ListType w) (a : lt) where+    representative = ConsListType representative representative++instance TestEquality w => TestEquality (ListType w) where+    testEquality NilListType NilListType = Just Refl+    testEquality (ConsListType wpa wpb) (ConsListType wqa wqb) = do+        Refl <- testEquality wpa wqa+        Refl <- testEquality wpb wqb+        return Refl+    testEquality _ _ = Nothing++instance (forall a. Show (w a)) => Show (ListType w lt) where+    show s = "[" <> intercalate "," (showAll s) <> "]"+      where+        showAll :: forall t. ListType w t -> [String]+        showAll NilListType = []+        showAll (ConsListType t1 tr) = show t1 : showAll tr++assembleListType :: [Some w] -> Some (ListType w)+assembleListType [] = MkSome NilListType+assembleListType ((MkSome wa):ww) =+    case assembleListType ww of+        MkSome wwa -> MkSome $ ConsListType wa wwa++mapMListType :: Applicative m => (forall t'. wita t' -> m (witb t')) -> ListType wita t -> m (ListType witb t)+mapMListType _ff NilListType = pure NilListType+mapMListType ff (ConsListType t tt) = ConsListType <$> ff t <*> mapMListType ff tt++joinMListType ::+       Applicative m+    => (forall t'. wita t' -> witb t' -> m (witc t'))+    -> ListType wita t+    -> ListType witb t+    -> m (ListType witc t)+joinMListType _ff NilListType NilListType = pure NilListType+joinMListType ff (ConsListType t1 t1t) (ConsListType t2 t2t) = ConsListType <$> ff t1 t2 <*> joinMListType ff t1t t2t++mapListType :: (forall t'. wita t' -> witb t') -> ListType wita t -> ListType witb t+mapListType ff l = runIdentity $ mapMListType (\wt -> Identity $ ff wt) l++joinListType :: (forall t'. wita t' -> witb t' -> witc t') -> ListType wita t -> ListType witb t -> ListType witc t+joinListType ff la lb = runIdentity $ joinMListType (\wta wtb -> Identity $ ff wta wtb) la lb++pairListType :: ListType wita t -> ListType witb t -> ListType (PairType wita witb) t+pairListType = joinListType MkPairType++listTypeLength :: ListType w lt -> Int+listTypeLength NilListType = 0+listTypeLength (ConsListType _ lt) = succ $ listTypeLength lt++listTypeToList :: (forall a. w a -> r) -> ListType w t -> [r]+listTypeToList _wr NilListType = []+listTypeToList wr (ConsListType wa rest) = (wr wa) : (listTypeToList wr rest)++listTypeFor :: Applicative m => ListType w t -> (forall a. w a -> m r) -> m [r]+listTypeFor NilListType _ = pure []+listTypeFor (ConsListType t tt) f = liftA2 (:) (f t) $ listTypeFor tt f++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
+ src/Data/Type/Witness/Specific/List/Product.hs view
@@ -0,0 +1,90 @@+module Data.Type.Witness.Specific.List.Product where++import Data.Type.Witness.General.Representative+import Data.Type.Witness.General.WitnessConstraint+import Data.Type.Witness.Specific.List.Element+import Data.Type.Witness.Specific.List.List+import Import+import Unsafe.Coerce++type ListProduct :: [Type] -> Type+type family ListProduct w = r | r -> w where+    ListProduct '[] = ()+    ListProduct (t : tt) = (t, ListProduct tt)++-- | workaround for https://gitlab.haskell.org/ghc/ghc/issues/10833+injectiveListProduct ::+       forall (a :: [Type]) (b :: [Type]). ListProduct a ~ ListProduct b+    => a :~: b+injectiveListProduct = unsafeCoerce Refl++listProductEq :: (forall a. w a -> Dict (Eq a)) -> ListType w t -> Dict (Eq (ListProduct t))+listProductEq _ NilListType = Dict+listProductEq f (ConsListType t tt) =+    case (f t, listProductEq f tt) of+        (Dict, Dict) -> Dict++listProductShow :: (forall a. w a -> Dict (Show a)) -> ListType w t -> Dict (Show (ListProduct t))+listProductShow _ NilListType = Dict+listProductShow f (ConsListType t tt) =+    case (f t, listProductShow f tt) of+        (Dict, Dict) -> Dict++fillListProduct :: ListType w t -> (forall a. w a -> a) -> ListProduct t+fillListProduct NilListType _f = ()+fillListProduct (ConsListType wa wr) f = (f wa, fillListProduct wr f)++mapListProduct :: ListType w t -> (forall a. w a -> a -> a) -> ListProduct t -> ListProduct t+mapListProduct NilListType _f () = ()+mapListProduct (ConsListType wa wr) f (a, rest) = (f wa a, mapListProduct wr f rest)++lift2ListProduct :: ListType w t -> (forall a. w a -> a -> a -> a) -> ListProduct t -> ListProduct t -> ListProduct t+lift2ListProduct NilListType _f () () = ()+lift2ListProduct (ConsListType wa wr) f (a, resta) (b, restb) = (f wa a b, lift2ListProduct wr f resta restb)++identityListProduct :: ListType Identity lt -> ListProduct lt+identityListProduct NilListType = ()+identityListProduct (ConsListType (Identity a) rest) = (a, identityListProduct rest)++sequenceListProduct :: Applicative f => ListType f lt -> f (ListProduct lt)+sequenceListProduct NilListType = pure ()+sequenceListProduct (ConsListType fa rest) = liftA2 (,) fa (sequenceListProduct rest)++listProductGetElement :: ListElementType list t -> ListProduct list -> t+listProductGetElement FirstElementType = fst -- using fst and snd for irrefutable matching+listProductGetElement (RestElementType lw) = listProductGetElement lw . snd++listProductPutElement :: ListElementType list t -> t -> ListProduct list -> ListProduct list+listProductPutElement FirstElementType t (_, r) = (t, r)+listProductPutElement (RestElementType lw) t (a, r) = (a, listProductPutElement lw t r)++listProductModifyElement :: ListElementType list t -> (t -> t) -> ListProduct list -> ListProduct list+listProductModifyElement n aa t = listProductPutElement n (aa (listProductGetElement n t)) t++type ListProductType :: (Type -> Type) -> (Type -> Type)+data ListProductType wit t where+    MkListProductType+        :: forall (wit :: Type -> Type) (lt :: [Type]). ListType wit lt -> ListProductType wit (ListProduct lt)++instance TestEquality wit => TestEquality (ListProductType wit) where+    testEquality (MkListProductType lt1) (MkListProductType lt2) =+        case testEquality lt1 lt2 of+            Just Refl -> Just Refl+            Nothing -> Nothing++instance WitnessConstraint Eq w => WitnessConstraint Eq (ListProductType w) where+    witnessConstraint (MkListProductType lt) = listProductEq witnessConstraint lt++instance Representative w => Representative (ListProductType w) where+    getRepWitness (MkListProductType NilListType) = Dict+    getRepWitness (MkListProductType (ConsListType a ar)) =+        case (getRepWitness a, getRepWitness $ MkListProductType ar) of+            (Dict, Dict) -> Dict++instance Representative w => Is (ListProductType w) () where+    representative = MkListProductType NilListType++instance (Is w a, Is (ListProductType w) ar) => Is (ListProductType w) (a, ar) where+    representative =+        case representative @_ @(ListProductType w) @ar of+            MkListProductType r -> MkListProductType $ ConsListType representative r
+ src/Data/Type/Witness/Specific/List/Sum.hs view
@@ -0,0 +1,62 @@+module Data.Type.Witness.Specific.List.Sum where++import Data.Type.Witness.General.Representative+import Data.Type.Witness.General.WitnessConstraint+import Data.Type.Witness.Specific.List.List+import Import+import Unsafe.Coerce++type ListSum :: [Type] -> Type+type family ListSum w = r | r -> w where+    ListSum '[] = Void+    ListSum (t : tt) = Either t (ListSum tt)++-- | workaround for https://gitlab.haskell.org/ghc/ghc/issues/10833+injectiveListSum ::+       forall (a :: [Type]) (b :: [Type]). ListSum a ~ ListSum b+    => a :~: b+injectiveListSum = unsafeCoerce Refl++listSumEq :: (forall a. w a -> Dict (Eq a)) -> ListType w t -> Dict (Eq (ListSum t))+listSumEq _ NilListType = Dict+listSumEq f (ConsListType t tt) =+    case (f t, listSumEq f tt) of+        (Dict, Dict) -> Dict++listSumShow :: (forall a. w a -> Dict (Show a)) -> ListType w t -> Dict (Show (ListSum t))+listSumShow _ NilListType = Dict+listSumShow f (ConsListType t tt) =+    case (f t, listSumShow f tt) of+        (Dict, Dict) -> Dict++mapListSum :: ListType w t -> (forall a. w a -> a -> a) -> ListSum t -> ListSum t+mapListSum NilListType _f v = v+mapListSum (ConsListType wa _wr) f (Left a) = Left $ f wa a+mapListSum (ConsListType _wa wr) f (Right rest) = Right $ mapListSum wr f rest++type ListSumType :: (Type -> Type) -> (Type -> Type)+data ListSumType wit t where+    MkListSumType :: forall (wit :: Type -> Type) (lt :: [Type]). ListType wit lt -> ListSumType wit (ListSum lt)++instance TestEquality wit => TestEquality (ListSumType wit) where+    testEquality (MkListSumType lt1) (MkListSumType lt2) =+        case testEquality lt1 lt2 of+            Just Refl -> Just Refl+            Nothing -> Nothing++instance WitnessConstraint Eq w => WitnessConstraint Eq (ListSumType w) where+    witnessConstraint (MkListSumType lt) = listSumEq witnessConstraint lt++instance Representative w => Representative (ListSumType w) where+    getRepWitness (MkListSumType NilListType) = Dict+    getRepWitness (MkListSumType (ConsListType a ar)) =+        case (getRepWitness a, getRepWitness $ MkListSumType ar) of+            (Dict, Dict) -> Dict++instance Representative w => Is (ListSumType w) Void where+    representative = MkListSumType NilListType++instance (Is w a, Is (ListSumType w) ar) => Is (ListSumType w) (Either a ar) where+    representative =+        case representative @_ @(ListSumType w) @ar of+            MkListSumType r -> MkListSumType $ ConsListType representative r
+ src/Data/Type/Witness/Specific/Natural.hs view
@@ -0,0 +1,91 @@+module Data.Type.Witness.Specific.Natural+    ( KnownNat+    , type (<=)+    , type (+)+    , type (*)+    , type (^)+    , type (-)+    , CmpNat+    , Div+    , Mod+    , Log2+    , Nat+    , NaturalType(..)+    , zeroNaturalType+    , succNaturalType+    , addNaturalType+    , multiplyNaturalType+    , PeanoToNatural+    , peanoToNaturalType+    ) where++import Data.PeanoNat+import Data.Type.Witness.General.AllConstraint+import Data.Type.Witness.General.Order+import Data.Type.Witness.General.Representative+import Data.Type.Witness.General.WitnessValue+import Data.Type.Witness.Specific.PeanoNat+import GHC.TypeNats+import Import+import Numeric.Natural+import Unsafe.Coerce++type NaturalType :: Nat -> Type+data NaturalType bn where+    MkNaturalType :: KnownNat bn => NaturalType bn++instance WitnessValue NaturalType where+    type WitnessValueType NaturalType = Natural+    witnessToValue :: forall t. NaturalType t -> Natural+    witnessToValue MkNaturalType = natVal (Proxy :: Proxy t)+    valueToWitness i cont =+        case someNatVal i of+            SomeNat p -> let+                psw :: forall (t :: Nat). KnownNat t+                    => Proxy t+                    -> NaturalType t+                psw _ = MkNaturalType+                in cont $ psw p++instance TestEquality NaturalType where+    testEquality (MkNaturalType :: NaturalType a) (MkNaturalType :: NaturalType b) = sameNat (Proxy @a) (Proxy @b)++instance TestOrder NaturalType where+    testCompare a b =+        case testEquality a b of+            Just Refl -> WEQ+            Nothing ->+                if witnessToValue a > witnessToValue b+                    then WGT+                    else WLT++instance Representative NaturalType where+    getRepWitness MkNaturalType = Dict++instance KnownNat bn => Is NaturalType bn where+    representative = MkNaturalType++instance Show (NaturalType bn) where+    show = show . witnessToValue++instance AllConstraint Show NaturalType where+    allConstraint = Dict++unsafeNaturalType :: forall n. Natural -> NaturalType n+unsafeNaturalType i = valueToWitness i $ \(nt :: NaturalType t) -> unsafeCoerce @(NaturalType t) @(NaturalType n) nt++zeroNaturalType :: NaturalType 0+zeroNaturalType = MkNaturalType++succNaturalType :: NaturalType a -> NaturalType (a + 1)+succNaturalType a = unsafeNaturalType $ succ $ witnessToValue a++addNaturalType :: NaturalType a -> NaturalType b -> NaturalType (a + b)+addNaturalType a b = unsafeNaturalType $ witnessToValue a + witnessToValue b++multiplyNaturalType :: NaturalType a -> NaturalType b -> NaturalType (a * b)+multiplyNaturalType a b = unsafeNaturalType $ witnessToValue a * witnessToValue b++peanoToNaturalType :: PeanoNatType pn -> NaturalType (PeanoToNatural pn)+peanoToNaturalType ZeroType = zeroNaturalType+peanoToNaturalType (SuccType n) = succNaturalType $ peanoToNaturalType n
+ src/Data/Type/Witness/Specific/Pair.hs view
@@ -0,0 +1,32 @@+module Data.Type.Witness.Specific.Pair where++import Data.Type.Witness.General.Order+import Data.Type.Witness.General.Representative+import Data.Type.Witness.General.WitnessConstraint+import Import++-- | a witness for pairs of witnesses+type PairType :: (k -> Type) -> (k -> Type) -> (k -> Type)+data PairType w1 w2 t =+    MkPairType (w1 t)+               (w2 t)++instance (Representative w1, Representative w2) => Representative (PairType w1 w2) where+    getRepWitness (MkPairType w1 w2) =+        case (getRepWitness w1, getRepWitness w2) of+            (Dict, Dict) -> Dict++instance (Is w1 t, Is w2 t) => Is (PairType w1 w2) t where+    representative = MkPairType representative representative++-- | left-biased+instance TestEquality w1 => TestEquality (PairType w1 w2) where+    testEquality (MkPairType a1 _) (MkPairType b1 _) = testEquality a1 b1++-- | left-biased+instance TestOrder w1 => TestOrder (PairType w1 w2) where+    testCompare (MkPairType a1 _) (MkPairType b1 _) = testCompare a1 b1++-- | right-biased+instance WitnessConstraint c w2 => WitnessConstraint c (PairType w1 w2) where+    witnessConstraint (MkPairType _ w2) = witnessConstraint w2
+ src/Data/Type/Witness/Specific/PeanoNat.hs view
@@ -0,0 +1,96 @@+module Data.Type.Witness.Specific.PeanoNat where++import Data.PeanoNat+import Data.Type.Witness.General.Order+import Data.Type.Witness.General.Representative+import Data.Type.Witness.General.WitnessValue+import Import++type PeanoNatType :: PeanoNat -> Type+data PeanoNatType t where+    ZeroType :: PeanoNatType 'Zero+    SuccType :: PeanoNatType t -> PeanoNatType ('Succ t)++instance TestEquality PeanoNatType where+    testEquality ZeroType ZeroType = return Refl+    testEquality (SuccType a) (SuccType b) = do+        Refl <- testEquality a b+        return Refl+    testEquality _ _ = Nothing++instance TestOrder PeanoNatType where+    testCompare ZeroType ZeroType = WEQ+    testCompare (SuccType a) (SuccType b) =+        case testCompare a b of+            WLT -> WLT+            WGT -> WGT+            WEQ -> WEQ+    testCompare (SuccType _) ZeroType = WGT+    testCompare ZeroType (SuccType _) = WLT++instance Representative PeanoNatType where+    getRepWitness ZeroType = Dict+    getRepWitness (SuccType n) =+        case getRepWitness n of+            Dict -> Dict++instance Is PeanoNatType 'Zero where+    representative = ZeroType++instance Is PeanoNatType n => Is PeanoNatType ('Succ n) where+    representative = SuccType representative++instance WitnessValue PeanoNatType where+    type WitnessValueType PeanoNatType = PeanoNat+    witnessToValue :: forall t. PeanoNatType t -> PeanoNat+    witnessToValue ZeroType = Zero+    witnessToValue (SuccType n) = Succ $ witnessToValue n+    valueToWitness Zero cont = cont ZeroType+    valueToWitness (Succ n) cont = valueToWitness n $ \t -> cont $ SuccType t++type GreaterEqual :: PeanoNat -> PeanoNat -> Type+data GreaterEqual a b where+    ZeroGreaterEqual :: GreaterEqual a 'Zero+    SuccGreaterEqual :: GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b)++samePeanoGreaterEqual :: PeanoNatType a -> GreaterEqual a a+samePeanoGreaterEqual ZeroType = ZeroGreaterEqual+samePeanoGreaterEqual (SuccType a) = SuccGreaterEqual $ samePeanoGreaterEqual a++diff1GreaterEqual :: GreaterEqual a b -> GreaterEqual ('Succ a) b+diff1GreaterEqual ZeroGreaterEqual = ZeroGreaterEqual+diff1GreaterEqual (SuccGreaterEqual ge) = SuccGreaterEqual $ diff1GreaterEqual ge++peanoGreaterEqual :: PeanoNatType a -> PeanoNatType b -> Maybe (GreaterEqual a b)+peanoGreaterEqual _ ZeroType = return ZeroGreaterEqual+peanoGreaterEqual ZeroType _ = Nothing+peanoGreaterEqual (SuccType a) (SuccType b) = do+    al <- peanoGreaterEqual a b+    return $ SuccGreaterEqual al++addPeanoNatType :: PeanoNatType a -> PeanoNatType b -> PeanoNatType (Add a b)+addPeanoNatType ZeroType b = b+addPeanoNatType (SuccType a) b = SuccType $ addPeanoNatType a b++addZeroPeanoNatTypeEqual :: PeanoNatType a -> Add a 'Zero :~: a+addZeroPeanoNatTypeEqual ZeroType = Refl+addZeroPeanoNatTypeEqual (SuccType a) =+    case addZeroPeanoNatTypeEqual a of+        Refl -> Refl++succAddPeanoNatTypeEqual' :: forall a b. PeanoNatType a -> 'Succ (Add a b) :~: Add a ('Succ b)+succAddPeanoNatTypeEqual' ZeroType = Refl+succAddPeanoNatTypeEqual' (SuccType a) =+    case succAddPeanoNatTypeEqual' @_ @b a of+        Refl -> Refl++succAddPeanoNatTypeEqual :: forall a b. PeanoNatType a -> PeanoNatType b -> 'Succ (Add a b) :~: Add a ('Succ b)+succAddPeanoNatTypeEqual a _ = succAddPeanoNatTypeEqual' @a @b a++addPeanoNatTypeGE :: PeanoNatType a -> PeanoNatType b -> GreaterEqual (Add a b) a+addPeanoNatTypeGE a ZeroType =+    case addZeroPeanoNatTypeEqual a of+        Refl -> samePeanoGreaterEqual a+addPeanoNatTypeGE a (SuccType b) =+    case succAddPeanoNatTypeEqual a b of+        Refl -> diff1GreaterEqual $ addPeanoNatTypeGE a b
+ src/Data/Type/Witness/Specific/Single.hs view
@@ -0,0 +1,15 @@+{-# OPTIONS -fno-warn-orphans #-}++module Data.Type.Witness.Specific.Single where++import Data.Type.Witness.Specific.All+import Import++type SingleType :: forall k. k -> k -> Type+type SingleType = (:~:)++singleAllOf :: t -> AllOf (SingleType t)+singleAllOf t = MkAllOf $ \Refl -> t++getSingleAllOf :: AllOf (SingleType t) -> t+getSingleAllOf (MkAllOf f) = f Refl
+ src/Data/Type/Witness/Specific/Some.hs view
@@ -0,0 +1,75 @@+module Data.Type.Witness.Specific.Some where++import Data.Type.Witness.General.AllConstraint+import Data.Type.Witness.General.Order+import Data.Type.Witness.General.WitnessConstraint+import Import++-- | Any value with a witness to a parameter of its type.+type SomeFor :: forall k. (k -> Type) -> (k -> Type) -> Type+data SomeFor f w =+    forall a. MkSomeFor (w a)+                        (f a)++mapSome ::+       forall k (g :: k -> Type) (w1 :: k -> Type) (w2 :: k -> Type).+       (forall t. w1 t -> w2 t)+    -> SomeFor g w1+    -> SomeFor g w2+mapSome f (MkSomeFor wt gt) = MkSomeFor (f wt) gt++matchSomeFor :: TestEquality w => w a -> SomeFor f w -> Maybe (f a)+matchSomeFor wit (MkSomeFor cwit cfa) = do+    Refl <- testEquality cwit wit+    return cfa++type SomeOf :: (Type -> Type) -> Type+type SomeOf = SomeFor Identity++pattern MkSomeOf :: w a -> a -> SomeOf w++pattern MkSomeOf wa a = MkSomeFor wa (Identity a)++{-# COMPLETE MkSomeOf #-}++instance (TestEquality w, WitnessConstraint Eq w) => Eq (SomeOf w) where+    MkSomeOf wa a == MkSomeOf wb b =+        case testEquality wa wb of+            Nothing -> False+            Just Refl ->+                case witnessConstraint @_ @Eq wa of+                    Dict -> a == b++matchSomeOf ::+       forall (w :: Type -> Type) (a :: Type). TestEquality w+    => w a+    -> SomeOf w+    -> Maybe a+matchSomeOf wit av = do+    Identity a <- matchSomeFor wit av+    return a++type Some :: forall k. (k -> Type) -> Type+type Some = SomeFor (Const ())++pattern MkSome :: w a -> Some w++pattern MkSome wa = MkSomeFor wa (Const ())++{-# COMPLETE MkSome #-}++matchSome ::+       forall k (w :: k -> Type) (a :: k). TestEquality w+    => w a+    -> Some w+    -> Bool+matchSome wit aw = isJust $ matchSomeFor wit aw++instance forall k (w :: k -> Type). TestEquality w => Eq (Some w) where+    (==) (MkSome wa) = matchSome wa++instance forall k (w :: k -> Type). TestOrder w => Ord (Some w) where+    compare (MkSome wa) (MkSome wb) = wOrderingToOrdering $ testCompare wa wb++instance forall k (w :: k -> Type). AllConstraint Show w => Show (Some w) where+    show (MkSome wa) = allShow wa
+ src/Data/Type/Witness/Specific/Symbol.hs view
@@ -0,0 +1,53 @@+module Data.Type.Witness.Specific.Symbol+    ( module Data.Type.Witness.Specific.Symbol+    , Symbol+    , KnownSymbol+    ) where++import Data.Type.Witness.General.AllConstraint+import Data.Type.Witness.General.Order+import Data.Type.Witness.General.Representative+import Data.Type.Witness.General.WitnessValue+import GHC.TypeLits+import Import++type SymbolType :: Symbol -> Type+data SymbolType symbol where+    MkSymbolType :: KnownSymbol symbol => SymbolType symbol++instance WitnessValue SymbolType where+    type WitnessValueType SymbolType = String+    witnessToValue :: forall t. SymbolType t -> String+    witnessToValue MkSymbolType = symbolVal (Proxy :: Proxy t)+    valueToWitness s cont =+        case someSymbolVal s of+            SomeSymbol p -> let+                psw :: forall (t :: Symbol). KnownSymbol t+                    => Proxy t+                    -> SymbolType t+                psw _ = MkSymbolType+                in cont $ psw p++instance TestEquality SymbolType where+    testEquality (MkSymbolType :: SymbolType a) (MkSymbolType :: SymbolType b) = sameSymbol (Proxy @a) (Proxy @b)++instance TestOrder SymbolType where+    testCompare a b =+        case testEquality a b of+            Just Refl -> WEQ+            Nothing ->+                if witnessToValue a > witnessToValue b+                    then WGT+                    else WLT++instance Representative SymbolType where+    getRepWitness MkSymbolType = Dict++instance KnownSymbol symbol => Is SymbolType symbol where+    representative = MkSymbolType++instance Show (SymbolType symbol) where+    show = witnessToValue++instance AllConstraint Show SymbolType where+    allConstraint = Dict
+ src/Data/Type/Witness/Specific/WitnessMap/For.hs view
@@ -0,0 +1,65 @@+module Data.Type.Witness.Specific.WitnessMap.For where++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 WitnessMapFor :: forall k. (k -> Type) -> (k -> Type) -> Type+newtype WitnessMapFor f w =+    MkWitnessMapFor [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 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 wit amap (MkWitnessMapFor cells) =+    MkWitnessMapFor (replaceFirst ((fmap ((MkSomeFor wit) . amap)) . (matchSomeFor wit)) cells)+  where+    replaceFirst :: (a -> Maybe a) -> [a] -> [a]+    replaceFirst ama (a:aa) =+        case ama a of+            Just newa -> (newa : aa)+            _ -> a : (replaceFirst ama aa)+    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 wit newfa = witnessMapForModify wit (const newfa)++-- | Add a witness and value as the first entry in the dictionary.+witnessMapForAdd :: w a -> f a -> WitnessMapFor f w -> WitnessMapFor f w+witnessMapForAdd wit fa (MkWitnessMapFor cells) = MkWitnessMapFor ((MkSomeFor wit fa) : cells)++-- | A dictionary for a single witness and value+witnessMapForSingle :: w a -> f a -> WitnessMapFor f w+witnessMapForSingle wit fa = MkWitnessMapFor $ pure $ MkSomeFor wit fa++witnessMapForFold :: Monoid m => WitnessMapFor f w -> (forall a. w a -> f a -> m) -> m+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 wit (MkWitnessMapFor cells) =+    MkWitnessMapFor (removeFirst (\(MkSomeFor cwit _) -> isJust (testEquality wit cwit)) cells)+  where+    removeFirst :: (a -> Bool) -> [a] -> [a]+    removeFirst p (a:as)+        | p a = as+    removeFirst p (a:as) = a : (removeFirst p as)+    removeFirst _ _ = []++-- | Create a dictionary from a list of witness\/value pairs+witnessMapForFromList :: [SomeFor f w] -> WitnessMapFor f w+witnessMapForFromList = MkWitnessMapFor++witnessMapForMapM :: Applicative m => (forall a. f a -> m (g a)) -> WitnessMapFor f w -> m (WitnessMapFor g w)+witnessMapForMapM fmg (MkWitnessMapFor cells) =+    fmap MkWitnessMapFor $ for cells $ \(MkSomeFor wit fa) -> fmap (MkSomeFor wit) $ fmg fa
+ src/Data/Type/Witness/Specific/WitnessMap/Of.hs view
@@ -0,0 +1,44 @@+module Data.Type.Witness.Specific.WitnessMap.Of where++import Data.Type.Witness.Specific.Some+import Data.Type.Witness.Specific.WitnessMap.For+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 WitnessMapOf :: (Type -> Type) -> Type+type WitnessMapOf = WitnessMapFor Identity++-- | An empty dictionary.+emptyWitnessMapOf :: WitnessMapOf w+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 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 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 wit newa = witnessMapOfModify wit $ const newa++witnessMapOfSingle :: w a -> a -> WitnessMapOf w+witnessMapOfSingle wit a = witnessMapForSingle wit $ Identity a++witnessMapOfFold :: Monoid m => WitnessMapOf w -> (forall a. w a -> a -> m) -> m+witnessMapOfFold d f = witnessMapForFold d $ \wa (Identity a) -> f wa a++-- | Add a witness and value as the first entry in the dictionary.+witnessMapOfAdd :: w a -> a -> WitnessMapOf w -> WitnessMapOf w+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 = witnessMapForRemove++-- | Create a dictionary from a list of witness\/value pairs+witnessMapOfFromList :: [SomeOf w] -> WitnessMapOf w+witnessMapOfFromList = MkWitnessMapFor
− src/Data/Witness.hs 
@@ -1,44 +0,0 @@-module Data.Witness-    ( module I-    , module Data.Witness-    ) where--import Data.Nat as I-import Data.Proxy as I-import Data.Type.Apply as I-import Data.Type.Equality as I-import Data.Type.Heterogeneous as I-import Data.Type.With as I-import Data.Witness.All as I-import Data.Witness.Any as I-import Data.Witness.ApplyStack as I-import Data.Witness.BigNat as I-import Data.Witness.Concat as I-import Data.Witness.Cons as I-import Data.Witness.Constraint as I-import Data.Witness.Either as I-import Data.Witness.Finite as I-import Data.Witness.HList as I-import Data.Witness.Kind as I-import Data.Witness.List as I-import Data.Witness.ListElement as I-import Data.Witness.Nat as I-import Data.Witness.Representative as I-import Data.Witness.Single as I-import Data.Witness.Submap as I-import Data.Witness.Symbol as I-import Data.Witness.WitnessDict as I-import Data.Witness.WitnessFDict as I-import Data.Witness.WitnessValue as I-import Prelude---- | See whether two represented and witnessed types are the same.-matchIs ::-       forall w a b. (TestEquality w, Is w a, Is w b)-    => Proxy w-    -> Maybe (a :~: b)-matchIs _ = testEquality r r-  where-    r :: forall t. (Is w t)-      => w t-    r = representative
− src/Data/Witness/All.hs 
@@ -1,39 +0,0 @@-module Data.Witness.All where--import Data.Functor.Identity-import Data.Kind-import Data.Type.Equality-import Data.Witness.Any-import Prelude--newtype AllF (w :: k -> Type) (f :: k -> Type) = MkAllF-    { getAllF :: forall (t :: k). w t -> f t-    }--newtype AllValue (w :: Type -> Type) = MkAllValue-    { getAllValue :: forall t. w t -> t-    }--setAllValue :: TestEquality wit => wit a -> a -> AllValue wit -> AllValue wit-setAllValue wa a (MkAllValue wtt) =-    MkAllValue $ \wa' ->-        case testEquality wa wa' of-            Just Refl -> a-            Nothing -> wtt wa'--allFToAllValue :: AllF w Identity -> AllValue w-allFToAllValue (MkAllF wtit) = MkAllValue $ \wt -> runIdentity $ wtit wt--allValueToAllF :: AllValue w -> AllF w Identity-allValueToAllF (MkAllValue wtt) = MkAllF $ \wt -> Identity $ wtt wt--type family UnAllValue (aw :: Type) :: Type -> Type where-    UnAllValue (AllValue w) = w--splitWitnessList :: TestEquality w => [AnyValue w] -> AllF w []-splitWitnessList [] = MkAllF $ \_ -> []-splitWitnessList ((MkAnyValue wt t):rr) =-    MkAllF $ \wt' ->-        case testEquality wt wt' of-            Just Refl -> t : (getAllF (splitWitnessList rr) wt')-            Nothing -> getAllF (splitWitnessList rr) wt'
− src/Data/Witness/Any.hs 
@@ -1,52 +0,0 @@-module Data.Witness.Any where--import Data.Functor.Const-import Data.Functor.Identity-import Data.Kind-import Data.Maybe-import Data.Type.Equality-import Data.Witness.Constraint-import Prelude---- | Any value with a witness to a parameter of its type.-data AnyF (w :: k -> Type) (f :: k -> Type) =-    forall (a :: k). MkAnyF (w a)-                            (f a)--matchAnyF :: TestEquality w => w a -> AnyF w f -> Maybe (f a)-matchAnyF wit (MkAnyF cwit cfa) = do-    Refl <- testEquality cwit wit-    return cfa--type AnyValue w = AnyF w Identity--pattern MkAnyValue :: w a -> a -> AnyValue w--pattern MkAnyValue wa a = MkAnyF wa (Identity a)--{-# COMPLETE MkAnyValue #-}--matchAnyValue :: TestEquality w => w a -> AnyValue w -> Maybe a-matchAnyValue wit av = do-    Identity a <- matchAnyF wit av-    return a--type AnyW w = AnyF w (Const ())--pattern MkAnyW :: w a -> AnyW w--pattern MkAnyW wa = MkAnyF wa (Const ())--{-# COMPLETE MkAnyW #-}--matchAnyW :: TestEquality w => w a -> AnyW w -> Bool-matchAnyW wit aw = isJust $ matchAnyF wit aw--instance TestEquality w => Eq (AnyW w) where-    (==) (MkAnyW wa) = matchAnyW wa--mapAnyW :: (forall t. w1 t -> w2 t) -> AnyW w1 -> AnyW w2-mapAnyW f (MkAnyW wt) = MkAnyW $ f wt--instance AllWitnessConstraint Show w => Show (AnyW w) where-    show (MkAnyW wa) = showAllWitness wa
− src/Data/Witness/ApplyStack.hs 
@@ -1,25 +0,0 @@-module Data.Witness.ApplyStack where--import Data.Type.Equality-import Data.Witness.Concat-import Data.Witness.List-import Data.Witness.Representative-import Prelude hiding ((.), id)--type family ApplyStack (f :: [k -> k]) (a :: k) :: k where-    ApplyStack '[] a = a-    ApplyStack (t ': tt) a = t (ApplyStack tt a)--witApplyConcatRefl ::-       forall k (f1 :: [k -> k]) (f2 :: [k -> k]) (a :: k) w.-       ListType w f1-    -> (ApplyStack (Concat f1 f2) a) :~: (ApplyStack f1 (ApplyStack f2 a))-witApplyConcatRefl NilListType = Refl-witApplyConcatRefl (ConsListType _ lt) =-    case witApplyConcatRefl @k @_ @f2 @a lt of-        Refl -> Refl--applyConcatRefl ::-       forall k (f1 :: [k -> k]) (f2 :: [k -> k]) (a :: k) w. Is (ListType w) f1-    => (ApplyStack (Concat f1 f2) a) :~: (ApplyStack f1 (ApplyStack f2 a))-applyConcatRefl = witApplyConcatRefl @k @f1 @f2 @a $ representative @_ @(ListType w) @f1
− src/Data/Witness/BigNat.hs 
@@ -1,48 +0,0 @@-module Data.Witness.BigNat-    ( module Data.Witness.BigNat-    , KnownNat-    ) where--import Data.Constraint-import Data.Proxy-import Data.Type.Equality-import Data.Witness.Constraint-import Data.Witness.Representative-import Data.Witness.WitnessValue-import GHC.TypeLits-import Numeric.Natural-import Prelude--type BigNat = Nat--data BigNatType (bn :: BigNat) where-    MkBigNatType :: KnownNat bn => BigNatType bn--instance WitnessValue BigNatType where-    type WitnessValueType BigNatType = Natural-    witnessToValue :: forall t. BigNatType t -> Natural-    witnessToValue MkBigNatType = fromInteger $ natVal (Proxy :: Proxy t)-    valueToWitness i cont =-        case someNatVal $ toInteger i of-            Just (SomeNat p) -> let-                psw :: forall (t :: BigNat). KnownNat t-                    => Proxy t-                    -> BigNatType t-                psw _ = MkBigNatType-                in cont $ psw p-            Nothing -> error "negative Natural"--instance TestEquality BigNatType where-    testEquality (MkBigNatType :: BigNatType a) (MkBigNatType :: BigNatType b) = sameNat (Proxy @a) (Proxy @b)--instance Representative BigNatType where-    getRepWitness MkBigNatType = Dict--instance KnownNat bn => Is BigNatType bn where-    representative = MkBigNatType--instance Show (BigNatType bn) where-    show = show . witnessToValue--instance AllWitnessConstraint Show BigNatType where-    allWitnessConstraint = Dict
− src/Data/Witness/Concat.hs 
@@ -1,34 +0,0 @@-module Data.Witness.Concat where--import Data.Constraint (Dict(..))-import Data.Type.Equality-import Data.Witness.List-import Data.Witness.Representative-import Prelude hiding ((.), id)--type family Concat (a :: [k]) (b :: [k]) :: [k] where-    Concat '[] bb = bb-    Concat (a ': aa) bb = a ': (Concat aa bb)--concatEmptyRefl :: ListType w a -> Concat a '[] :~: a-concatEmptyRefl NilListType = Refl-concatEmptyRefl (ConsListType _ la) =-    case concatEmptyRefl la of-        Refl -> Refl--concatIsDict ::-       forall w aa bb. (Representative w, Is (ListType w) aa, Is (ListType w) bb)-    => Dict (Is (ListType w) (Concat aa bb))-concatIsDict = let-    build :: forall aa'. ListType w aa' -> Dict (Is (ListType w) (Concat aa' bb))-    build NilListType = Dict-    build (ConsListType wa la) =-        case build la of-            Dict ->-                case getRepWitness wa of-                    Dict -> Dict-    in build $ representative @_ @(ListType w) @aa--concatListType :: ListType w a -> ListType w b -> ListType w (Concat a b)-concatListType NilListType lb = lb-concatListType (ConsListType wa la) lb = ConsListType wa $ concatListType la lb
− src/Data/Witness/Cons.hs 
@@ -1,98 +0,0 @@-module Data.Witness.Cons where--import Data.Constraint-import Data.Countable-import Data.Empty-import Data.Kind-import Data.Proxy-import Data.Searchable-import Data.Type.Equality-import Data.Witness.All-import Data.Witness.Constraint-import Data.Witness.Finite-import Data.Witness.List-import Data.Witness.ListElement-import Data.Witness.Representative-import Prelude--newtype EmptyType t =-    MkEmptyType None-    deriving (Eq, Countable, Searchable, Empty)--instance Finite (EmptyType t) where-    allValues = []-    assemble _ = pure never--instance TestEquality EmptyType where-    testEquality = never--instance Representative EmptyType where-    getRepWitness = never--instance FiniteWitness EmptyType where-    assembleWitnessF _ = pure emptyAllF--instance WitnessConstraint c EmptyType where-    witnessConstraint = never--emptyAll :: AllValue EmptyType-emptyAll = MkAllValue never--emptyAllF :: AllF EmptyType f-emptyAllF = MkAllF never--data ConsType a r t where-    FirstType :: ConsType t r t-    RestType :: r t -> ConsType a r t--instance TestEquality r => TestEquality (ConsType a r) where-    testEquality FirstType FirstType = return Refl-    testEquality (RestType r1) (RestType r2) = do-        Refl <- testEquality r1 r2-        return Refl-    testEquality _ _ = Nothing--instance FiniteWitness r => FiniteWitness (ConsType a r) where-    assembleWitnessF getsel =-        (\f (MkAllF r) ->-             MkAllF $ \wt ->-                 case wt of-                     FirstType -> f-                     RestType rt -> r rt) <$>-        getsel FirstType <*>-        assembleWitnessF (getsel . RestType)--instance (c a, WitnessConstraint c r) => WitnessConstraint c (ConsType a r) where-    witnessConstraint FirstType = Dict-    witnessConstraint (RestType rt) =-        case witnessConstraint @_ @c rt of-            Dict -> Dict--consAll :: a -> AllValue r -> AllValue (ConsType a r)-consAll a (MkAllValue tup) =-    MkAllValue $ \esel ->-        case esel of-            FirstType -> a-            RestType sel -> tup sel--class Is (ListType Proxy) (FiniteConsWitness sel) => IsFiniteConsWitness (sel :: k -> Type) where-    type FiniteConsWitness sel :: [k]-    toLTW :: forall t. sel t -> ListElementType (FiniteConsWitness sel) t-    fromLTW :: forall t. ListElementType (FiniteConsWitness sel) t -> sel t--instance Is (ListType Proxy) edits => IsFiniteConsWitness (ListElementType edits) where-    type FiniteConsWitness (ListElementType edits) = edits-    toLTW = id-    fromLTW = id--instance IsFiniteConsWitness EmptyType where-    type FiniteConsWitness EmptyType = '[]-    toLTW wit = never wit-    fromLTW lt = never lt--instance IsFiniteConsWitness lt => IsFiniteConsWitness (ConsType a lt) where-    type FiniteConsWitness (ConsType a lt) = a : (FiniteConsWitness lt)-    toLTW FirstType = FirstElementType-    toLTW (RestType sel) = RestElementType $ toLTW sel-    fromLTW FirstElementType = FirstType-    fromLTW (RestElementType lt) = RestType $ fromLTW lt
− src/Data/Witness/Constraint.hs 
@@ -1,23 +0,0 @@-module Data.Witness.Constraint where--import Data.Constraint-import Data.Kind-import Data.Type.Equality-import Prelude--class AllWitnessConstraint (c :: kw -> Constraint) (w :: kt -> kw) where-    allWitnessConstraint :: forall (t :: kt). Dict (c (w t))--instance AllWitnessConstraint Show ((:~:) t) where-    allWitnessConstraint = Dict--showAllWitness ::-       forall w t. AllWitnessConstraint Show w-    => w t-    -> String-showAllWitness wt =-    case allWitnessConstraint @_ @_ @Show @w @t of-        Dict -> show wt--class WitnessConstraint (c :: k -> Constraint) (w :: k -> Type) where-    witnessConstraint :: forall (t :: k). w t -> Dict (c t)
− src/Data/Witness/Either.hs 
@@ -1,66 +0,0 @@-module Data.Witness.Either where--import Data.Constraint-import Data.Kind-import Data.Type.Equality-import Data.Witness.All-import Data.Witness.Constraint-import Data.Witness.Finite-import Prelude--data EitherType (colsel1 :: k -> Type) (colsel2 :: k -> Type) (t :: k)-    = LeftType (colsel1 t)-    | RightType (colsel2 t)--instance (TestEquality colsel1, TestEquality colsel2) => TestEquality (EitherType colsel1 colsel2) where-    testEquality (LeftType s1) (LeftType s2) = do-        Refl <- testEquality s1 s2-        return Refl-    testEquality (RightType s1) (RightType s2) = do-        Refl <- testEquality s1 s2-        return Refl-    testEquality _ _ = Nothing--instance (FiniteWitness p, FiniteWitness q) => FiniteWitness (EitherType p q) where-    assembleWitnessF getsel =-        (\(MkAllF p) (MkAllF q) ->-             MkAllF $ \wt ->-                 case wt of-                     LeftType rt -> p rt-                     RightType rt -> q rt) <$>-        assembleWitnessF (getsel . LeftType) <*>-        assembleWitnessF (getsel . RightType)--instance (WitnessConstraint c p, WitnessConstraint c q) => WitnessConstraint c (EitherType p q) where-    witnessConstraint (LeftType rt) =-        case witnessConstraint @_ @c rt of-            Dict -> Dict-    witnessConstraint (RightType rt) =-        case witnessConstraint @_ @c rt of-            Dict -> Dict--instance (Show (p t), Show (q t)) => Show (EitherType p q t) where-    show (LeftType rt) = show rt-    show (RightType rt) = show rt--instance (AllWitnessConstraint Show p, AllWitnessConstraint Show q) => AllWitnessConstraint Show (EitherType p q) where-    allWitnessConstraint :: forall t. Dict (Show (EitherType p q t))-    allWitnessConstraint =-        case allWitnessConstraint @_ @_ @Show @p @t of-            Dict ->-                case allWitnessConstraint @_ @_ @Show @q @t of-                    Dict -> Dict--eitherAll :: AllValue sel1 -> AllValue sel2 -> AllValue (EitherType sel1 sel2)-eitherAll (MkAllValue tup1) (MkAllValue tup2) =-    MkAllValue $ \esel ->-        case esel of-            LeftType sel -> tup1 sel-            RightType sel -> tup2 sel--eitherAllF :: AllF sel1 f -> AllF sel2 f -> AllF (EitherType sel1 sel2) f-eitherAllF (MkAllF tup1) (MkAllF tup2) =-    MkAllF $ \esel ->-        case esel of-            LeftType sel -> tup1 sel-            RightType sel -> tup2 sel
− src/Data/Witness/Finite.hs 
@@ -1,51 +0,0 @@-{-# OPTIONS -fno-warn-orphans #-}--module Data.Witness.Finite where--import Data.Constraint-import Data.Countable-import Data.Functor.Const-import Data.Functor.Identity-import Data.Kind-import Data.List (intercalate)-import Data.Searchable-import Data.Type.Equality-import Data.Witness.All-import Data.Witness.Any-import Data.Witness.Constraint-import Prelude--class FiniteWitness (w :: k -> Type) where-    assembleWitnessF :: Applicative m => (forall t. w t -> m (f t)) -> m (AllF w f)--instance (TestEquality w, FiniteWitness w) => Countable (AnyW w) where-    countPrevious = finiteCountPrevious-    countMaybeNext = finiteCountMaybeNext--instance (TestEquality w, FiniteWitness w) => Searchable (AnyW w) where-    search = finiteSearch--instance (TestEquality w, FiniteWitness w) => Finite (AnyW w) where-    assemble ::-           forall b f. Applicative f-        => (AnyW w -> f b)-        -> f (AnyW w -> b)-    assemble afb =-        fmap (\(MkAllF wtcb) (MkAnyW wt) -> getConst $ wtcb wt) $ assembleWitnessF $ \wt -> fmap Const $ afb $ MkAnyW wt-    allValues = getConst $ assembleWitnessF $ \wt -> Const [MkAnyW wt]--allWitnesses :: FiniteWitness w => [AnyW w]-allWitnesses = getConst $ assembleWitnessF $ \wt -> Const [MkAnyW wt]--instance (FiniteWitness w, AllWitnessConstraint Show w, WitnessConstraint Show w) => Show (AllValue w) where-    show (MkAllValue wtt) = let-        showItem :: AnyW w -> String-        showItem (MkAnyW wt) =-            showAllWitness wt ++-            " -> " ++-            case witnessConstraint @_ @Show wt of-                Dict -> show (wtt wt)-        in "{" ++ intercalate "," (fmap showItem allWitnesses) ++ "}"--assembleWitness :: (FiniteWitness w, Applicative m) => (forall t. w t -> m t) -> m (AllValue w)-assembleWitness wtmt = fmap allFToAllValue $ assembleWitnessF $ \wt -> fmap Identity $ wtmt wt
− src/Data/Witness/HList.hs 
@@ -1,267 +0,0 @@-module Data.Witness.HList where--import Control.Applicative-import Control.Category-import Control.Category.Tensor-import Data.Constraint (Dict(..))-import Data.Functor.Identity as Import-import Data.Kind-import Data.Type.Equality-import Data.Witness.Either-import Data.Witness.List-import Data.Witness.ListElement-import Prelude hiding ((.), id)-import Unsafe.Coerce--type family HList (w :: [Type]) = (r :: Type) | r -> w where-    HList '[] = ()-    HList (t : tt) = (t, HList tt)---- workaround for https://gitlab.haskell.org/ghc/ghc/issues/10833-injectiveHList ::-       forall (a :: [Type]) (b :: [Type]). HList a ~ HList b-    => a :~: b-injectiveHList = unsafeCoerce Refl--hListEq :: (forall a. w a -> Dict (Eq a)) -> ListType w t -> Dict (Eq (HList t))-hListEq _ NilListType = Dict-hListEq f (ConsListType t tt) =-    case (f t, hListEq f tt) of-        (Dict, Dict) -> Dict--hListShow :: (forall a. w a -> Dict (Show a)) -> ListType w t -> Dict (Show (HList t))-hListShow _ NilListType = Dict-hListShow f (ConsListType t tt) =-    case (f t, hListShow f tt) of-        (Dict, Dict) -> Dict--data HListWit (wit :: Type -> Type) (t :: Type) where-    MkHListWit :: forall (wit :: Type -> Type) (lt :: [Type]). ListType wit lt -> HListWit wit (HList lt)--listFill :: ListType w t -> (forall a. w a -> a) -> HList t-listFill NilListType _f = ()-listFill (ConsListType wa wr) f = (f wa, listFill wr f)--listMap :: ListType w t -> (forall a. w a -> a -> a) -> HList t -> HList t-listMap NilListType _f () = ()-listMap (ConsListType wa wr) f (a, rest) = (f wa a, listMap wr f rest)--listLift2 :: ListType w t -> (forall a. w a -> a -> a -> a) -> HList t -> HList t -> HList t-listLift2 NilListType _f () () = ()-listLift2 (ConsListType wa wr) f (a, resta) (b, restb) = (f wa a b, listLift2 wr f resta restb)--listIdentity :: ListType Identity lt -> HList lt-listIdentity NilListType = ()-listIdentity (ConsListType (Identity a) rest) = (a, listIdentity rest)--listSequence :: (Applicative f) => ListType f lt -> f (HList lt)-listSequence NilListType = pure ()-listSequence (ConsListType fa rest) = liftA2 (,) fa (listSequence rest)--getListElement :: ListElementType list t -> HList list -> t-getListElement FirstElementType = fst -- using fst and snd for irrefutable matching-getListElement (RestElementType lw) = getListElement lw . snd--putListElement :: ListElementType list t -> t -> HList list -> HList list-putListElement FirstElementType t (_, r) = (t, r)-putListElement (RestElementType lw) t (a, r) = (a, putListElement lw t r)--modifyListElement :: ListElementType list t -> (t -> t) -> HList list -> HList list-modifyListElement n aa t = putListElement n (aa (getListElement n t)) t--data AppendList w la lb = forall lr. MkAppendList-    { listAppendWitness :: ListType w lr-    , listAppend :: HList la -> HList lb -> HList lr-    , listSplit :: HList lr -> (HList la, HList lb)-    }--appendList :: ListType w la -> ListType w lb -> AppendList w la lb-appendList NilListType wlb =-    MkAppendList {listAppendWitness = wlb, listAppend = \() lb -> lb, listSplit = \lb -> ((), lb)}-appendList (ConsListType wa wla) wlb =-    case appendList wla wlb of-        MkAppendList wit join split ->-            MkAppendList-                { listAppendWitness = ConsListType wa wit-                , listAppend = \(a, la) lb -> (a, join la lb)-                , listSplit =-                      \(a, lab) ->-                          case split lab of-                              (la, lb) -> ((a, la), lb)-                }--data AddItemList w a l = forall lr. MkAddItemList-    { listAddItemWitness :: ListType w lr-    , listAddItem :: a -> HList l -> HList lr-    , listSplitItem :: HList lr -> (a, HList l)-    }--addListItem :: w a -> ListType w l -> AddItemList w a l-addListItem wa wl = MkAddItemList {listAddItemWitness = ConsListType wa wl, listAddItem = (,), listSplitItem = id}--data MergeItemList w a l = forall lr. MkMergeItemList-    { listMergeItemWitness :: ListType w lr-    , listMergeItem :: (Maybe a -> a) -> HList l -> HList lr-    , listUnmergeItem :: HList lr -> (a, HList l)-    }--mergeListItem :: (TestEquality w) => ListType w l -> w a -> MergeItemList w a l-mergeListItem NilListType wa =-    MkMergeItemList-        { listMergeItemWitness = ConsListType wa NilListType-        , listMergeItem = \maa () -> (maa Nothing, ())-        , listUnmergeItem = id-        }-mergeListItem wl@(ConsListType wa' _) wa-    | Just Refl <- testEquality wa wa' =-        MkMergeItemList-            { listMergeItemWitness = wl-            , listMergeItem = \maa (a, l) -> (maa (Just a), l)-            , listUnmergeItem = \(a, l) -> (a, (a, l))-            }-mergeListItem (ConsListType wa' wl) wa =-    case mergeListItem wl wa of-        MkMergeItemList wit merge unmerge ->-            MkMergeItemList-                { listMergeItemWitness = ConsListType wa' wit-                , listMergeItem = \maa (a', l) -> (a', merge maa l)-                , listUnmergeItem =-                      \(a', l') ->-                          case unmerge l' of-                              (a, l) -> (a, (a', l))-                }--data MergeList w la lb = forall lr. MkMergeList-    { listMergeWitness :: ListType w lr-    , listMerge :: (forall t. w t -> t -> t -> t) -> HList la -> HList lb -> HList lr-    , listUnmerge :: HList lr -> (HList la, HList lb)-    }--mergeList :: (TestEquality w) => ListType w la -> ListType w lb -> MergeList w la lb-mergeList wla NilListType =-    MkMergeList {listMergeWitness = wla, listMerge = \_ la () -> la, listUnmerge = \la -> (la, ())}-mergeList wla (ConsListType wb wlb) =-    case mergeListItem wla wb of-        MkMergeItemList wla' mergeItem unmergeItem ->-            case mergeList wla' wlb of-                MkMergeList wlr merge unmerge ->-                    MkMergeList-                        { listMergeWitness = wlr-                        , listMerge =-                              \f la (b, lb) ->-                                  merge-                                      f-                                      (mergeItem-                                           (\mb' ->-                                                case mb' of-                                                    Just b' -> f wb b' b-                                                    Nothing -> b)-                                           la)-                                      lb-                        , listUnmerge =-                              \lr ->-                                  case unmerge lr of-                                      (la', lb) ->-                                          case unmergeItem la' of-                                              (b, la) -> (la, (b, lb))-                        }--type MapWitness cc w1 w2 = forall r v1. w1 v1 -> (forall v2. w2 v2 -> (cc v1 v2) -> r) -> r--sameMapWitness :: (forall v. w v -> cc v v) -> MapWitness cc w w-sameMapWitness wc w wcr = wcr w (wc w)--data MapList cc w2 l = forall lr. MkMapList-    { listMapWitness :: ListType w2 lr-    , listMapW :: cc (HList l) (HList lr)-    }--mapList :: (Tensor cc) => MapWitness cc w1 w2 -> ListType w1 l -> MapList cc w2 l-mapList _ NilListType = MkMapList {listMapWitness = NilListType, listMapW = tensorUnit}-mapList mapwit (ConsListType w rest) =-    case mapList mapwit rest of-        MkMapList wit listMapW' ->-            mapwit-                w-                (\w' vmap -> MkMapList {listMapWitness = ConsListType w' wit, listMapW = tensorPair vmap listMapW'})--data RemoveFromList w a l = forall lr. MkRemoveFromList-    { listRemoveWitness :: ListType w lr-    , listInsert :: a -> HList lr -> HList l-    , listRemove :: HList l -> HList lr-    }--removeAllMatching :: (TestEquality w) => w a -> ListType w l -> RemoveFromList w a l-removeAllMatching _ NilListType =-    MkRemoveFromList {listRemoveWitness = NilListType, listInsert = \_ -> id, listRemove = id}-removeAllMatching wa (ConsListType wb rest) =-    case removeAllMatching wa rest of-        MkRemoveFromList wit ins rm ->-            case testEquality wa wb of-                Just Refl ->-                    MkRemoveFromList-                        {listRemoveWitness = wit, listInsert = \a l2 -> (a, ins a l2), listRemove = \(_, l1) -> rm l1}-                Nothing ->-                    MkRemoveFromList-                        { listRemoveWitness = ConsListType wb wit-                        , listInsert = \a (b, l2) -> (b, ins a l2)-                        , listRemove = \(b, l1) -> (b, rm l1)-                        }--data RemoveManyFromList wit lx l = forall lr. MkRemoveManyFromList-    { listRemoveManyWitness :: ListType wit lr-    , listInsertMany :: HList lx -> HList lr -> HList l-    , listRemoveMany :: HList l -> HList lr-    }--removeAllMatchingMany :: (TestEquality wit) => ListType wit lx -> ListType wit l -> RemoveManyFromList wit lx l-removeAllMatchingMany NilListType wl =-    MkRemoveManyFromList {listRemoveManyWitness = wl, listInsertMany = \_ lr -> lr, listRemoveMany = \l -> l}-removeAllMatchingMany (ConsListType wa wlx) wl =-    case removeAllMatching wa wl of-        MkRemoveFromList wl' ins rm ->-            case removeAllMatchingMany wlx wl' of-                MkRemoveManyFromList wl'' insM remM ->-                    MkRemoveManyFromList-                        { listRemoveManyWitness = wl''-                        , listInsertMany = \(a, lx) lr -> ins a (insM lx lr)-                        , listRemoveMany = remM . rm-                        }--data PartitionList wit1 wit2 l = forall l1 l2. MkPartitionList-    { listPartitionWitness1 :: ListType wit1 l1-    , listPartitionWitness2 :: ListType wit2 l2-    , listFromPartition :: HList l1 -> HList l2 -> HList l-    , listToPartition1 :: HList l -> HList l1-    , listToPartition2 :: HList l -> HList l2-    }--partitionList :: ListType (EitherType w1 w2) l -> PartitionList w1 w2 l-partitionList NilListType =-    MkPartitionList-        { listPartitionWitness1 = NilListType-        , listPartitionWitness2 = NilListType-        , listFromPartition = \() () -> ()-        , listToPartition1 = \() -> ()-        , listToPartition2 = \() -> ()-        }-partitionList (ConsListType (LeftType w1a) rest) =-    case partitionList rest of-        MkPartitionList pw1 pw2 fp tp1 tp2 ->-            MkPartitionList-                { listPartitionWitness1 = ConsListType w1a pw1-                , listPartitionWitness2 = pw2-                , listFromPartition = \(a, l1) l2 -> (a, fp l1 l2)-                , listToPartition1 = \(a, l) -> (a, tp1 l)-                , listToPartition2 = \(_, l) -> tp2 l-                }-partitionList (ConsListType (RightType w2a) rest) =-    case partitionList rest of-        MkPartitionList pw1 pw2 fp tp1 tp2 ->-            MkPartitionList-                { listPartitionWitness1 = pw1-                , listPartitionWitness2 = ConsListType w2a pw2-                , listFromPartition = \l1 (a, l2) -> (a, fp l1 l2)-                , listToPartition1 = \(_, l) -> tp1 l-                , listToPartition2 = \(a, l) -> (a, tp2 l)-                }
− src/Data/Witness/Kind.hs 
@@ -1,80 +0,0 @@-module Data.Witness.Kind where--import Data.Constraint-import Data.Kind-import Data.Witness.Constraint-import Data.Witness.Representative-import GHC.TypeLits-import Prelude--type family KindWitness k :: k -> Type--type InKind (a :: k) = Is (KindWitness k) a--inKind ::-       forall k (a :: k). InKind a-    => KindWitness k a-inKind = representative---- NoWitness-data NoWitness (t :: k) =-    MkNoWitness--instance Representative NoWitness where-    getRepWitness MkNoWitness = Dict--instance Is NoWitness a where-    representative = MkNoWitness---- Type-type instance KindWitness Type = NoWitness---- Constraint-type instance KindWitness Constraint = NoWitness---- Nat-type instance KindWitness Nat = NoWitness---- kp -> kq-data FunctionKindWitness (wp :: kp -> Type) (wq :: kq -> Type) (t :: kp -> kq) where-    MkFunctionKindWitness-        :: forall kp kq (wp :: kp -> Type) (wq :: kq -> Type) (t :: kp -> kq).-           (forall (p :: kp). Is wp p => Is wq (t p))-        => FunctionKindWitness wp wq t--applyFunctionKindWitness ::-       forall kp kq (wp :: kp -> Type) (wq :: kq -> Type) (t :: kp -> kq) (p :: kp) (proxy :: kp -> Type). Is wp p-    => FunctionKindWitness wp wq t-    -> proxy p-    -> Dict (Is wq (t p))-applyFunctionKindWitness MkFunctionKindWitness _ = Dict--type instance KindWitness (kp -> kq) =-     FunctionKindWitness (KindWitness kp) (KindWitness kq)--instance forall kp kq (wp :: kp -> Type) (wq :: kq -> Type). Representative (FunctionKindWitness wp wq) {- Representative wq => -}-                                                                                                                                   where-    getRepWitness MkFunctionKindWitness = Dict--instance (forall p. Is wp p => Is wq (f p)) =>-             Is (FunctionKindWitness (wp :: kp -> Type) (wq :: kq -> Type)) (f :: kp -> kq) where-    representative = MkFunctionKindWitness---- (kp,kq)-data PairWitness (wp :: kp -> Type) (wq :: kq -> Type) (t :: (kp, kq)) where-    MkPairWitness :: (Is wp p, Is wq q) => PairWitness wp wq '( p, q)--instance (Representative wp, Representative wq) => Representative (PairWitness wp wq) where-    getRepWitness MkPairWitness = Dict--instance (Is wp p, Is wq q) => Is (PairWitness wp wq) '( p, q) where-    representative = MkPairWitness--type instance KindWitness (kp, kq) =-     PairWitness (KindWitness kp) (KindWitness kq)--data AnyInKind (wit :: k -> Type) =-    forall (t :: k). InKind t => MkAnyInKind (wit t)--instance AllWitnessConstraint Show w => Show (AnyInKind w) where-    show (MkAnyInKind wa) = showAllWitness wa
− src/Data/Witness/List.hs 
@@ -1,73 +0,0 @@-module Data.Witness.List where--import Data.Constraint (Dict(..))-import Data.Functor.Identity-import Data.Kind-import Data.List (intercalate)-import Data.Nat-import Data.Type.Equality-import Data.Witness.Any-import Data.Witness.Representative-import Prelude hiding ((.), id)---- | a witness type for lists of types--- The @w@ parameter is the witness type of the elements.-data ListType (w :: k -> Type) (lt :: [k]) where-    NilListType :: ListType w '[]-    ConsListType :: w a -> ListType w lt -> ListType w (a : lt)--instance Representative w => Representative (ListType w) where-    getRepWitness NilListType = Dict-    getRepWitness (ConsListType w lw) =-        case (getRepWitness w, getRepWitness lw) of-            (Dict, Dict) -> Dict--instance Representative w => Is (ListType w) '[] where-    representative = NilListType--instance (Is w a, Is (ListType w) lt) => Is (ListType w) (a : lt) where-    representative = ConsListType representative representative--instance TestEquality w => TestEquality (ListType w) where-    testEquality NilListType NilListType = Just Refl-    testEquality (ConsListType wpa wpb) (ConsListType wqa wqb) = do-        Refl <- testEquality wpa wqa-        Refl <- testEquality wpb wqb-        return Refl-    testEquality _ _ = Nothing--instance (forall a. Show (w a)) => Show (ListType w lt) where-    show s = "[" <> intercalate "," (showAll s) <> "]"-      where-        showAll :: forall t. ListType w t -> [String]-        showAll NilListType = []-        showAll (ConsListType t1 tr) = show t1 : showAll tr--assembleListType :: [AnyW w] -> AnyW (ListType w)-assembleListType [] = MkAnyW NilListType-assembleListType ((MkAnyW wa):ww) =-    case assembleListType ww of-        MkAnyW wwa -> MkAnyW $ ConsListType wa wwa--mapMListType :: Applicative m => (forall t'. wita t' -> m (witb t')) -> ListType wita t -> m (ListType witb t)-mapMListType _ff NilListType = pure NilListType-mapMListType ff (ConsListType t tt) = ConsListType <$> ff t <*> mapMListType ff tt--mapListType :: (forall t'. wita t' -> witb t') -> ListType wita t -> ListType witb t-mapListType ff l = runIdentity $ mapMListType (\wt -> Identity $ ff wt) l--type family ListElement (n :: Nat) (list :: [k]) :: k where-    ListElement 'Zero (a : aa) = a-    ListElement ('Succ n) (a : aa) = ListElement n aa--listTypeLength :: ListType w lt -> Int-listTypeLength NilListType = 0-listTypeLength (ConsListType _ lt) = succ $ listTypeLength lt--listTypeToList :: (forall a. w a -> r) -> ListType w t -> [r]-listTypeToList _wr NilListType = []-listTypeToList wr (ConsListType wa rest) = (wr wa) : (listTypeToList wr rest)--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
− src/Data/Witness/ListElement.hs 
@@ -1,49 +0,0 @@-module Data.Witness.ListElement where--import Data.Countable-import Data.Empty-import Data.Kind-import Data.Maybe-import Data.Searchable-import Data.Type.Equality-import Data.Witness.List-import Prelude--data ListElementType (kk :: [k]) (t :: k) where-    FirstElementType :: ListElementType (t : tt) t-    RestElementType :: ListElementType aa t -> ListElementType (a : aa) t--instance TestEquality (ListElementType tt) where-    testEquality FirstElementType FirstElementType = Just Refl-    testEquality (RestElementType lt1) (RestElementType lt2) = do-        Refl <- testEquality lt1 lt2-        return Refl-    testEquality _ _ = Nothing--instance Searchable (ListElementType '[] t) where-    search = finiteSearch--instance Eq (ListElementType tt t) where-    lt1 == lt2 = isJust $ testEquality lt1 lt2--instance Countable (ListElementType '[] t) where-    countPrevious = finiteCountPrevious-    countMaybeNext = finiteCountMaybeNext--instance Finite (ListElementType '[] t) where-    allValues = []--instance Empty (ListElementType '[] t) where-    never lt = case lt of {}--lookUpListElement ::-       forall k (w :: k -> Type) (t :: k) (lt :: [k]). TestEquality w-    => w t-    -> ListType w lt-    -> Maybe (ListElementType lt t)-lookUpListElement _ NilListType = Nothing-lookUpListElement wt (ConsListType wt' _)-    | Just Refl <- testEquality wt wt' = Just FirstElementType-lookUpListElement wt (ConsListType _ lt) = do-    et <- lookUpListElement wt lt-    return $ RestElementType et
− src/Data/Witness/Nat.hs 
@@ -1,81 +0,0 @@-module Data.Witness.Nat where--import Data.Constraint (Dict(..))-import Data.Maybe-import Data.Nat-import Data.Type.Equality-import Data.Witness.Representative-import Prelude hiding ((.), id)--data NatType (t :: Nat) where-    ZeroType :: NatType 'Zero-    SuccType :: NatType t -> NatType ('Succ t)--instance TestEquality NatType where-    testEquality ZeroType ZeroType = return Refl-    testEquality (SuccType a) (SuccType b) = do-        Refl <- testEquality a b-        return Refl-    testEquality _ _ = Nothing--instance Representative NatType where-    getRepWitness ZeroType = Dict-    getRepWitness (SuccType n) =-        case getRepWitness n of-            Dict -> Dict--instance Is NatType 'Zero where-    representative = ZeroType--instance (Is NatType n) => Is NatType ('Succ n) where-    representative = SuccType representative--data GreaterEqual (a :: Nat) (b :: Nat) where-    ZeroGreaterEqual :: GreaterEqual a 'Zero-    SuccGreaterEqual :: GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b)--sameGreaterEqualWit :: NatType a -> GreaterEqual a a-sameGreaterEqualWit ZeroType = ZeroGreaterEqual-sameGreaterEqualWit (SuccType a) = SuccGreaterEqual $ sameGreaterEqualWit a--diff1GreaterEqualWit :: GreaterEqual a b -> GreaterEqual ('Succ a) b-diff1GreaterEqualWit ZeroGreaterEqual = ZeroGreaterEqual-diff1GreaterEqualWit (SuccGreaterEqual ge) = SuccGreaterEqual $ diff1GreaterEqualWit ge--natGreaterEqual :: NatType a -> NatType b -> Maybe (GreaterEqual a b)-natGreaterEqual _ ZeroType = return ZeroGreaterEqual-natGreaterEqual ZeroType _ = Nothing-natGreaterEqual (SuccType a) (SuccType b) = do-    al <- natGreaterEqual a b-    return $ SuccGreaterEqual al--type family Add (a :: Nat) (b :: Nat) :: Nat where-    Add 'Zero b = b-    Add ('Succ a) b = 'Succ (Add a b)--addWit :: NatType a -> NatType b -> NatType (Add a b)-addWit ZeroType b = b-addWit (SuccType a) b = SuccType $ addWit a b--addZeroWit :: NatType a -> Add a 'Zero :~: a-addZeroWit ZeroType = Refl-addZeroWit (SuccType a) =-    case addZeroWit a of-        Refl -> Refl--succAddWit' :: forall a b. NatType a -> 'Succ (Add a b) :~: Add a ('Succ b)-succAddWit' ZeroType = Refl-succAddWit' (SuccType a) =-    case succAddWit' @_ @b a of-        Refl -> Refl--succAddWit :: forall a b. NatType a -> NatType b -> 'Succ (Add a b) :~: Add a ('Succ b)-succAddWit a _ = succAddWit' @a @b a--addGreaterEqualWit :: NatType a -> NatType b -> GreaterEqual (Add a b) a-addGreaterEqualWit a ZeroType =-    case addZeroWit a of-        Refl -> sameGreaterEqualWit a-addGreaterEqualWit a (SuccType b) =-    case succAddWit a b of-        Refl -> diff1GreaterEqualWit $ addGreaterEqualWit a b
− src/Data/Witness/Representative.hs 
@@ -1,60 +0,0 @@-module Data.Witness.Representative where--import Data.Constraint-import Data.Functor.Compose-import Data.Kind-import Data.Proxy-import Data.Type.Equality-import Data.Witness.Any--isWitnessRepresentative :: Dict (Is rep a) -> rep a-isWitnessRepresentative Dict = representative--type Subrepresentative (p :: k -> Type) (q :: k -> Type) = forall (a :: k). p a -> Dict (Is q a)--withSubrepresentative :: Subrepresentative p q -> p a -> (Is q a => r) -> r-withSubrepresentative subrep pa f =-    case subrep pa of-        Dict -> f--class Representative (rep :: k -> Type) where-    -- | Every value is an instance of 'Is'.-    getRepWitness :: Subrepresentative rep rep--instance Representative Proxy where-    getRepWitness Proxy = Dict--withRepresentative :: Representative rep => rep a -> (Is rep a => r) -> r-withRepresentative = withSubrepresentative getRepWitness---- | If two representatives have the same type, then they have the same value.-class Representative rep => Is (rep :: k -> Type) (a :: k) where-    -- | The representative value for type @a@.-    representative :: rep a--instance Is Proxy a where-    representative = Proxy--getRepresentative :: Is rep a => a -> rep a-getRepresentative _ = representative--rerepresentative :: Is rep a => p a -> rep a-rerepresentative _ = representative--mkAny :: Is rep a => a -> AnyValue rep-mkAny a = MkAnyValue representative a--mkAnyF :: Is rep a => f a -> AnyF rep f-mkAnyF fa = MkAnyF representative fa--instance Representative ((:~:) (t :: k)) where-    getRepWitness Refl = Dict--instance Is ((:~:) (t :: k)) (t :: k) where-    representative = Refl--instance Representative (Compose Dict c) where-    getRepWitness (Compose Dict) = Dict--instance c t => Is (Compose Dict c) t where-    representative = Compose Dict
− src/Data/Witness/Single.hs 
@@ -1,24 +0,0 @@-{-# OPTIONS -fno-warn-orphans #-}--module Data.Witness.Single where--import Data.Constraint-import Data.Type.Equality-import Data.Witness.All-import Data.Witness.Constraint-import Data.Witness.Finite-import Prelude--type SingleType = (:~:)--instance FiniteWitness (SingleType t) where-    assembleWitnessF getsel = fmap (\ft -> MkAllF $ \Refl -> ft) $ getsel Refl--instance c t => WitnessConstraint c (SingleType t) where-    witnessConstraint Refl = Dict--singleAll :: t -> AllValue (SingleType t)-singleAll t = MkAllValue $ \Refl -> t--getSingleAll :: AllValue (SingleType t) -> t-getSingleAll (MkAllValue f) = f Refl
− src/Data/Witness/Submap.hs 
@@ -1,29 +0,0 @@-module Data.Witness.Submap where--import Data.Kind-import Data.Witness.All-import Data.Witness.Any-import Data.Witness.Either-import Data.Witness.Finite-import Prelude--data SubmapWitness (w :: k -> Type) (f :: k -> Type) = MkSubmapWitness-    { subWitnessDomain :: [AnyW w]-    , subWitnessMap :: forall (t :: k). w t -> f t-    }--subWitnessCodomain :: SubmapWitness w f -> [AnyW f]-subWitnessCodomain schema = fmap (\(MkAnyW st) -> MkAnyW $ subWitnessMap schema st) $ subWitnessDomain schema--mapSubmapWitness :: (forall t. f1 t -> f2 t) -> SubmapWitness w f1 -> SubmapWitness w f2-mapSubmapWitness ff (MkSubmapWitness ai i) = MkSubmapWitness ai $ \s -> ff $ i s--eitherSubmapWitness ::-       SubmapWitness sel1 itemSchema -> SubmapWitness sel2 itemSchema -> SubmapWitness (EitherType sel1 sel2) itemSchema-eitherSubmapWitness (MkSubmapWitness a1 i1) (MkSubmapWitness a2 i2) =-    MkSubmapWitness-        ((fmap (mapAnyW LeftType) a1) ++ (fmap (mapAnyW RightType) a2))-        (getAllF $ eitherAllF (MkAllF i1) (MkAllF i2))--finiteSubmapWitness :: FiniteWitness w => (forall t. w t -> f t) -> SubmapWitness w f-finiteSubmapWitness wf = MkSubmapWitness allWitnesses wf
− src/Data/Witness/Symbol.hs 
@@ -1,45 +0,0 @@-module Data.Witness.Symbol-    ( module Data.Witness.Symbol-    , Symbol-    , KnownSymbol-    ) where--import Data.Constraint-import Data.Proxy-import Data.Type.Equality-import Data.Witness.Constraint-import Data.Witness.Representative-import Data.Witness.WitnessValue-import GHC.TypeLits-import Prelude--data SymbolType (symbol :: Symbol) where-    MkSymbolType :: KnownSymbol symbol => SymbolType symbol--instance WitnessValue SymbolType where-    type WitnessValueType SymbolType = String-    witnessToValue :: forall t. SymbolType t -> String-    witnessToValue MkSymbolType = symbolVal (Proxy :: Proxy t)-    valueToWitness s cont =-        case someSymbolVal s of-            SomeSymbol p -> let-                psw :: forall (t :: Symbol). KnownSymbol t-                    => Proxy t-                    -> SymbolType t-                psw _ = MkSymbolType-                in cont $ psw p--instance TestEquality SymbolType where-    testEquality (MkSymbolType :: SymbolType a) (MkSymbolType :: SymbolType b) = sameSymbol (Proxy @a) (Proxy @b)--instance Representative SymbolType where-    getRepWitness MkSymbolType = Dict--instance KnownSymbol symbol => Is SymbolType symbol where-    representative = MkSymbolType--instance Show (SymbolType symbol) where-    show = witnessToValue--instance AllWitnessConstraint Show SymbolType where-    allWitnessConstraint = Dict
− src/Data/Witness/WitnessDict.hs 
@@ -1,55 +0,0 @@-module Data.Witness.WitnessDict where--import Data.Kind-import Data.Maybe-import Data.Type.Equality-import Data.Witness.Any-import Prelude---- | 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.-newtype WitnessDict (w :: Type -> Type) =-    MkWitnessDict [AnyValue w]---- | An empty dictionary.-emptyWitnessDict :: WitnessDict w-emptyWitnessDict = MkWitnessDict []---- | Look up the first value in the dictionary that matches the given witness.-witnessDictLookup :: (TestEquality w) => w a -> WitnessDict w -> Maybe a-witnessDictLookup wit (MkWitnessDict cells) = listToMaybe (mapMaybe (matchAnyValue wit) cells)---- | Modify the first value in the dictionary that matches a particular witness.-witnessDictModify :: (TestEquality w) => w a -> (a -> a) -> WitnessDict w -> WitnessDict w-witnessDictModify wit amap (MkWitnessDict cells) =-    MkWitnessDict (replaceFirst ((fmap ((MkAnyValue wit) . amap)) . (matchAnyValue wit)) cells)-  where-    replaceFirst :: (a -> Maybe a) -> [a] -> [a]-    replaceFirst ama (a:aa) =-        case ama a of-            Just newa -> (newa : aa)-            _ -> a : (replaceFirst ama aa)-    replaceFirst _ _ = []---- | Replace the first value in the dictionary that matches the witness-witnessDictReplace :: (TestEquality w) => w a -> a -> WitnessDict w -> WitnessDict w-witnessDictReplace wit newa = witnessDictModify wit (const newa)---- | Add a witness and value as the first entry in the dictionary.-witnessDictAdd :: w a -> a -> WitnessDict w -> WitnessDict w-witnessDictAdd wit a (MkWitnessDict cells) = MkWitnessDict ((MkAnyValue wit a) : cells)---- | Remove the first entry in the dictionary that matches the given witness.-witnessDictRemove :: (TestEquality w) => w a -> WitnessDict w -> WitnessDict w-witnessDictRemove wit (MkWitnessDict cells) =-    MkWitnessDict (removeFirst (\(MkAnyValue cwit _) -> isJust (testEquality wit cwit)) cells)-  where-    removeFirst :: (a -> Bool) -> [a] -> [a]-    removeFirst p (a:as)-        | p a = as-    removeFirst p (a:as) = a : (removeFirst p as)-    removeFirst _ _ = []---- | Create a dictionary from a list of witness\/value pairs-witnessDictFromList :: [AnyValue w] -> WitnessDict w-witnessDictFromList = MkWitnessDict
− src/Data/Witness/WitnessFDict.hs 
@@ -1,55 +0,0 @@-module Data.Witness.WitnessFDict where--import Data.Kind-import Data.Maybe-import Data.Type.Equality-import Data.Witness.Any-import Prelude---- | 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.-newtype WitnessFDict (w :: k -> Type) (f :: k -> Type) =-    MkWitnessFDict [AnyF w f]---- | An empty dictionary.-emptyWitnessFDict :: WitnessFDict w f-emptyWitnessFDict = MkWitnessFDict []---- | Look up the first value in the dictionary that matches the given witness.-witnessFDictLookup :: (TestEquality w) => w a -> WitnessFDict w f -> Maybe (f a)-witnessFDictLookup wit (MkWitnessFDict cells) = listToMaybe (mapMaybe (matchAnyF wit) cells)---- | Modify the first value in the dictionary that matches a particular witness.-witnessFDictModify :: (TestEquality w) => w a -> (f a -> f a) -> WitnessFDict w f -> WitnessFDict w f-witnessFDictModify wit amap (MkWitnessFDict cells) =-    MkWitnessFDict (replaceFirst ((fmap ((MkAnyF wit) . amap)) . (matchAnyF wit)) cells)-  where-    replaceFirst :: (a -> Maybe a) -> [a] -> [a]-    replaceFirst ama (a:aa) =-        case ama a of-            Just newa -> (newa : aa)-            _ -> a : (replaceFirst ama aa)-    replaceFirst _ _ = []---- | Replace the first value in the dictionary that matches the witness-witnessFDictReplace :: (TestEquality w) => w a -> f a -> WitnessFDict w f -> WitnessFDict w f-witnessFDictReplace wit newfa = witnessFDictModify wit (const newfa)---- | Add a witness and value as the first entry in the dictionary.-witnessFDictAdd :: w a -> f a -> WitnessFDict w f -> WitnessFDict w f-witnessFDictAdd wit fa (MkWitnessFDict cells) = MkWitnessFDict ((MkAnyF wit fa) : cells)---- | Remove the first entry in the dictionary that matches the given witness.-witnessFDictRemove :: (TestEquality w) => w a -> WitnessFDict w f -> WitnessFDict w f-witnessFDictRemove wit (MkWitnessFDict cells) =-    MkWitnessFDict (removeFirst (\(MkAnyF cwit _) -> isJust (testEquality wit cwit)) cells)-  where-    removeFirst :: (a -> Bool) -> [a] -> [a]-    removeFirst p (a:as)-        | p a = as-    removeFirst p (a:as) = a : (removeFirst p as)-    removeFirst _ _ = []---- | Create a dictionary from a list of witness\/value pairs-witnessFDictFromList :: [AnyF w f] -> WitnessFDict w f-witnessFDictFromList = MkWitnessFDict
− src/Data/Witness/WitnessValue.hs 
@@ -1,21 +0,0 @@-module Data.Witness.WitnessValue where--import Data.Kind-import Data.Witness.Any--class WitnessValue (w :: k -> Type) where-    type WitnessValueType w :: Type-    witnessToValue :: forall (t :: k). w t -> WitnessValueType w-    valueToWitness :: forall r. WitnessValueType w -> (forall (t :: k). w t -> r) -> r--anyToValue ::-       forall k (w :: k -> Type). WitnessValue w-    => AnyW w-    -> WitnessValueType w-anyToValue (MkAnyW wt) = witnessToValue wt--valueToAny ::-       forall k (w :: k -> Type). WitnessValue w-    => WitnessValueType w-    -> AnyW w-valueToAny v = valueToWitness v MkAnyW
+ src/Import.hs view
@@ -0,0 +1,20 @@+module Import+    ( module I+    ) where++import Control.Applicative as I+import Control.Category as I+import Data.Constraint as I (Dict(..))+import Data.Countable as I+import Data.Empty as I+import Data.Functor.Compose as I+import Data.Functor.Identity as I+import Data.Kind as I+import Data.List as I (intercalate)+import Data.Maybe as I+import Data.Proxy as I+import Data.Searchable as I+import Data.Traversable as I+import Data.Type.Equality as I+import Data.Void as I+import Prelude as I hiding ((.), id)
witness.cabal view
@@ -1,64 +1,111 @@-cabal-version: 1.12+cabal-version: 2.2 --- This file has been generated from package.yaml by hpack version 0.33.0.+-- This file has been generated from package.yaml by hpack version 0.34.4. -- -- see: https://github.com/sol/hpack ----- hash: 05878bc4862c4de5349ab302faa8396dafc84f16a102fdd267c48f3aae1e6319+-- hash: a76cbdba6c2986d516e94b90eb9a51cf636e600c1915604c67d33e50e06f3127  name:           witness-version:        0.5+version:        0.6 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 simple witnesses, that constrain a type variable to a single type, and equality witnesses, that constrain two type variables to be the same type. It also provides classes for representatives, which are values that represent types. See the paper /Witnesses and Open Witnesses/ (<http://semantic.org/stuff/Open-Witnesses.pdf>).+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 homepage:       https://github.com/AshleyYakeley/witness bug-reports:    https://github.com/AshleyYakeley/witness/issues author:         Ashley Yakeley maintainer:     <ashley@semantic.org>-copyright:      (c) 2017-2019 Ashley Yakeley-license:        BSD3+copyright:      (c) 2017-2022 Ashley Yakeley+license:        BSD-2-Clause license-file:   LICENSE build-type:     Simple+extra-source-files:+    changelog.md  library   hs-source-dirs:       src-  default-extensions: AllowAmbiguousTypes Arrows ConstraintKinds DataKinds DefaultSignatures EmptyCase EmptyDataDecls ExistentialQuantification FlexibleContexts FlexibleInstances ForeignFunctionInterface FunctionalDependencies GADTs GeneralizedNewtypeDeriving ImplicitParams NoImplicitPrelude InstanceSigs KindSignatures LambdaCase MultiParamTypeClasses OverloadedLabels OverloadedStrings PartialTypeSignatures PatternGuards PatternSynonyms PolyKinds QuantifiedConstraints RankNTypes RecordWildCards RecursiveDo ScopedTypeVariables StandaloneDeriving NoStarIsType TemplateHaskell TypeApplications TypeFamilies TypeFamilyDependencies TypeInType TypeOperators TypeSynonymInstances UndecidableInstances UndecidableSuperClasses ViewPatterns+  default-extensions:+      AllowAmbiguousTypes+      Arrows+      ConstraintKinds+      DataKinds+      DefaultSignatures+      EmptyCase+      EmptyDataDecls+      ExistentialQuantification+      FlexibleContexts+      FlexibleInstances+      ForeignFunctionInterface+      FunctionalDependencies+      GADTs+      GeneralizedNewtypeDeriving+      ImplicitParams+      NoImplicitPrelude+      InstanceSigs+      KindSignatures+      LambdaCase+      MultiParamTypeClasses+      OverloadedLabels+      OverloadedStrings+      PartialTypeSignatures+      PatternGuards+      PatternSynonyms+      PolyKinds+      QuantifiedConstraints+      RankNTypes+      RecordWildCards+      RecursiveDo+      ScopedTypeVariables+      StandaloneDeriving+      StandaloneKindSignatures+      NoStarIsType+      TemplateHaskell+      TypeApplications+      TypeFamilies+      TypeFamilyDependencies+      TypeInType+      TypeOperators+      TypeSynonymInstances+      UndecidableInstances+      UndecidableSuperClasses+      ViewPatterns   ghc-options: -Wall -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat -Wnoncanonical-monad-instances   build-depends:-      base >=4.14 && <5-    , constraints-    , countable-    , semigroupoids-    , transformers+      base >=4.15 && <5+    , constraints >=0.13+    , countable >=1.2   exposed-modules:-      Data.Type.With-      Data.Type.Apply-      Data.Type.Heterogeneous-      Data.Nat-      Control.Category.Tensor-      Data.Witness.Kind-      Data.Witness.Any-      Data.Witness.All-      Data.Witness.Constraint-      Data.Witness.WitnessValue-      Data.Witness.Symbol-      Data.Witness.Finite-      Data.Witness.Single-      Data.Witness.Cons-      Data.Witness.Either-      Data.Witness.Submap-      Data.Witness.WitnessDict-      Data.Witness.WitnessFDict-      Data.Witness.Nat-      Data.Witness.BigNat-      Data.Witness.ListElement-      Data.Witness.List-      Data.Witness.Concat-      Data.Witness.ApplyStack-      Data.Witness.HList-      Data.Witness.Representative-      Data.Witness+      Data.Type.Witness.Apply+      Data.PeanoNat+      Data.Type.Witness.General.TestHetEquality+      Data.Type.Witness.General.HetConstraint+      Data.Type.Witness.Specific.Some+      Data.Type.Witness.Specific.All+      Data.Type.Witness.General.AllConstraint+      Data.Type.Witness.General.WitnessConstraint+      Data.Type.Witness.General.WitnessValue+      Data.Type.Witness.General.ListElement+      Data.Type.Witness.Specific.Symbol+      Data.Type.Witness.General.Finite+      Data.Type.Witness.Specific.Single+      Data.Type.Witness.Specific.Pair+      Data.Type.Witness.Specific.Empty+      Data.Type.Witness.Specific.Either+      Data.Type.Witness.Specific.FiniteAllFor+      Data.Type.Witness.Specific.WitnessMap.Of+      Data.Type.Witness.Specific.WitnessMap.For+      Data.Type.Witness.Specific.PeanoNat+      Data.Type.Witness.Specific.Natural+      Data.Type.Witness.Specific.List.Element+      Data.Type.Witness.Specific.List.List+      Data.Type.Witness.Specific.Concat+      Data.Type.Witness.Specific.ApplyStack+      Data.Type.Witness.Specific.List.Product+      Data.Type.Witness.Specific.List.Sum+      Data.Type.Witness.General.Representative+      Data.Type.Witness.General.Order+      Data.Type.Witness   other-modules:-      Paths_witness+      Import   default-language: Haskell2010