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

[Plamen Dimitrov]

To simplify the above reproducer even further, considering the background context:

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

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

the original example mentioned inability to perform implicit coercion of x in

def q₂ (y x: Bool.Binary C) : ℚ := sorry

-- explicit coercion works
def explicit_type_coersion_works (y x: Binary C W) : q₂ y (x : Bool.Binary C) = 0 := sorry
-- implicit coercion doesn't work:
/-
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
-/
def implicit_type_coersion_does_not_work (y x: Binary C W) : q₂ y x = 0 := sorry

Note that the working case only needs one argument (the second one) to be coerced and works without coercing the first so I guess Lean needs a more coherent one-time way of being informed about the type.

A second interesting example involves use of global variables like:

variable (x : Binary C W)
def q (x : Bool.Binary C) : ℚ := sorry

-- using the expected type in a definition-local variable works
def ex1 (x : Bool.Binary C) : Prop := q x = 1
-- explicit coercion works
def ex2 : Prop := q (x : Bool.Binary C) = 1
-- implicit coercion of the defined variable doesn't work:
/-
Application type mismatch: The argument
  x
has type
  Binary C W
but is expected to have type
  Bool.Binary ?m.3
in the application
  q x
-/
def ex3 : Prop := q x = 1

[Jakub Nowak]

Looks like this works with Coe. Seems like problems is caused by CoeOut?

import Lean

variable (x : Int)
def q (x : Lean.Json) : Nat := sorry

-- using the expected type in a definition-local variable works
def ex1 (x : Lean.Json) : Prop := q x = 1
-- explicit coercion works
def ex2 : Prop := q (x : Lean.Json) = 1
-- implicit coercion of the defined variable doesn't work:
/-
Application type mismatch: The argument
  x
has type
  Binary C W
but is expected to have type
  Bool.Binary ?m.3
in the application
  q x
-/
def ex3 := q x = 1

[Plamen Dimitrov]

Jakub Nowak said:

def q (x : Lean.Json) : Nat := sorry

I think you need a more elaborate type with one or two type parameters in order to reproduce this on your side. Let me know if you know about any such types from the standard library or Mathlib.