8000 Possible regression in 2.8.0-rc1 due to instance resolution · Issue #7882 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Possible regression in 2.8.0-rc1 due to instance resolution #7882

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
carlostome opened this issue May 14, 2025 · 1 comment · Fixed by #7885
Closed

Possible regression in 2.8.0-rc1 due to instance resolution #7882

carlostome opened this issue May 14, 2025 · 1 comment · Fixed by #7885
Labels
instance postponement issues --experimental-lazy-instances, discrim-based deferral of instance candidate checking instance Instance resolution regression on master Unreleased regression in development version (Change to "regression in ..." should it be released!)
Milestone
2.8.0

Comments

@carlostome
Copy link
Contributor

Using:

Agda version 2.7.20250510
Built with flags (cabal -f)
 - enable-cluster-counting: unicode cluster counting in LaTeX backend using the ICU library
 - optimise-heavily: extra optimisations

the following code fails to typecheck:

module ex where

open import Agda.Primitive
open import Agda.Builtin.Equality

variable 
  a b c : Level

infixr 1 _⊎_

data _⊎_ (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

⊎-map₂ : {A B D : Set} → (B → D) → (A ⊎ B → A ⊎ D)
⊎-map₂ g (inj₁ x) = inj₁ x
⊎-map₂ g (inj₂ y) = inj₂ (g y)

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B fst

open Σ public

infixr 4 _,_

_×_ : ∀ (A : Set a) (B : Set b) → Set (a ⊔ b)
A × B = Σ A λ _ → B

×-map₂ : ∀ {A : Set a} {B : A → Set b} {C : A → Set c} →
        (∀ {x} → B x → C x) → Σ A B → Σ A C
×-map₂ f x = x .fst , f (x .snd)

id : {A : Set} → A → A
id x = x

record Bifunctor (F : Set a → Set b → Set (a ⊔ b)) : Set (lsuc (a ⊔ b)) where
  field
    bimap : ∀ {A A′ : Set a} {B B′ : Set b} → (A → A′) → (B → B′) → F A B → F A′ B′

open Bifunctor ⦃...⦄ public

instance
  Bifunctor-⊎ : Bifunctor {a}{b} _⊎_
  Bifunctor-⊎ .bimap f g (inj₁ x) = inj₁ (f x)
  Bifunctor-⊎ .bimap f g (inj₂ y) = inj₂ (g y)

  Bifunctor-× : Bifunctor {a}{b} _×_
  Bifunctor-× .bimap f g x = f (x .fst) , g (x .snd)

variable
  S : Set
  s s' : S
  Err : Set

module _ (STS : S → S → Set) where
  record Computational Err : Set₀ where
    field
      computeProof : (s : S) → Err ⊎ (Σ S (STS s))
      completeness : (s : S) (s' : S)
        → STS s s' → ⊎-map₂ fst (computeProof s) ≡ inj₂ s'

open Computational ⦃...⦄

data STS* {STS : S → S → Set} : S → S → Set where
  BS-base :
    STS s s' → STS* s s'

module _ {STS : S → S → Set} ⦃ _ : Computational STS Err ⦄ where
  Computational-* : Computational (STS* {STS = STS}) Err
  Computational-* .computeProof s = bimap id (×-map₂ BS-base) (computeProof s) -- fails
  -- Computational-* .computeProof s = bimap ⦃ Bifunctor-⊎ ⦄ id (×-map₂ BS-base) (computeProof s) -- doesn't fail
  Computational-* .completeness s s' (BS-base p)
    with computeProof {STS = STS} s | completeness {STS = STS} _ _ p
  ... | inj₂ x | refl = refl

with error:

/tmp/agda-bug/ex.agda:77.25-29: error: [MetaCannotDependOn]
Cannot instantiate the metavariable _y.fst_195 to solution fst x
since it contains the variable x
which is not in scope of the metavariable
when checking that the expression refl has type
⊎-map₂ (λ r → fst r) (inj₂ (_y.fst_195 , _y.snd_196)) ≡
inj₂ (fst x)

In contrast, Agda version 2.7.0.1 typechecks the code just fine.

I found two alternative ways of avoiding getting the error in 2.7.20250510:

  1. Commenting out the Bifunctor-× instance
  2. Passing the instance argument explicitly to bimap (see commented out line)

This might be related to #7847.
@carlostome carlostome changed the title Possible regression in rc1 due to instance resolution Possible regre 8000 ssion in 2.8.0-rc1 due to instance resolution May 14, 2025
@carlostome carlostome mentioned this issue May 14, 2025
Open
@andreasabel andreasabel added the instance Instance resolution label May 14, 2025
@andreasabel andreasabel added this to the 2.8.0 milestone May 14, 2025
@andreasabel andreasabel added the regression on master Unreleased regression in development version (Change to "regression in ..." should it be released!) label May 14, 2025
@plt-amy
Copy link
Member
plt-amy commented May 14, 2025

Not related to #7847; this is #7846/#7799: the implementation of instance search can not tell your two instances of Bifunctor apart other than by the slow linear-search behaviour that we're trying to get rid of. There is a hack to re-enable it in places where it's actually needed but checking the type of a with function had not been one of these places yet.

plt-amy added a commit that referenced this issue May 14, 2025
@plt-amy
disable discrim-based instance deferral by default
58d6a35 
but keep it as a flag. i am so tired but also i am going to make this
work, mark my words. also fixes #7882 en passant
@plt-amy plt-amy mentioned this issue May 14, 2025
Merged
@plt-amy plt-amy added the instance postponement issues --experimental-lazy-instances, discrim-based deferral of instance candidate checking label May 14, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
instance postponement issues --experimental-lazy-instances, discrim-based deferral of instance candidate checking instance Instance resolution regression on master Unreleased regression in development version (Change to "regression in ..." should it be released!)
Projects
None yet
Milestone
2.8.0
Development

Successfully merging a pull request may close this issue.

disable discrim-based instance deferral by default agda/agda
3 participants
@andreasabel @carlostome @plt-amy
0