Instance of Coe giving an error I don't understand

Stream: new members

[Javier Lopez-Contreras]

Hello,

I am getting a error message that I have never seen, and I cannot find any information online. Does anyone happen to understand it?
image.png

This is the minimal recreation

import Mathlib
open CategoryTheory Ring

variable {𝓞 : Type u} [CommRing 𝓞] [IsLocalRing 𝓞] [IsNoetherianRing 𝓞]

variable (𝓞) in
def CommAlgCat := Under (CommRingCat.of 𝓞)

variable (𝓞) in
instance : Coe (CommAlgCat 𝓞) (CommRingCat) where
  coe A := A.right
  -- what is this error?

[Floris van Doorn]

Short version: replace Coe by CoeOut and it will work.

Long version: the first argument (i.e. domain) of Coe is marked in a special way (semiOutParam) which means that the first argument has to be deducible from the second argument. The reason is that Coe-instances can be chained multiple times right-to-left.
In your instance that is not the case, but you can mark it as CoeOut, which means that it will chain this coercion left-to-right. This is the class to use if the domain depends on a variable that does not occur in the codomain.

[Floris van Doorn]

You can find more information about this by jumping to the definition of the Coe class and reading the module doc & docstrings there.

[Javier Lopez-Contreras]

Makes total sense and your solutions works. Thanks! Extra question just for my general knowledge: when you say the first argument needs to be deducible from the second argument, where can I read about what it formally means for a Type to be deducible from another type?

[Floris van Doorn]

it just means that all the variables occurring in the first argument should also occur in the second argument.
For CoeOut it's the other way around.