failed to synthesize implicit argument

Stream: lean4

[Anders Christiansen Sørby]

I have a problem trying to synthesize the transformer in this call

def toBase64 {I: Type u} {transformer : Into ByteArray I} (input : I) (pad: Bool := true) : String := do
...

def Blake3Hash : Type := { r : ByteArray // r.size = BLAKE3_OUT_LEN }

@[defaultInstance]
instance : Into ByteArray Blake3Hash := ⟨Subtype.val⟩

instance : Into String Blake3Hash := ⟨fun b => toBase64 b true⟩

Which leads to

Blake3> Blake3.lean:43:47: error: don't know how to synthesize implicit argument
Blake3>   @toBase64 Blake3Hash (?m.1002 b) b true
Blake3> context:
Blake3> b : Blake3Hash
Blake3> ⊢ Into ByteArray Blake3Hash
Blake3> Blake3.lean:44:35: error: don't know how to synthesize implicit argument
Blake3>   @toBase64 Blake3Hash ?m.1018 _uniq.1021 true
Blake3> context:
Blake3> ⊢ Into ByteArray Blake3Hash

Why can't this be synthesized and how can I annotate it to work?

[Chris B]

Does it work if you add @[reducible] to Blake3Hash?

[Chris B]

Also how is Into defined?

[Sebastian Ullrich]

Class parameters use [], not {}

def toBase64 {I : Type u} [Into ByteArray I] ...

[Chris B]

I didn't even notice that lol.

[Anders Christiansen Sørby]

Yes, I figured it out. This could be made clearer in the implicit argument section and the type class section.

[Anders Christiansen Sørby]

I'm getting this error:

Tests> Tests.lean:11:10: error: don't know how to synthesize implicit argument
Tests>   @isValid? (?m.527 args board x✝) (?m.528 args board x✝) board
Tests> context:
Tests> args : List String
Tests> board : Board
Tests> ⊢ Nat
Tests> Tests.lean:11:10: error: don't know how to synthesize implicit argument
Tests>   @isValid? (?m.527 args board x✝) (?m.528 args board x✝) board
Tests> context:
Tests> args : List String
Tests> board : Board
Tests> ⊢ Nat

for this code:

/-
A Sudoku board not validated
-/
structure Board where
  h : Nat
  w : Nat
  ax : h ≥ 1 ∧ w ≥ 1
  elementBound := { min := 1, max := (h*w), isMinMax := (one_le_size ax) : Bound }
  -- A rows first matrix
  arr : Array (Option <| BNat elementBound)
  axArr : arr.size = h*h*w*w


def main (args : List String) : IO UInt32 := do
  try
    let board : Board ← parseFile <| FilePath.mk "board1.txt"
    println! "Board 1:\n{board}"
    match board.isValid? with -- <-- This is the error
    | Except.ok () => println! "board is valid"
    | Except.error e => println! "board not valid: {e}"
    pure 0
  catch e =>
    IO.eprintln <| "error: " ++ toString e -- avoid "uncaught exception: ..."
    pure 1

def isValid? (b : Board) : Except String Unit := do
  -- Not pretty but a first draft
  -- let mut er := 1
  -- let mut ec := 1
  let mut valid := true
  for r in [1:h] do
    for c in [1:w] do
      let cell : Slice <| Option (BNat b.elementBound) := b.getCell (r.toBNat.get! : b.CellRowIndex) (c.toBNat.get! : b.CellColIndex)
      if not (validateSlice cell) then
        valid := false
        -- er := r
        -- ec := c
        break
  if valid then
    return ()
  else
    throw s!"invalid at"

But I can't tell which implicit variables it actually mentions. I've also added more explicit annotations but to no avail.

[Alex J. Best]

Can you try and create a MWE, its very hard to help from the code you have posted as there are multiple errors.
There's a lot of things wrong with the snippet you posted (things aren't in the board namespace, functions not defined, fuctions in the wrong order) so its almost impossible to see the actual error you are seeing

[Alex J. Best]

Also, what Lean commit?

[Mario Carneiro]

My guess is that the references to h and w in isValid? are being auto-bound, making isValid? take three arguments. If you #print isValid? it should show the type and names of the implicit arguments

[Mario Carneiro]

If you use b.h andb.w instead then the error should go away

[Sebastian Ullrich]

Auto-implicits should only trigger in the definition header. I hope.

[Mario Carneiro]

still, those two are definitely free variables. Perhaps there is a variables {h w : Nat} up above?

[Anders Christiansen Sørby]

It was because of a bad rewrite. I had forgotten to replace h and w with b.h and b.w as you can see in the for loops. I think we can have better error messages here.

[Anders Christiansen Sørby]

Like if the error message had given the location and names of the erroneous meta variables this would have been much easier to see.

[Sebastian Ullrich]

There isn't really anything to discuss here without an MWE. Or rather MNWE.

[Notification Bot]

Anders Christiansen Sørby has marked this topic as resolved.

[Notification Bot]

Anders Christiansen Sørby has marked this topic as unresolved.

[Anders Christiansen Sørby]

Why should binding these unfilled values not cause an error? Is there any way to fill them when calling the function?

[Arthur Paulino]

I think some code would really help :+1: