Reopen PR "Add `record where` syntax sugar (#6603)"

[andreasabel]

This reopens

• #6603

and continues the discussion started there.

There is a few points to discuss and address in the proposed record where feature:

1. The currently implemented semantics of record where decls[fields] is in terms of let decls in record { fields = fields }. This restricts the declarations to the ones accepted in let, which is usually a source of confusion. An alternative semantics would be to define an anonymous module M containing decls and then form record{M}. However, there is the technical problem where to place M (since record where is an expression). Also, currently defining a module M would not work as the scope checker would complain about redefinitions of the fields (see #3801).
2. If we stick to the let semantics, a more suggestive name would be record let decls. Keyword where suggests that you can use the declaration forms that are allowed in where blocks.
3. The current implementation implements the recognition of record where (desugaring) but does not produce a record where (resugaring). That goes against our ideal to reproduce what the user has written, if at all possible. In this particular case, we would need a new Origin for the record expression and use this in the printer. Example:

   open import Agda.Builtin.Equality
   open import Agda.Builtin.Nat
   open import Agda.Builtin.Sigma 
   
   test : record { fst = 1; snd = 2}
        ≡ record where
            fst = 3
            snd = 4
   test = refl
   

   Current error:

   1 != 3 of type Nat
   when checking that the expression refl has type
   record { fst = 1 ; snd = _8 } ≡ record { fst = 3 ; snd = _14 }
   

   (does not reproduce record where).
4. The current examples in CHANGELOG and docs do not motivate this new sugar, as plain record expressions aren't longer (needing braces and semicolons, but not needing where). Better motivation could be supplied, e.g. using open (something of the form record where... open M...f = foo).