facebook / facebook/pyrefly

Incremental comment-only edit drops recursive non-convergence warning

Open
#4,216 2 comments 0 reactions 1 assignee Claimed by @teerthsharma View on GitHub
language-server
Dominant language
Rust
Stars
7k
Forks
519
PR merge metrics
No merged PRs in 30d

Description

## Summary

A comment-only edit to one member of a two-module recursive binding cycle can make an incremental check lose a `non-convergent-recursion` warning that a fresh check emits for the byte-identical final sources.

I found this while prototyping a local type-checking workflow for a small DSL and stress-testing incremental behavior. I reduced it to the synthetic two-module case below; the DSL itself is not involved in the reproducer.

This minimized cycle still fails on both proposed scheduler fixes, although the observable failures differ:

- On @kinto0's #4188 (`00ad074b6`), the transaction completes but the incremental check loses the warning described below.
- On the earlier head of my #4190 (`5c7ccaf6a`), the same one-worker regression panics with `Transaction has uncommitted changes` before reaching the warm/cold diagnostic comparison.

The current #4190 head (`9ae92ac1b`) contains the proposed fix: mutable-cycle detection now uses the same dependency-first SCC stabilization as the epoch-cap fallback. On that commit, the transaction completes and the warm and cold checks both report exactly one `non-convergent-recursion` warning. #4188 still exposes the diagnostic-loss behavior described below. On current `main`, the older capped-propagation failure occurs first.

## Reproducer

Initial sources:

```python
# m_0.py
from m_1 import f as f_1
f = (0, f_1)
```

```python
# m_1.py
from m_0 import f as f_0
f = (1, f_0)
```

Using one worker:

1. Check the initial sources while demanding only `m_0`.
2. Append `# topology control` to `m_0.py`; do not change `m_1.py`.
3. Incrementally recheck `m_0`.
4. Create a fresh state and check the exact same final source vector.

The test asserts that the warm and cold final sources are byte-for-byte equal.

## Actual result

The incremental result has no diagnostics:

```text
[]
```

The fresh result has one warning at the `m_0` import:

```text
Warn: non-convergent-recursion: Fixpoint iteration did not converge ...
```

The one-worker comment-only case reproduced 5/5. With the default three workers it reproduced 4/5, so the proposed regression test fixes the worker count at one.

## Expected result

For byte-identical final sources and the same demanded module:

```text
diagnostics(incremental(final_sources)) == diagnostics(cold(final_sources))
```

## Controls

- Removing either recursive edge restores warm/cold equality (3/3).
- Adding explicit `object` annotations restores equality (3/3).
- Two independent cold checks produce the same one warning (3/3).
- Comment-editing and rebuilding both modules restores equality with the warning present.

## Root-cause hypothesis

The evidence suggests cached-answer/error-collector asymmetry. The edit rebuilds `m_0` with a fresh error collector, while unchanged `m_1` retains a cached answer. The cached cross-module lookup can bypass SCC fixpoint iteration, so the solver-side warning is neither regenerated nor replayed into the rebuilt module's collector. Rebuilding both SCC members restores the warning, which supports this hypothesis.

## Interface scope

A cold CLI check with `--threads 1` emits the warning. In a synchronized root-only LSP experiment, both warm and cold runs omitted it, so I am not claiming an LSP warm-vs-cold mismatch here. The demonstrated invariant violation is in the incremental transaction/test path versus a fresh check.

I searched for a duplicate. #2783 appears performance-only; #4171/#4180 cover the preceding propagation panic rather than this diagnostic-loss behavior. The comparison above documents how the minimized case behaves on both #4188 and #4190.

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.