Implement overloaded projections

[andreasabel]

AIM XXIII code sprint. Milestone 1:

module _ (A : Set) (a : A) where

record R B : Set where
  field f : B
open R

record S B : Set where
  field f : B
open S

r : R A
R.f r = a

s : S A
S.f s = f r

[andreasabel]

Does not work yet with copied projections:

module _ where

module M (A : Set) where
  record R : Set where
    field f : A

module N A = M A

open M using (R)
open M.R using (f)
open N.R using (f)

r : ∀ A (a : A) → R A
f (r A a) = a

test : ∀ A (a : A) → A
test A a = f (r A a)

Cannot resolve overloaded projection f because several matching
candidates found: [Issue1944-module.M.R.f,Issue1944-module.N.R.f]
when checking that the expression f (r A a) has type A

[WolframKahl]

The original post here provides a test case for this proposed change (and possibly enhancement).

I would feel safer if there was also a future ChangeLog entry... (that is, a specification...) 😉