Implicit coercion of type doesn't take place

Stream: new members

[Plamen Dimitrov]

Hi all, I have the following example with a working and non-working case at the very end:

import Mathlib

namespace Bin
inductive Bit : Type
| zero : Bit
| one : Bit
deriving DecidableEq
abbrev Binary := List Bit
end Bin

namespace Bool
def Binary (C : ℕ) : Type := { enc : Bin.Binary // List.length enc = C }
end Bool

def rr₀ (y x: Bool.Binary C) : ℚ := sorry

structure Binary (C : ℕ) (W : Bin.Binary → ℕ) where
  val : Bool.Binary C
instance : CoeOut (Binary C W) (Bool.Binary C) := ⟨fun x => x.val⟩

def explicit_type_coersion_works (x: Binary C W) : rr₀ x (x : Bool.Binary C) = 0 := sorry
def implicit_type_coersion_does_not_work (x: Binary C W) : rr₀ x x = 0 := sorry

and if you try it on the playground the second line will produce and error like

Application type mismatch: The argument
  x
has type
  Binary C W
but is expected to have type
  Bool.Binary ?m.3
in the application
  rr₀ ?m.4 x

and it seems the C of the rr-expected type was overshadowed as a metavariable m.3. Why do we need the explicit type specification as in the first case and Lean 4 cannot pick the C from the CoeOut instance we have already specified?

[Plamen Dimitrov]

Perhaps this is some important detail about the order of type resolution and auto-coercion steps that would somehow end up not performing the provided auto-coercion on time?

[Aaron Liu]

I think since it still has metavariables finding the coercion is postponed