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

[JasonGross]

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]

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]

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]

This already works correctly in 2.6.2.