Disable in some tests

Author: nomeata

src/Lean/Meta/Match/Match.lean

@@ -330,8 +330,10 @@ private abbrev isCtorIdxIneq? (e : Expr) : Option FVarId := do
 
 private partial def contradiction (mvarId : MVarId) : MetaM Bool := do
   mvarId.withContext do
-    trace[Meta.Match.match] "match contradiction:\n{mvarId}"
+    withTraceNode `Meta.Match.match (msg := (return m!"{exceptBoolEmoji ·} Match.contradiction")) do
+    trace[Meta.Match.match] m!"Match.contradiction:\n{mvarId}"
     if (← mvarId.contradictionCore {}) then
+      trace[Meta.Match.match] "Contradiction found!"
       return true
     else
       -- Try harder by splitting `ctorIdx x ≠ 23` assumptions
@@ -587,7 +589,7 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do
     else
       -- A catch-all case
       let subst := subgoal.subst
-      trace[Meta.Match.match] "constructor catch-all case. subst: {subst.map.toList.map fun p => (mkFVar p.1, p.2)}"
+      trace[Meta.Match.match] "constructor catch-all case"
       let examples := p.examples.map <| Example.applyFVarSubst subst
       let newVars := p.vars.map fun x => x.applyFVarSubst subst
       let newAlts := p.alts.filter fun alt => match alt.patterns with

tests/lean/matchErrorMsg.lean.expected.out

@@ -1,2 +1,2 @@
 matchErrorMsg.lean:2:1-2:6: error: Missing cases:
-(Prod.mk Nat.zero (Nat.succ _))
+(Prod.mk Nat.zero _)

tests/lean/matchUnknownFVarBug.lean.expected.out

@@ -1,8 +1,8 @@
 matchUnknownFVarBug.lean:2:2-2:7: error: Missing cases:
-(some (Nat.succ _)), (some _)
-(some (Nat.succ _)), none
 none, (some _)
 none, none
+(some _), (some _)
+(some _), none
 matchUnknownFVarBug.lean:3:18-3:19: error: unsolved goals
 n? x✝ : Option Nat
 h : n? = some 0

tests/lean/patvar.lean.expected.out

@@ -1,6 +1,6 @@
 patvar.lean:3:0-3:22: error: Missing cases:
-(List.cons _ _)
+_
 patvar.lean:10:0-10:16: error: Missing cases:
-(List.cons _ _)
+_
 patvar.lean:14:2-14:9: error: Invalid pattern variable: Variable name must be atomic, but `foo.bar` has multiple components
 patvar.lean:17:2-17:9: error: Invalid pattern variable: Variable name must be atomic, but `foo.bar` has multiple components

tests/lean/run/bv_decide_enum_universe.lean

@@ -65,6 +65,7 @@ def test4 (x : PBool.{1}) : Bool :=
   | .false => false
   | .true => false
 
+set_option match.use_sparse_cases false -- TODO
 def test5 (x : PBool) : Bool :=
   match x with
   | .true => false

tests/lean/run/bv_decide_enums_two.lean

@@ -4,6 +4,7 @@ inductive State : Type
 | A : State
 | B : State
 
+set_option match.use_sparse_cases false
 
 def myFunc (s : State) : Bool :=
   match s with

tests/lean/run/match_int_lit_issue.lean

@@ -1,3 +1,16 @@
+set_option match.use_sparse_cases false -- TODO
+-- set_option trace.Meta.Match.match true
+
+/-
+This breaks because of less case splitting, and moving the case splitting to
+the contradiction phase is not enough, as `contradiction` does not look more than
+one constructor deep:
+```
+example (n : Nat) (h : n.succ = 0) : False := by contradiction
+example (n : Nat) (h : Int.ofNat n.succ = 0) : False := by contradiction
+```
+-/
+
 theorem Int.eq_zero_of_sign_eq_zero' : ∀ {a : Int}, sign a = 0 → a = 0
   | 0, _ => rfl