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

C-c C-s (solve constraints) infers the incorrect module to project from #5293

Closed
JasonGross opened this issue Mar 29, 2021 · 3 comments
Closed

C-c C-s (solve constraints) infers the incorrect module to project from #5293

JasonGross opened this issue Mar 29, 2021 · 3 comments
Assignees
@andreasabel
Labels
status: already-fixed type: bug Issues and pull requests about actual bugs ux: display Issues relating to how terms are printed for display
Milestone
2.6.2

Comments

@JasonGross
Copy link
Contributor

JasonGross commented Mar 29, 2021 •
edited by jespercockx
Loading

Consider

record Cat : Set₁ where
  field Obj : Set
  field Hom : Obj → Obj → Set
  record Iso (a b : Obj) : Set where
    field fwd : Hom a b
    field bak : Hom b a

data _≡_ {A : Set} (a : A) : A → Set where
  refl : a ≡ a

foo : (C D : Cat) → (x y : Cat.Obj D) → (f g : Cat.Iso D x y) → Cat.Iso.fwd f ≡ Cat.Iso.fwd f
foo C D x y f g = refl {Hom D x y} ?
  where module D = Cat D; module C = Cat C; open Cat

C-c C-s generated the C.Iso.fwd f for me, but it's incorrect and when C-c C-s attempts to refine I get the error message

D != C of type Cat
when checking that the expression f has type C.Iso _a_22 _b_23

It seems that the solver just looks for the most recently declared module of the relevant type or something? Switching module D = Cat D and module C = Cat C results in the correct inference.

I'm running Agda version 2.6.1.2
@andreasabel andreasabel added ux: display Issues relating to how terms are printed for display type: bug Issues and pull requests about actual bugs labels Mar 31, 2021
@andreasabel
Copy link
Member

andreasabel commented Mar 31, 2021 •
edited
Loading

Without further investigation, I would guess this is a display-form issue.
So Agda decides to print Cat.Iso.fwd f as C.Iso.fwd f, based on the display forms introduced by the module aliases module D = Cat D and module C = Cat C.

E.g., this works:

works : (C D : Cat) → (x y : Cat.Obj D) → (f g : Cat.Iso D x y) → Cat.Iso.fwd f ≡ Cat.Iso.fwd f
works C D x y f g = refl {Hom D x y} {{!Iso.fwd f !}}
  where open Cat

@jespercockx jespercockx added this to the 2.6.3 milestone Aug 23, 2022
@jespercockx
Copy link
Member

I tried this on current master and now C-c C-s generates a valid solution:

...
foo C D x y f g = refl {Hom D x y} {Iso.fwd f}
...

so I'm marking this as already fixed.

@andreasabel andreasabel mentioned this issue Oct 24, 2022
Closed
@andreasabel andreasabel modified the milestones: 2.6.3, 2.6.2 Oct 25, 2022
@andreasabel
Copy link
Member

This already works correctly in 2.6.2.

@andreasabel andreasabel self-assigned this Oct 25, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andreasabel andreasabel

Labels
status: already-fixed type: bug Issues and pull requests about actual bugs ux: display Issues relating to how terms are printed for display
Projects
None yet
Milestone
2.6.2
Development

No branches or pull requests
3 participants
@JasonGross @andreasabel @jespercockx