From dc076b636ddcea43bbf3efe3f407b60dec40d4ea Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Tue, 19 Sep 2023 18:05:43 +0200
Subject: [PATCH] fix warnings

---
 lib/Quox/FreeVars.idr    | 42 ++++++++++++++++++++--------------------
 tests/Tests/FreeVars.idr | 12 ++++++++----
 2 files changed, 29 insertions(+), 25 deletions(-)

diff --git a/lib/Quox/FreeVars.idr b/lib/Quox/FreeVars.idr
index e4031b9..130c37c 100644
--- a/lib/Quox/FreeVars.idr
+++ b/lib/Quox/FreeVars.idr
@@ -84,19 +84,19 @@ toSet (FV vs) =
 
 
 public export
-interface HasFreeVars (0 term : Nat -> Type) where
+interface HasFreeVars (0 tm : Nat -> Type) where
   constructor HFV
-  fv : {n : Nat} -> term n -> FreeVars n
+  fv : {n : Nat} -> tm n -> FreeVars n
 
 public export
-interface HasFreeDVars (0 term : TermLike) where
+interface HasFreeDVars (0 tm : TermLike) where
   constructor HFDV
-  fdv : {d, n : Nat} -> term d n -> FreeVars d
+  fdv : {d, n : Nat} -> tm d n -> FreeVars d
 
 export
-Fdv : (0 term : TermLike) -> {n : Nat} ->
-      HasFreeDVars term => HasFreeVars (\d => term d n)
-Fdv term @{HFDV fdv} = HFV fdv
+Fdv : (0 tm : TermLike) -> {n : Nat} ->
+      HasFreeDVars tm => HasFreeVars (\d => tm d n)
+Fdv tm @{HFDV fdv} = HFV fdv
 
 
 export
@@ -119,26 +119,26 @@ HasFreeVars Dim where
 
 
 export
-{s : Nat} -> HasFreeVars term => HasFreeVars (Scoped s term) where
+{s : Nat} -> HasFreeVars tm => HasFreeVars (Scoped s tm) where
   fv (S _ (Y body)) = FV $ drop s (fv body).vars
   fv (S _ (N body)) = fv body
 
 export
 implementation [DScope]
-  {s : Nat} -> HasFreeDVars term =>
-  HasFreeDVars (\d, n => Scoped s (\d' => term d' n) d)
+  {s : Nat} -> HasFreeDVars tm =>
+  HasFreeDVars (\d, n => Scoped s (\d' => tm d' n) d)
 where
   fdv (S _ (Y body)) = FV $ drop s (fdv body).vars
   fdv (S _ (N body)) = fdv body
 
 export
-fvD : {0 term : TermLike} -> {n : Nat} -> (forall d. HasFreeVars (term d)) =>
-      Scoped s (\d => term d n) d -> FreeVars n
+fvD : {0 tm : TermLike} -> {n : Nat} -> (forall d. HasFreeVars (tm d)) =>
+      Scoped s (\d => tm d n) d -> FreeVars n
 fvD (S _ (Y body)) = fv body
 fvD (S _ (N body)) = fv body
 
 export
-fdvT : HasFreeDVars term => {s, d, n : Nat} -> Scoped s (term d) n -> FreeVars d
+fdvT : HasFreeDVars tm => {s, d, n : Nat} -> Scoped s (tm d) n -> FreeVars d
 fdvT (S _ (Y body)) = fdv body
 fdvT (S _ (N body)) = fdv body
 
@@ -149,8 +149,8 @@ guardM b x = if b then x else neutral
 
 export
 implementation
-  (HasFreeVars term, HasFreeVars env) =>
-  HasFreeVars (WithSubst term env)
+  (HasFreeVars tm, HasFreeVars env) =>
+  HasFreeVars (WithSubst tm env)
 where
   fv (Sub term subst) =
     let Val from = getFrom subst in
@@ -158,8 +158,8 @@ where
 
 export
 implementation [WithSubst]
-  ((forall d. HasFreeVars (term d)), HasFreeDVars term, HasFreeDVars env) =>
-  HasFreeDVars (\d => WithSubst (term d) (env d))
+  ((forall d. HasFreeVars (tm d)), HasFreeDVars tm, HasFreeDVars env) =>
+  HasFreeDVars (\d => WithSubst (tm d) (env d))
 where
   fdv (Sub term subst) =
     let Val from = getFrom subst in
@@ -227,8 +227,8 @@ expandDSubst (t ::: th) = expandDSubst th :< t
 
 
 private
-fdvSubst' : {d1, d2, n : Nat} -> HasFreeDVars term =>
-            term d1 n -> DSubst d1 d2 -> FreeVars d2
+fdvSubst' : {d1, d2, n : Nat} -> HasFreeDVars tm =>
+            tm d1 n -> DSubst d1 d2 -> FreeVars d2
 fdvSubst' t th =
   fold $ zipWith maybeOnly (fdv t).vars (expandDSubst th)
 where
@@ -237,8 +237,8 @@ where
   maybeOnly _    _       = none
 
 private
-fdvSubst : {d, n : Nat} -> HasFreeDVars term =>
-           WithSubst (\d => term d n) Dim d -> FreeVars d
+fdvSubst : {d, n : Nat} -> HasFreeDVars tm =>
+           WithSubst (\d => tm d n) Dim d -> FreeVars d
 fdvSubst (Sub t th) = let Val from = getFrom th in fdvSubst' t th
 
 
diff --git a/tests/Tests/FreeVars.idr b/tests/Tests/FreeVars.idr
index 0633c42..a51ab9d 100644
--- a/tests/Tests/FreeVars.idr
+++ b/tests/Tests/FreeVars.idr
@@ -38,17 +38,21 @@ testFreeVars lbl tm dims terms =
     Right ()
 
 private
-prettyWith : (a -> Eff Pretty (Doc (Opts 80))) -> a -> String
+Doc80 : Type
+Doc80 = Doc $ Opts 80
+
+private
+prettyWith : (a -> Eff Pretty Doc80) -> a -> String
 prettyWith f = trim . render _ . runPretty . f
 
 parameters {d, n : Nat} (ds : BContext d) (ts : BContext n)
   private
-  withContext : {opts : _} -> Doc opts -> Eff Pretty (Doc opts)
-  withContext {opts} doc =
+  withContext : Doc80 -> Eff Pretty Doc80
+  withContext doc =
     if null ds && null ts then pure $ hsep ["⊢", doc]
     else pure $ sep [hsep [!(ctx1 ds), "|", !(ctx1 ts), "⊢"], doc]
   where
-    ctx1 : forall k. BContext k -> Eff Pretty (Doc opts)
+    ctx1 : forall k. BContext k -> Eff Pretty Doc80
     ctx1 [<] = pure "·"
     ctx1 ctx = fillSeparateTight !commaD . toList' <$>
                traverse' (pure . prettyBind') ctx