Coercion from Nat to Unit

Stream: mathlib4

[Jovan Gerbscheid]

I just found out that this type checks:

def foo (n : Nat) : Unit := n

Is this intended behaviour? I think it is confusing.

[Jireh Loreaux]

Yes, it's intended, at least if the coercion it's finding is the the same as the one mine found. It's getting a docs#NatCast instance from the docs#Semiring instance for Unit.

[David Renshaw]

complete example (the import is needed):

import Mathlib.Algebra.PUnitInstances

def foo (n : Nat) : Unit := n

set_option pp.all true in
#print foo
/-
def foo : Nat → Unit :=
fun (n : Nat) ↦
  @Nat.cast.{0} Unit
    (@Semiring.toNatCast.{0} Unit
      (@CommSemiring.toSemiring.{0} Unit (@CommRing.toCommSemiring.{0} Unit PUnit.commRing.{0})))
    n
-/

[Jireh Loreaux]

import Mathlib.Algebra.PUnitInstances is the minimal import

[Jovan Gerbscheid]

It seems like the constant Semiring.toNatCast doesn't have a definition anywhere.

[Jireh Loreaux]

It's generated by the extends keyword in the definition of docs#Semiring

[Jireh Loreaux]

Although it's a little nonobvious to see why

[Jovan Gerbscheid]

Aha, but strangely ctrl+click doesn't work on Semiring.toNatCast for me.

[Jireh Loreaux]

Technically, the line is:

class Semiring (α : Type u) extends NonUnitalSemiring α, NonAssocSemiring α, MonoidWithZero α

but some of these classes share fields. As a result, Lean takes a NonUnitalSemiring as the sole "true" parent, and then takes the remaining fields from NonAssocSemiring and makes them fields of the new class. But one of the non-overlapping fields of NonAssocSemiring is toNatCast

[Jireh Loreaux]

The same thing happens for docs#NonAssocSemiring, which is:

class NonAssocSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, MulZeroOneClass α,
    AddCommMonoidWithOne α

And the same thing happens again with docs#AddCommMonoidWithOne until you get to docs#AddMonoidWithOne which has an honest-to-god docs#NatCast in its extends clause.

[Jireh Loreaux]

Jovan Gerbscheid said:

Aha, but strangely ctrl+click doesn't work on Semiring.toNatCast for me.

I'm not sure about the reason for this.

[Jovan Gerbscheid]

when viewing the definition in the online documentation, I see

class Semiring (α : Type u) extends NonUnitalSemiring , One , NatCast : Type u

[Jovan Gerbscheid]

Is that intended?

[Jovan Gerbscheid]

Would it be worth it to make the group, ring, etc. instances of Unit scoped? In general I wouldn't want anything to coerce to a Unit or PUnit.

[Kyle Miller]

I think it makes sense not having Unit itself be a semiring, or at least scoping it. I'd even be inclined to define def ZeroSemiring := Unit and giving this synonym the instances instead.

(I'm moving this discussion to the mathlib stream)

[Notification Bot]

This topic was moved here from #lean4 > Coercion from Nat to Unit by Kyle Miller.

[Floris van Doorn]

Kyle Miller said:

I think it makes sense not having Unit itself be a semiring, or at least scoping it. I'd even be inclined to define def ZeroSemiring := Unit and giving this synonym the instances instead.

(I'm moving this discussion to the mathlib stream)

I don't mind keeping the current state.
If we want to have a type synonym, then I think we should have a single type synonym (TrivialStructure?) that has all trivial algebraic structures, and not different synonyms for e.g. TrivialGroup and TrivialRing.