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

__IMPOSSIBLE__ when tactic is used on record fields that are functions #5712

Closed
Trebor-Huang opened this issue Dec 28, 2021 · 3 comments · Fixed by #5717
Closed

__IMPOSSIBLE__ when tactic is used on record fields that are functions #5712

Trebor-Huang opened this issue Dec 28, 2021 · 3 comments · Fixed by #5717
Assignees
@andreasabel
Labels
coverage Pattern-matching coverage checker internal-error Concerning internal errors of Agda regression in 2.6.1 Regression that first appeared in Agda 2.6.1 tactic tactic annotations
Milestone
2.6.2.2

Comments

@Trebor-Huang
Copy link

Trebor-Huang commented Dec 28, 2021 •
edited
Loading

MWE:

open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit
module MWE where

nothing : Term -> TC ⊤
nothing hole = returnTC _

record Foo : Set1 where
    field
        A : Set
        @(tactic nothing) foo : A -> A

F : Foo
Foo.A F = ⊤
Foo.foo F n = _

This produces:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Coverage.hs:521:22 in Agd-2.6.2.1-2f8a192b:Agda.TypeChecking.Coverage

It only occurs when foo is a function, and the definition of F includes that field. (When the last line in the code is left out, it runs fine because Agda can infer a value of ⊤ even when the tactic is doing nothing.)
@andreasabel
Copy link
Member

This passes without error on 2.6.1. Running bisect:

agda-bisect --good v2.6.1 --bad v2.6.2 -w ghc-8.8.4 --with-cabal=cabal-3.4 Issue5712.agda

@andreasabel
Copy link
Member

andreasabel commented Dec 29, 2021 •
edited
Loading

Error here:

agda/src/full/Agda/TypeChecking/Coverage.hs

Line 480 in 9428b1d

| finalSplit = __IMPOSSIBLE__ -- already ruled out by lhs checker

This is a regression in 2.6.2 introduced by me by the fix of #5358:
0cdd208 is the first bad commit
Date: Fri May 7 21:51:20 2021 +0200
[ fixed #5358 ] don't expand clauses with tactics attached to them

@andreasabel andreasabel added regression in 2.6.1 Regression that first appeared in Agda 2.6.1 coverage Pattern-matching coverage checker tactic tactic annotations labels Dec 29, 2021
andreasabel added a commit that referenced this issue Dec 31, 2021
@andreasabel
Fix #5712: coverage: trailing args inserting in presence of domTactic
dfefbea 
Fix of #5358 prevented trailing arg insertion in the coverage checker
if there was a tactic (at function type).  However, in the presence of
a user written arg, the insertion should not be prevented.
@andreasabel andreasabel mentioned this issue Dec 31, 2021
Merged
@andreasabel andreasabel self-assigned this Dec 31, 2021
@andreasabel andreasabel added this to the 2.6.3 milestone Dec 31, 2021
@andreasabel andreasabel added the internal-error Concerning internal errors of Agda label Dec 31, 2021
@jespercockx jespercockx mentioned this issue Jan 3, 2022
Open
andreasabel added a commit that referenced this issue Jan 3, 2022
@andreasabel
Fix #5712: coverage: trailing args inserting in presence of domTactic
ec80338 
Fix of #5358 prevented trailing arg insertion in the coverage checker
if there was a tactic (at function type).  However, in the presence of
a user written arg, the insertion should not be prevented.
@andreasabel andreasabel mentioned this issue Mar 23, 2022
Closed
41 tasks
@andreasabel andreasabel modified the milestones: 2.6.3, 2.6.2.2 Mar 23, 2022
@andreasabel
Copy link
Member

Picked for 2.6.2.2-rc2 (with easily fixed merge conflict).

andreasabel added a commit that referenced this issue Mar 27, 2022
@andreasabel
Fix #5712: coverage: trailing args inserting in presence of domTactic
0241bf9 
Fix of #5358 prevented trailing arg insertion in the coverage checker
if there was a tactic (at function type).  However, in the presence of
a user written arg, the insertion should not be prevented.

Conflicts:
	src/full/Agda/TypeChecking/Coverage.hs
@andreasabel andreasabel mentioned this issue Aug 23, 2023
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andreasabel andreasabel

Labels
coverage Pattern-matching coverage checker internal-error Concerning internal errors of Agda regression in 2.6.1 Regression that first appeared in Agda 2.6.1 tactic tactic annotations
Projects
None yet
Milestone
2.6.2.2
Development

Successfully merging a pull request may close this issue.

Fix #5712: coverage: trailing args inserting in presence of domTactic agda/agda
2 participants
@andreasabel @Trebor-Huang