Hide n argument in Tactic.RingSolver.NonReflective._⊜_ (#1149)

Author: dylanede

CHANGELOG.md

@@ -21,6 +21,8 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
+* The `n` argument to `_⊜_` in `Tactic.RingSolver.NonReflective` has been made implict rather than explicit.
+
 * `Data.Empty.Polymorphic` and `Data.Unit.Polymorphic` were rewritten
   to explicitly use `Lift` rather that defining new types. This means
   that these are now compatible with `⊥` and `⊤` from the rest of the

src/Tactic/RingSolver.agda

@@ -154,7 +154,7 @@ private
       callSolver : Vec String numVars → Term → Term → Args Type
       callSolver nms lhs rhs =
           2 ⋯⟅∷⟆ ring ⟨∷⟩ toTerm numVars ⟨∷⟩
-          vlams nms (quote _⊜_  $ʳ (toTerm numVars ⟨∷⟩ E lhs ⟨∷⟩ E rhs ⟨∷⟩ [])) ⟨∷⟩
+          vlams nms (quote _⊜_  $ʳ (toTerm numVars ⟅∷⟆ E lhs ⟨∷⟩ E rhs ⟨∷⟩ [])) ⟨∷⟩
           hlams nms (quote refl $ʳ (1 ⋯⟅∷⟆ [])) ⟨∷⟩
           []
         where

src/Tactic/RingSolver/NonReflective.agda

@@ -93,9 +93,9 @@ solve : ∀ (n : ℕ) →
 solve = Ops.solve
 {-# INLINE solve #-}
 
-_⊜_ : ∀ (n : ℕ) →
+_⊜_ : ∀ {n : ℕ} →
       Expr Carrier n →
       Expr Carrier n →
       Expr Carrier n × Expr Carrier n
-_⊜_ _ = _,_
+_⊜_ = _,_
 {-# INLINE _⊜_ #-}