1 files changed, 6 insertions, 0 deletions
diff --git a/src/AST/Weaken.hs b/src/AST/Weaken.hs
index d882e28..3a97fd1 100644
--- a/src/AST/Weaken.hs
+++ b/src/AST/Weaken.hs
@@ -19,6 +19,7 @@ module AST.Weaken (module AST.Weaken, Append) where
 
 import Data.Bifunctor (first)
 import Data.Functor.Const
+import Data.GADT.Compare
 import Data.Kind (Type)
 
 import Data
@@ -31,6 +32,11 @@ data Idx env t where
   IS :: Idx env t -> Idx (a : env) t
 deriving instance Show (Idx env t)
 
+instance GEq (Idx env) where
+  geq IZ IZ = Just Refl
+  geq (IS i) (IS j) | Just Refl <- geq i j = Just Refl
+  geq _ _ = Nothing
+
 splitIdx :: forall env2 env1 t f. SList f env1 -> Idx (Append env1 env2) t -> Either (Idx env1 t) (Idx env2 t)
 splitIdx SNil i = Right i
 splitIdx (SCons _ _) IZ = Left IZ