Needing to import Data.Integer.Base (pos) for an instance for ℚ.positive ½ is unintuitive

[Taneb]

I don't really understand the instance mechanics so I don't know what the right solution is here, but can we re-export or wrap pos (and neg etc) from Data.Rational.Base and Data.Rational.Unnormalised.Base?

[jamesmckinna]

Data.Rational.Properties.mkℚ+-pos?

[Taneb]

@jamesmckinna that lets me define a proof, but doesn't get the instance into scope, which is what I wanted

[jamesmckinna]

Is the objection to widening the import list from Data.Integer.Base in Data.Rational.*.Base, or in subsequent client modules? The former seems harmless, at least for the constants defined there, the latter does speak to your wish... but it should (?) be easy to add companion instance declarations to Rational by analogy with those for Integer?

[Taneb]

I was writing a something using rational numbers, when I made this issue (almost a year ago so I may be a little hazy on the details).

I had a function that needed an instance .{{_ : Positive n}}, and wanted to pass ½ to it. This didn't work straight away, and it wasn't obvious why, until I tracked through the definitions and documentation on instances, and discovered I needed Data.Integer.Base.pos in scope, which has nothing to do with rational numbers directly.

I believe the solution to this would be to make Positive for rationals and unnormalized rationals not (visibly) a synonym of the integer definition wtih some argument, so that the new instances wouldn't cause ambiguities, and then add the relevant instance.

[jamesmckinna]

Yes, I see. (Now).

One 'problem'/'issue' with the current Constructors/Destructors design of the irrelevant-instance numeric predicates is that instance inference is explicitly turned off for 'instances' derived from explicit arguments.

So there's a (possible) refactoring/redesign opportunity (a version of which would be your rebinding of instance pos... based on the Integer version.

Offering a low(er?)-energy solution, why not (appropriately) specialise _/_ to a positive integer first argument (or a NonZero Nat?), and then add the corresponding irrelevant/implicit instance? Maybe that's all you are asking for?

[jamesmckinna]

So, I tried writing the following in Data.Rational.Unnormalised.Base:

-- Instances

instance

  pos-/ : ∀ {n} {d} → .{{_ : ℕ.NonZero n}} → .{{_ : ℕ.NonZero d}} → Positive (+ n / d)
  pos-/ {n = suc _} = _ where instance _ = ℤ.posℕ {n = n}

and was surprised by two things:

• I had had already to rename ℤ.pos to ℤ.posℕ to avoid a clash between the instance ℤ.pos and the constructor Agda.Builtin.Int.Int.pos (despite this being renamed to +_ in Data.Integer.Base;... (is this a bug?)
• the type checker rejects the above declaration, because in the where clause, it says n not in scope; (is this not a bug?)

There's a separate problem, which I don't understand, about whether the typechecker can correctly unfold Positive (+ n / d) to ℤ.Positive n, to do with no-eta; pattern in the definition of ℚᵘ.

[jamesmckinna]

For the exact above code (agda: v2.6.3; stdlib: master) does anyone else get the same (anomalous) typechecking behaviour as I do?

[jamesmckinna]

Re: ℤ.pos/ℤ.posℕ. I certainly got confused with pos being declared as both a record field name for Positive, and also as a distinguished instance... should this (separately?) be renamed in some way? The idiomatics work fine for Data.Nat.Base.nonZero both as field name for NonZero, and as instance, so I don't know why they don't seem to here for Integer. A puzzle!

[MatthewDaggitt]

Best solution I think is just to have the Rational modules publicly re-export the instances from Data.Nat.Base and Data.Integer.Base.