Flipped type signatures in comments

MatthiasHu commented 1 year ago

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:

https://github.com/agda/agda-stdlib/blob/ebfb8814b4330b314da8fb9cae527e6a6fab01aa/src/Data/Nat/Properties.agda#L1196

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: https://github.com/agda/agda-stdlib/blob/ebfb8814b4330b314da8fb9cae527e6a6fab01aa/src/Algebra/Construct/NaturalChoice/MinOp.agda#L43

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 commented 1 year ago

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

MatthiasHu commented 1 year ago

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.