Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[ fix ] Ensure local defs with no claim are local #3017

Merged
merged 2 commits into from
Jul 18, 2023

Conversation

dunhamsteve
Copy link
Contributor

Description

PR #1952 introduced top level aliases - definitions without a type declaration. This had a number of side effects, including local function names being exposed at top level and strange type errors for local function definitions without type declarations.

It turns out that the root cause was the function names not being added to nested. This PR addresses that by looking at IDef in addition to IClaim when determining the list of locally defined names. It fixes #2782, #2592, and #2593, which are included in the test case. It also addresses a case raised on discord.

I believe it addresses #3016, but note that, as with top level declarations, the definitions have to have simple bind variables on the LHS. (A constraint imposed by the #1952 code.)

src/TTImp/TTImp.idr Outdated Show resolved Hide resolved
@andrevidela andrevidela merged commit 6be16a3 into idris-lang:main Jul 18, 2023
20 checks passed
@dunhamsteve dunhamsteve deleted the issue-3016 branch July 18, 2023 14:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

let parameters within a function specified in a certain way leak into main
3 participants