Coercions using additional type parameters

Stream: new members

[Plamen Dimitrov]

I have the following structures

namespace Bin
...
abbrev Binary := List Bit
end Bin

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

namespace Count
/-- Custom binary type with both value and weight. -/
structure Binary where
  val : Bin.Binary
  weight : ℕ
instance : Coe Binary Bin.Binary := ⟨fun x => x.val⟩
end Count

namespace Relative
/-- Custom C-length binary type with both value and weight. -/
structure Binary (C : ℕ) where
  val : Bool.Binary C
  weight : ℕ
instance : Coe (Binary 4) Count.Binary := ⟨fun x => { val := x.val.val, weight := x.weight }⟩
end Relative

Why for the final coercion I cannot use

instance : Coe (Binary C) Count.Binary := ⟨fun x => { val := x.val.val, weight := x.weight }⟩

which would instead lead to

instance does not provide concrete values for (semi-)out-params
  Coe (Binary ?C)

A similar coercion will work if the input and output type both contain the C parameter for instance. I clearly cannot list all of the possible C values and I need the typeclass-based coercions in situation where an explicit one won't do.

[Aaron Liu]

docs#CoeOut

[Plamen Dimitrov]

Thank you @Aaron Liu, interesting that the various LLMs I tried with all of their verbosity could not have suggested that the Coe being 2-way coercion is the cause of this and one way like this would fix it.

[Plamen Dimitrov]

Looking at simpler case here like

import Mathlib

inductive Bit : Type
| zero : Bit
| one : Bit
deriving DecidableEq
abbrev Binary := List Bit
def CBinary (C : ℕ) : Type := { enc : Binary // List.length enc = C }
instance : CoeOut (CBinary C) Binary := ⟨fun x => x.val⟩

def print (b : Binary) : String := b.foldr (fun bit acc => if bit == Bit.one then "1" ++ acc else "0" ++ acc) ""

instance : BooleanAlgebra (CBinary C) := sorry

def literal_encoding4 : CBinary 4 := { val := [Bit.zero, Bit.one, Bit.zero, Bit.one], property := by decide }
#eval print literal_encoding4
#eval print (literal_encoding4 ⊓ literal_encoding4).val

it seems like I cannot use #eval print (literal_encoding4 ⊓ literal_encoding4) instead as the last line since the coercion would not work with the ⊓ meet, isn't the ⊓ interpret simply as a bi-argument function that should then apply automatically to make use of the explicit coercion defined above?

[Plamen Dimitrov]

All of this is assuming a BooleanAlgebra instance proof that I have omitted here for brevity and the fact that `literal_encoding4 ⊓ literal_encoding4 : CBinary C already where the coercion is defined.

[Aaron Liu]

The types are propagated "outside-in" so since print expects a Binary it tries to find a way to do inf on Binary and fails

[Plamen Dimitrov]

Is there any way to make to work around this outside-in order then? Override the order via brackets or some other way to tell Lean how to process this?

[Jovan Gerbscheid]

You can write print (literal_encoding4 ⊓ literal_encoding4:). Writing ( ... :) is a way to tell lean to elaborate that expression without an expected type. It is mostly the same as (... : _). You can also give the expected type explicitly as print (literal_encoding4 ⊓ literal_encoding4 : CBinary 4)

[Plamen Dimitrov]

Thank you, the "smiley face" worked splendidly and preserves as much of the coercion automation as possible with a minimum extra typing overhead.