From 6389aa40996fa6c7e1837a709ff0666e988efef0 Mon Sep 17 00:00:00 2001
From: Sventimir <svantimir@gmail.com>
Date: Tue, 11 Aug 2020 18:27:06 +0200
Subject: [PATCH 01/16] Add initial validation framework.

---
 libs/contrib/Control/Validation.idr | 192 ++++++++++++++++++++++++++++
 1 file changed, 192 insertions(+)
 create mode 100644 libs/contrib/Control/Validation.idr

diff --git a/libs/contrib/Control/Validation.idr b/libs/contrib/Control/Validation.idr
new file mode 100644
index 000000000..084a0bf0d
--- /dev/null
+++ b/libs/contrib/Control/Validation.idr
@@ -0,0 +1,192 @@
+module Control.Validation
+
+-- Main purpose of this module is verifying programmer's assumptions about
+-- user input. On one hand we want to write precisely typed programs, including
+-- assumptions about input expressed in types and prove correctness of these
+-- programs. On the other we get an unstructured user input as a string or even
+-- a raw sequence of bytes.
+
+-- This module intends to provide a framework for verifying our assumptions
+-- about user input and constructing proofs that input is indeed valid or
+-- failing early with a nice error message if it isn't.
+
+import Control.Monad.Syntax
+import Data.Nat
+import Data.Strings
+import Data.Vect
+import Decidable.Equality
+
+%default total
+
+
+public export
+Result : Type -> Type
+Result = Either String
+
+||| Validators in this module come in two flavours: Structural Validators and
+||| Property Validators. They are both wrappers around functions which take
+||| some input and confirm that it's valid (returning some witness of its
+||| validity) or fail with an error described by a string.
+|||
+||| Structural Validators work by refining the type of input, for instance
+||| checking whether a string encodes a number and returning that number if it
+||| does. More generally, they convert raw input to some more restricted type.
+|||
+||| Property Validators try to prove that (usually already refined) input has
+||| some property and return the proof if it does.
+public export
+data Validator : Type -> Type -> Type where
+    StructValidator : (a -> Result b) -> Validator a b
+    PropValidator : {0 a, b : Type} -> {0 p : b -> Type} -> {0 x : b} -> (a -> Result (p x)) -> Validator a (p x)
+
+
+unwrap : Validator a b -> a -> Result b
+unwrap (StructValidator f) = f
+unwrap (PropValidator f) = f
+
+export
+Functor (Validator a) where
+    map f v = StructValidator (map f . unwrap v)
+
+export
+Applicative (Validator a) where
+    pure a = StructValidator (const $ pure a)
+    f <*> a = StructValidator (\x => unwrap f x <*> unwrap a x)
+
+export
+Monad (Validator a) where
+    v >>= f = StructValidator $ \x => do
+        r <- unwrap v x
+        unwrap (f r) x
+
+||| Run validation on given input, returning (Right refinedInput) if everything
+||| is all right or (Left errorMessage) if it's not.
+export
+validate : Validator a b -> a -> Result b
+validate (StructValidator v) = v
+validate (PropValidator v) = v
+
+replaceError : String -> Result a -> Result a
+replaceError e (Left _) = Left e
+replaceError _ (Right x) = Right x
+
+||| Replace validator's default error message.
+export
+withError : String -> Validator a b -> Validator a b
+withError e (StructValidator f) = StructValidator (replaceError e . f)
+withError e (PropValidator {p} {x} f) = PropValidator {p} {x} (replaceError e . f)
+
+||| A validator which always fails with a given message.
+export
+fail : String -> Validator a b
+fail s = StructValidator $ \_ => Left s
+
+infixl 2 >>>
+
+||| Compose two validators so that the second validates the output of the first.
+export
+(>>>) : Validator a b -> Validator b c -> Validator a c
+left >>> right = StructValidator (unwrap left >=> unwrap right)
+
+Alternative (Validator a) where
+    left <|> right = StructValidator \x =>
+        case unwrap left x of
+            Right b => pure b
+            Left e => case unwrap right x of
+                Right b => pure b
+                Left e' => Left (e <+> " / " <+> e')
+
+||| Alter the input before validation using given function.
+export
+contramap : (a -> b) -> Validator b c -> Validator a c
+contramap f v = StructValidator (unwrap v . f)
+
+
+||| Given a value x and a decision procedure for property p, validate if p x
+||| holds, returning a proof if it does. The procedure also has access to the
+||| raw input in case it was helpful.
+export
+decide : {0 a, b : Type} -> String -> (x : b) -> {p : b -> Type} -> (a -> (x : b) -> Dec (p x)) -> Validator a (p x)
+decide {a} {b} msg x {p} f = PropValidator {p} {x} $ \a => case f a x of
+    Yes prf => Right prf
+    No _ => Left msg
+
+||| Given a function converting a into Maybe b, build a Validator of a
+||| converting it into b.
+export
+fromMaybe : (a -> String) -> (a -> Maybe b) -> Validator a b
+fromMaybe e f = StructValidator \a => case f a of
+    Nothing => Left $ e a
+    Just b => Right b
+
+||| Verify whether a String represents a natural number.
+export
+natural : Validator String Nat
+natural = fromMaybe mkError parsePositive
+    where
+    mkError : String -> String
+    mkError s = "'" <+> s <+> "' is not a natural number."
+
+||| Verify whether a String represents an Integer
+export
+integral : (Num a, Neg a) => Validator String a
+integral = fromMaybe mkError parseInteger
+    where
+    mkError : String -> String
+    mkError s = "'" <+> s <+> "' is not an integer."
+
+||| Verify that a string represents a decimal fraction.
+export
+double : Validator String Double
+double = fromMaybe mkError parseDouble
+    where
+    mkError : String -> String
+    mkError s = "'" <+> s <+> "is not a decimal."
+
+
+||| Verify whether a list has a desired length.
+export
+length : (l : Nat) -> Validator (List a) (Vect l a)
+length l = StructValidator (validateVector l)
+    where
+    validateVector : (l : Nat) -> List a -> Result (Vect l a)
+    validateVector Z [] = Right []
+    validateVector (S _) [] = Left "Missing list element."
+    validateVector Z (_ :: _) = Left "Excessive list element."
+    validateVector (S k) (x :: xs) = do
+        ys <- validateVector k xs
+        pure (x :: ys)
+
+||| Verify that certain values are equal.
+export
+equal : DecEq a => (x, y : a) -> Validator z (x = y)
+equal x y = PropValidator {p = \z => fst z = snd z} {x = (x, y)} dec
+    where
+    dec : z -> Result (x = y)
+    dec _ = case decEq x y of
+        Yes prf => Right prf
+        No _ => Left "Values are not equal."
+
+||| Verify that a Nat is less than or equal to  certain bound.
+export
+lteNat : {0 a : Type} -> (bound, n : Nat) -> Validator a (LTE n bound)
+lteNat {a} bound n = decide
+    (show n <+> " is not lower or equal to " <+> show bound)
+    {p = \x => LTE x bound}
+    n
+    (\_, x => isLTE x bound)
+
+||| Verify that a Nat is greater than or equal to certain bound.
+export
+gteNat : {0 a : Type} -> (bound, n : Nat) -> Validator a (GTE n bound)
+gteNat {a} bound n = lteNat n bound
+
+||| Verify that a Nat is strictly less than a certain bound.
+export
+ltNat : {0 a : Type} -> (bound, n : Nat) -> Validator a (LT n bound)
+ltNat bound n = lteNat bound (S n)
+
+||| Verify that a Nat is strictly greate than a certain bound.
+export
+gtNat : {0 a : Type} -> (bound, n : Nat) -> Validator a (GT n bound)
+gtNat bound n = ltNat n bound

From 208fb6fe04a8a840ad196ccfd9c74efce0656688 Mon Sep 17 00:00:00 2001
From: Sventimir <svantimir@gmail.com>
Date: Tue, 11 Aug 2020 20:51:51 +0200
Subject: [PATCH 02/16] Turn Validator into a proper monad transformer.

---
 libs/contrib/Control/Monad/Trans/Either.idr |  55 +++++++
 libs/contrib/Control/Validation.idr         | 151 +++++++++++---------
 2 files changed, 140 insertions(+), 66 deletions(-)
 create mode 100644 libs/contrib/Control/Monad/Trans/Either.idr

diff --git a/libs/contrib/Control/Monad/Trans/Either.idr b/libs/contrib/Control/Monad/Trans/Either.idr
new file mode 100644
index 000000000..3f1b78c6b
--- /dev/null
+++ b/libs/contrib/Control/Monad/Trans/Either.idr
@@ -0,0 +1,55 @@
+module Control.Monad.Trans.Either
+
+%default total
+
+
+public export
+record EitherT m a b where
+    constructor MkEitherT
+    runEitherT : m (Either a b)
+
+export
+Functor m => Functor (EitherT m a) where
+    map f (MkEitherT runEitherT) = MkEitherT (map (map f) runEitherT)
+
+export
+Monad m => Applicative (EitherT m a) where
+    pure = MkEitherT . pure . Right
+    (MkEitherT left) <*> (MkEitherT right) = MkEitherT $ do
+        l <- left
+        r <- right
+        pure (l <*> r)
+
+export
+Monad m => Monad (EitherT m a) where
+    join (MkEitherT runEitherT) = MkEitherT $ do
+        case !runEitherT of
+            Left l => pure (Left l)
+            Right (MkEitherT inner) => inner
+
+
+export
+eitherT : Monad m => (a -> m c) -> (b -> m c) -> EitherT m a b -> m c
+eitherT f g (MkEitherT runEitherT) = case !runEitherT of
+    Left l => f l
+    Right r => g r
+
+export
+bimapEitherT : Functor m => (a -> c) -> (b -> d) -> EitherT m a b -> EitherT m c d
+bimapEitherT f g (MkEitherT runEitherT) = MkEitherT (map m runEitherT)
+    where
+    m : Either a b -> Either c d
+    m (Left l) = Left (f l)
+    m (Right r) = Right (g r)
+
+export
+mapEitherT : (m (Either a b) -> n (Either c d)) -> EitherT m a b -> EitherT n c d
+mapEitherT f (MkEitherT runEitherT) = MkEitherT $ f runEitherT
+
+export
+hoist : Applicative m => Either a b -> EitherT m a b
+hoist e = MkEitherT $ pure e
+
+export
+fail : Applicative m => a -> EitherT m a b
+fail = MkEitherT . pure . Left
diff --git a/libs/contrib/Control/Validation.idr b/libs/contrib/Control/Validation.idr
index 084a0bf0d..f0a0817d9 100644
--- a/libs/contrib/Control/Validation.idr
+++ b/libs/contrib/Control/Validation.idr
@@ -10,7 +10,9 @@ module Control.Validation
 -- about user input and constructing proofs that input is indeed valid or
 -- failing early with a nice error message if it isn't.
 
+import Control.Monad.Identity
 import Control.Monad.Syntax
+import Control.Monad.Trans.Either
 import Data.Nat
 import Data.Strings
 import Data.Vect
@@ -20,8 +22,8 @@ import Decidable.Equality
 
 
 public export
-Result : Type -> Type
-Result = Either String
+Result : (Type -> Type) -> Type -> Type
+Result m = EitherT m String
 
 ||| Validators in this module come in two flavours: Structural Validators and
 ||| Property Validators. They are both wrappers around functions which take
@@ -34,94 +36,111 @@ Result = Either String
 |||
 ||| Property Validators try to prove that (usually already refined) input has
 ||| some property and return the proof if it does.
-public export
-data Validator : Type -> Type -> Type where
-    StructValidator : (a -> Result b) -> Validator a b
-    PropValidator : {0 a, b : Type} -> {0 p : b -> Type} -> {0 x : b} -> (a -> Result (p x)) -> Validator a (p x)
-
-
-unwrap : Validator a b -> a -> Result b
-unwrap (StructValidator f) = f
-unwrap (PropValidator f) = f
-
 export
-Functor (Validator a) where
-    map f v = StructValidator (map f . unwrap v)
+data ValidatorT : (Type -> Type) -> Type -> Type -> Type where
+    StructValidator : (a -> Result m b) -> ValidatorT m a b
+    PropValidator : {0 a, b : Type} -> {0 p : b -> Type} -> {0 x : b} -> (a -> Result m (p x)) -> ValidatorT m a (p x)
 
-export
-Applicative (Validator a) where
-    pure a = StructValidator (const $ pure a)
-    f <*> a = StructValidator (\x => unwrap f x <*> unwrap a x)
+Validator : Type -> Type -> Type
+Validator = ValidatorT Identity
 
-export
-Monad (Validator a) where
-    v >>= f = StructValidator $ \x => do
-        r <- unwrap v x
-        unwrap (f r) x
 
 ||| Run validation on given input, returning (Right refinedInput) if everything
 ||| is all right or (Left errorMessage) if it's not.
 export
-validate : Validator a b -> a -> Result b
-validate (StructValidator v) = v
-validate (PropValidator v) = v
+validateT : ValidatorT m a b -> a -> Result m b
+validateT (StructValidator v) = v
+validateT (PropValidator v) = v
 
-replaceError : String -> Result a -> Result a
-replaceError e (Left _) = Left e
-replaceError _ (Right x) = Right x
+||| Run validation within the Identity monad and unwrap result immediately.
+export
+validate : Validator a b -> a -> Either String b
+validate v = runIdentity . runEitherT . validateT v
+
+||| Given a function from input to Either String output, make a structural
+||| validator.
+export
+structValidator : (a -> Result m b) -> ValidatorT m a b
+structValidator = StructValidator
+
+||| Given a refined input and a decision procedure for a property, make a
+||| validator checking whether input has that property. NOTE: the input is
+||| required for type-checking only. It's user's responsibility to make sure
+||| that supplied function actually uses it.
+export
+propValidator : {0 a, b : Type} -> {0 p : b -> Type} -> (0 x : b) -> (a -> Result m (p x)) -> ValidatorT m a (p x)
+propValidator {p} x = PropValidator {p} {x}
+
+export
+Functor m => Functor (ValidatorT m a) where
+    map f v = StructValidator (map f . validateT v)
+
+export
+Monad m => Applicative (ValidatorT m a) where
+    pure a = StructValidator (const $ pure a)
+    f <*> a = StructValidator (\x => validateT f x <*> validateT a x)
+
+export
+Monad m => Monad (ValidatorT m a) where
+    v >>= f = StructValidator $ \x => do
+        r <- validateT v x
+        validateT (f r) x
+
+replaceError : Monad m => String -> Result m a -> Result m a
+replaceError e = bimapEitherT (const e) id
 
 ||| Replace validator's default error message.
 export
-withError : String -> Validator a b -> Validator a b
+withError : Monad m => String -> ValidatorT m a b -> ValidatorT m a b
 withError e (StructValidator f) = StructValidator (replaceError e . f)
 withError e (PropValidator {p} {x} f) = PropValidator {p} {x} (replaceError e . f)
 
 ||| A validator which always fails with a given message.
 export
-fail : String -> Validator a b
-fail s = StructValidator $ \_ => Left s
+fail : Applicative m => String -> ValidatorT m a b
+fail s = StructValidator $ \_ => fail s
 
 infixl 2 >>>
 
 ||| Compose two validators so that the second validates the output of the first.
 export
-(>>>) : Validator a b -> Validator b c -> Validator a c
-left >>> right = StructValidator (unwrap left >=> unwrap right)
+(>>>) : Monad m => ValidatorT m a b -> ValidatorT m b c -> ValidatorT m a c
+left >>> right = StructValidator (validateT left >=> validateT right)
 
-Alternative (Validator a) where
-    left <|> right = StructValidator \x =>
-        case unwrap left x of
-            Right b => pure b
-            Left e => case unwrap right x of
-                Right b => pure b
-                Left e' => Left (e <+> " / " <+> e')
+Monad m => Alternative (ValidatorT m a) where
+    left <|> right = StructValidator \x => MkEitherT $ do
+        case !(runEitherT $ validateT left x) of
+            (Right r) => pure $ Right r
+            (Left e) => case !(runEitherT $ validateT right x) of
+                (Right r) => pure $ Right r
+                (Left e') => pure $ Left (e <+> " / " <+> e')
 
 ||| Alter the input before validation using given function.
 export
-contramap : (a -> b) -> Validator b c -> Validator a c
-contramap f v = StructValidator (unwrap v . f)
+contramap : (a -> b) -> ValidatorT m b c -> ValidatorT m a c
+contramap f v = StructValidator (validateT v . f)
 
 
-||| Given a value x and a decision procedure for property p, validate if p x
+||| Given a value x and a decision procedure for property p, validateT if p x
 ||| holds, returning a proof if it does. The procedure also has access to the
 ||| raw input in case it was helpful.
 export
-decide : {0 a, b : Type} -> String -> (x : b) -> {p : b -> Type} -> (a -> (x : b) -> Dec (p x)) -> Validator a (p x)
+decide : Monad m => {0 a, b : Type} -> String -> (x : b) -> {p : b -> Type} -> (a -> (x : b) -> Dec (p x)) -> ValidatorT m a (p x)
 decide {a} {b} msg x {p} f = PropValidator {p} {x} $ \a => case f a x of
-    Yes prf => Right prf
-    No _ => Left msg
+    Yes prf => pure prf
+    No _ => fail msg
 
 ||| Given a function converting a into Maybe b, build a Validator of a
 ||| converting it into b.
 export
-fromMaybe : (a -> String) -> (a -> Maybe b) -> Validator a b
+fromMaybe : Monad m => (a -> String) -> (a -> Maybe b) -> ValidatorT m a b
 fromMaybe e f = StructValidator \a => case f a of
-    Nothing => Left $ e a
-    Just b => Right b
+    Nothing => fail $ e a
+    Just b => pure b
 
 ||| Verify whether a String represents a natural number.
 export
-natural : Validator String Nat
+natural : Monad m => ValidatorT m String Nat
 natural = fromMaybe mkError parsePositive
     where
     mkError : String -> String
@@ -129,7 +148,7 @@ natural = fromMaybe mkError parsePositive
 
 ||| Verify whether a String represents an Integer
 export
-integral : (Num a, Neg a) => Validator String a
+integral : (Num a, Neg a, Monad m) => ValidatorT m String a
 integral = fromMaybe mkError parseInteger
     where
     mkError : String -> String
@@ -137,7 +156,7 @@ integral = fromMaybe mkError parseInteger
 
 ||| Verify that a string represents a decimal fraction.
 export
-double : Validator String Double
+double : Monad m => ValidatorT m String Double
 double = fromMaybe mkError parseDouble
     where
     mkError : String -> String
@@ -146,30 +165,30 @@ double = fromMaybe mkError parseDouble
 
 ||| Verify whether a list has a desired length.
 export
-length : (l : Nat) -> Validator (List a) (Vect l a)
+length : Monad m => (l : Nat) -> ValidatorT m (List a) (Vect l a)
 length l = StructValidator (validateVector l)
     where
-    validateVector : (l : Nat) -> List a -> Result (Vect l a)
-    validateVector Z [] = Right []
-    validateVector (S _) [] = Left "Missing list element."
-    validateVector Z (_ :: _) = Left "Excessive list element."
+    validateVector : (l : Nat) -> List a -> Result m (Vect l a)
+    validateVector Z [] = pure []
+    validateVector (S _) [] = fail "Missing list element."
+    validateVector Z (_ :: _) = fail "Excessive list element."
     validateVector (S k) (x :: xs) = do
         ys <- validateVector k xs
         pure (x :: ys)
 
 ||| Verify that certain values are equal.
 export
-equal : DecEq a => (x, y : a) -> Validator z (x = y)
+equal : (DecEq a, Monad m) => (x, y : a) -> ValidatorT m z (x = y)
 equal x y = PropValidator {p = \z => fst z = snd z} {x = (x, y)} dec
     where
-    dec : z -> Result (x = y)
+    dec : z -> Result m (x = y)
     dec _ = case decEq x y of
-        Yes prf => Right prf
-        No _ => Left "Values are not equal."
+        Yes prf => pure prf
+        No _ => fail "Values are not equal."
 
 ||| Verify that a Nat is less than or equal to  certain bound.
 export
-lteNat : {0 a : Type} -> (bound, n : Nat) -> Validator a (LTE n bound)
+lteNat : Monad m => {0 a : Type} -> (bound, n : Nat) -> ValidatorT m a (LTE n bound)
 lteNat {a} bound n = decide
     (show n <+> " is not lower or equal to " <+> show bound)
     {p = \x => LTE x bound}
@@ -178,15 +197,15 @@ lteNat {a} bound n = decide
 
 ||| Verify that a Nat is greater than or equal to certain bound.
 export
-gteNat : {0 a : Type} -> (bound, n : Nat) -> Validator a (GTE n bound)
+gteNat : Monad m => {0 a : Type} -> (bound, n : Nat) -> ValidatorT m a (GTE n bound)
 gteNat {a} bound n = lteNat n bound
 
 ||| Verify that a Nat is strictly less than a certain bound.
 export
-ltNat : {0 a : Type} -> (bound, n : Nat) -> Validator a (LT n bound)
+ltNat : Monad m => {0 a : Type} -> (bound, n : Nat) -> ValidatorT m a (LT n bound)
 ltNat bound n = lteNat bound (S n)
 
 ||| Verify that a Nat is strictly greate than a certain bound.
 export
-gtNat : {0 a : Type} -> (bound, n : Nat) -> Validator a (GT n bound)
+gtNat : Monad m => {0 a : Type} -> (bound, n : Nat) -> ValidatorT m a (GT n bound)
 gtNat bound n = ltNat n bound

From f3168d16aa8db2d2f2818b51dbf5b1ad238f7929 Mon Sep 17 00:00:00 2001
From: Sventimir <svantimir@gmail.com>
Date: Wed, 12 Aug 2020 17:12:35 +0200
Subject: [PATCH 03/16] Add a proof that (NotBothZero 0 0) is uninhabited.

---
 libs/base/Data/Nat.idr | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/libs/base/Data/Nat.idr b/libs/base/Data/Nat.idr
index 3cb2901c6..61da3f800 100644
--- a/libs/base/Data/Nat.idr
+++ b/libs/base/Data/Nat.idr
@@ -58,6 +58,10 @@ data NotBothZero : (n, m : Nat) -> Type where
   LeftIsNotZero  : NotBothZero (S n) m
   RightIsNotZero : NotBothZero n     (S m)
 
+Uninhabited (NotBothZero 0 0) where
+  uninhabited LeftIsNotZero impossible
+  uninhabited RightIsNotZero impossible
+
 public export
 data LTE  : (n, m : Nat) -> Type where
   LTEZero : LTE Z    right

From 67bab6b08800e30dc2817cb10f8baf5d40d269f0 Mon Sep 17 00:00:00 2001
From: Sventimir <svantimir@gmail.com>
Date: Wed, 12 Aug 2020 17:33:25 +0200
Subject: [PATCH 04/16] Add Control.Validation module to contrib package.

---
 libs/base/Data/Nat.idr    | 1 +
 libs/contrib/contrib.ipkg | 2 ++
 2 files changed, 3 insertions(+)

diff --git a/libs/base/Data/Nat.idr b/libs/base/Data/Nat.idr
index 61da3f800..403b01ef2 100644
--- a/libs/base/Data/Nat.idr
+++ b/libs/base/Data/Nat.idr
@@ -58,6 +58,7 @@ data NotBothZero : (n, m : Nat) -> Type where
   LeftIsNotZero  : NotBothZero (S n) m
   RightIsNotZero : NotBothZero n     (S m)
 
+export
 Uninhabited (NotBothZero 0 0) where
   uninhabited LeftIsNotZero impossible
   uninhabited RightIsNotZero impossible
diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg
index bd2314657..56f2443c2 100644
--- a/libs/contrib/contrib.ipkg
+++ b/libs/contrib/contrib.ipkg
@@ -12,6 +12,8 @@ modules = Control.ANSI,
           Control.Algebra.Laws,
           Control.Algebra.Implementations,
 
+          Control.Validation,
+
           Data.Bool.Algebra,
 
           Data.Linear.Array,

From 41444e50501c0a4ce2d83adff70a53c8d4c2f657 Mon Sep 17 00:00:00 2001
From: Sventimir <svantimir@gmail.com>
Date: Wed, 12 Aug 2020 17:37:48 +0200
Subject: [PATCH 05/16] Export publicly the Validator type alias.

---
 libs/contrib/Control/Validation.idr | 1 +
 1 file changed, 1 insertion(+)

diff --git a/libs/contrib/Control/Validation.idr b/libs/contrib/Control/Validation.idr
index f0a0817d9..d5ffb9e88 100644
--- a/libs/contrib/Control/Validation.idr
+++ b/libs/contrib/Control/Validation.idr
@@ -41,6 +41,7 @@ data ValidatorT : (Type -> Type) -> Type -> Type -> Type where
     StructValidator : (a -> Result m b) -> ValidatorT m a b
     PropValidator : {0 a, b : Type} -> {0 p : b -> Type} -> {0 x : b} -> (a -> Result m (p x)) -> ValidatorT m a (p x)
 
+public export
 Validator : Type -> Type -> Type
 Validator = ValidatorT Identity
 

From b0bcfe9180295b13c124ce1361d1f0be027a824e Mon Sep 17 00:00:00 2001
From: Sventimir <svantimir@gmail.com>
Date: Wed, 12 Aug 2020 18:37:00 +0200
Subject: [PATCH 06/16] Export EitherT monad transformer as well.

---
 libs/contrib/contrib.ipkg | 1 +
 1 file changed, 1 insertion(+)

diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg
index 56f2443c2..0ed64c299 100644
--- a/libs/contrib/contrib.ipkg
+++ b/libs/contrib/contrib.ipkg
@@ -7,6 +7,7 @@ modules = Control.ANSI,
           Control.Linear.LIO,
           Control.Monad.Algebra,
           Control.Monad.Syntax,
+          Control.Monad.Trans.Either,
 
           Control.Algebra,
           Control.Algebra.Laws,

From daad29deb6bad7c59b4f82a800c7b56be24ee830 Mon Sep 17 00:00:00 2001
From: Sventimir <svantimir@gmail.com>
Date: Thu, 13 Aug 2020 17:49:22 +0200
Subject: [PATCH 07/16] Remove redundant constructor to the ValidatorT type.

---
 libs/contrib/Control/Validation.idr | 47 +++++++++++------------------
 1 file changed, 18 insertions(+), 29 deletions(-)

diff --git a/libs/contrib/Control/Validation.idr b/libs/contrib/Control/Validation.idr
index d5ffb9e88..ae48d7ff0 100644
--- a/libs/contrib/Control/Validation.idr
+++ b/libs/contrib/Control/Validation.idr
@@ -1,4 +1,4 @@
-module Control.Validation
+module Validation
 
 -- Main purpose of this module is verifying programmer's assumptions about
 -- user input. On one hand we want to write precisely typed programs, including
@@ -38,8 +38,7 @@ Result m = EitherT m String
 ||| some property and return the proof if it does.
 export
 data ValidatorT : (Type -> Type) -> Type -> Type -> Type where
-    StructValidator : (a -> Result m b) -> ValidatorT m a b
-    PropValidator : {0 a, b : Type} -> {0 p : b -> Type} -> {0 x : b} -> (a -> Result m (p x)) -> ValidatorT m a (p x)
+    MkValidator : (a -> Result m b) -> ValidatorT m a b
 
 public export
 Validator : Type -> Type -> Type
@@ -50,8 +49,7 @@ Validator = ValidatorT Identity
 ||| is all right or (Left errorMessage) if it's not.
 export
 validateT : ValidatorT m a b -> a -> Result m b
-validateT (StructValidator v) = v
-validateT (PropValidator v) = v
+validateT (MkValidator v) = v
 
 ||| Run validation within the Identity monad and unwrap result immediately.
 export
@@ -61,29 +59,21 @@ validate v = runIdentity . runEitherT . validateT v
 ||| Given a function from input to Either String output, make a structural
 ||| validator.
 export
-structValidator : (a -> Result m b) -> ValidatorT m a b
-structValidator = StructValidator
-
-||| Given a refined input and a decision procedure for a property, make a
-||| validator checking whether input has that property. NOTE: the input is
-||| required for type-checking only. It's user's responsibility to make sure
-||| that supplied function actually uses it.
-export
-propValidator : {0 a, b : Type} -> {0 p : b -> Type} -> (0 x : b) -> (a -> Result m (p x)) -> ValidatorT m a (p x)
-propValidator {p} x = PropValidator {p} {x}
+validator : (a -> Result m b) -> ValidatorT m a b
+validator = MkValidator
 
 export
 Functor m => Functor (ValidatorT m a) where
-    map f v = StructValidator (map f . validateT v)
+    map f v = MkValidator (map f . validateT v)
 
 export
 Monad m => Applicative (ValidatorT m a) where
-    pure a = StructValidator (const $ pure a)
-    f <*> a = StructValidator (\x => validateT f x <*> validateT a x)
+    pure a = MkValidator (const $ pure a)
+    f <*> a = MkValidator (\x => validateT f x <*> validateT a x)
 
 export
 Monad m => Monad (ValidatorT m a) where
-    v >>= f = StructValidator $ \x => do
+    v >>= f = MkValidator $ \x => do
         r <- validateT v x
         validateT (f r) x
 
@@ -93,23 +83,22 @@ replaceError e = bimapEitherT (const e) id
 ||| Replace validator's default error message.
 export
 withError : Monad m => String -> ValidatorT m a b -> ValidatorT m a b
-withError e (StructValidator f) = StructValidator (replaceError e . f)
-withError e (PropValidator {p} {x} f) = PropValidator {p} {x} (replaceError e . f)
+withError e (MkValidator f) = MkValidator (replaceError e . f)
 
 ||| A validator which always fails with a given message.
 export
 fail : Applicative m => String -> ValidatorT m a b
-fail s = StructValidator $ \_ => fail s
+fail s = MkValidator $ \_ => fail s
 
 infixl 2 >>>
 
 ||| Compose two validators so that the second validates the output of the first.
 export
 (>>>) : Monad m => ValidatorT m a b -> ValidatorT m b c -> ValidatorT m a c
-left >>> right = StructValidator (validateT left >=> validateT right)
+left >>> right = MkValidator (validateT left >=> validateT right)
 
 Monad m => Alternative (ValidatorT m a) where
-    left <|> right = StructValidator \x => MkEitherT $ do
+    left <|> right = MkValidator \x => MkEitherT $ do
         case !(runEitherT $ validateT left x) of
             (Right r) => pure $ Right r
             (Left e) => case !(runEitherT $ validateT right x) of
@@ -119,7 +108,7 @@ Monad m => Alternative (ValidatorT m a) where
 ||| Alter the input before validation using given function.
 export
 contramap : (a -> b) -> ValidatorT m b c -> ValidatorT m a c
-contramap f v = StructValidator (validateT v . f)
+contramap f v = MkValidator (validateT v . f)
 
 
 ||| Given a value x and a decision procedure for property p, validateT if p x
@@ -127,7 +116,7 @@ contramap f v = StructValidator (validateT v . f)
 ||| raw input in case it was helpful.
 export
 decide : Monad m => {0 a, b : Type} -> String -> (x : b) -> {p : b -> Type} -> (a -> (x : b) -> Dec (p x)) -> ValidatorT m a (p x)
-decide {a} {b} msg x {p} f = PropValidator {p} {x} $ \a => case f a x of
+decide {a} {b} msg x {p} f = MkValidator $ \a => case f a x of
     Yes prf => pure prf
     No _ => fail msg
 
@@ -135,7 +124,7 @@ decide {a} {b} msg x {p} f = PropValidator {p} {x} $ \a => case f a x of
 ||| converting it into b.
 export
 fromMaybe : Monad m => (a -> String) -> (a -> Maybe b) -> ValidatorT m a b
-fromMaybe e f = StructValidator \a => case f a of
+fromMaybe e f = MkValidator \a => case f a of
     Nothing => fail $ e a
     Just b => pure b
 
@@ -167,7 +156,7 @@ double = fromMaybe mkError parseDouble
 ||| Verify whether a list has a desired length.
 export
 length : Monad m => (l : Nat) -> ValidatorT m (List a) (Vect l a)
-length l = StructValidator (validateVector l)
+length l = MkValidator (validateVector l)
     where
     validateVector : (l : Nat) -> List a -> Result m (Vect l a)
     validateVector Z [] = pure []
@@ -180,7 +169,7 @@ length l = StructValidator (validateVector l)
 ||| Verify that certain values are equal.
 export
 equal : (DecEq a, Monad m) => (x, y : a) -> ValidatorT m z (x = y)
-equal x y = PropValidator {p = \z => fst z = snd z} {x = (x, y)} dec
+equal x y = MkValidator dec
     where
     dec : z -> Result m (x = y)
     dec _ = case decEq x y of

From ffbfecb376c09d995ff907c344820d1efcd5ae5d Mon Sep 17 00:00:00 2001
From: Sventimir <svantimir@gmail.com>
Date: Thu, 13 Aug 2020 17:52:43 +0200
Subject: [PATCH 08/16] Fix broken name of the module.

---
 libs/contrib/Control/Validation.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/libs/contrib/Control/Validation.idr b/libs/contrib/Control/Validation.idr
index ae48d7ff0..e7d67472f 100644
--- a/libs/contrib/Control/Validation.idr
+++ b/libs/contrib/Control/Validation.idr
@@ -1,4 +1,4 @@
-module Validation
+module Control.Validation
 
 -- Main purpose of this module is verifying programmer's assumptions about
 -- user input. On one hand we want to write precisely typed programs, including

From 021a5a61548fcc06733e4b3ee47aa13d7ec3e5bf Mon Sep 17 00:00:00 2001
From: Sventimir <svantimir@gmail.com>
Date: Thu, 13 Aug 2020 18:28:39 +0200
Subject: [PATCH 09/16] Update the docs.

---
 libs/contrib/Control/Validation.idr | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

diff --git a/libs/contrib/Control/Validation.idr b/libs/contrib/Control/Validation.idr
index e7d67472f..d87132005 100644
--- a/libs/contrib/Control/Validation.idr
+++ b/libs/contrib/Control/Validation.idr
@@ -29,13 +29,6 @@ Result m = EitherT m String
 ||| Property Validators. They are both wrappers around functions which take
 ||| some input and confirm that it's valid (returning some witness of its
 ||| validity) or fail with an error described by a string.
-|||
-||| Structural Validators work by refining the type of input, for instance
-||| checking whether a string encodes a number and returning that number if it
-||| does. More generally, they convert raw input to some more restricted type.
-|||
-||| Property Validators try to prove that (usually already refined) input has
-||| some property and return the proof if it does.
 export
 data ValidatorT : (Type -> Type) -> Type -> Type -> Type where
     MkValidator : (a -> Result m b) -> ValidatorT m a b
@@ -56,8 +49,7 @@ export
 validate : Validator a b -> a -> Either String b
 validate v = runIdentity . runEitherT . validateT v
 
-||| Given a function from input to Either String output, make a structural
-||| validator.
+||| Given a function from input to Either String output, make a validator.
 export
 validator : (a -> Result m b) -> ValidatorT m a b
 validator = MkValidator

From c6d8ef30edd77562e3c489a6a1b7ad73c8ebd67c Mon Sep 17 00:00:00 2001
From: Sventimir <svantimir@gmail.com>
Date: Sat, 15 Aug 2020 14:27:27 +0200
Subject: [PATCH 10/16] Add Control.Category module ported from Idris.

---
 libs/contrib/Control/Category.idr | 27 +++++++++++++++++++++++++++
 libs/contrib/contrib.ipkg         |  2 ++
 2 files changed, 29 insertions(+)
 create mode 100644 libs/contrib/Control/Category.idr

diff --git a/libs/contrib/Control/Category.idr b/libs/contrib/Control/Category.idr
new file mode 100644
index 000000000..a506f59e6
--- /dev/null
+++ b/libs/contrib/Control/Category.idr
@@ -0,0 +1,27 @@
+module Control.Category
+
+import Data.Morphisms
+
+
+public export
+interface Category (cat : Type -> Type -> Type) where
+  id  : cat a a
+  (.) : cat b c -> cat a b -> cat a c
+
+public export
+Category Morphism where
+  id                = Mor id
+  -- disambiguation needed below, because unification can now get further
+  -- here with Category.(.) and it's only interface resolution that fails!
+  (Mor f) . (Mor g) = Mor $ Basics.(.) f g
+
+public export
+Monad m => Category (Kleislimorphism m) where
+  id                        = Kleisli (pure . id)
+  (Kleisli f) . (Kleisli g) = Kleisli $ \a => g a >>= f
+
+infixr 1 >>>
+
+public export
+(>>>) : Category cat => cat a b -> cat b c -> cat a c
+f >>> g = g . f
diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg
index 0ed64c299..bebe30876 100644
--- a/libs/contrib/contrib.ipkg
+++ b/libs/contrib/contrib.ipkg
@@ -13,6 +13,8 @@ modules = Control.ANSI,
           Control.Algebra.Laws,
           Control.Algebra.Implementations,
 
+          Control.Category,
+
           Control.Validation,
 
           Data.Bool.Algebra,

From 886c70c19614bd4c7a46a314feb408e90b547ce6 Mon Sep 17 00:00:00 2001
From: Sventimir <svantimir@gmail.com>
Date: Sat, 15 Aug 2020 14:28:08 +0200
Subject: [PATCH 11/16] Add Data.Either module ported from Idris.

---
 libs/contrib/Data/Either.idr | 103 +++++++++++++++++++++++++++++++++++
 libs/contrib/contrib.ipkg    |   2 +
 2 files changed, 105 insertions(+)
 create mode 100644 libs/contrib/Data/Either.idr

diff --git a/libs/contrib/Data/Either.idr b/libs/contrib/Data/Either.idr
new file mode 100644
index 000000000..02a12f59e
--- /dev/null
+++ b/libs/contrib/Data/Either.idr
@@ -0,0 +1,103 @@
+ module Data.Either
+
+--------------------------------------------------------------------------------
+-- Syntactic tests
+--------------------------------------------------------------------------------
+
+public export
+||| True if the argument is Left, False otherwise
+isLeft : Either a b -> Bool
+isLeft (Left l)  = True
+isLeft (Right r) = False
+
+public export
+||| True if the argument is Right, False otherwise
+isRight : Either a b -> Bool
+isRight (Left l)  = False
+isRight (Right r) = True
+
+--------------------------------------------------------------------------------
+-- Misc.
+--------------------------------------------------------------------------------
+
+public export
+||| Keep the payloads of all Left constructors in a list of Eithers
+lefts : List (Either a b) -> List a
+lefts []      = []
+lefts (x::xs) =
+  case x of
+    Left  l => l :: lefts xs
+    Right r => lefts xs
+
+public export
+||| Keep the payloads of all Right constructors in a list of Eithers
+rights : List (Either a b) -> List b
+rights []      = []
+rights (x::xs) =
+  case x of
+    Left  l => rights xs
+    Right r => r :: rights xs
+
+public export
+||| Split a list of Eithers into a list of the left elements and a list of the right elements
+partitionEithers : List (Either a b) -> (List a, List b)
+partitionEithers l = (lefts l, rights l)
+
+public export
+||| Remove a "useless" Either by collapsing the case distinction
+fromEither : Either a a -> a
+fromEither (Left l)  = l
+fromEither (Right r) = r
+
+public export
+||| Right becomes left and left becomes right
+mirror : Either a b -> Either b a
+mirror (Left  x) = Right x
+mirror (Right x) = Left x
+
+--------------------------------------------------------------------------------
+-- Conversions
+--------------------------------------------------------------------------------
+
+public export
+||| Convert a Maybe to an Either by using a default value in case of Nothing
+||| @ e the default value
+maybeToEither : (def : Lazy e) -> Maybe a -> Either e a
+maybeToEither def (Just j) = Right j
+maybeToEither def Nothing  = Left  def
+
+public export
+||| Convert an Either to a Maybe from Right injection
+eitherToMaybe : Either e a -> Maybe a
+eitherToMaybe (Left _) = Nothing
+eitherToMaybe (Right x) = Just x
+
+--------------------------------------------------------------------------------
+-- Implementations
+--------------------------------------------------------------------------------
+
+public export
+(Eq a, Eq b) => Eq (Either a b) where
+  (==) (Left x)  (Left y)  = x == y
+  (==) (Right x) (Right y) = x == y
+  (==) _         _         = False
+
+
+
+--------------------------------------------------------------------------------
+-- Injectivity of constructors
+--------------------------------------------------------------------------------
+
+total
+public export
+||| Left is injective
+leftInjective : {b : Type} -> {x : a} -> {y : a}
+                    -> (Left {b = b} x = Left {b = b} y) -> (x = y)
+leftInjective Refl = Refl
+
+total
+public export
+||| Right is injective
+rightInjective : {a : Type} -> {x : b} -> {y : b}
+                     -> (Right {a = a} x = Right {a = a} y) -> (x = y)
+rightInjective Refl = Refl
diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg
index bebe30876..7c53de555 100644
--- a/libs/contrib/contrib.ipkg
+++ b/libs/contrib/contrib.ipkg
@@ -28,6 +28,8 @@ modules = Control.ANSI,
           Data.List.Views.Extra,
           Data.List.Palindrome,
 
+          Data.Either,
+
           Data.Fin.Extra,
 
           Data.Logic.Propositional,

From ba197a230e7de431e35f9e659aff946f8a46fc67 Mon Sep 17 00:00:00 2001
From: Sventimir <svantimir@gmail.com>
Date: Sat, 15 Aug 2020 16:42:00 +0200
Subject: [PATCH 12/16] Port Control.Arrow from Idris.

---
 libs/contrib/Control/Arrow.idr | 124 +++++++++++++++++++++++++++++++++
 libs/contrib/contrib.ipkg      |   1 +
 2 files changed, 125 insertions(+)
 create mode 100644 libs/contrib/Control/Arrow.idr

diff --git a/libs/contrib/Control/Arrow.idr b/libs/contrib/Control/Arrow.idr
new file mode 100644
index 000000000..5d74c4dce
--- /dev/null
+++ b/libs/contrib/Control/Arrow.idr
@@ -0,0 +1,124 @@
+module Control.Arrow
+
+import Control.Category
+import Data.Either
+import Data.Morphisms
+
+
+infixr 5 <++>
+infixr 3 ***
+infixr 3 &&&
+infixr 2 +++
+infixr 2 \|/
+
+public export
+interface Category arr => Arrow (arr : Type -> Type -> Type) where
+  arrow  : (a -> b) -> arr a b
+  first  : arr a b -> arr (a, c) (b, c)
+
+  second : arr a b -> arr (c, a) (c, b)
+  second f = arrow {arr = arr} swap >>> first f >>> arrow {arr = arr} swap
+    where
+    swap : (x, y) -> (y, x)
+    swap (a, b) = (b, a)
+
+  (***)  : arr a b -> arr a' b' -> arr (a, a') (b, b')
+  f *** g = first f >>> second g
+
+  (&&&)  : arr a b -> arr a b' -> arr a (b, b')
+  f &&& g = arrow dup >>> f *** g
+    where
+    dup : x -> (x,x)
+    dup x = (x,x)
+
+public export
+implementation Arrow Morphism where
+  arrow  f            = Mor f
+  first  (Mor f)      = Mor $ \(a, b) => (f a, b)
+  second (Mor f)      = Mor $ \(a, b) => (a, f b)
+  (Mor f) *** (Mor g) = Mor $ \(a, b) => (f a, g b)
+  (Mor f) &&& (Mor g) = Mor $ \a => (f a, g a)
+
+public export
+implementation Monad m => Arrow (Kleislimorphism m) where
+  arrow f = Kleisli (pure . f)
+  first (Kleisli f) =  Kleisli $ \(a, b) => do x <- f a
+                                               pure (x, b)
+
+  second (Kleisli f) = Kleisli $ \(a, b) => do x <- f b
+                                               pure (a, x)
+
+  (Kleisli f) *** (Kleisli g) = Kleisli $ \(a, b) => do x <- f a
+                                                        y <- g b
+                                                        pure (x, y)
+
+  (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a
+                                                   y <- g a
+                                                   pure (x, y)
+
+public export
+interface Arrow arr => ArrowZero (arr : Type -> Type -> Type) where
+  zeroArrow : arr a b
+
+public export
+interface ArrowZero arr => ArrowPlus (arr : Type -> Type -> Type) where
+  (<++>) : arr a b -> arr a b -> arr a b
+
+public export
+interface Arrow arr => ArrowChoice (arr : Type -> Type -> Type) where
+  left  : arr a b -> arr (Either a c) (Either b c)
+
+  right : arr a b -> arr (Either c a) (Either c b)
+  right f = arrow mirror >>> left f >>> arrow mirror
+
+
+  (+++) : arr a b -> arr c d -> arr (Either a c) (Either b d)
+  f +++ g = left f >>> right g
+
+  (\|/) : arr a b -> arr c b -> arr (Either a c) b
+  f \|/ g = f +++ g >>> arrow fromEither
+    where
+    fromEither : Either b b -> b
+    fromEither (Left b) = b
+    fromEither (Right b) = b
+
+public export
+implementation Monad m => ArrowChoice (Kleislimorphism m) where
+  left f                      = f          +++ (arrow id)
+  right f                     = (arrow id) +++ f
+  f           +++ g           = (f >>> (arrow Left)) \|/ (g >>> (arrow Right))
+  (Kleisli f) \|/ (Kleisli g) = Kleisli (either f g)
+
+public export
+interface Arrow arr => ArrowApply (arr : Type -> Type -> Type) where
+  app : arr (arr a b, a) b
+
+public export
+implementation Monad m => ArrowApply (Kleislimorphism m) where
+  app = Kleisli $ \(Kleisli f, x) => f x
+
+public export
+data ArrowMonad : (Type -> Type -> Type) -> Type -> Type where
+  MkArrowMonad : (runArrowMonad : arr (the Type ()) a) -> ArrowMonad arr a
+
+public export
+runArrowMonad : ArrowMonad arr a -> arr (the Type ()) a
+runArrowMonad (MkArrowMonad a) = a
+
+public export
+implementation Arrow a => Functor (ArrowMonad a) where
+  map f (MkArrowMonad m) = MkArrowMonad $ m >>> arrow f
+
+public export
+implementation Arrow a => Applicative (ArrowMonad a) where
+  pure x = MkArrowMonad $ arrow $ \_ => x
+  (MkArrowMonad f) <*> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)
+
+public export
+implementation ArrowApply a => Monad (ArrowMonad a) where
+  (MkArrowMonad m) >>= f =
+    MkArrowMonad $ m >>> (arrow $ \x => (runArrowMonad (f x), ())) >>> app
+
+public export
+interface Arrow arr => ArrowLoop (arr : Type -> Type -> Type) where
+  loop : arr (Pair a c) (Pair b c) -> arr a b
diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg
index 7c53de555..b94ecffdd 100644
--- a/libs/contrib/contrib.ipkg
+++ b/libs/contrib/contrib.ipkg
@@ -13,6 +13,7 @@ modules = Control.ANSI,
           Control.Algebra.Laws,
           Control.Algebra.Implementations,
 
+          Control.Arrow,
           Control.Category,
 
           Control.Validation,

From 01e6263a87a3a60b15457bd08aca2fada15413fc Mon Sep 17 00:00:00 2001
From: Sventimir <svantimir@gmail.com>
Date: Tue, 18 Aug 2020 13:56:21 +0200
Subject: [PATCH 13/16] Introduce the notion of PropValidator so that value
 under validation gets ignored more explicitly in those.

---
 libs/contrib/Control/Validation.idr | 60 ++++++++++++++++++-----------
 1 file changed, 38 insertions(+), 22 deletions(-)

diff --git a/libs/contrib/Control/Validation.idr b/libs/contrib/Control/Validation.idr
index d87132005..926833cd4 100644
--- a/libs/contrib/Control/Validation.idr
+++ b/libs/contrib/Control/Validation.idr
@@ -33,6 +33,14 @@ export
 data ValidatorT : (Type -> Type) -> Type -> Type -> Type where
     MkValidator : (a -> Result m b) -> ValidatorT m a b
 
+||| A type of validator trying to prove properties of values. It's type is
+||| significantly different than that of an ordinary validator and cannot be
+||| made an instance of Monad interface, because it's last parameter is
+||| (t -> Type) instead of just Type. Therefore it must be explicitly turned
+||| into an ordinary validator using the prop function below.
+data PropValidator : (Type -> Type) -> (t : Type) -> (t -> Type) -> Type where
+    MkPropValidator : ((x : t) -> Result m (p x)) -> PropValidator m t p
+
 public export
 Validator : Type -> Type -> Type
 Validator = ValidatorT Identity
@@ -69,6 +77,13 @@ Monad m => Monad (ValidatorT m a) where
         r <- validateT v x
         validateT (f r) x
 
+||| Plug a property validator into the chain of other validators. The value
+||| under validation will be ignored and the value whose property is going to
+||| be checked must be supplied manually. Otherwise Idris won;t be able to
+||| unify.
+prop : PropValidator m t p -> (x : t) -> ValidatorT m a (p x)
+prop (MkPropValidator v) x = MkValidator (const $ v x)
+
 replaceError : Monad m => String -> Result m a -> Result m a
 replaceError e = bimapEitherT (const e) id
 
@@ -107,10 +122,10 @@ contramap f v = MkValidator (validateT v . f)
 ||| holds, returning a proof if it does. The procedure also has access to the
 ||| raw input in case it was helpful.
 export
-decide : Monad m => {0 a, b : Type} -> String -> (x : b) -> {p : b -> Type} -> (a -> (x : b) -> Dec (p x)) -> ValidatorT m a (p x)
-decide {a} {b} msg x {p} f = MkValidator $ \a => case f a x of
+decide : Monad m => (t -> String) -> ((x : t) -> Dec (p x)) -> PropValidator m t p
+decide msg dec = MkPropValidator \x => case dec x of
     Yes prf => pure prf
-    No _ => fail msg
+    No _ => fail (msg x)
 
 ||| Given a function converting a into Maybe b, build a Validator of a
 ||| converting it into b.
@@ -160,34 +175,35 @@ length l = MkValidator (validateVector l)
 
 ||| Verify that certain values are equal.
 export
-equal : (DecEq a, Monad m) => (x, y : a) -> ValidatorT m z (x = y)
-equal x y = MkValidator dec
-    where
-    dec : z -> Result m (x = y)
-    dec _ = case decEq x y of
-        Yes prf => pure prf
-        No _ => fail "Values are not equal."
+equal : (DecEq t, Monad m) => (a : t) -> PropValidator m t (\b => a = b)
+equal a = MkPropValidator \b => case decEq a b of
+    Yes prf => pure prf
+    No _ => fail "Values are not equal."
 
 ||| Verify that a Nat is less than or equal to  certain bound.
 export
-lteNat : Monad m => {0 a : Type} -> (bound, n : Nat) -> ValidatorT m a (LTE n bound)
-lteNat {a} bound n = decide
-    (show n <+> " is not lower or equal to " <+> show bound)
-    {p = \x => LTE x bound}
-    n
-    (\_, x => isLTE x bound)
+lteNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip LTE bound)
+lteNat bound = decide
+    (\n => show n <+> " is not lower or equal to " <+> show bound)
+    (\n => isLTE n bound)
 
 ||| Verify that a Nat is greater than or equal to certain bound.
 export
-gteNat : Monad m => {0 a : Type} -> (bound, n : Nat) -> ValidatorT m a (GTE n bound)
-gteNat {a} bound n = lteNat n bound
+gteNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip GTE bound)
+gteNat bound = decide
+    (\n => show n <+> " is not greater or equal to " <+> show bound)
+    (isLTE bound)
 
 ||| Verify that a Nat is strictly less than a certain bound.
 export
-ltNat : Monad m => {0 a : Type} -> (bound, n : Nat) -> ValidatorT m a (LT n bound)
-ltNat bound n = lteNat bound (S n)
+ltNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip LT bound)
+ltNat bound = decide
+    (\n => show n <+> " is not strictly lower than " <+> show bound)
+    (\n => isLTE (S n) bound)
 
 ||| Verify that a Nat is strictly greate than a certain bound.
 export
-gtNat : Monad m => {0 a : Type} -> (bound, n : Nat) -> ValidatorT m a (GT n bound)
-gtNat bound n = ltNat n bound
+gtNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip GT bound)
+gtNat bound = decide
+    (\n => show n <+> " is not strictly greater than " <+> show bound)
+    (isLTE (S bound))

From 016cd213b92b559a8935bdfee257827f29f69237 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9=20Videla?= <andre.videla@gmail.com>
Date: Fri, 22 Jan 2021 00:53:12 +0000
Subject: [PATCH 14/16] Delete Either.idr

---
 libs/contrib/Data/Either.idr | 103 -----------------------------------
 1 file changed, 103 deletions(-)
 delete mode 100644 libs/contrib/Data/Either.idr

diff --git a/libs/contrib/Data/Either.idr b/libs/contrib/Data/Either.idr
deleted file mode 100644
index 02a12f59e..000000000
--- a/libs/contrib/Data/Either.idr
+++ /dev/null
@@ -1,103 +0,0 @@
- module Data.Either
-
---------------------------------------------------------------------------------
--- Syntactic tests
---------------------------------------------------------------------------------
-
-public export
-||| True if the argument is Left, False otherwise
-isLeft : Either a b -> Bool
-isLeft (Left l)  = True
-isLeft (Right r) = False
-
-public export
-||| True if the argument is Right, False otherwise
-isRight : Either a b -> Bool
-isRight (Left l)  = False
-isRight (Right r) = True
-
---------------------------------------------------------------------------------
--- Misc.
---------------------------------------------------------------------------------
-
-public export
-||| Keep the payloads of all Left constructors in a list of Eithers
-lefts : List (Either a b) -> List a
-lefts []      = []
-lefts (x::xs) =
-  case x of
-    Left  l => l :: lefts xs
-    Right r => lefts xs
-
-public export
-||| Keep the payloads of all Right constructors in a list of Eithers
-rights : List (Either a b) -> List b
-rights []      = []
-rights (x::xs) =
-  case x of
-    Left  l => rights xs
-    Right r => r :: rights xs
-
-public export
-||| Split a list of Eithers into a list of the left elements and a list of the right elements
-partitionEithers : List (Either a b) -> (List a, List b)
-partitionEithers l = (lefts l, rights l)
-
-public export
-||| Remove a "useless" Either by collapsing the case distinction
-fromEither : Either a a -> a
-fromEither (Left l)  = l
-fromEither (Right r) = r
-
-public export
-||| Right becomes left and left becomes right
-mirror : Either a b -> Either b a
-mirror (Left  x) = Right x
-mirror (Right x) = Left x
-
---------------------------------------------------------------------------------
--- Conversions
---------------------------------------------------------------------------------
-
-public export
-||| Convert a Maybe to an Either by using a default value in case of Nothing
-||| @ e the default value
-maybeToEither : (def : Lazy e) -> Maybe a -> Either e a
-maybeToEither def (Just j) = Right j
-maybeToEither def Nothing  = Left  def
-
-public export
-||| Convert an Either to a Maybe from Right injection
-eitherToMaybe : Either e a -> Maybe a
-eitherToMaybe (Left _) = Nothing
-eitherToMaybe (Right x) = Just x
-
---------------------------------------------------------------------------------
--- Implementations
---------------------------------------------------------------------------------
-
-public export
-(Eq a, Eq b) => Eq (Either a b) where
-  (==) (Left x)  (Left y)  = x == y
-  (==) (Right x) (Right y) = x == y
-  (==) _         _         = False
-
-
-
---------------------------------------------------------------------------------
--- Injectivity of constructors
---------------------------------------------------------------------------------
-
-total
-public export
-||| Left is injective
-leftInjective : {b : Type} -> {x : a} -> {y : a}
-                    -> (Left {b = b} x = Left {b = b} y) -> (x = y)
-leftInjective Refl = Refl
-
-total
-public export
-||| Right is injective
-rightInjective : {a : Type} -> {x : b} -> {y : b}
-                     -> (Right {a = a} x = Right {a = a} y) -> (x = y)
-rightInjective Refl = Refl

From 2e063544e816b08f362cc97a89dd2fa8d51d6360 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9=20Videla?= <andre.videla@gmail.com>
Date: Fri, 22 Jan 2021 00:53:59 +0000
Subject: [PATCH 15/16] Update Category.idr

---
 libs/contrib/Control/Category.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/libs/contrib/Control/Category.idr b/libs/contrib/Control/Category.idr
index a506f59e6..05ca06ef4 100644
--- a/libs/contrib/Control/Category.idr
+++ b/libs/contrib/Control/Category.idr
@@ -4,7 +4,7 @@ import Data.Morphisms
 
 
 public export
-interface Category (cat : Type -> Type -> Type) where
+interface Category (0 cat : Type -> Type -> Type) where
   id  : cat a a
   (.) : cat b c -> cat a b -> cat a c
 

From 3bd2fae5257011cb27a34483ca40dc571a6b14cd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9=20Videla?= <andre.videla@gmail.com>
Date: Fri, 22 Jan 2021 00:54:58 +0000
Subject: [PATCH 16/16] Update Arrow.idr

---
 libs/contrib/Control/Arrow.idr | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/libs/contrib/Control/Arrow.idr b/libs/contrib/Control/Arrow.idr
index 5d74c4dce..c74d67171 100644
--- a/libs/contrib/Control/Arrow.idr
+++ b/libs/contrib/Control/Arrow.idr
@@ -12,7 +12,7 @@ infixr 2 +++
 infixr 2 \|/
 
 public export
-interface Category arr => Arrow (arr : Type -> Type -> Type) where
+interface Category arr => Arrow (0 arr : Type -> Type -> Type) where
   arrow  : (a -> b) -> arr a b
   first  : arr a b -> arr (a, c) (b, c)
 
@@ -57,15 +57,15 @@ implementation Monad m => Arrow (Kleislimorphism m) where
                                                    pure (x, y)
 
 public export
-interface Arrow arr => ArrowZero (arr : Type -> Type -> Type) where
+interface Arrow arr => ArrowZero (0 arr : Type -> Type -> Type) where
   zeroArrow : arr a b
 
 public export
-interface ArrowZero arr => ArrowPlus (arr : Type -> Type -> Type) where
+interface ArrowZero arr => ArrowPlus (0 arr : Type -> Type -> Type) where
   (<++>) : arr a b -> arr a b -> arr a b
 
 public export
-interface Arrow arr => ArrowChoice (arr : Type -> Type -> Type) where
+interface Arrow arr => ArrowChoice (0 arr : Type -> Type -> Type) where
   left  : arr a b -> arr (Either a c) (Either b c)
 
   right : arr a b -> arr (Either c a) (Either c b)
@@ -90,7 +90,7 @@ implementation Monad m => ArrowChoice (Kleislimorphism m) where
   (Kleisli f) \|/ (Kleisli g) = Kleisli (either f g)
 
 public export
-interface Arrow arr => ArrowApply (arr : Type -> Type -> Type) where
+interface Arrow arr => ArrowApply (0 arr : Type -> Type -> Type) where
   app : arr (arr a b, a) b
 
 public export
@@ -120,5 +120,5 @@ implementation ArrowApply a => Monad (ArrowMonad a) where
     MkArrowMonad $ m >>> (arrow $ \x => (runArrowMonad (f x), ())) >>> app
 
 public export
-interface Arrow arr => ArrowLoop (arr : Type -> Type -> Type) where
+interface Arrow arr => ArrowLoop (0 arr : Type -> Type -> Type) where
   loop : arr (Pair a c) (Pair b c) -> arr a b