Why is Data.List.Relation.Binary.Subset.Setoid.Properties not parametrized on the Setoid as a whole

[andreasabel]

Module Data.List.Relation.Binary.Subset.Setoid is parametrized on a Setoid, but its Properties module not:

agda-stdlib/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda

Line 9 in bfd7a7b

module Data.List.Relation.Binary.Subset.Setoid.Properties where

Instead, each function is parametrized there individually, via anonymous modules.
Is there a reason why it is organized like this?

I would have expected to open the Properties module in the same way as its parent module.

• fail in solving instance of ⊆-refl in Agda 2.6.4.3 agda#7294

[JacquesCarette]

This tends to be for historical reasons rather than any 'good' reason. Evolution of the library happens haphazardly sometimes (no matter how hard we try to review PRs).

In other words, I'd call this a plain bug awaiting a PR to fix it.

[MatthewDaggitt]

No, there's a good reason for all such Properties modules being designed this way. If you parameterise it by a single setoid, then you can't prove properties of functions that move between different types, e.g. map.

[jamesmckinna]

But as @omelkonian writes on #2389 , this is not the case for eg Data.List.Relation.Binary.Permutation.Setoid.Properties, leading to undesirable consequences... wrt map :-( so @JacquesCarette 's point about historical/legacy inconsistency stands.

Ditto. The proposed addition in #2393 ...?

[jamesmckinna]

No, there's a good reason for all such Properties modules being designed this way. If you parameterise it by a single setoid, then you can't prove properties of functions that move between different types, e.g. map.

Is this design principle documented anywhere?

[MatthewDaggitt]

But as @omelkonian #2389 (comment), this is not the case for eg Data.List.Relation.Binary.Permutation.Setoid.Properties, leading to undesirable consequences... wrt map :-(

Yes that should really be fixed.

Is this design principle documented anywhere?

No, sadly not 😓