From c218c8a80155ea8c2c760f2f15fbd6642046cbd5 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Thu, 14 Nov 2024 15:02:51 +0000 Subject: [PATCH 1/4] fix: stack overflow at `mkBinding` if type occurs check fails. --- src/Lean/MetavarContext.lean | 68 +++++++++++++++++------------------- 1 file changed, 32 insertions(+), 36 deletions(-) diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 1401e44c9027..987b4354197d 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -910,6 +910,10 @@ structure Context where binderInfoForMVars : BinderInfo := BinderInfo.implicit /-- Set of unassigned metavariables being abstracted. -/ mvarIdsToAbstract : MVarIdSet := {} + /-- Map of metavariable assignments that haven't yet been added to the context. + This is necessary to deal with metavariables that contain themselves in their own type. + Without this, such a situation would lead to infinite recursion. -/ + mvarIdsInProgress : AssocList MVarId Expr := {} abbrev MCore := EStateM Exception State abbrev M := ReaderT Context MCore @@ -941,7 +945,7 @@ private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr) /-- Given `toRevert` an array of free variables s.t. `lctx` contains their declarations, - return a new array of free variables that contains `toRevert` and all variables + return a new array of free variables that contains `toRevert` and all free variables in `lctx` that may depend on `toRevert`. Remark: the result is sorted by `LocalDecl` indices. @@ -1005,7 +1009,7 @@ def collectForwardDeps (lctx : LocalContext) (toRevert : Array Expr) : M (Array We use this function when we create auxiliary metavariables at `elimMVarDepsAux`. -/ def reduceLocalContext (lctx : LocalContext) (toRevert : Array Expr) : LocalContext := toRevert.foldr (init := lctx) fun x lctx => - if x.isFVar then lctx.erase x.fvarId! else lctx + lctx.erase x.fvarId! /-- Return free variables in `xs` that are in the local context `lctx` -/ private def getInScope (lctx : LocalContext) (xs : Array Expr) : Array Expr := @@ -1030,12 +1034,9 @@ private def getInScope (lctx : LocalContext) (xs : Array Expr) : Array Expr := how let-decl free variables are handled. -/ private def mkMVarApp (lctx : LocalContext) (mvar : Expr) (xs : Array Expr) (kind : MetavarKind) : Expr := xs.foldl (init := mvar) fun e x => - if !x.isFVar then - e - else - match kind with - | MetavarKind.syntheticOpaque => mkApp e x - | _ => if (lctx.getFVar! x).isLet then e else mkApp e x + match kind with + | MetavarKind.syntheticOpaque => mkApp e x + | _ => if (lctx.getFVar! x).isLet then e else mkApp e x mutual @@ -1054,7 +1055,7 @@ mutual | e => return e /-- - Given a metavariable with type `e`, kind `kind` and free/meta variables `xs` in its local context `lctx`, + Given a metavariable with type `e`, kind `kind` and free variables `xs` in its local context `lctx`, create the type for a new auxiliary metavariable. These auxiliary metavariables are created by `elimMVar`. See "Gruesome details" section in the beginning of the file. @@ -1065,30 +1066,22 @@ mutual let e ← abstractRangeAux xs xs.size e xs.size.foldRevM (init := e) fun i e => do let x := xs[i]! - if x.isFVar then - match lctx.getFVar! x with - | LocalDecl.cdecl _ _ n type bi _ => - let type := type.headBeta - let type ← abstractRangeAux xs i type - return Lean.mkForall n bi type e - | LocalDecl.ldecl _ _ n type value nonDep _ => - let type := type.headBeta - let type ← abstractRangeAux xs i type - let value ← abstractRangeAux xs i value - let e := mkLet n type value e nonDep - match kind with - | MetavarKind.syntheticOpaque => - -- See "Gruesome details" section in the beginning of the file - let e := e.liftLooseBVars 0 1 - return mkForall n BinderInfo.default type e - | _ => pure e - else - -- `xs` may contain metavariables as "may dependencies" (see `findExprDependsOn`) - let mvarDecl := (← get).mctx.getDecl x.mvarId! - let type := mvarDecl.type.headBeta + match lctx.getFVar! x with + | LocalDecl.cdecl _ _ n type bi _ => + let type := type.headBeta let type ← abstractRangeAux xs i type - let id ← if mvarDecl.userName.isAnonymous then mkFreshBinderName else pure mvarDecl.userName - return Lean.mkForall id (← read).binderInfoForMVars type e + return Lean.mkForall n bi type e + | LocalDecl.ldecl _ _ n type value nonDep _ => + let type := type.headBeta + let type ← abstractRangeAux xs i type + let value ← abstractRangeAux xs i value + let e := mkLet n type value e nonDep + match kind with + | MetavarKind.syntheticOpaque => + -- See "Gruesome details" section in the beginning of the file + let e := e.liftLooseBVars 0 1 + return mkForall n BinderInfo.default type e + | _ => pure e where abstractRangeAux (xs : Array Expr) (i : Nat) (e : Expr) : M Expr := do let e ← elim xs e @@ -1123,16 +1116,16 @@ mutual let newMVarKind := if !(← mvarId.isAssignable) then MetavarKind.syntheticOpaque else mvarDecl.kind let args ← args.mapM (visit xs) -- Note that `toRevert` only contains free variables at this point since it is the result of `getInScope`; - -- after `collectForwardDeps`, this may no longer be the case because it may include metavariables - -- whose local contexts depend on `toRevert` (i.e. "may dependencies") + -- after `collectForwardDeps`, this is still the case. let toRevert ← collectForwardDeps mvarLCtx toRevert let newMVarLCtx := reduceLocalContext mvarLCtx toRevert let newLocalInsts := mvarDecl.localInstances.filter fun inst => toRevert.all fun x => inst.fvar != x -- Remark: we must reset the cache before processing `mkAuxMVarType` because `toRevert` may not be equal to `xs` - let newMVarType ← withFreshCache do mkAuxMVarType mvarLCtx toRevert newMVarKind mvarDecl.type let newMVarId := { name := (← get).ngen.curr } let newMVar := mkMVar newMVarId let result := mkMVarApp mvarLCtx newMVar toRevert newMVarKind + let newMVarType ← withReader (fun ctx => { ctx with mvarIdsInProgress := ctx.mvarIdsInProgress.cons mvarId result }) do + withFreshCache do mkAuxMVarType mvarLCtx toRevert newMVarKind mvarDecl.type let numScopeArgs := mvarDecl.numScopeArgs + result.getAppNumArgs modify fun s => { s with mctx := s.mctx.addExprMVarDecl newMVarId Name.anonymous newMVarLCtx newLocalInsts newMVarType newMVarKind numScopeArgs, @@ -1170,7 +1163,10 @@ mutual if (← read).mvarIdsToAbstract.contains mvarId then return mkAppN f (← args.mapM (visit xs)) else - return (← elimMVar xs mvarId args).1 + if let some result := (← read).mvarIdsInProgress.find? mvarId then + return result + else + return (← elimMVar xs mvarId args).1 | _ => return mkAppN (← visit xs f) (← args.mapM (visit xs)) From 7006895a0819320efcbefdc166f4468191d023fb Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Thu, 14 Nov 2024 15:36:28 +0000 Subject: [PATCH 2/4] fix: name generator problem --- src/Lean/MetavarContext.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 987b4354197d..95e3924adf2a 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -1122,15 +1122,14 @@ mutual let newLocalInsts := mvarDecl.localInstances.filter fun inst => toRevert.all fun x => inst.fvar != x -- Remark: we must reset the cache before processing `mkAuxMVarType` because `toRevert` may not be equal to `xs` let newMVarId := { name := (← get).ngen.curr } + modify fun s => { s with ngen := s.ngen.next } let newMVar := mkMVar newMVarId let result := mkMVarApp mvarLCtx newMVar toRevert newMVarKind let newMVarType ← withReader (fun ctx => { ctx with mvarIdsInProgress := ctx.mvarIdsInProgress.cons mvarId result }) do withFreshCache do mkAuxMVarType mvarLCtx toRevert newMVarKind mvarDecl.type let numScopeArgs := mvarDecl.numScopeArgs + result.getAppNumArgs modify fun s => { s with - mctx := s.mctx.addExprMVarDecl newMVarId Name.anonymous newMVarLCtx newLocalInsts newMVarType newMVarKind numScopeArgs, - ngen := s.ngen.next - } + mctx := s.mctx.addExprMVarDecl newMVarId Name.anonymous newMVarLCtx newLocalInsts newMVarType newMVarKind numScopeArgs } if !mvarDecl.kind.isSyntheticOpaque then mvarId.assign result else From 1cf08e89837493cb98bfea61d92ac429c229f161 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Fri, 15 Nov 2024 13:47:57 +0000 Subject: [PATCH 3/4] add test and cleanup --- src/Lean/MetavarContext.lean | 67 +++++++++++++++++++------------ tests/lean/run/6013.lean | 77 ++++++++++++++++++++++++++++++++++++ 2 files changed, 119 insertions(+), 25 deletions(-) create mode 100644 tests/lean/run/6013.lean diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 95e3924adf2a..f73fd1fe3f55 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -910,9 +910,14 @@ structure Context where binderInfoForMVars : BinderInfo := BinderInfo.implicit /-- Set of unassigned metavariables being abstracted. -/ mvarIdsToAbstract : MVarIdSet := {} - /-- Map of metavariable assignments that haven't yet been added to the context. + /-- + Map of metavariable assignments that haven't yet been added to the metavariable context. This is necessary to deal with metavariables that contain themselves in their own type. - Without this, such a situation would lead to infinite recursion. -/ + Without this, such a situation would lead to infinite recursion. (see #6013 and #3150) + + We claim it is not necessary to run `elim` on this cached value again, because the + dependencies on the free variables are already eliminated. This stops the infinite recursion. + -/ mvarIdsInProgress : AssocList MVarId Expr := {} abbrev MCore := EStateM Exception State @@ -945,7 +950,7 @@ private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr) /-- Given `toRevert` an array of free variables s.t. `lctx` contains their declarations, - return a new array of free variables that contains `toRevert` and all free variables + return a new array of free variables that contains `toRevert` and all variables in `lctx` that may depend on `toRevert`. Remark: the result is sorted by `LocalDecl` indices. @@ -1009,7 +1014,7 @@ def collectForwardDeps (lctx : LocalContext) (toRevert : Array Expr) : M (Array We use this function when we create auxiliary metavariables at `elimMVarDepsAux`. -/ def reduceLocalContext (lctx : LocalContext) (toRevert : Array Expr) : LocalContext := toRevert.foldr (init := lctx) fun x lctx => - lctx.erase x.fvarId! + if x.isFVar then lctx.erase x.fvarId! else lctx /-- Return free variables in `xs` that are in the local context `lctx` -/ private def getInScope (lctx : LocalContext) (xs : Array Expr) : Array Expr := @@ -1034,9 +1039,12 @@ private def getInScope (lctx : LocalContext) (xs : Array Expr) : Array Expr := how let-decl free variables are handled. -/ private def mkMVarApp (lctx : LocalContext) (mvar : Expr) (xs : Array Expr) (kind : MetavarKind) : Expr := xs.foldl (init := mvar) fun e x => - match kind with - | MetavarKind.syntheticOpaque => mkApp e x - | _ => if (lctx.getFVar! x).isLet then e else mkApp e x + if !x.isFVar then + e + else + match kind with + | MetavarKind.syntheticOpaque => mkApp e x + | _ => if (lctx.getFVar! x).isLet then e else mkApp e x mutual @@ -1055,7 +1063,7 @@ mutual | e => return e /-- - Given a metavariable with type `e`, kind `kind` and free variables `xs` in its local context `lctx`, + Given a metavariable with type `e`, kind `kind` and free/meta variables `xs` in its local context `lctx`, create the type for a new auxiliary metavariable. These auxiliary metavariables are created by `elimMVar`. See "Gruesome details" section in the beginning of the file. @@ -1066,22 +1074,30 @@ mutual let e ← abstractRangeAux xs xs.size e xs.size.foldRevM (init := e) fun i e => do let x := xs[i]! - match lctx.getFVar! x with - | LocalDecl.cdecl _ _ n type bi _ => - let type := type.headBeta + if x.isFVar then + match lctx.getFVar! x with + | LocalDecl.cdecl _ _ n type bi _ => + let type := type.headBeta + let type ← abstractRangeAux xs i type + return Lean.mkForall n bi type e + | LocalDecl.ldecl _ _ n type value nonDep _ => + let type := type.headBeta + let type ← abstractRangeAux xs i type + let value ← abstractRangeAux xs i value + let e := mkLet n type value e nonDep + match kind with + | MetavarKind.syntheticOpaque => + -- See "Gruesome details" section in the beginning of the file + let e := e.liftLooseBVars 0 1 + return mkForall n BinderInfo.default type e + | _ => pure e + else + -- `xs` may contain metavariables as "may dependencies" (see `findExprDependsOn`) + let mvarDecl := (← get).mctx.getDecl x.mvarId! + let type := mvarDecl.type.headBeta let type ← abstractRangeAux xs i type - return Lean.mkForall n bi type e - | LocalDecl.ldecl _ _ n type value nonDep _ => - let type := type.headBeta - let type ← abstractRangeAux xs i type - let value ← abstractRangeAux xs i value - let e := mkLet n type value e nonDep - match kind with - | MetavarKind.syntheticOpaque => - -- See "Gruesome details" section in the beginning of the file - let e := e.liftLooseBVars 0 1 - return mkForall n BinderInfo.default type e - | _ => pure e + let id ← if mvarDecl.userName.isAnonymous then mkFreshBinderName else pure mvarDecl.userName + return Lean.mkForall id (← read).binderInfoForMVars type e where abstractRangeAux (xs : Array Expr) (i : Nat) (e : Expr) : M Expr := do let e ← elim xs e @@ -1116,7 +1132,8 @@ mutual let newMVarKind := if !(← mvarId.isAssignable) then MetavarKind.syntheticOpaque else mvarDecl.kind let args ← args.mapM (visit xs) -- Note that `toRevert` only contains free variables at this point since it is the result of `getInScope`; - -- after `collectForwardDeps`, this is still the case. + -- after `collectForwardDeps`, this may no longer be the case because it may include metavariables + -- whose local contexts depend on `toRevert` (i.e. "may dependencies") let toRevert ← collectForwardDeps mvarLCtx toRevert let newMVarLCtx := reduceLocalContext mvarLCtx toRevert let newLocalInsts := mvarDecl.localInstances.filter fun inst => toRevert.all fun x => inst.fvar != x @@ -1125,7 +1142,7 @@ mutual modify fun s => { s with ngen := s.ngen.next } let newMVar := mkMVar newMVarId let result := mkMVarApp mvarLCtx newMVar toRevert newMVarKind - let newMVarType ← withReader (fun ctx => { ctx with mvarIdsInProgress := ctx.mvarIdsInProgress.cons mvarId result }) do + let newMVarType ← withReader (fun ctx => { ctx with mvarIdsInProgress := ctx.mvarIdsInProgress.insert mvarId result }) do withFreshCache do mkAuxMVarType mvarLCtx toRevert newMVarKind mvarDecl.type let numScopeArgs := mvarDecl.numScopeArgs + result.getAppNumArgs modify fun s => { s with diff --git a/tests/lean/run/6013.lean b/tests/lean/run/6013.lean new file mode 100644 index 000000000000..62769d54097c --- /dev/null +++ b/tests/lean/run/6013.lean @@ -0,0 +1,77 @@ + +/-- +error: failed to synthesize + OfNat (String → String) 10 +numerals are polymorphic in Lean, but the numeral `10` cannot be used in a context where the expected type is + String → String +due to the absence of the instance above +Additional diagnostic information may be available using the `set_option diagnostics true` command. +-/ +#guard_msgs in +example (a : String) : String := + let x : String → String := _ + have : x = 10 := by rfl + "tested" + + + + +structure A where + α : Type + a : α + +structure B (f : (α : Type) → α → α) extends A where + b : α + a := f α b + +/-- +error: don't know how to synthesize placeholder +context: +⊢ { α := Nat, a := id ?_ }.α +-/ +#guard_msgs in +example : B @id where + α := Nat + b := _ + + + + +class One (α : Type) where + one : α + +variable (R A : Type) [One R] [One A] + +class OneHom where + toFun : R → A + map_one : toFun One.one = One.one + +structure Subone where + mem : R → Prop + one_mem : mem One.one + +structure Subalgebra [OneHom R A] extends Subone A : Type where + algebraMap_mem : ∀ r : R, mem (OneHom.toFun r) + one_mem := OneHom.map_one (R := R) (A := A) ▸ algebraMap_mem One.one + +/-- +error: don't know how to synthesize placeholder +context: +R A : Type +inst✝² : One R +inst✝¹ : One A +inst✝ : OneHom R A +⊢ ∀ (r : R), { mem := ?_ R A _example, one_mem := ⋯ }.mem (OneHom.toFun r) +--- +error: don't know how to synthesize placeholder +context: +R A : Type +inst✝² : One R +inst✝¹ : One A +inst✝ : OneHom R A +⊢ A → Prop +-/ +#guard_msgs in +example [OneHom R A] : Subalgebra R A where + mem := _ + algebraMap_mem := _ From b7bd6ad0506f45bbe399787b5177af61256f6200 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Fri, 15 Nov 2024 14:08:12 +0000 Subject: [PATCH 4/4] . --- tests/lean/run/6013.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/lean/run/6013.lean b/tests/lean/run/6013.lean index 62769d54097c..7af76019b129 100644 --- a/tests/lean/run/6013.lean +++ b/tests/lean/run/6013.lean @@ -27,7 +27,7 @@ structure B (f : (α : Type) → α → α) extends A where /-- error: don't know how to synthesize placeholder context: -⊢ { α := Nat, a := id ?_ }.α +⊢ { α := Nat, a := id ?m }.α -/ #guard_msgs in example : B @id where @@ -61,7 +61,7 @@ R A : Type inst✝² : One R inst✝¹ : One A inst✝ : OneHom R A -⊢ ∀ (r : R), { mem := ?_ R A _example, one_mem := ⋯ }.mem (OneHom.toFun r) +⊢ ∀ (r : R), { mem := ?m R A _example, one_mem := ⋯ }.mem (OneHom.toFun r) --- error: don't know how to synthesize placeholder context: