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.

Sign up for GitHub

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

Jump to bottom

Architectural problem: unhygienic import handling, lack of sandboxing #4272

Open
andreasabel opened this issue Dec 8, 2019 · 0 comments
Open

Architectural problem: unhygienic import handling, lack of sandboxing #4272

andreasabel opened this issue Dec 8, 2019 · 0 comments
Labels
import Issues to do with importing modules type: task Concerning the development of Agda (not in changelog)
Milestone
later

Comments

@andreasabel
Copy link
Member

andreasabel commented Dec 8, 2019 •
edited

This issue points out a general problem in way Agda handles imports:
The state accumulates the signatures of imported modules in a component stImports : Signature. This way information from previous imports may leak into the type checking process of later imports.

Instead, when checking

import A
import B

the checking of module B should happen in a sandbox such that information from A cannot flow accidentially into B.

Issue(s) caused by this architectural problem:
@andreasabel andreasabel added import Issues to do with importing modules type: task Concerning the development of Agda (not in changelog) labels Dec 8, 2019
@andreasabel andreasabel added this to the 2.6.2 milestone Dec 8, 2019
andreasabel added a commit that referenced this issue Dec 8, 2019
@andreasabel
[ fixed #4267 ] record expressions need the record type in scope
36d1a81 
It might be a sensible restriction that the type of

  record { fields = exprs }

can only be inferred if it could be written as well, i.e., if the record
type is in scope.

This fixes #4267; but the root cause of #4267 is the unhygienic import
handling of Agda, see #4272.
@andreasabel andreasabel mentioned this issue Dec 8, 2019
Closed
andreasabel added a commit that referenced this issue Dec 9, 2019
@andreasabel
[ fixed #4267 ] record expressions need the record type "in scope"
f83832c 
This fixes #4267; but the root cause of #4267 is the unhygienic import
handling of Agda, see #4272.

The fix filter possible candidates for (record) types of a record
expression by Agda.Syntax.Scope.Base.isNameInScope.

It is not entirely clear what this check entails (this function is
entirely undocumented); for instance, it does not entail that the name
that Agda infers for the record type could actually be written by the
user (see test case Issue4267a).

However, it seems to do the job to fix the present bug (test case
Issue4267 passes now without unsolved metas).
@nad nad mentioned this issue Dec 19, 2019
Closed
@sattlerc sattlerc mentioned this issue Dec 30, 2019
Closed
sattlerc added a commit that referenced this issue Dec 30, 2019
@sattlerc
[ re #4333 ] Add missing test case.
dbe9919 
Test case is in test/interaction because of #4272.
@sattlerc sattlerc mentioned this issue Dec 30, 2019
Open
@nad nad mentioned this issue Apr 27, 2020
Closed
@andreasabel andreasabel mentioned this issue Jun 3, 2020
Open
@UlfNorell UlfNorell modified the milestones: 2.6.2, 2.6.3 Feb 9, 2021
@jespercockx jespercockx modified the milestones: 2.6.3, Later Aug 26, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
import Issues to do with importing modules type: task Concerning the development of Agda (not in changelog)
Projects
None yet
Milestone
later
Development

No branches or pull requests
3 participants
@UlfNorell @andreasabel @jespercockx