8000 Internal error related to generalisable variables · Issue #3655 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Internal error related to generalisable variables #3655

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
Closed
nad opened this issue Mar 29, 2019 · 2 comments · Fixed by #3681
Closed

Internal error related to generalisable variables #3655

nad opened this issue Mar 29, 2019 · 2 comments · Fixed by #3681
Labels
generalize Related to generalisable variables not-in-changelog This issue should not be listed in the changelog. type: bug Issues and pull requests about actual bugs
Milestone
2.6.0

Comments

@nad
Copy link
Contributor
nad commented Mar 29, 2019

With Agda 2.6.0-29a2758:

open import Agda.Primitive

postulate
  F : (a : Level) → Set a → Set a
  P : (a : Level) (A : Set a) → F a A → Set a
  p : (a : Level) (A : Set a) (x : F a A) → P a A x
  Q : (a : Level) (A : Set a) → A → Set a

variable
  a : Level
  A : Set a

postulate
  q : (x : F _ A) → Q a _ (p a A x)
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs:97

If I replace the final underscore with a hole and try to give P _ _ x, then I get the following error message:

(Set "dummyTerm: src/full/Agda/TypeChecking/Generalize.hs:399") is
not less or equal than (Set a)
when checking that the expression P _ _ x has type Set a
@nad nad added type: bug Issues and pull requests about actual bugs generalize Related to generalisable variables labels Mar 29, 2019
@nad nad added this to the 2.6.0 milestone Mar 29, 2019
@asr asr added the not-in-changelog This issue should not be listed in the changelog. label Mar 29, 2019
@asr
Copy link
Member
asr commented Mar 29, 2019

Since that generalisable variables is a feature not released, the closed issues with label generalize and milestone 2.6.0 should have the not-in-changelog label. I'll also add this label to the other issues.

@UlfNorell UlfNorell mentioned this issue Mar 30, 2019
Merged
UlfNorell added a commit that referenced this issue Mar 30, 2019
@UlfNorell
Merge pull request #3664 from agda/issue3655
c242ca0 
Fix for #3655
@nad
Copy link
Contributor Author
nad commented Apr 1, 2019

I can still trigger this internal error:

open import Agda.Builtin.Bool

postulate
  A : Set

F : Bool → Set
F true  = A
F false = A

data D {b : Bool} (x : F b) : Set where

variable
  b : Bool
  x : F b

postulate
  f : D x → (P : F b → Set) → P x

The inferred type of f:

{x : F "dummyTerm: src/full/Agda/TypeChecking/Generalize.hs:416"}
{b : Bool} →
D x → (P : F b → Set) → P x

@nad nad reopened this Apr 1, 2019
UlfNorell added a commit that referenced this issue Apr 3, 2019
@UlfNorell
[ fix #3672 ] prune unsolved metas that are not generalized over
63f3278 
also fixes #3655 and fixes #3673 which are the same issue
UlfNorell added a commit that referenced this issue Apr 3, 2019
@UlfNorell
[ fix #3672 ] prune unsolved metas that are not generalized over
87b26ca 
also fixes #3655 and fixes #3673 which are the same issue
UlfNorell added a commit that referenced this issue Apr 4, 2019
@UlfNorell
[ fix #3672 ] prune unsolved metas that are not generalized over
6b4af08 
Previously we only eta expanded the generalized variable record in the metas (#3340),
but we need to also repect dependencies.

Also fixes #3655 (again) and fixes #3673 both of which are this same issue.
This was referenced Apr 4, 2019
Merged
Closed
andreasabel added a commit that referenced this issue Sep 10, 2024
@andreasabel
Test #3655: remove stray "I" from generalization error message
b385869
andreasabel added a commit that referenced this issue Sep 10, 2024
@andreasabel
Test #3655: remove stray "I" from generalization error message
47908a3
andreasabel added a commit that referenced this issue Sep 10, 2024
@andreasabel
Test #3655: remove stray "I" from generalization error message
28812b7
fredins pushed a commit to fredins/agda that referenced this issue Nov 24, 2024
@andreasabel @fredins
Test agda#3655: remove stray "I" from generalization error message
24c7dee
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
generalize Related to generalisable variables not-in-changelog This issue should not be listed in the changelog. type: bug Issues and pull requests about actual bugs
Projects
None yet
Milestone
2.6.0
Development

Successfully merging a pull request may close this issue.

Fix 3672: prune unsolved metas that are not generalized over agda/agda
2 participants
@nad @asr
0