feat: (generalizing := true) is the default behavior for match-expressions

closes #1018

RELEASES.md

@@ -56,3 +56,5 @@ we can now write
 match h : sort.swap a b with
 | (r₁, r₂) => ... -- `h : sort.swap a b = (r₁, r₂)`
 ```
+
+* `(generalizing := true)` is the default behavior for `match` expressions even if the expected type is not a proposition.

src/Lean/Elab/Match.lean

@@ -588,8 +588,6 @@ where
   "Generalize" variables that depend on the discriminants.
 
   Remarks and limitations:
-  - If `matchType` is a proposition, then we generalize even when the user did not provide `(generalizing := true)`.
-    Motivation: users should have control about the actual `match`-expressions in their programs.
   - We currently do not generalize let-decls.
   - We abort generalization if the new `matchType` is type incorrect.
   - Only discriminants that are free variables are considered during specialization.
@@ -598,10 +596,7 @@ where
     this is the exact behavior users would get if they had written it by hand. Recall there is no `clear` in term mode.
 -/
 private def generalize (discrs : Array Expr) (matchType : Expr) (altViews : Array MatchAltView) (generalizing? : Option Bool) : TermElabM (Array Expr × Expr × Array MatchAltView × Bool) := do
-  let gen ←
-    match generalizing? with
-    | some g => pure g
-    | _ => isProp matchType
+  let gen := if let some g := generalizing? then g else true
   if !gen then
     return (discrs, matchType, altViews, false)
   else

tests/lean/matchErrorLocation.lean

@@ -1,6 +1,6 @@
-
+--
 
 def head {α} (xs : List α) (h : xs = [] → False) : α :=
-match he:xs with
+match (generalizing := false) he:xs with
 | []   => h he
 | x::_ => x

tests/lean/run/1018.lean

@@ -0,0 +1,15 @@
+inductive Fam : Type → Type 1 where
+  | any : Fam α
+  | nat : Nat → Fam Nat
+
+example (a : α) : Fam α → α
+  | Fam.any => a
+  | Fam.nat n => n
+
+inductive Fam2 : Type → Type → Type 1 where
+  | any : Fam2 α α
+  | nat : Nat → Fam2 Nat Nat
+
+example (a : α) : Fam2 α β → β
+  | Fam2.any   => a
+  | Fam2.nat n => n