stack overflow during elaboration

[JovanGerb]

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
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• 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 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[Kha]

A quick dbg_trace suggests a loop between the mvars for _ and OfNat 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]

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]

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]

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)

lean4/src/Lean/MetavarContext.lean

Line 1078 in 9f42368

let e := mkLet n type value e nonDep

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