10000 Internal error in generate-helper (C-c C-h) · Issue #7105 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Internal error in generate-helper (C-c C-h) #7105

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
andreasabel opened this issue Feb 11, 2024 · 1 comment
Closed

Internal error in generate-helper (C-c C-h) #7105

andreasabel opened this issue Feb 11, 2024 · 1 comment
Labels
internal-error Concerning internal errors of Agda regression in 2.6.4 Regression that first surfaced in Agda 2.6.4 ux: generate helper Generation of helper function type signatures (C-c C-h) ux: interaction Issues to do with interactive development (holes, case splitting, etc)
Milestone
2.6.4.2

Comments

@andreasabel
Copy link
Member

Generated-helper under a pattern-let generates an internal error:

open import Agda.Primitive renaming (Set to Type)
open import Agda.Builtin.Sigma

postulate
  ℕ : Type

data T (n : ℕ) : Type where
  conv : ∀ m → T m → T n

test : ∀ n → T n → Σ ℕ T
test n (conv m t) = let n' , t' = test m t in {!helper t'!}  -- C-c C-h

-- An internal error has occurred. Please report this as a bug.
-- Location of the error: impossible, called at src/full/Agda/Interaction/BasicOps.hs:980:49

Error location is pointing to this impossible:

agda/src/full/Agda/Interaction/BasicOps.hs

Lines 977 to 980 in 2816d75

-- Konstantin, 2022-10-23: We don't want to print section parameters in helper type.
freeVars <- getCurrentModuleFreeVars
contextForAbstracting <- drop freeVars . reverse <$> getContext
let escapeAbstractedContext = escapeContext impossible (length contextForAbstracting)

CC @knisht
@andreasabel andreasabel added ux: generate helper Generation of helper function type signatures (C-c C-h) ux: interaction Issues to do with interactive development (holes, case splitting, etc) internal-error Concerning internal errors of Agda regression in 2.6.4 Regression that first surfaced in Agda 2.6.4 labels Feb 11, 2024
@andreasabel andreasabel added this to the 2.6.4.2 milestone Feb 11, 2024
knisht added a commit that referenced this issue Feb 11, 2024
@knisht
#7105 Do not try to fold let-bindings during printing of the helper f…
8000
d626bfc 
…unction
andreasabel pushed a commit that referenced this issue Feb 14, 2024
@knisht @andreasabel
#7105 Do not try to fold let-bindings during printing of the helper f…
c0ceac7 
…unction
@andreasabel
Copy link
Member Author

Fixed by #7106.

andreasabel pushed a commit that referenced this issue Feb 16, 2024
@knisht @andreasabel
#7105 Do not try to fold let-bindings during printing of the helper f…
009626b 
…unction
@andreasabel andreasabel mentioned this issue Feb 17, 2024
Closed
3 tasks
VitalyAnkh pushed a commit to VitalyAnkh/agda that referenced this issue Mar 5, 2024
@knisht @VitalyAnkh
agda#7105 Do not try to fold let-bindings during printing of the help…
b55f879 
…er function
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 12, 2024
@knisht @JobPetrovcic
agda#7105 Do not try to fold let-bindings during printing of the help…
7efa893 
…er function
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
internal-error Concerning internal errors of Agda regression in 2.6.4 Regression that first surfaced in Agda 2.6.4 ux: generate helper Generation of helper function type signatures (C-c C-h) ux: interaction Issues to do with interactive development (holes, case splitting, etc)
Projects
None yet
Milestone
2.6.4.2
Development

No branches or pull requests
1 participant
@andreasabel
0