Flipped type signatures in comments

[MatthiasHu]

When reexporting things, there are sometimes type signatures stated in comments. I think I found a few places where these type signatures are inaccurate, for example:

agda-stdlib/src/Data/Nat/Properties.agda

Line 1196 in ebfb881

; x≤y⊔x to m≤n⊔m -- : ∀ m n → m ≤ n ⊔ m

This function actually takes the n argument first and the m argument second, because x≤y⊔x is a renaming of x⊓y≤y which of course takes the x argument first:

agda-stdlib/src/Algebra/Construct/NaturalChoice/MinOp.agda

Line 43 in ebfb881

x⊓y≤y : ∀ x y → x ⊓ y ≤ y

The same issue is present in all four places where x≤y⊔x is re-exported:

src/Data/Integer/Properties.agda:  ; x≤y⊔x     to i≤j⊔i        -- : ∀ i j → i ≤ j ⊔ i
src/Data/Nat/Properties.agda:  ; x≤y⊔x     to m≤n⊔m        -- : ∀ m n → m ≤ n ⊔ m
src/Data/Rational/Properties.agda:  ; x≤y⊔x     to p≤q⊔p        -- : ∀ p q → p ≤ q ⊔ p
src/Data/Rational/Unnormalised/Properties.agda:  ; x≤y⊔x      to p≤q⊔p          -- : ∀ p q → p ≤ q ⊔ p

The same thing happens for example for x≤y⇒x≤z⊔y (which is a renaming of x≤y⇒z⊓x≤y), but here only the order of the implicit arguments is flipped:

src/Data/Integer/Properties.agda:  ; x≤y⇒x≤z⊔y to i≤j⇒i≤k⊔j    -- : ∀ {i j} k → i ≤ j → i ≤ k ⊔ j
src/Data/Nat/Properties.agda:  ; x≤y⇒x≤z⊔y to m≤n⇒m≤o⊔n    -- : ∀ {m n} o → m ≤ n → m ≤ o ⊔ n
src/Data/Rational/Properties.agda:  ; x≤y⇒x≤z⊔y to p≤q⇒p≤r⊔q    -- : ∀ {p q} r → p ≤ q → p ≤ r ⊔ q
src/Data/Rational/Unnormalised/Properties.agda:  ; x≤y⇒x≤z⊔y  to p≤q⇒p≤r⊔q      -- : ∀ {p q} r → p ≤ q → p ≤ r ⊔ q

[MatthewDaggitt]

Thank you, nice spot! Wish these weren't necessary and we had editor support...

[MatthiasHu]

I wonder if it could be best here to change the actual type signatures of x≤y⊔x and x≤y⇒x≤z⊔y (and similar cases) to reflect the order in which the variables x, y, z appear in the name.

[JacquesCarette]

In your "I wonder", do you mean that the rename

  ; x⊓y≤y      to x≤y⊔x

should instead be

  ; x⊓y≤y      to y≤x⊔y

?

[MatthiasHu]

No, I meant that there should be this:

x≤y⊔x : ∀ x y → x ≤ y ⊔ x

This can not be achieved by a renaming-reexport of x⊓y≤y, one would need a separate definition to flip the arguments.

[Saransh-cpp]

Also, n≤m⊔n was deprecated and m≤n⊔m was introduced -

agda-stdlib/src/Data/Nat/Properties.agda

Lines 2261 to 2264 in 0661b59

	n≤m⊔n = m≤n⊔m
	{-# WARNING_ON_USAGE n≤m⊔n
	"Warning: n≤m⊔n was deprecated in v1.6. Please use m≤n⊔m instead."
	#-}

Should I just update the type signature in the comments?

[jamesmckinna]

We bumped this from v2.0 to v2.1... suggest we do so again to v2.2 unless someone feels like tackling this before the end of June?