diff --git a/src/Lean/Meta/Tactic/Grind/Canon.lean b/src/Lean/Meta/Tactic/Grind/Canon.lean
index e397605666..0c2bcc3463 100644
--- a/src/Lean/Meta/Tactic/Grind/Canon.lean
+++ b/src/Lean/Meta/Tactic/Grind/Canon.lean
@@ -233,7 +233,12 @@ where
             let arg := args[i]
             trace_goal[grind.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}"
             let arg' ← match (← shouldCanon pinfos i arg) with
-              | .canonType => canonType e f i arg
+              | .canonType =>
+                /-
+                The type may have nested propositions and terms that may need to be canonicalized too.
+                So, we must recurse over it. See issue #10232
+                -/
+                canonType e f i (← visit arg)
               | .canonImplicit => canonImplicit e f i (← visit arg)
               | .visit => visit arg
               | .canonInst =>
diff --git a/tests/lean/run/grind_10232.lean b/tests/lean/run/grind_10232.lean
new file mode 100644
index 0000000000..e8e777736d
--- /dev/null
+++ b/tests/lean/run/grind_10232.lean
@@ -0,0 +1,9 @@
+def U {shape : Std.PRange.RangeShape} (b : Std.PRange.Bound shape.upper α) : Unit := sorry
+
+structure T (l : α) : Type u where
+
+def mysorry : α := sorry -- instead of `mysorry`, we could also use `sorry`.
+
+example (inv : (T (U (shape := ⟨.closed, .closed⟩) 1)) → Prop)
+    (h : inv mysorry) : True := by
+  grind