From c2dd824c585a423b00458ac30b5c63cb341f2230 Mon Sep 17 00:00:00 2001
From: 0xd34df00d <0xd34df00d@gmail.com>
Date: Sun, 2 Oct 2022 13:54:07 -0500
Subject: [PATCH] [ base ] Implement Uninhabited for impossible Pointwise
 equalities

---
 CHANGELOG.md           |  1 +
 libs/base/Data/Fin.idr | 10 ++++++++++
 2 files changed, 11 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 976e1520d..9098d1763 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -135,6 +135,7 @@
   which takes a witness of `finToNat k = finToNat l` and proves `k ~~~ l`.
 * Drop first argument (path to the `node` executable) from `System.getArgs` on
   the Node.js backend to make it consistent with other backends.
+* Adds `Uninhabited` instances for `FZ ~~~ FS k` and `FS k ~~~ FZ`.
 
 #### Test
 
diff --git a/libs/base/Data/Fin.idr b/libs/base/Data/Fin.idr
index c0b659362..3e74869e3 100644
--- a/libs/base/Data/Fin.idr
+++ b/libs/base/Data/Fin.idr
@@ -304,6 +304,16 @@ namespace Equality
   (~~~) : Fin m -> Fin n -> Type
   (~~~) = Pointwise
 
+  export
+  Uninhabited (FS k ~~~ FZ) where
+    uninhabited FZ impossible
+    uninhabited (FS _) impossible
+
+  export
+  Uninhabited (FZ ~~~ FS k) where
+    uninhabited FZ impossible
+    uninhabited (FS _) impossible
+
   ||| Pointwise equality is reflexive
   export
   reflexive : {k : Fin m} -> k ~~~ k