[Agda] PreorderReasoning not Polymorphic Enough?

[Shin-Cheng Mu]

Hi,

In the Standard Library, the (very useful) combinators for
equational reasoning is defined in a parameterised module
Relation.Binary.PreorderReasoning which, given any Preorder,
produces the needed operators begin_, _≈⟨_⟩_, and _∎.

However, it appears that I have to generate one instance
of these operators for every carrier type I am performing
equational reasoning on. The problem seems to have been
noticed before, as seen in the comments in
PropositionalEquality.agda:

   -- Relation.Binary.EqReasoning is more convenient to use with _≡_  
if
   -- the combinators take the type argument (a) as a hidden argument,
   -- instead of being locked to a fixed type at module instantiation
   -- time.

That is, rather than being tied to a fixed carrier, we may
need a module that somehow accepts, for example, these information:

      (_∼_ : {A : Set} -> A -> A -> Set)
      (refl : {A : Set}{x : A} -> x ∼ x)
      (trans : {A : Set}{x y z : A} -> x ∼ y -> y ∼ z -> x ∼ z)

and produces combinators of type (e.g):

     _∼⟨_⟩_ :  {A : Set} (x : A) {y z : A} -> x ∼ y ->
                 y IsRelatedTo z -> x IsRelatedTo z

However, even this may not be enough. In a recent experiment of
mine I wished to reason about functions using pointwise
equality (that is, f ≐ g iff forall a -> f a = g a). The
types of _≐_ and its reflexive and transitivity rules look like:

   _≐_ : {A B : Set} -> (A -> B) -> (A -> B) -> Set
   ≐-refl : {A B : Set}{f : A -> B} -> f ≐ f
   ≐-trans : {A B : Set}{f g h : A -> B} -> f ≐ g -> g ≐ h -> f  
≐ h

And therefore, I may need a module offering combinators
having types:

   _∼⟨_⟩_ :  {A B : Set} (x : F A B) {y z : F A B} -> x ∼ y ->
               y IsRelatedTo z -> x IsRelatedTo z

where (F : Set -> Set -> Set) is also a parameter to
the module.

Now I am using my revised version of these modules for
the particular cases I need. Is there a general solution?

sincerely,
Shin