fix: regression on match expressions with builtin literals

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.ProjFns
+import Lean.Meta.CtorRecognizer
 import Lean.Compiler.BorrowedAnnotation
 import Lean.Compiler.LCNF.Types
 import Lean.Compiler.LCNF.Bind
@@ -619,7 +620,7 @@ where
       let rhs ← liftMetaM do Meta.whnf args[inductVal.numParams + inductVal.numIndices + 2]!
       let lhs := lhs.toCtorIfLit
       let rhs := rhs.toCtorIfLit
-      match lhs.isConstructorApp? (← getEnv), rhs.isConstructorApp? (← getEnv) with
+      match (← liftMetaM <| Meta.isConstructorApp? lhs), (← liftMetaM <| Meta.isConstructorApp? rhs) with
       | some lhsCtorVal, some rhsCtorVal =>
         if lhsCtorVal.name == rhsCtorVal.name then
           etaIfUnderApplied e (arity+1) do

src/Lean/Elab/Match.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Mario Carneiro
 -/
 prelude
 import Lean.Util.ForEachExprWhere
+import Lean.Meta.CtorRecognizer
 import Lean.Meta.Match.Match
 import Lean.Meta.GeneralizeVars
 import Lean.Meta.ForEachExpr
@@ -442,7 +443,7 @@ private def applyRefMap (e : Expr) (map : ExprMap Expr) : Expr :=
 -/
 private def whnfPreservingPatternRef (e : Expr) : MetaM Expr := do
   let eNew ← whnf e
-  if eNew.isConstructorApp (← getEnv) then
+  if (← isConstructorApp eNew) then
     return eNew
   else
     return applyRefMap eNew (mkPatternRefMap e)

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Eqns
+import Lean.Meta.CtorRecognizer
 import Lean.Util.CollectFVars
 import Lean.Util.ForEachExprWhere
 import Lean.Meta.Tactic.Split
@@ -218,13 +219,14 @@ where
 -/
 private def shouldUseSimpMatch (e : Expr) : MetaM Bool := do
   let env ← getEnv
-  return Option.isSome <| e.find? fun e => Id.run do
-    if let some info := isMatcherAppCore? env e then
-      let args := e.getAppArgs
-      for discr in args[info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do
-        if discr.isConstructorApp env then
-          return true
-    return false
+  let find (root : Expr) : ExceptT Unit MetaM Unit :=
+    root.forEach fun e => do
+      if let some info := isMatcherAppCore? env e then
+        let args := e.getAppArgs
+        for discr in args[info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do
+          if (← Meta.isConstructorApp discr) then
+            throwThe Unit ()
+  return (← (find e).run) matches .error _
 
 partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
   let (_, eqnTypes) ← go mvarId |>.run { declNames } |>.run #[]

src/Lean/Meta/CtorRecognizer.lean

@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.LitValues
+
+namespace Lean.Meta
+
+private def getConstructorVal? (env : Environment) (ctorName : Name) : Option ConstructorVal :=
+  match env.find? ctorName with
+  | some (.ctorInfo v) => v
+  | _                  => none
+
+
+/--
+If `e` is a constructor application or a builtin literal defeq to a constructor application,
+then return the corresponding `ConstructorVal`.
+-/
+def isConstructorApp? (e : Expr) : MetaM (Option ConstructorVal) := do
+  let e ← litToCtor e
+  let .const n _ := e.getAppFn | return none
+  let some v := getConstructorVal? (← getEnv) n | return none
+  if v.numParams + v.numFields == e.getAppNumArgs then
+    return some v
+  else
+    return none
+
+/--
+Similar to `isConstructorApp?`, but uses `whnf`.
+-/
+def isConstructorApp'? (e : Expr) : MetaM (Option ConstructorVal) := do
+  if let some r ← isConstructorApp? e then
+    return r
+  isConstructorApp? (← whnf e)
+
+/--
+Returns `true`, if `e` is constructor application of builtin literal defeq to
+a constructor application.
+-/
+def isConstructorApp (e : Expr) : MetaM Bool :=
+  return (← isConstructorApp? e).isSome
+
+/--
+Returns `true` if `isConstructorApp e` or `isConstructorApp (← whnf e)`
+-/
+def isConstructorApp' (e : Expr) : MetaM Bool := do
+  if (← isConstructorApp e) then return true
+  return (← isConstructorApp (← whnf e))
+
+/--
+If `e` is a constructor application, return a pair containing the corresponding `ConstructorVal` and the constructor
+application arguments.
+-/
+def constructorApp? (e : Expr) : MetaM (Option (ConstructorVal × Array Expr)) := do
+  let e ← litToCtor e
+  let .const declName _ := e.getAppFn | return none
+  let some v := getConstructorVal? (← getEnv) declName | return none
+  if v.numParams + v.numFields == e.getAppNumArgs then
+    return some (v, e.getAppArgs)
+  else
+    return none
+
+/--
+Similar to `constructorApp?`, but on failure it puts `e` in WHNF and tries again.
+-/
+def constructorApp'? (e : Expr) : MetaM (Option (ConstructorVal × Array Expr)) := do
+  if let some r ← constructorApp? e then
+    return some r
+  else
+    constructorApp? (← whnf e)
+
+end Lean.Meta

src/Lean/Meta/LitValues.lean

@@ -103,7 +103,7 @@ def getUInt64Value? (e : Expr) : MetaM (Option UInt64) := OptionT.run do
   return UInt64.ofNat n
 
 /--
-If `e` is literal value, ensure it is encoded using the standard representation.
+If `e` is a literal value, ensure it is encoded using the standard representation.
 Otherwise, just return `e`.
 -/
 def normLitValue (e : Expr) : MetaM Expr := do
@@ -120,4 +120,32 @@ def normLitValue (e : Expr) : MetaM Expr := do
   if let some n ← getUInt64Value? e then return toExpr n
   return e
 
+/--
+If `e` is a `Nat`, `Int`, or `Fin` literal value, converts it into a constructor application.
+Otherwise, just return `e`.
+-/
+-- TODO: support other builtin literals if needed
+def litToCtor (e : Expr) : MetaM Expr := do
+  let e ← instantiateMVars e
+  if let some n ← getNatValue? e then
+    if n = 0 then
+      return mkConst ``Nat.zero
+    else
+      return .app (mkConst ``Nat.succ) (toExpr (n-1))
+  if let some n ← getIntValue? e then
+    if n < 0 then
+      return .app (mkConst ``Int.negSucc) (toExpr (- (n+1)).toNat)
+    else
+      return .app (mkConst ``Int.ofNat) (toExpr n.toNat)
+  if let some ⟨n, v⟩ ← getFinValue? e then
+    let i := toExpr v.val
+    let n := toExpr n
+    -- Remark: we construct the proof manually here to avoid a cyclic dependency.
+    let p := mkApp4 (mkConst ``LT.lt [0]) (mkConst ``Nat) (mkConst ``instLTNat) i n
+    let h := mkApp3 (mkConst ``of_decide_eq_true) p
+      (mkApp2 (mkConst ``Nat.decLt) i n)
+      (mkApp2 (mkConst ``Eq.refl [1]) (mkConst ``Bool) (mkConst ``true))
+    return mkApp3 (mkConst ``Fin.mk) n i h
+  return e
+
 end Lean.Meta

src/Lean/Meta/Match/Match.lean

@@ -7,6 +7,7 @@ prelude
 import Lean.Meta.LitValues
 import Lean.Meta.Check
 import Lean.Meta.Closure
+import Lean.Meta.CtorRecognizer
 import Lean.Meta.Tactic.Cases
 import Lean.Meta.Tactic.Contradiction
 import Lean.Meta.GeneralizeTelescope
@@ -409,14 +410,13 @@ private def hasRecursiveType (x : Expr) : MetaM Bool := do
    update the next patterns with the fields of the constructor.
    Otherwise, return none. -/
 def processInaccessibleAsCtor (alt : Alt) (ctorName : Name) : MetaM (Option Alt) := do
-  let env ← getEnv
   match alt.patterns with
   | p@(.inaccessible e) :: ps =>
     trace[Meta.Match.match] "inaccessible in ctor step {e}"
     withExistingLocalDecls alt.fvarDecls do
       -- Try to push inaccessible annotations.
       let e ← whnfD e
-      match e.constructorApp? env with
+      match (← constructorApp? e) with
       | some (ctorVal, ctorArgs) =>
         if ctorVal.name == ctorName then
           let fields := ctorArgs.extract ctorVal.numParams ctorArgs.size
@@ -497,12 +497,12 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do
 private def altsAreCtorLike (p : Problem) : MetaM Bool := withGoalOf p do
   p.alts.allM fun alt => do match alt.patterns with
     | .ctor .. :: _ => return true
-    | .inaccessible e :: _ => return (← whnfD e).isConstructorApp (← getEnv)
+    | .inaccessible e :: _ => isConstructorApp e
     | _ => return false
 
 private def processNonVariable (p : Problem) : MetaM Problem := withGoalOf p do
   let x :: xs := p.vars | unreachable!
-  if let some (ctorVal, xArgs) := (← whnfD x).constructorApp? (← getEnv) then
+  if let some (ctorVal, xArgs) ← withTransparency .default <| constructorApp'? x then
     if (← altsAreCtorLike p) then
       let alts ← p.alts.filterMapM fun alt => do
         match alt.patterns with

src/Lean/Meta/Match/MatchEqs.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.CtorRecognizer
 import Lean.Meta.Match.Match
 import Lean.Meta.Match.MatchEqsExt
 import Lean.Meta.Tactic.Apply
@@ -250,7 +251,7 @@ private def processNextEq : M Bool := do
           return true
         -- If it is not possible, we try to show the hypothesis is redundant by substituting even variables that are not at `s.xs`, and then use contradiction.
         else
-          match lhs.isConstructorApp? (← getEnv), rhs.isConstructorApp? (← getEnv) with
+          match (← isConstructorApp? lhs), (← isConstructorApp? rhs) with
           | some lhsCtor, some rhsCtor =>
             if lhsCtor.name != rhsCtor.name then
               return false -- If the constructors are different, we can discard the hypothesis even if it a heterogeneous equality
@@ -378,7 +379,7 @@ private def injectionAnyCandidate? (type : Expr) : MetaM (Option (Expr × Expr))
       return some (lhs, rhs)
   return none
 
-private def injectionAny (mvarId : MVarId) : MetaM InjectionAnyResult :=
+private def injectionAny (mvarId : MVarId) : MetaM InjectionAnyResult := do
   mvarId.withContext do
     for localDecl in (← getLCtx) do
       if let some (lhs, rhs) ← injectionAnyCandidate? localDecl.type then

src/Lean/Meta/MatchUtil.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Util.Recognizers
 import Lean.Meta.Basic
+import Lean.Meta.CtorRecognizer
 
 namespace Lean.Meta
 
@@ -62,8 +63,6 @@ def matchNe? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) :=
       return none
 
 def matchConstructorApp? (e : Expr) : MetaM (Option ConstructorVal) := do
-  let env ← getEnv
-  matchHelper? e fun e =>
-    return e.isConstructorApp? env
+  matchHelper? e isConstructorApp?
 
 end Lean.Meta

src/Lean/Meta/Tactic/Acyclic.lean

@@ -14,7 +14,7 @@ private def isTarget (lhs rhs : Expr) : MetaM Bool := do
   if !lhs.isFVar || !lhs.occurs rhs then
     return false
   else
-    return (← whnf rhs).isConstructorApp (← getEnv)
+    isConstructorApp' rhs
 
 /--
   Close the given goal if `h` is a proof for an equality such as `as = a :: as`.

src/Lean/Meta/Tactic/Injection.lean

@@ -34,19 +34,19 @@ def injectionCore (mvarId : MVarId) (fvarId : FVarId) : MetaM InjectionResultCor
       match type.eq? with
       | none           => throwTacticEx `injection mvarId "equality expected"
       | some (_, a, b) =>
-        let a ← whnf a
-        let b ← whnf b
         let target ← mvarId.getType
-        let env ← getEnv
-        match a.isConstructorApp? env, b.isConstructorApp? env with
+        match (← isConstructorApp'? a), (← isConstructorApp'? b) with
         | some aCtor, some bCtor =>
-          let val ← mkNoConfusion target prf
+          -- We use the default transparency because `a` and `b` may be builtin literals.
+          let val ← withTransparency .default <| mkNoConfusion target prf
           if aCtor.name != bCtor.name then
             mvarId.assign val
             return InjectionResultCore.solved
           else
             let valType ← inferType val
-            let valType ← whnf valType
+            -- We use the default transparency setting here because `a` and `b` may be builtin literals
+            -- that need to expanded into constructors.
+            let valType ← whnfD valType
             match valType with
             | Expr.forallE _ newTarget _ _ =>
               let newTarget := newTarget.headBeta

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -69,7 +69,7 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
           unless e.getAppNumArgs > projInfo.numParams do
             return none
           let major := e.getArg! projInfo.numParams
-          unless major.isConstructorApp (← getEnv) do
+          unless (← isConstructorApp major) do
             return none
           reduceProjCont? (← withDefault <| unfoldDefinition? e)
       else

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -168,22 +168,11 @@ where
   inErasedSet (thm : SimpTheorem) : Bool :=
     erased.contains thm.origin
 
--- TODO: workaround for `Expr.constructorApp?` limitations. We should handle `OfNat.ofNat` there
-private def reduceOfNatNat (e : Expr) : MetaM Expr := do
-  unless e.isAppOfArity ``OfNat.ofNat 3 do
-    return e
-  unless (← whnfD (e.getArg! 0)).isConstOf ``Nat do
-    return e
-  return e.getArg! 1
-
 def simpCtorEq : Simproc := fun e => withReducibleAndInstances do
   match e.eq? with
   | none => return .continue
   | some (_, lhs, rhs) =>
-    let lhs ← reduceOfNatNat (← whnf lhs)
-    let rhs ← reduceOfNatNat (← whnf rhs)
-    let env ← getEnv
-    match lhs.constructorApp? env, rhs.constructorApp? env with
+    match (← constructorApp'? lhs), (← constructorApp'? rhs) with
     | some (c₁, _), some (c₂, _) =>
       if c₁.name != c₂.name then
         withLocalDeclD `h e fun h =>

src/Lean/Meta/Tactic/UnifyEq.lean

@@ -70,8 +70,7 @@ def unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := {})
           else
             throwError "dependent elimination failed, failed to solve equation{indentExpr eqDecl.type}"
         let rec injection (a b : Expr) := do
-          let env ← getEnv
-          if a.isConstructorApp env && b.isConstructorApp env then
+          if (← isConstructorApp a <&&> isConstructorApp b) then
             /- ctor_i ... = ctor_j ... -/
             match (← injectionCore mvarId eqFVarId) with
             | InjectionResultCore.solved                   => return none -- this alternative has been solved

src/Lean/Meta/WHNF.lean

@@ -8,6 +8,7 @@ import Lean.Structure
 import Lean.Util.Recognizers
 import Lean.Meta.GetUnfoldableConst
 import Lean.Meta.FunInfo
+import Lean.Meta.CtorRecognizer
 import Lean.Meta.Match.MatcherInfo
 import Lean.Meta.Match.MatchPatternAttr
 
@@ -133,7 +134,7 @@ private def toCtorWhenStructure (inductName : Name) (major : Expr) : MetaM Expr
   let env ← getEnv
   if !isStructureLike env inductName then
     return major
-  else if let some _ := major.isConstructorApp? env then
+  else if let some _ ← isConstructorApp? major then
     return major
   else
     let majorType ← inferType major
@@ -754,7 +755,7 @@ mutual
                 let numArgs := e.getAppNumArgs
                 if recArgPos >= numArgs then return none
                 let recArg := e.getArg! recArgPos numArgs
-                if !(← whnfMatcher recArg).isConstructorApp (← getEnv) then return none
+                if !(← isConstructorApp (← whnfMatcher recArg)) then return none
                 return some r
             | _ =>
               if (← getMatcherInfo? fInfo.name).isSome then

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -178,7 +178,7 @@ def shouldShowMotive (motive : Expr) (opts : Options) : MetaM Bool := do
 def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStructureInstances do
   let env ← getEnv
   let e ← getExpr
-  let some s ← pure $ e.isConstructorApp? env | failure
+  let some s ← isConstructorApp? e | failure
   guard $ isStructure env s.induct;
   /- If implicit arguments should be shown, and the structure has parameters, we should not
      pretty print using { ... }, because we will not be able to see the parameters. -/

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -6,6 +6,7 @@ Authors: Daniel Selsam
 prelude
 import Lean.Data.RBMap
 import Lean.Meta.SynthInstance
+import Lean.Meta.CtorRecognizer
 import Lean.Util.FindMVar
 import Lean.Util.FindLevelMVar
 import Lean.Util.CollectLevelParams
@@ -152,7 +153,7 @@ def isIdLike (arg : Expr) : Bool :=
   | _ => false
 
 def isStructureInstance (e : Expr) : MetaM Bool := do
-  match e.isConstructorApp? (← getEnv) with
+  match (← isConstructorApp? e) with
   | some s => return isStructure (← getEnv) s.induct
   | none   => return false
 

src/Lean/Util/Recognizers.lean

@@ -106,52 +106,4 @@ def arrayLit? (e : Expr) : Option (Expr × List Expr) :=
 def prod? (e : Expr) : Option (Expr × Expr) :=
   e.app2? ``Prod
 
-private def getConstructorVal? (env : Environment) (ctorName : Name) : Option ConstructorVal :=
-  match env.find? ctorName with
-  | some (ConstantInfo.ctorInfo v) => v
-  | _                              => none
-
-def isConstructorApp? (env : Environment) (e : Expr) : Option ConstructorVal :=
-  match e with
-  | Expr.lit (Literal.natVal n) => if n == 0 then getConstructorVal? env `Nat.zero else getConstructorVal? env `Nat.succ
-  | _ =>
-    match e.getAppFn with
-    | Expr.const n _ => match getConstructorVal? env n with
-      | some v => if v.numParams + v.numFields == e.getAppNumArgs then some v else none
-      | none   => none
-    | _ => none
-
-def isConstructorApp (env : Environment) (e : Expr) : Bool :=
-  e.isConstructorApp? env |>.isSome
-
-/--
-If `e` is a constructor application, return a pair containing the corresponding `ConstructorVal` and the constructor
-application arguments.
-This function treats numerals as constructors. For example, if `e` is the numeral `2`, the result pair
-is `ConstructorVal` for `Nat.succ`, and the array `#[1]`. The parameter `useRaw` controls how the resulting
-numeral is represented. If `useRaw := false`, then `mkNatLit` is used, otherwise `mkRawNatLit`.
-Recall that `mkNatLit` uses the `OfNat.ofNat` application which is the canonical way of representing numerals
-in the elaborator and tactic framework. We `useRaw := false` in the compiler (aka code generator).
-
-Remark: This function does not treat `(ofNat 0 : Nat)` applications as constructors.
--/
-def constructorApp? (env : Environment) (e : Expr) (useRaw := false) : Option (ConstructorVal × Array Expr) := do
-  match e with
-  | Expr.lit (Literal.natVal n) =>
-    if n == 0 then do
-      let v ← getConstructorVal? env `Nat.zero
-      pure (v, #[])
-    else do
-      let v ← getConstructorVal? env `Nat.succ
-      pure (v, #[if useRaw then mkRawNatLit (n-1) else mkNatLit (n-1)])
-  | _ =>
-    match e.getAppFn with
-    | Expr.const n _ => do
-      let v ← getConstructorVal? env n
-      if v.numParams + v.numFields == e.getAppNumArgs then
-        pure (v, e.getAppArgs)
-      else
-        none
-    | _ => none
-
 end Lean.Expr

tests/lean/run/depElim1.lean

@@ -31,8 +31,7 @@ match env.find? ctorName with
 | some (ConstantInfo.ctorInfo v) => if args.size == v.numParams + v.numFields then return some (v, fn, args) else return none
 | _                              => return none
 
-private def constructorApp? (e : Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do
-let env ← getEnv
+private def ctorApp? (e : Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do
 match e with
 | Expr.lit (Literal.natVal n) =>
    if n == 0 then getConstructorVal `Nat.zero (mkConst `Nat.zero) #[] else getConstructorVal `Nat.succ (mkConst `Nat.succ) #[mkNatLit (n-1)]
@@ -70,7 +69,7 @@ partial def mkPattern : Expr → MetaM Pattern
       return Pattern.arrayLit elemType pats
     | none =>
       let e ← whnfD e
-      let r? ← constructorApp? e
+      let r? ← ctorApp? e
       match r? with
       | none      => throwError "unexpected pattern"
       | some (cval, fn, args) =>

tests/lean/run/litToCtor.lean

@@ -0,0 +1,58 @@
+import Lean
+open Lean Meta
+def test [ToExpr α] (a : α) : MetaM Unit := do
+   let a := toExpr a
+   let c ← litToCtor a
+   check c
+   IO.println s!"{← ppExpr c}"
+   assert! (← isDefEq c a)
+/--
+info: Nat.succ 9
+-/
+#guard_msgs in
+#eval test 10
+/--
+info: Nat.succ 0
+-/
+#guard_msgs in
+#eval test 1
+/--
+info: Nat.zero
+-/
+#guard_msgs in
+#eval test 0
+/--
+info: Int.negSucc 1
+-/
+#guard_msgs in
+#eval test (-2)
+/--
+info: Int.negSucc 0
+-/
+#guard_msgs in
+#eval test (-1)
+/--
+info: Int.ofNat 0
+-/
+#guard_msgs in
+#eval test (0 : Int)
+/--
+info: Int.ofNat 3
+-/
+#guard_msgs in
+#eval test (3 : Int)
+/--
+info: { val := 3, isLt := ⋯ }
+-/
+#guard_msgs in
+#eval test (3 : Fin 5)
+/--
+info: { val := 0, isLt := ⋯ }
+-/
+#guard_msgs in
+#eval test (0 : Fin 5)
+/--
+info: { val := 1, isLt := ⋯ }
+-/
+#guard_msgs in
+#eval test (6 : Fin 5)

tests/lean/run/match_lit_regression.lean

@@ -0,0 +1,17 @@
+structure cmplx where
+  X : Nat → Type
+  d : ∀ i j, X i → X j
+  shape : ∀ i j, ¬ i = j + 1 → d i j = sorry
+
+def augment (C : cmplx) {X : Type} (f : C.X 0 → X) :
+    cmplx where
+  X | 0 => X
+    | i + 1 => C.X i
+  d | 1, 0 => f
+    | i + 1, j + 1 => C.d i j
+    | _, _ => sorry
+  shape
+    | 1, 0, h => absurd rfl h
+    | i + 2, 0, _ => sorry
+    | 0, _, _ => sorry
+    | i + 1, j + 1, h => by simp; sorry