refactor Uninhabited implementation for Elem types

CHANGELOG_NEXT.md

@@ -244,6 +244,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
   `SIsNonZero` was made to be an alias for `ItIsSucc`, was marked as deprecated,
   and won't work on LHS anymore.
 
+* Refactor `Uninhabited` implementation for `Data.List.Elem`, `Data.List1.Elem`, `Data.SnocList.Elem` and `Data.Vect.Elem`
+  so it can be used for homogeneous (===) and heterogeneous (~=~) equality.
+
 #### Contrib
 
 * `Data.List.Lazy` was moved from `contrib` to `base`.

libs/base/Data/List/Elem.idr

@@ -19,11 +19,11 @@ data Elem : a -> List a -> Type where
      There : Elem x xs -> Elem x (y :: xs)
 
 export
-Uninhabited (Here = There e) where
+Uninhabited (Here {x} {xs} = There {x = x'} {y} {xs = xs'} e) where
   uninhabited Refl impossible
 
 export
-Uninhabited (There e = Here) where
+Uninhabited (There {x} {y} {xs} e = Here {x = x'} {xs = xs'}) where
   uninhabited Refl impossible
 
 export

libs/base/Data/List1/Elem.idr

@@ -21,11 +21,11 @@ data Elem : a -> List1 a -> Type where
      There : Elem x xs -> Elem x (y ::: xs)
 
 export
-Uninhabited (List1.Elem.Here = List1.Elem.There e) where
+Uninhabited (List1.Elem.Here {x} {xs} = List1.Elem.There {x = x'} {y} {xs = xs'} e) where
   uninhabited Refl impossible
 
 export
-Uninhabited (List1.Elem.There e = List1.Elem.Here) where
+Uninhabited (List1.Elem.There {x} {y} {xs} e = List1.Elem.Here {x = x'} {xs = xs'}) where
   uninhabited Refl impossible
 
 export
@@ -84,4 +84,3 @@ export
 elemMap : (0 f : a -> b) -> List1.Elem.Elem x xs -> List1.Elem.Elem (f x) (map f xs)
 elemMap f  Here      = Here
 elemMap f (There el) = There $ elemMap f el
-

libs/base/Data/SnocList/Elem.idr

@@ -14,11 +14,11 @@ data Elem : a -> SnocList a -> Type where
   There : {0 x, y : a} -> Elem x sx -> Elem x (sx :< y)
 
 export
-Uninhabited (Here = There e) where
+Uninhabited (Here {x} {sx} = There {x = x'} {y} {sx = sx'} e) where
   uninhabited Refl impossible
 
 export
-Uninhabited (There e = Here) where
+Uninhabited (There {x} {y} {sx} e = Here {x = x'} {sx = sx'}) where
   uninhabited Refl impossible
 
 export

libs/base/Data/Vect/Elem.idr

@@ -17,11 +17,11 @@ data Elem : a -> Vect k a -> Type where
   There : (later : Elem x xs) -> Elem x (y::xs)
 
 export
-Uninhabited (Here = There e) where
+Uninhabited (Here {x} {xs} = There {x = x'} {y} {xs = xs'} e) where
   uninhabited Refl impossible
 
 export
-Uninhabited (There e = Here) where
+Uninhabited (There {x} {y} {xs} e = Here {x = x'} {xs = xs'}) where
   uninhabited Refl impossible
 
 export

tests/base/data_list003/Elem.idr

@@ -0,0 +1,27 @@
+import Data.List
+import Data.List.Elem
+
+decHomogeneousElem : (el1 : Elem x xs) -> (el2 : Elem x xs) -> Dec (el1 === el2)
+decHomogeneousElem Here         Here         = Yes Refl
+decHomogeneousElem (There _)    Here         = No uninhabited
+decHomogeneousElem Here         (There _)    = No uninhabited
+decHomogeneousElem (There el1') (There el2') = case decHomogeneousElem el1' el2' of
+                                                Yes Refl => Yes Refl
+                                                No contra => No $ \Refl => contra Refl
+
+decHomogeneousElem' : (el1 : Elem x xs) -> (el2 : Elem x xs) -> Dec (el1 = el2)
+decHomogeneousElem' = decHomogeneousElem
+
+decHeterogeneousElem : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 ~=~ el2)
+decHeterogeneousElem Here         Here         = Yes Refl
+decHeterogeneousElem (There _)    Here         = No uninhabited
+decHeterogeneousElem Here         (There _)    = No uninhabited
+decHeterogeneousElem (There el1') (There el2') = case decHeterogeneousElem el1' el2' of
+                                                  Yes Refl => Yes Refl
+                                                  No contra => No $ \Refl => contra Refl
+
+decHeterogeneousElem' : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 = el2)
+decHeterogeneousElem' = decHeterogeneousElem
+
+main : IO ()
+main = printLn "OK"

tests/base/data_list003/expected

@@ -0,0 +1 @@
+"OK"

tests/base/data_list003/run

@@ -0,0 +1,3 @@
+. ../../testutils.sh
+
+run Elem.idr

tests/base/data_listone001/Elem.idr

@@ -0,0 +1,45 @@
+import Data.List
+import Data.List.Elem
+import Data.List1
+import Data.List1.Elem
+
+decHomogeneousElemList : (el1 : Data.List.Elem.Elem x xs) -> (el2 : Data.List.Elem.Elem x xs) -> Dec (el1 === el2)
+decHomogeneousElemList Here         Here         = Yes Refl
+decHomogeneousElemList (There _)    Here         = No uninhabited
+decHomogeneousElemList Here         (There _)    = No uninhabited
+decHomogeneousElemList (There el1') (There el2') = case decHomogeneousElemList el1' el2' of
+                                                    Yes Refl => Yes Refl
+                                                    No contra => No $ \Refl => contra Refl
+
+decHeterogeneousElemList : (el1 : Data.List.Elem.Elem x xs) -> (el2 : Data.List.Elem.Elem y xs) -> Dec (el1 ~=~ el2)
+decHeterogeneousElemList Here         Here         = Yes Refl
+decHeterogeneousElemList (There _)    Here         = No uninhabited
+decHeterogeneousElemList Here         (There _)    = No uninhabited
+decHeterogeneousElemList (There el1') (There el2') = case decHeterogeneousElemList el1' el2' of
+                                                      Yes Refl => Yes Refl
+                                                      No contra => No $ \Refl => contra Refl
+
+decHomogeneousElem : (el1 : Data.List1.Elem.Elem x xs) -> (el2 : Data.List1.Elem.Elem x xs) -> Dec (el1 === el2)
+decHomogeneousElem Here         Here         = Yes Refl
+decHomogeneousElem (There _)    Here         = No uninhabited
+decHomogeneousElem Here         (There _)    = No uninhabited
+decHomogeneousElem (There el1') (There el2') = case decHomogeneousElemList el1' el2' of
+                                                Yes Refl => Yes Refl
+                                                No contra => No $ \Refl => contra Refl
+
+decHomogeneousElem' : (el1 : Data.List1.Elem.Elem x xs) -> (el2 : Data.List1.Elem.Elem x xs) -> Dec (el1 = el2)
+decHomogeneousElem' = decHomogeneousElem
+
+decHeterogeneousElem : (el1 : Data.List1.Elem.Elem x xs) -> (el2 : Data.List1.Elem.Elem y xs) -> Dec (el1 ~=~ el2)
+decHeterogeneousElem Here         Here         = Yes Refl
+decHeterogeneousElem (There _)    Here         = No uninhabited
+decHeterogeneousElem Here         (There _)    = No uninhabited
+decHeterogeneousElem (There el1') (There el2') = case decHeterogeneousElemList el1' el2' of
+                                                  Yes Refl => Yes Refl
+                                                  No contra => No $ \Refl => contra Refl
+
+decHeterogeneousElem' : (el1 : Data.List1.Elem.Elem x xs) -> (el2 : Data.List1.Elem.Elem y xs) -> Dec (el1 = el2)
+decHeterogeneousElem' = decHeterogeneousElem
+
+main : IO ()
+main = printLn "OK"

tests/base/data_listone001/expected

@@ -0,0 +1 @@
+"OK"

tests/base/data_listone001/run

@@ -0,0 +1,3 @@
+. ../../testutils.sh
+
+run Elem.idr

tests/base/data_snoclist002/Elem.idr

@@ -0,0 +1,27 @@
+import Data.SnocList
+import Data.SnocList.Elem
+
+decHomogeneousElem : (el1 : Elem x xs) -> (el2 : Elem x xs) -> Dec (el1 === el2)
+decHomogeneousElem Here         Here         = Yes Refl
+decHomogeneousElem (There _)    Here         = No uninhabited
+decHomogeneousElem Here         (There _)    = No uninhabited
+decHomogeneousElem (There el1') (There el2') = case decHomogeneousElem el1' el2' of
+                                                Yes Refl => Yes Refl
+                                                No contra => No $ \Refl => contra Refl
+
+decHomogeneousElem' : (el1 : Elem x xs) -> (el2 : Elem x xs) -> Dec (el1 = el2)
+decHomogeneousElem' = decHomogeneousElem
+
+decHeterogeneousElem : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 ~=~ el2)
+decHeterogeneousElem Here         Here         = Yes Refl
+decHeterogeneousElem (There _)    Here         = No uninhabited
+decHeterogeneousElem Here         (There _)    = No uninhabited
+decHeterogeneousElem (There el1') (There el2') = case decHeterogeneousElem el1' el2' of
+                                                  Yes Refl => Yes Refl
+                                                  No contra => No $ \Refl => contra Refl
+
+decHeterogeneousElem' : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 = el2)
+decHeterogeneousElem' = decHeterogeneousElem
+
+main : IO ()
+main = printLn "OK"

tests/base/data_snoclist002/expected

@@ -0,0 +1 @@
+"OK"

tests/base/data_snoclist002/run

@@ -0,0 +1,3 @@
+. ../../testutils.sh
+
+run Elem.idr

tests/base/data_vect002/Elem.idr

@@ -0,0 +1,27 @@
+import Data.Vect
+import Data.Vect.Elem
+
+decHomogeneousElem : (el1 : Elem x xs) -> (el2 : Elem x xs) -> Dec (el1 === el2)
+decHomogeneousElem Here         Here         = Yes Refl
+decHomogeneousElem (There _)    Here         = No uninhabited
+decHomogeneousElem Here         (There _)    = No uninhabited
+decHomogeneousElem (There el1') (There el2') = case decHomogeneousElem el1' el2' of
+                                                Yes Refl => Yes Refl
+                                                No contra => No $ \Refl => contra Refl
+
+decHomogeneousElem' : (el1 : Elem x xs) -> (el2 : Elem x xs) -> Dec (el1 = el2)
+decHomogeneousElem' = decHomogeneousElem
+
+decHeterogeneousElem : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 ~=~ el2)
+decHeterogeneousElem Here         Here         = Yes Refl
+decHeterogeneousElem (There _)    Here         = No uninhabited
+decHeterogeneousElem Here         (There _)    = No uninhabited
+decHeterogeneousElem (There el1') (There el2') = case decHeterogeneousElem el1' el2' of
+                                                  Yes Refl => Yes Refl
+                                                  No contra => No $ \Refl => contra Refl
+
+decHeterogeneousElem' : (el1 : Elem x xs) -> (el2 : Elem y xs) -> Dec (el1 = el2)
+decHeterogeneousElem' = decHeterogeneousElem
+
+main : IO ()
+main = printLn "OK"

tests/base/data_vect002/expected

@@ -0,0 +1 @@
+"OK"

tests/base/data_vect002/run

@@ -0,0 +1,3 @@
+. ../../testutils.sh
+
+run Elem.idr