fix: only run processInaccessibleAsCtor if there is at least one constructor around

This PR fixes #10792.

Author: nomeata

tests/lean/run/issue10792.lean

@@ -0,0 +1,8 @@
+inductive Vec (α : Type) : Nat → Type where
+  | nil : Vec α 0
+  | cons (x : α) (xs : Vec α n) : Vec α (n.succ)
+
+-- set_option trace.Meta.Match.match true
+
+def test : Vec Unit 10000 → Nat
+  | Vec.cons () _ => 1