Setting up automatic coercion

Stream: mathlib4

[Michael Stoll]

I would like a DirichletCharacter R n (where n > 1) to be coerced to an Nat.ArithmeticFunction R automatically where appropriate. I was trying

import Mathlib.NumberTheory.DirichletCharacter.Basic

@[coe]
noncomputable def DirichletCharacter.toArithmeticFunction {R : Type*} [CommMonoidWithZero R]
    {n : ℕ} [Fact (1 < n)] (χ : DirichletCharacter R n) : Nat.ArithmeticFunction R where
      toFun := χ.toFun ∘ Nat.cast
      map_zero' := by simp

variable {n : ℕ} [Fact (1 < n)] (χ : DirichletCharacter ℂ n)
#check Nat.ArithmeticFunction.LSeries (χ : Nat.ArithmeticFunction ℂ)
-- type mismatch
--   χ
-- has type
--   DirichletCharacter ℂ n : Type
-- but is expected to have type
 --  Nat.ArithmeticFunction ℂ : Type

Trying

noncomputable instance {R : Type*} [CommMonoidWithZero R] {n : ℕ} [Fact (1 < n)] :
    Coe (DirichletCharacter R n) (Nat.ArithmeticFunction R) where
      coe := DirichletCharacter.toArithmeticFunction

gives an error "cannot find synthesization order ... all remaining arguments have metavariables:
Fact (1 < ?n)", which I don't really know how to fix: if presented with an object of type DirichletCharacter R n, it should be clear what R and n must be. Adding random outParams doesn't seem to help.

Perhaps somebody more knowledgeable of how coercions work can give me a hint?

[Alex J. Best]

Use CoeHead in place of Coe, this is a coercion that indeed n is determined for if we go left to right, but not right to left

[Michael Stoll]

Thanks, this seems to work!

[Michael Stoll]

BTW, is there documentation somewhere that explains how it works?

[Yury G. Kudryashov]

Documentation strings of docs#CoeHead etc

[Yury G. Kudryashov]

Also, the module docstring of that file (scroll up)

[Michael Stoll]

So, for future reference: Init.Coe

[Alex J. Best]

And I think re-reading that now maybe CoeOut is the correct one in your case! Sorry for the hasty response before :smile: