fix: grind canonicalizer (#10237)

This PR fixes a missing case in the `grind` canonicalizer. Some types
may include terms or propositions that are internalized later in the
`grind` state.

closes #10232

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 =>

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