Skip to content

use withAll when evaluating %foreign strings#3801

Open
ear7h wants to merge 1 commit into
idris-lang:mainfrom
ear7h:issue-3790-fix-foreign-string
Open

use withAll when evaluating %foreign strings#3801
ear7h wants to merge 1 commit into
idris-lang:mainfrom
ear7h:issue-3790-fix-foreign-string

Conversation

@ear7h

@ear7h ear7h commented Jun 17, 2026

Copy link
Copy Markdown
Contributor

Description

The compiler was getting stuck when normalizing %foreign and %foreign_impl resulting in Error: %foreign calling convention must evaluate to a String. This was caused by getFnString using nf instead of nfOpts withAll which evaluates private names. This change reflects (heh) what's implemented in runElab:

nfstm <- nfOpts withAll defs env stm

nfOpts withAll defs env !(reflect fc defs False env tm)

Self-check

  • This is my first time contributing, I've carefully read CONTRIBUTING.md
    and I've updated CONTRIBUTORS with my name.
  • If this is a fix, user-facing change, a compiler change, or a new paper
    implementation, I have updated CHANGELOG_NEXT.md
  • I confirm that this contribution did not involve GenerativeAI nor Large Language Models.

@ear7h
ear7h force-pushed the issue-3790-fix-foreign-string branch from ec5dd82 to d146260 Compare June 17, 2026 15:04
closes idris-lang#3790

Also adds some more details to the error messages when the expression
evaluates to smething unexpected.
@ear7h
ear7h force-pushed the issue-3790-fix-foreign-string branch from d146260 to 849111c Compare June 17, 2026 15:05
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.

1 participant