fix: grind sort internalization (#10477)

This PR ensures sorts are internalized by `grind`.

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -380,7 +380,13 @@ where
     trace_goal[grind.internalize] "[{generation}] {e}"
     match e with
     | .bvar .. => unreachable!
-    | .sort .. => return ()
+    | .sort .. =>
+      /-
+      **Note**: It may seem wasteful to create ENodes for sorts, but it is useful for the E-matching module.
+      The E-matching module assumes that the arguments of an internalized application have also been internalized,
+      unless they are `grind` gadgets.
+      -/
+      mkENode' e generation
     | .fvar .. =>
       mkENode' e generation
       checkAndAddSplitCandidate e

tests/lean/run/grind_sort_intern.lean

@@ -0,0 +1,16 @@
+def f (α : Sort u) (_ : α) : Nat := 0
+
+theorem feq : f (List α) x = 0 := rfl
+
+/--
+error: `grind` failed
+case grind
+h : ¬f Prop True = 0
+⊢ False
+-/
+#guard_msgs in
+example: f Prop True = 0 := by
+  grind -verbose [feq] -- must not produce error `Prop` has not been internalized
+
+example: f Prop True = 0 := by
+  grind [f]