stack overflow during elaboration

JovanGerb commented 1 week ago

Prerequisites

Please put an X between the brackets as you perform the following steps:

[ ] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
[x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
[x] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

Elaborating the following code causes a stack overflow:

def test (a : String) : String :=
  let x : String → String := _
  have : x = 10 := by rfl

Context

I found this by accident

Steps to Reproduce

write the above function

Expected behavior: Elaboration fails. And if we extend the example to

def test (a : String) : String :=
  let x : String → String := _
  have : x = 10 := by rfl
  "tested"

it should complain about

failed to synthesize
  OfNat (String → String) 10`

Actual behavior:

A stack overflow happens, crashing the lean server

Versions

The bug is present from 4.9.0 until now, 4.14.0-rc2 It was introduced in lean#3940, commit 97a7d4234bd76bc0f61e43b8c6a78117c1376df

Additional Information

From the stack trace we can see the source of the infinite recursion. It is a mutual block in MetavarContext.lean, and has the following pattern of function calls appearing repeatedly:

mkAuxMVarType.abstractRangeAux
mkAuxMVarType
elimMVar
elimApp
visit
Array.mapMUnsafe.map._at._private.src.Lean.MetavarContext.0.Lean.MetavarContext.MkBinding.elimApp._spec_6
elimApp
visit
elimApp
visit
elim

(the top of the list corresponds to the top of the stack, so each function calls the one above it)

This infinite loop is reached via a call to mkLambdaFVars, which calls mkBinding. In particular this call in elabFunValues in MutualDef.lean. So I think the particular lambda that is trying to be created is

fun a : String =>
  let x : String → String := _
  have : x = 10 := by rfl

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

Kha commented 1 week ago

A quick dbgtrace suggests a loop between the mvars for `andOfNat Nat 10`

elim ?_uniq.31
elim let x : String -> String := ?_uniq.9; OfNat.{?_uniq.16} (String -> String) 10
elim ?_uniq.9
elim OfNat.ofNat.{0} (String -> String) 10 ?_uniq.31

JovanGerb commented 1 week ago

I have found out what causes the problem. It is a subtle violation of the occurs check. Consider

set_option trace.Meta.isDefEq.assign true

def test :=
  let x : String → String := _
  have : x = 10 := by rfl

We can see the assignment

[Meta.isDefEq.assign] ✅️ ?m.7 := @OfNat.ofNat (String → String) 10 ?m.29

and hovering over ?m.29 shows that

?m.29 : let x := ?m.7;
  OfNat (String → String) 10

So ?m.7 appears in the type of the new assignment.

Such a problem would usually be caught by the function typeOccursCheck. However, it applies skipAtMostNumBinders type 0 to the type of the metavariable, which causes the let x := ?m.7; to be instantiated, so this check doesn't manage to find ?m.7.

JovanGerb commented 1 week ago

I don't think this is a problem with the implementation of typeOccursCheck. Instead, the elim that is called by mkLambdaFVars should probably do a reduction similar to that of skipAtMostNumBinders, taking into account the kinds of occurs check failures that can appear.

JovanGerb commented 6 days ago

A somewhat easier way to fix this problem is at the place where the let-expression is created, to make it so that the let expression isn't created if the bound variable doesn't appear in the body. (similar to how mkBinding is usually used with usedLetOnly := true)

https://github.com/leanprover/lean4/blob/9f42368e1ae749ae122bfb44e2f082e6cc3ba604/src/Lean/MetavarContext.lean#L1078

However, I'm not sure if that fixes the underlying problem.

leanprover / lean4