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

Internal error related to abstract and variable #4006

Closed
nad opened this issue Aug 19, 2019 · 1 comment · Fixed by #4248
Closed

Internal error related to abstract and variable #4006

nad opened this issue Aug 19, 2019 · 1 comment · Fixed by #4248
Labels
abstract Issues relating to abstract blocks generalize Related to generalisable variables type: bug Issues and pull requests about actual bugs
Milestone
2.6.1

Comments

@nad
Copy link
Contributor

nad commented Aug 19, 2019

The following code is rejected:

module Bug where

data I : Set where
  i : I

variable
  x : I

abstract

  data D : I → Set where
    d : D i

  accepted : {x : I} → D x → Set₁
  accepted {x = i} d = Set

  rejected : D x → Set₁
  rejected {x = i} d = Set

Error message:

Not in scope:
  Bug.D.d at […]/Bug.agda:12,5-6
    (did you mean
       'D' or
       'd'?)
@nad nad added type: bug Issues and pull requests about actual bugs abstract Issues relating to abstract blocks generalize Related to generalisable variables labels Aug 19, 2019
@nad nad added this to the 2.6.1 milestone Aug 19, 2019
@nad
Copy link
Contributor Author

nad commented Nov 2, 2019

Now the code triggers an internal error (also if {x = i} is removed):

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Monad/Signature.hs:662

@nad nad changed the title Bug related to abstract and variable Internal error related to abstract and variable Nov 2, 2019
UlfNorell added a commit that referenced this issue Nov 28, 2019
@UlfNorell
[ fix #4006 ] ignore abstract when translating compiled clauses
1e820c1 
so that we don't crash if the function matches on "abstract" (i.e. not-in-scope)
constructors
UlfNorell added a commit that referenced this issue Nov 28, 2019
@UlfNorell
[ fix #4006 ] ignore abstract when translating compiled clauses
7c3b7a0 
so that we don't crash if the function matches on "abstract" (i.e. not-in-scope)
constructors
@UlfNorell UlfNorell mentioned this issue Nov 28, 2019
Merged
UlfNorell added a commit that referenced this issue Nov 28, 2019
@UlfNorell
[ fix #4006 ] ignore abstract when translating compiled clauses
dee9171 
so that we don't crash if the function matches on "abstract" (i.e. not-in-scope)
constructors
L-TChen pushed a commit that referenced this issue Dec 2, 2019
@UlfNorell @L-TChen
[ fix #4006 ] ignore abstract when translating compiled clauses
3647109 
so that we don't crash if the function matches on "abstract" (i.e. not-in-scope)
constructors
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
abstract Issues relating to abstract blocks generalize Related to generalisable variables type: bug Issues and pull requests about actual bugs
Projects
None yet
Milestone
2.6.1
Development

Successfully merging a pull request may close this issue.

[ fix #4006 ] ignore abstract when translating compiled clauses agda/agda
1 participant
@nad