Deep recursion was detected at 'replace'

[stop-cran]

Prerequisites

Lean 3.4.1 for Windows (githash: 17fe3decaf8ae236f0d0ff51ac8fd7f6940acdee). Also reproducible in the web editor.

Description

I played around with simple dependent type examples. However, following expression has failed to reduce:

def calc_type : bool → Type
| ff := ℕ
| tt := char

def calc_str : Π (b : bool), calc_type b → string
| ff := λ (n : ℕ), "nat"
| tt := λ (c : char), "char"

#check calc_str ff           -- success: calc_str ff : calc_type ff → string
#eval (calc_str ff) nat.zero -- success: "nat"
#reduce calc_type ff         -- success: ℕ
#reduce calc_str ff          -- hangs

The error message shown by executing lean.exe src\main.lean (the web editor hangs silently):

...\lean\src\main.lean:12:0: error: deep recursion was detected at 'replace' (potential solution: increase stack space in your system)

Also I would expect the type of calc_str ff to be reduced ℕ → string, but I'm not sure if #check should do it. Anyway, #reduce calc_type ff → string yields ℕ → string_imp.

[digama0]

This is not a bug, this is lean running out of memory / stack space because you tried to #reduce a complicated definition. #eval often works better, but here you aren't evaluating the function. #reduce is computationally intensive here because it has to reduce "nat". Even #reduce 'n' overflows, because the char contains a proof that the natural number is less than 1114112, and that has to be unfolded to a million nat.succ's.

A possible point of confusion: #reduce calc_str ff does not calculate the type of calc_str ff, it calculates the value, which means reducing the lambda to a normal form (i.e. symbolically evaluating the function). To reduce the type of calc_str ff, you can #check it as you did to get the manifest type calc_type ff → string, and then #reduce that to get ℕ → string_imp as you (may or may not) expect.

[x13pixels]

FWIW, I'm seeing the same thing with this "complicated" definition:

theorem theorem1 : "Hello World" = "Hello " ++ "World" := rfl
#reduce theorem1

[digama0]

@x13pixels It's the same issue. You should basically never expect #reduce on anything about strings to work. Even the very simplest example, #reduce 'a', still has to perform an amount of computation proportional to the number of unicode characters that exist. #reduce theorem1 is about 11 times as much computation as that.