make tighten into an interface

src/Quox/OPE.idr

@@ -52,6 +52,24 @@ dropInnerN 0     = Id
 dropInnerN (S m) = Drop $ dropInnerN m
 
 
+public export
+interface Tighten t where
+  tighten : Alternative f => OPE m n -> t n -> f (t m)
+
+parameters {auto _ : Tighten t} {auto _ : Alternative f}
+  export
+  tightenInner : {n : Nat} -> m `LTE` n -> t n -> f (t m)
+  tightenInner = tighten . dropInner
+
+  export
+  tightenN : (m : Nat) -> t (m + n) -> f (t n)
+  tightenN m = tighten $ dropInnerN m
+
+  export
+  tighten1 : t (S n) -> f (t n)
+  tighten1 = tightenN 1
+
+
 
 -- [todo] can this be done with fancy nats too?
 -- with bitmasks sure but that might not be worth the effort

src/Quox/Syntax/Var.idr

@@ -264,23 +264,10 @@ decEqFromBool i j =
 
 public export %inline DecEq (Var n) where decEq = varDecEq
 
-parameters {auto _ : Alternative f}
 export
-  tighten : OPE m n -> Var n -> f (Var m)
+Tighten Var where
   tighten Id       i      = pure i
   tighten (Drop q) VZ     = empty
   tighten (Drop q) (VS i) = tighten q i
   tighten (Keep q) VZ     = pure VZ
   tighten (Keep q) (VS i) = VS <$> tighten q i
-
-  export
-  tightenInner : {n : Nat} -> m `LTE` n -> Var n -> f (Var m)
-  tightenInner = tighten . dropInner
-
-  export
-  tightenN : (m : Nat) -> Var (m + n) -> f (Var n)
-  tightenN m = tighten $ dropInnerN m
-
-  export
-  tighten1 : Var (S n) -> f (Var n)
-  tighten1 = tightenN 1