diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9b647d5114..602ddc29fa 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -358,6 +358,38 @@ Non-backwards compatible changes
   3. Finally, if the above approaches are not viable then you may be forced to explicitly
 	 use `cong` combined with a lemma that proves the old reduction behaviour.
 
+### Change to the definition of `LeftCancellative` and `RightCancellative`
+
+* The definitions of the types for cancellativity in `Algebra.Definitions` previously
+  made some of their arguments implicit. This was under the assumption that the operators were
+  defined by pattern matching on the left argument so that Agda could always infer the 
+  argument on the RHS.
+  
+* Although many of the operators defined in the library follow this convention, this is not
+  always true and cannot be assumed in user's code.
+  
+* Therefore the definitions have been changed as follows to make all their arguments explicit:
+  - `LeftCancellative _•_` 
+	- From: `∀ x {y z} → (x • y) ≈ (x • z) → y ≈ z` 
+	- To: `∀ x y z → (x • y) ≈ (x • z) → y ≈ z`
+
+  - `RightCancellative _•_`
+    - From: `∀ {x} y z → (y • x) ≈ (z • x) → y ≈ z`
+	- To: `∀ x y z → (y • x) ≈ (z • x) → y ≈ z`
+
+  - `AlmostLeftCancellative e _•_`
+    - From: `∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z`
+	- To: `∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z`
+
+  - `AlmostRightCancellative e _•_`
+	- From: `∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z`
+	- To: `∀ x y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z`
+
+* Correspondingly some proofs of the above types will need additional arguments passed explicitly.
+  Instances can easily be fixed by adding additional underscores, e.g. 
+  - `∙-cancelˡ x` to `∙-cancelˡ x _ _`
+  - `∙-cancelʳ y z` to `∙-cancelʳ _ y z`
+  
 ### Change in the definition of `Prime`
 
 * The definition of `Prime` in `Data.Nat.Primality` was:
diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda
index 8e97b77305..11723af49d 100644
--- a/src/Algebra/Consequences/Setoid.agda
+++ b/src/Algebra/Consequences/Setoid.agda
@@ -34,14 +34,14 @@ open import Algebra.Consequences.Base public
 module _ {_•_ : Op₂ A} (comm : Commutative _•_) where
 
   comm+cancelˡ⇒cancelʳ : LeftCancellative _•_ → RightCancellative _•_
-  comm+cancelˡ⇒cancelʳ cancelˡ {x} y z eq = cancelˡ x $ begin
+  comm+cancelˡ⇒cancelʳ cancelˡ x y z eq = cancelˡ x y z $ begin
     x • y ≈⟨ comm x y ⟩
     y • x ≈⟨ eq ⟩
     z • x ≈⟨ comm z x ⟩
     x • z ∎
 
   comm+cancelʳ⇒cancelˡ : RightCancellative _•_ → LeftCancellative _•_
-  comm+cancelʳ⇒cancelˡ cancelʳ x {y} {z} eq = cancelʳ y z $ begin
+  comm+cancelʳ⇒cancelˡ cancelʳ x y z eq = cancelʳ x y z $ begin
     y • x ≈⟨ comm y x ⟩
     x • y ≈⟨ eq ⟩
     x • z ≈⟨ comm x z ⟩
@@ -90,8 +90,8 @@ module _ {_•_ : Op₂ A} (comm : Commutative _•_) {e : A} where
 
   comm+almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _•_ →
                                      AlmostRightCancellative e _•_
-  comm+almostCancelˡ⇒almostCancelʳ cancelˡ-nonZero {x} y z x≉e yx≈zx =
-    cancelˡ-nonZero y z x≉e $ begin
+  comm+almostCancelˡ⇒almostCancelʳ cancelˡ-nonZero x y z x≉e yx≈zx =
+    cancelˡ-nonZero x y z x≉e $ begin
       x • y ≈⟨ comm x y ⟩
       y • x ≈⟨ yx≈zx ⟩
       z • x ≈⟨ comm z x ⟩
@@ -99,8 +99,8 @@ module _ {_•_ : Op₂ A} (comm : Commutative _•_) {e : A} where
 
   comm+almostCancelʳ⇒almostCancelˡ : AlmostRightCancellative e _•_ →
                                      AlmostLeftCancellative e _•_
-  comm+almostCancelʳ⇒almostCancelˡ cancelʳ-nonZero {x} y z x≉e xy≈xz =
-    cancelʳ-nonZero y z x≉e $ begin
+  comm+almostCancelʳ⇒almostCancelˡ cancelʳ-nonZero x y z x≉e xy≈xz =
+    cancelʳ-nonZero x y z x≉e $ begin
       y • x ≈⟨ comm y x ⟩
       x • y ≈⟨ xy≈xz ⟩
       x • z ≈⟨ comm x z ⟩
diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index a87bbb7bf6..9947f2f84b 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -7,6 +7,12 @@
 -- The contents of this module should be accessed via `Algebra`, unless
 -- you want to parameterise it via the equality relation.
 
+-- Note that very few of the element arguments are made implicit here,
+-- as we do not assume that the Agda can infer either the right or left
+-- argument of the binary operators. This is despite the fact that the
+-- library defines most of its concrete operators (e.g. in
+-- `Data.Nat.Base`) as being left-biased.
+
 {-# OPTIONS --without-K --safe #-}
 
 open import Relation.Binary.Core
@@ -124,19 +130,19 @@ Involutive : Op₁ A → Set _
 Involutive f = ∀ x → f (f x) ≈ x
 
 LeftCancellative : Op₂ A → Set _
-LeftCancellative _•_ = ∀ x {y z} → (x • y) ≈ (x • z) → y ≈ z
+LeftCancellative _•_ = ∀ x y z → (x • y) ≈ (x • z) → y ≈ z
 
 RightCancellative : Op₂ A → Set _
-RightCancellative _•_ = ∀ {x} y z → (y • x) ≈ (z • x) → y ≈ z
+RightCancellative _•_ = ∀ x y z → (y • x) ≈ (z • x) → y ≈ z
 
 Cancellative : Op₂ A → Set _
 Cancellative _•_ = (LeftCancellative _•_) × (RightCancellative _•_)
 
 AlmostLeftCancellative : A → Op₂ A → Set _
-AlmostLeftCancellative e _•_ = ∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z
+AlmostLeftCancellative e _•_ = ∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z
 
 AlmostRightCancellative : A → Op₂ A → Set _
-AlmostRightCancellative e _•_ = ∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z
+AlmostRightCancellative e _•_ = ∀ x y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z
 
 AlmostCancellative : A → Op₂ A → Set _
 AlmostCancellative e _•_ = AlmostLeftCancellative e _•_ × AlmostRightCancellative e _•_
diff --git a/src/Algebra/Morphism/MagmaMonomorphism.agda b/src/Algebra/Morphism/MagmaMonomorphism.agda
index 2cad60e77e..90d5d72957 100644
--- a/src/Algebra/Morphism/MagmaMonomorphism.agda
+++ b/src/Algebra/Morphism/MagmaMonomorphism.agda
@@ -79,14 +79,14 @@ module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where
     ⟦ y ⟧          ∎))
 
   cancelˡ : LeftCancellative _≈₂_ _◦_ → LeftCancellative _≈₁_ _∙_
-  cancelˡ cancelˡ x {y} {z} x∙y≈x∙z = injective (cancelˡ ⟦ x ⟧ (begin
+  cancelˡ cancelˡ x y z x∙y≈x∙z = injective (cancelˡ ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ (begin
     ⟦ x ⟧ ◦ ⟦ y ⟧  ≈˘⟨ homo x y ⟩
     ⟦ x ∙ y ⟧      ≈⟨  ⟦⟧-cong x∙y≈x∙z ⟩
     ⟦ x ∙ z ⟧      ≈⟨  homo x z ⟩
     ⟦ x ⟧ ◦ ⟦ z ⟧  ∎))
 
   cancelʳ : RightCancellative _≈₂_ _◦_ → RightCancellative _≈₁_ _∙_
-  cancelʳ cancelʳ {x} y z y∙x≈z∙x = injective (cancelʳ ⟦ y ⟧ ⟦ z ⟧ (begin
+  cancelʳ cancelʳ x y z y∙x≈z∙x = injective (cancelʳ ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ (begin
     ⟦ y ⟧ ◦ ⟦ x ⟧  ≈˘⟨ homo y x ⟩
     ⟦ y ∙ x ⟧      ≈⟨  ⟦⟧-cong y∙x≈z∙x ⟩
     ⟦ z ∙ x ⟧      ≈⟨  homo z x ⟩
diff --git a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
index 69b2e122eb..081050800a 100644
--- a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
+++ b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
@@ -31,7 +31,7 @@ xy≈0⇒x≈0∨y≈0 _≟_ {x} {y} xy≈0 with x ≟ 0# | y ≟ 0#
 ... | no  x≉0 | no  y≉0 = contradiction y≈0 y≉0
   where
   xy≈x*0 = trans xy≈0 (sym (zeroʳ x))
-  y≈0    = *-cancelˡ-nonZero y 0# x≉0 xy≈x*0
+  y≈0    = *-cancelˡ-nonZero _ y 0# x≉0 xy≈x*0
 
 x≉0∧y≉0⇒xy≉0 : Decidable _≈_ → ∀ {x y} → x ≉ 0# → y ≉ 0# → x * y ≉ 0#
 x≉0∧y≉0⇒xy≉0 _≟_ x≉0 y≉0 xy≈0 with xy≈0⇒x≈0∨y≈0 _≟_ xy≈0
diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda
index 8ce8378b46..7b81768869 100644
--- a/src/Algebra/Properties/Group.agda
+++ b/src/Algebra/Properties/Group.agda
@@ -39,14 +39,14 @@ private
     x ⁻¹ ∙ (x ∙ y) ∎
 
 ∙-cancelˡ : LeftCancellative _∙_
-∙-cancelˡ x {y} {z} eq = begin
+∙-cancelˡ x y z eq = begin
               y  ≈⟨ right-helper x y ⟩
   x ⁻¹ ∙ (x ∙ y) ≈⟨ ∙-congˡ eq ⟩
   x ⁻¹ ∙ (x ∙ z) ≈˘⟨ right-helper x z ⟩
               z  ∎
 
 ∙-cancelʳ : RightCancellative _∙_
-∙-cancelʳ {x} y z eq = begin
+∙-cancelʳ x y z eq = begin
   y            ≈⟨ left-helper y x ⟩
   y ∙ x ∙ x ⁻¹ ≈⟨ ∙-congʳ eq ⟩
   z ∙ x ∙ x ⁻¹ ≈˘⟨ left-helper z x ⟩
@@ -63,14 +63,14 @@ private
   x                    ∎
 
 ⁻¹-injective : ∀ {x y} → x ⁻¹ ≈ y ⁻¹ → x ≈ y
-⁻¹-injective {x} {y} eq = ∙-cancelʳ x y ( begin
+⁻¹-injective {x} {y} eq = ∙-cancelʳ _ _ _ ( begin
   x ∙ x ⁻¹ ≈⟨ inverseʳ x ⟩
   ε        ≈˘⟨ inverseʳ y ⟩
   y ∙ y ⁻¹ ≈˘⟨ ∙-congˡ eq ⟩
   y ∙ x ⁻¹ ∎ )
 
 ⁻¹-anti-homo-∙ : ∀ x y → (x ∙ y) ⁻¹ ≈ y ⁻¹ ∙ x ⁻¹
-⁻¹-anti-homo-∙ x y = ∙-cancelˡ _ ( begin
+⁻¹-anti-homo-∙ x y = ∙-cancelˡ _ _ _ ( begin
   x ∙ y ∙ (x ∙ y) ⁻¹    ≈⟨ inverseʳ _ ⟩
   ε                     ≈˘⟨ inverseʳ _ ⟩
   x ∙ x ⁻¹              ≈⟨ ∙-congʳ (left-helper x y) ⟩
diff --git a/src/Algebra/Properties/Quasigroup.agda b/src/Algebra/Properties/Quasigroup.agda
index 9fb8cecf4c..ae722855ec 100644
--- a/src/Algebra/Properties/Quasigroup.agda
+++ b/src/Algebra/Properties/Quasigroup.agda
@@ -16,14 +16,14 @@ open import Relation.Binary.Reasoning.Setoid setoid
 open import Data.Product
 
 cancelˡ : LeftCancellative _∙_
-cancelˡ x {y} {z} eq = begin
+cancelˡ x y z eq = begin
   y             ≈⟨ sym( leftDividesʳ x y) ⟩
   x \\ (x ∙ y)  ≈⟨ \\-congˡ eq ⟩
   x \\ (x ∙ z)  ≈⟨ leftDividesʳ x z ⟩
   z             ∎
 
 cancelʳ : RightCancellative _∙_
-cancelʳ {x} y z eq = begin
+cancelʳ x y z eq = begin
   y             ≈⟨ sym( rightDividesʳ x y) ⟩
   (y ∙ x) // x  ≈⟨ //-congʳ eq ⟩
   (z ∙ x) // x  ≈⟨ rightDividesʳ x z ⟩
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 4ecd2bc722..566a0163ad 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -654,7 +654,7 @@ combine-injectiveˡ i j k l cᵢⱼ≡cₖₗ with <-cmp i k
 combine-injectiveʳ : ∀ (i : Fin m) (j : Fin n) (k : Fin m) (l : Fin n) →
                      combine i j ≡ combine k l → j ≡ l
 combine-injectiveʳ {m} {n} i j k l cᵢⱼ≡cₖₗ with combine-injectiveˡ i j k l cᵢⱼ≡cₖₗ
-... | refl = toℕ-injective (ℕₚ.+-cancelˡ-≡ (n ℕ.* toℕ i) (begin
+... | refl = toℕ-injective (ℕₚ.+-cancelˡ-≡ (n ℕ.* toℕ i) _ _ (begin
   n ℕ.* toℕ i ℕ.+ toℕ j ≡˘⟨ toℕ-combine i j ⟩
   toℕ (combine i j)     ≡⟨ cong toℕ cᵢⱼ≡cₖₗ ⟩
   toℕ (combine i l)     ≡⟨ toℕ-combine i l ⟩
diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index e0f131b98c..d8a9d3b30d 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -1599,8 +1599,8 @@ abs-*-commute i j = abs-◃ _ _
 *-cancelʳ-≡ : ∀ i j k .{{_ : NonZero k}} → i * k ≡ j * k → i ≡ j
 *-cancelʳ-≡ i j k eq with sign-cong′ eq
 ... | inj₁ s[ik]≡s[jk] = ◃-cong
-  (𝕊ₚ.*-cancelʳ-≡ {sign k} (sign i) (sign j) s[ik]≡s[jk])
-  (ℕ.*-cancelʳ-≡ ∣ i ∣ ∣ j ∣ (abs-cong eq))
+  (𝕊ₚ.*-cancelʳ-≡ (sign k) (sign i) (sign j) s[ik]≡s[jk])
+  (ℕ.*-cancelʳ-≡ ∣ i ∣ ∣ j ∣ _ (abs-cong eq))
 ... | inj₂ (∣ik∣≡0 , ∣jk∣≡0) = trans
   (∣i∣≡0⇒i≡0 (ℕ.m*n≡0⇒m≡0 _ _ ∣ik∣≡0))
   (sym (∣i∣≡0⇒i≡0 (ℕ.m*n≡0⇒m≡0 _ _ ∣jk∣≡0)))
@@ -1785,10 +1785,10 @@ neg-distribʳ-* i j = begin
 *-monoʳ-<-pos i {j} {k} rewrite *-comm j i | *-comm k i = *-monoˡ-<-pos i
 
 *-cancelˡ-<-nonNeg : ∀ k .{{_ : NonNegative k}} → k * i < k * j → i < j
-*-cancelˡ-<-nonNeg {+ i}       {+ j}       (+ n) leq = +<+ (ℕ.*-cancelˡ-< n (+◃-cancel-< leq))
+*-cancelˡ-<-nonNeg {+ i}       {+ j}       (+ n) leq = +<+ (ℕ.*-cancelˡ-< n _ _ (+◃-cancel-< leq))
 *-cancelˡ-<-nonNeg {+ i}       { -[1+ j ]} (+ n) leq = contradiction leq +◃≮-◃
 *-cancelˡ-<-nonNeg { -[1+ i ]} {+ j}       (+ n)leq = -<+
-*-cancelˡ-<-nonNeg { -[1+ i ]} { -[1+ j ]} (+ n) leq = -<- (ℕ.≤-pred (ℕ.*-cancelˡ-< n (neg◃-cancel-< leq)))
+*-cancelˡ-<-nonNeg { -[1+ i ]} { -[1+ j ]} (+ n) leq = -<- (ℕ.≤-pred (ℕ.*-cancelˡ-< n _ _ (neg◃-cancel-< leq)))
 
 *-cancelʳ-<-nonNeg : ∀ k .{{_ : NonNegative k}} → i * k < j * k → i < j
 *-cancelʳ-<-nonNeg {i} {j} k rewrite *-comm i k | *-comm j k = *-cancelˡ-<-nonNeg k
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 898f29f85f..ced3a6f3a1 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -183,18 +183,18 @@ module _ {A : Set a} where
   ++-identityˡ-unique {xs = x ∷ xs} (y ∷ []   ) eq | ()
   ++-identityˡ-unique {xs = x ∷ xs} (y ∷ _ ∷ _) eq | ()
 
-  ++-cancelˡ : ∀ xs {ys zs : List A} → xs ++ ys ≡ xs ++ zs → ys ≡ zs
-  ++-cancelˡ []       ys≡zs             = ys≡zs
-  ++-cancelˡ (x ∷ xs) x∷xs++ys≡x∷xs++zs = ++-cancelˡ xs (∷-injectiveʳ x∷xs++ys≡x∷xs++zs)
+  ++-cancelˡ : LeftCancellative _++_
+  ++-cancelˡ []       _ _ ys≡zs             = ys≡zs
+  ++-cancelˡ (x ∷ xs) _ _ x∷xs++ys≡x∷xs++zs = ++-cancelˡ xs _ _ (∷-injectiveʳ x∷xs++ys≡x∷xs++zs)
 
-  ++-cancelʳ : ∀ {xs : List A} ys zs → ys ++ xs ≡ zs ++ xs → ys ≡ zs
-  ++-cancelʳ {_}  []       []       _             = refl
-  ++-cancelʳ {xs} []       (z ∷ zs) eq =
+  ++-cancelʳ : RightCancellative _++_
+  ++-cancelʳ _  []       []       _             = refl
+  ++-cancelʳ xs []       (z ∷ zs) eq =
     contradiction (trans (cong length eq) (length-++ (z ∷ zs))) (m≢1+n+m (length xs))
-  ++-cancelʳ {xs} (y ∷ ys) []       eq =
+  ++-cancelʳ xs (y ∷ ys) []       eq =
     contradiction (trans (sym (length-++ (y ∷ ys))) (cong length eq)) (m≢1+n+m (length xs) ∘ sym)
-  ++-cancelʳ {_}  (y ∷ ys) (z ∷ zs) eq =
-    cong₂ _∷_ (∷-injectiveˡ eq) (++-cancelʳ ys zs (∷-injectiveʳ eq))
+  ++-cancelʳ _  (y ∷ ys) (z ∷ zs) eq =
+    cong₂ _∷_ (∷-injectiveˡ eq) (++-cancelʳ _ ys zs (∷-injectiveʳ eq))
 
   ++-cancel : Cancellative _++_
   ++-cancel = ++-cancelˡ , ++-cancelʳ
diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda
index cbf46664a1..06a6110e82 100644
--- a/src/Data/Nat/Binary/Properties.agda
+++ b/src/Data/Nat/Binary/Properties.agda
@@ -179,7 +179,7 @@ toℕ-injective : Injective _≡_ _≡_ toℕ
 toℕ-injective {zero}     {zero}     _               =  refl
 toℕ-injective {2[1+ x ]} {2[1+ y ]} 2[1+xN]≡2[1+yN] =  cong 2[1+_] x≡y
   where
-  1+xN≡1+yN = ℕₚ.*-cancelˡ-≡ {ℕ.suc _} {ℕ.suc _} 2 2[1+xN]≡2[1+yN]
+  1+xN≡1+yN = ℕₚ.*-cancelˡ-≡ (ℕ.suc _) (ℕ.suc _) 2 2[1+xN]≡2[1+yN]
   xN≡yN     = cong ℕ.pred 1+xN≡1+yN
   x≡y       = toℕ-injective xN≡yN
 
@@ -192,7 +192,7 @@ toℕ-injective {1+[2 x ]} {2[1+ y ]} 1+2xN≡2[1+yN] =
 toℕ-injective {1+[2 x ]} {1+[2 y ]} 1+2xN≡1+2yN =  cong 1+[2_] x≡y
   where
   2xN≡2yN = cong ℕ.pred 1+2xN≡1+2yN
-  xN≡yN   = ℕₚ.*-cancelˡ-≡ 2 2xN≡2yN
+  xN≡yN   = ℕₚ.*-cancelˡ-≡ _ _ 2 2xN≡2yN
   x≡y     = toℕ-injective xN≡yN
 
 toℕ-surjective : Surjective _≡_ toℕ
@@ -302,17 +302,17 @@ toℕ-cancel-< : ∀ {x y} → toℕ x ℕ.< toℕ y → x < y
 toℕ-cancel-< {zero}     {2[1+ y ]} x<y = 0<even
 toℕ-cancel-< {zero}     {1+[2 y ]} x<y = 0<odd
 toℕ-cancel-< {2[1+ x ]} {2[1+ y ]} x<y =
-  even<even (toℕ-cancel-< (ℕ.≤-pred (ℕₚ.*-cancelˡ-< 2 x<y)))
+  even<even (toℕ-cancel-< (ℕ.≤-pred (ℕₚ.*-cancelˡ-< 2 _ _ x<y)))
 toℕ-cancel-< {2[1+ x ]} {1+[2 y ]} x<y
   rewrite ℕₚ.*-distribˡ-+ 2 1 (toℕ x) =
-  even<odd (toℕ-cancel-< (ℕₚ.*-cancelˡ-< 2 (ℕₚ.≤-trans (s≤s (ℕₚ.n≤1+n _)) (ℕₚ.≤-pred x<y))))
+  even<odd (toℕ-cancel-< (ℕₚ.*-cancelˡ-< 2 _ _ (ℕₚ.≤-trans (s≤s (ℕₚ.n≤1+n _)) (ℕₚ.≤-pred x<y))))
 toℕ-cancel-< {1+[2 x ]} {2[1+ y ]} x<y with toℕ x ℕₚ.≟ toℕ y
 ... | yes x≡y = odd<even (inj₂ (toℕ-injective x≡y))
 ... | no  x≢y
   rewrite ℕₚ.+-suc (toℕ y) (toℕ y ℕ.+ 0) =
-  odd<even (inj₁ (toℕ-cancel-< (ℕₚ.≤∧≢⇒< (ℕₚ.*-cancelˡ-≤ 2 (ℕₚ.+-cancelˡ-≤ 2 x<y)) x≢y)))
+  odd<even (inj₁ (toℕ-cancel-< (ℕₚ.≤∧≢⇒< (ℕₚ.*-cancelˡ-≤ 2 (ℕₚ.+-cancelˡ-≤ 2 _ _ x<y)) x≢y)))
 toℕ-cancel-< {1+[2 x ]} {1+[2 y ]} x<y =
-  odd<odd (toℕ-cancel-< (ℕₚ.*-cancelˡ-< 2 (ℕ.≤-pred x<y)))
+  odd<odd (toℕ-cancel-< (ℕₚ.*-cancelˡ-< 2 _ _ (ℕ.≤-pred x<y)))
 
 fromℕ-cancel-< : ∀ {x y} → fromℕ x < fromℕ y → x ℕ.< y
 fromℕ-cancel-< = subst₂ ℕ._<_ (toℕ-fromℕ _) (toℕ-fromℕ _) ∘ toℕ-mono-<
diff --git a/src/Data/Nat/Binary/Subtraction.agda b/src/Data/Nat/Binary/Subtraction.agda
index c68c9c6424..d5c30c4825 100644
--- a/src/Data/Nat/Binary/Subtraction.agda
+++ b/src/Data/Nat/Binary/Subtraction.agda
@@ -146,7 +146,7 @@ x<y⇒y∸x>0 {x} {y} = toℕ-cancel-< ∘ subst (ℕ._> 0) (sym (toℕ-homo-∸
   where open ≡-Reasoning
 
 x+y∸y≡x : ∀ x y → (x + y) ∸ y ≡ x
-x+y∸y≡x x y = +-cancelʳ-≡ _ x ([x∸y]+y≡x (x≤y+x y x))
+x+y∸y≡x x y = +-cancelʳ-≡ _ _ x ([x∸y]+y≡x (x≤y+x y x))
 
 [x+y]∸x≡y : ∀ x y → (x + y) ∸ x ≡ y
 [x+y]∸x≡y x y = trans (cong (_∸ x) (+-comm x y)) (x+y∸y≡x y x)
diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index 785fc5889e..622b2f8b92 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -222,7 +222,7 @@ m/n≤m m n = *-cancelʳ-≤ (m / n) m n (begin
   m * n       ∎)
 
 m/n<m : ∀ m n .{{_ : NonZero m}} .{{_ : NonZero n}} → n ≥ 2 → m / n < m
-m/n<m m n n≥2 = *-cancelʳ-< (m / n) m (begin-strict
+m/n<m m n n≥2 = *-cancelʳ-< _ (m / n) m (begin-strict
   (m / n) * n ≤⟨ m/n*n≤m m n ⟩
   m           <⟨ m<m*n m n n≥2 ⟩
   m * n       ∎)
@@ -390,7 +390,7 @@ m/n/o≡m/[n*o] m n o = begin-equality
 
 /-*-interchange : ∀ {m n o p} .{{_ : NonZero o}} .{{_ : NonZero p}} .{{_ : NonZero (o * p)}} →
                   o ∣ m → p ∣ n → (m * n) / (o * p) ≡ (m / o) * (n / p)
-/-*-interchange {m} {n} {o@(suc _)} {p@(suc _)} o∣m p∣n = *-cancelˡ-≡ (o * p) (begin-equality
+/-*-interchange {m} {n} {o@(suc _)} {p@(suc _)} o∣m p∣n = *-cancelˡ-≡ _ _ (o * p) (begin-equality
   (o * p) * ((m * n) / (o * p)) ≡⟨  m*[n/m]≡n (*-pres-∣ o∣m p∣n) ⟩
   m * n                         ≡˘⟨ cong₂ _*_ (m*[n/m]≡n o∣m) (m*[n/m]≡n p∣n) ⟩
   (o * (m / o)) * (p * (n / p)) ≡⟨ [m*n]*[o*p]≡[m*o]*[n*p] o (m / o) p (n / p) ⟩
diff --git a/src/Data/Nat/DivMod/Core.agda b/src/Data/Nat/DivMod/Core.agda
index 00b9fe4036..61d225f39a 100644
--- a/src/Data/Nat/DivMod/Core.agda
+++ b/src/Data/Nat/DivMod/Core.agda
@@ -244,7 +244,7 @@ a*n[divₕ]n≡a acc (suc a) n = begin-equality
   acc + divₕ 0 (k + j) n j       ≡⟨ cong (acc +_) (divₕ-offsetEq _ n j _ (m≤n+m j k) ≤-refl case) ⟩
   acc + divₕ 0 (k + j) n (k + j) ∎
   where
-  case = inj₂′ (refl , +-cancelˡ-≤ (suc k) leq , m≤n+m j k)
+  case = inj₂′ (refl , +-cancelˡ-≤ (suc k) _ _ leq , m≤n+m j k)
 
 divₕ-mono-≤ : ∀ {acc} k {m n o p} → m ≤ n → p ≤ o → divₕ acc (k + o) m o ≤ divₕ acc (k + p) n p
 divₕ-mono-≤ {acc} k {0} {n} {_} {p} z≤n p≤o = acc≤divₕ[acc] (k + p) n p
diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda
index b81781dfc4..3dbb4a3933 100644
--- a/src/Data/Nat/Divisibility.agda
+++ b/src/Data/Nat/Divisibility.agda
@@ -199,7 +199,7 @@ m*n∣⇒n∣ m n rewrite *-comm m n = m*n∣⇒m∣ n m
 
 *-cancelˡ-∣ : ∀ {i j} k .{{_ : NonZero k}} → k * i ∣ k * j → i ∣ j
 *-cancelˡ-∣ {i} {j} k@(suc _) (divides q eq) =
-  divides q $ *-cancelʳ-≡ j (q * i) $ begin-equality
+  divides q $ *-cancelʳ-≡ j (q * i) _ $ begin-equality
     j * k        ≡⟨ *-comm j k ⟩
     k * j        ≡⟨ eq ⟩
     q * (k * i)  ≡⟨ cong (q *_) (*-comm k i) ⟩
diff --git a/src/Data/Nat/GCD/Lemmas.agda b/src/Data/Nat/GCD/Lemmas.agda
index 18fa834053..27c4ccd29d 100644
--- a/src/Data/Nat/GCD/Lemmas.agda
+++ b/src/Data/Nat/GCD/Lemmas.agda
@@ -150,7 +150,7 @@ lem₁₀ : ∀ {a′} b c {d} e f → let a = suc a′ in
 lem₁₀ {a′} b c {d} e f eq =
   m*n≡1⇒n≡1 (e * f ∸ b * c) d
     (lem₀ (e * f) (b * c) d 1
-       (*-cancelʳ-≡ (e * f * d) (b * c * d + 1) (begin
+       (*-cancelʳ-≡ (e * f * d) (b * c * d + 1) _ (begin
           e * f * d * a        ≡⟨ solve 4 (λ e f d a → e :* f :* d :* a
                                                    :=  e :* (f :* d :* a))
                                           refl e f d a ⟩
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 6bcd643f3a..69cc5d6da5 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -532,8 +532,8 @@ open ≤-Reasoning
   n + suc m   ∎
 
 +-cancelˡ-≡ : LeftCancellative _≡_ _+_
-+-cancelˡ-≡ zero    eq = eq
-+-cancelˡ-≡ (suc m) eq = +-cancelˡ-≡ m (cong pred eq)
++-cancelˡ-≡ zero    _ _ eq = eq
++-cancelˡ-≡ (suc m) _ _ eq = +-cancelˡ-≡ m _ _ (cong pred eq)
 
 +-cancelʳ-≡ : RightCancellative _≡_ _+_
 +-cancelʳ-≡ = comm+cancelˡ⇒cancelʳ +-comm +-cancelˡ-≡
@@ -650,21 +650,21 @@ m+n≡0⇒n≡0 m {n} m+n≡0 = m+n≡0⇒m≡0 n (trans (+-comm n m) (m+n≡0))
 -- Properties of _+_ and _≤_/_<_
 
 +-cancelˡ-≤ : LeftCancellative _≤_ _+_
-+-cancelˡ-≤ zero    le       = le
-+-cancelˡ-≤ (suc m) (s≤s le) = +-cancelˡ-≤ m le
++-cancelˡ-≤ zero    _ _ le       = le
++-cancelˡ-≤ (suc m) _ _ (s≤s le) = +-cancelˡ-≤ m _ _ le
 
 +-cancelʳ-≤ : RightCancellative _≤_ _+_
-+-cancelʳ-≤ {m} n o le =
-  +-cancelˡ-≤ m (subst₂ _≤_ (+-comm n m) (+-comm o m) le)
++-cancelʳ-≤ m n o le =
+  +-cancelˡ-≤ m _ _ (subst₂ _≤_ (+-comm n m) (+-comm o m) le)
 
 +-cancel-≤ : Cancellative _≤_ _+_
 +-cancel-≤ = +-cancelˡ-≤ , +-cancelʳ-≤
 
 +-cancelˡ-< : LeftCancellative _<_ _+_
-+-cancelˡ-< m {n} {o} = +-cancelˡ-≤ m ∘ subst (_≤ m + o) (sym (+-suc m n))
++-cancelˡ-< m n o = +-cancelˡ-≤ m (suc n) o ∘ subst (_≤ m + o) (sym (+-suc m n))
 
 +-cancelʳ-< : RightCancellative _<_ _+_
-+-cancelʳ-< n o n+m<o+m = +-cancelʳ-≤ (suc n) o n+m<o+m
++-cancelʳ-< m n o n+m<o+m = +-cancelʳ-≤ m (suc n) o n+m<o+m
 
 +-cancel-< : Cancellative _<_ _+_
 +-cancel-< = +-cancelˡ-< , +-cancelʳ-<
@@ -912,13 +912,13 @@ m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)
 ------------------------------------------------------------------------
 -- Other properties of _*_ and _≡_
 
-*-cancelʳ-≡ : ∀ m n {o} .{{_ : NonZero o}} → m * o ≡ n * o → m ≡ n
-*-cancelʳ-≡ zero    zero    {suc o} eq = refl
-*-cancelʳ-≡ (suc m) (suc n) {suc o} eq =
-  cong suc (*-cancelʳ-≡ m n (+-cancelˡ-≡ (suc o) eq))
+*-cancelʳ-≡ : ∀ m n o .{{_ : NonZero o}} → m * o ≡ n * o → m ≡ n
+*-cancelʳ-≡ zero    zero    (suc o) eq = refl
+*-cancelʳ-≡ (suc m) (suc n) (suc o) eq =
+  cong suc (*-cancelʳ-≡ m n (suc o) (+-cancelˡ-≡ (suc o) (m * suc o) (n * suc o) eq))
 
-*-cancelˡ-≡ : ∀ {m n} o .{{_ : NonZero o}} → o * m ≡ o * n → m ≡ n
-*-cancelˡ-≡ {m} {n} o rewrite *-comm o m | *-comm o n = *-cancelʳ-≡ m n
+*-cancelˡ-≡ : ∀ m n o .{{_ : NonZero o}} → o * m ≡ o * n → m ≡ n
+*-cancelˡ-≡ m n o rewrite *-comm o m | *-comm o n = *-cancelʳ-≡ m n o
 
 m*n≡0⇒m≡0∨n≡0 : ∀ m {n} → m * n ≡ 0 → m ≡ 0 ⊎ n ≡ 0
 m*n≡0⇒m≡0∨n≡0 zero    {n}     eq = inj₁ refl
@@ -953,7 +953,7 @@ m*n≡1⇒n≡1 m n eq = m*n≡1⇒m≡1 n m (trans (*-comm n m) eq)
 *-cancelʳ-≤ : ∀ m n o .{{_ : NonZero o}} → m * o ≤ n * o → m ≤ n
 *-cancelʳ-≤ zero    _       (suc o) _  = z≤n
 *-cancelʳ-≤ (suc m) (suc n) (suc o) le =
-  s≤s (*-cancelʳ-≤ m n (suc o) (+-cancelˡ-≤ (suc o) le))
+  s≤s (*-cancelʳ-≤ m n (suc o) (+-cancelˡ-≤ _ _ _ le))
 
 *-cancelˡ-≤ : ∀ {m n} o .{{_ : NonZero o}} → o * m ≤ o * n → m ≤ n
 *-cancelˡ-≤ {m} {n} o rewrite *-comm o m | *-comm o n = *-cancelʳ-≤ m n o
@@ -1011,13 +1011,13 @@ m<n⇒m<o*n {m} {n} o m<n = begin-strict
   o * n ∎
 
 *-cancelʳ-< : RightCancellative _<_ _*_
-*-cancelʳ-< {zero}  zero    (suc o) _     = 0<1+n
-*-cancelʳ-< {suc m} zero    (suc o) _     = 0<1+n
-*-cancelʳ-< {m}     (suc n) (suc o) nm<om =
-  s≤s (*-cancelʳ-< n o (+-cancelˡ-< m nm<om))
+*-cancelʳ-< zero    zero    (suc o) _     = 0<1+n
+*-cancelʳ-< (suc m) zero    (suc o) _     = 0<1+n
+*-cancelʳ-< m       (suc n) (suc o) nm<om =
+  s≤s (*-cancelʳ-< m n o (+-cancelˡ-< m _ _ nm<om))
 
 *-cancelˡ-< : LeftCancellative _<_ _*_
-*-cancelˡ-< x {y} {z} rewrite *-comm x y | *-comm x z = *-cancelʳ-< y z
+*-cancelˡ-< x y z rewrite *-comm x y | *-comm x z = *-cancelʳ-< x y z
 
 *-cancel-< : Cancellative _<_ _*_
 *-cancel-< = *-cancelˡ-< , *-cancelʳ-<
@@ -2071,7 +2071,7 @@ _>″?_ = flip _<″?_
 ≤″-irrelevant : Irrelevant _≤″_
 ≤″-irrelevant {m} (less-than-or-equal eq₁)
                   (less-than-or-equal eq₂)
-  with +-cancelˡ-≡ m (trans eq₁ (sym eq₂))
+  with +-cancelˡ-≡ m _ _ (trans eq₁ (sym eq₂))
 ... | refl = cong less-than-or-equal (≡-irrelevant eq₁ eq₂)
 
 <″-irrelevant : Irrelevant _<″_
diff --git a/src/Data/Sign/Properties.agda b/src/Data/Sign/Properties.agda
index 14b5954c49..440d5740b1 100644
--- a/src/Data/Sign/Properties.agda
+++ b/src/Data/Sign/Properties.agda
@@ -82,14 +82,14 @@ s*s≡+ - = refl
 *-assoc - - - = refl
 
 *-cancelʳ-≡ : RightCancellative _*_
-*-cancelʳ-≡ - - _  = refl
-*-cancelʳ-≡ - + eq = ⊥-elim (s≢opposite[s] _ $ sym eq)
-*-cancelʳ-≡ + - eq = ⊥-elim (s≢opposite[s] _ eq)
-*-cancelʳ-≡ + + _  = refl
+*-cancelʳ-≡ _ - - _  = refl
+*-cancelʳ-≡ _ - + eq = ⊥-elim (s≢opposite[s] _ $ sym eq)
+*-cancelʳ-≡ _ + - eq = ⊥-elim (s≢opposite[s] _ eq)
+*-cancelʳ-≡ _ + + _  = refl
 
 *-cancelˡ-≡ : LeftCancellative _*_
-*-cancelˡ-≡ - eq = opposite-injective eq
-*-cancelˡ-≡ + eq = eq
+*-cancelˡ-≡ - _ _ eq = opposite-injective eq
+*-cancelˡ-≡ + _ _ eq = eq
 
 *-cancel-≡ : Cancellative _*_
 *-cancel-≡ = *-cancelˡ-≡ , *-cancelʳ-≡
diff --git a/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda b/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda
index 871547d8b3..c7bddf4a5a 100644
--- a/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda
+++ b/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda
@@ -29,7 +29,7 @@ infix 10 _∼_
 
 ∼-trans : ∀ {i j k} → i ∼ j → j ∼ k → i ∼ k
 ∼-trans {x₁ , y₁} {x₂ , y₂} {x₃ , y₃} p q =
-  ≡-to-≅ $ +-cancelˡ-≡ y₂ $ ≅-to-≡ $ begin
+  ≡-to-≅ $ +-cancelˡ-≡ y₂ _ _ $ ≅-to-≡ $ begin
   y₂ + (x₁ + y₃) ≡⟨ ≡.sym (+-assoc y₂ x₁ y₃) ⟩
   y₂ + x₁ + y₃   ≡⟨ ≡.cong (_+ y₃) (+-comm y₂ x₁) ⟩
   x₁ + y₂ + y₃   ≅⟨ cong (_+ y₃) p ⟩