Confusing instance error

Stream: lean4

[Tom]

I asked a question in "new members"; I seem to get an error from the Eleborator but the code still type checks/works. Not sure if this is a bug/unintended behavior:

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Lean.20gives.20error.20but.20eval.20works.3F/near/471538887

Thought I'd surface just in case.

[Kyle Miller]

Summarizing here, the "cannot find synthesization order" error message led @Tom to think that there was an error in the instance definition itself. However, the error doesn't mean the instance definition itself has any real errors, other than the fact that a synth order couldn't be computed — this is the plan that instance synthesis will use when trying to apply the instance — the impact is that the instance might not be applicable.

[Kyle Miller]

In this particular case, there's an HAdd instance argument that has some arguments that only appear in an outParam. Interestingly, the Add default instance makes the instance succeed anyway in the end.

[Kyle Miller]

Given that the only way this instance works is by applying a default instance, I think it should use Add instead of HAdd.

[Kyle Miller]

Still, the error message probably should mention that it will use some default synth order as a backup and warn that the instance is likely never applicable.

[Edward van de Meent]

perhaps this should be a warning rather than an error, then?

[Kyle Miller]

Yeah, I think that could make sense.

[Kyle Miller]

lean4#5399 proposes the change

[Tom]

So does the above discussion also mean that in general, I can't use CoeFun to generate a polymorphic function? That was basically what I experimenting with. Perhaps simplifying further,

structure MyAdd

instance [Add α] [OfNat α 5]: CoeFun (MyAdd) (fun _ => (α -> α)) where
  coe f := fun x : α => x + 5

def myAdd := MyAdd.mk

#check myAdd 3
#eval myAdd 3

Also note that the inferred type is now USize! Is that concerning?

[Tom]

Kyle Miller said:

lean4#5399 proposes the change

Just saw this, thank you!

[Kyle Miller]

The issue here is that the second argument to CoeFun is an outParam, meaning that the instance is responsible for filling it in. The non-outParam argument MyAdd doesn't mention α, so it's not able to solve for α.

I'm surprised USize pops up here though! You'd have to trace instance synthesis to get to the bottom of that one.

[Kyle Miller]

Tom said:

Just saw this, thank you!

Be sure to check whether the wording would have helped, and feel free to leave a github comment!

[Tom]

Kyle Miller said:

Tom said:

Just saw this, thank you!

Be sure to check whether the wording would have helped, and feel free to leave a github comment!

Already looking! :bow:

[Edward van de Meent]

for what it's worth, you can make a polymorphic function this way. you just have to tell lean about the fact that the coersion has to happen regardless of what the type of the second operand is going to be.

set_option autoImplicit false
universe u v w

structure MyAdd (α:Type u) where
  myval : α


instance {α :Type u} : CoeFun (MyAdd α) (fun _ => {β : Type v} → {γ : Type w} → [HAdd α β γ] → β → γ) where
  coe x := fun b => x.myval + b


def myAdd := MyAdd.mk 5

#check myAdd 3
#eval myAdd 3

[Tom]

Hi @Edward van de Meent

Wow, that's cool. I can just about read/understand this but wouldn't have never been able to come up with it!

What's the reason for the autoImplicit false? Is that some magic required to make this work or is that a coding style preference wrt to being explicit about universe levels?

And forgive the silly question but when I change the last line to

#eval myAdd (3 : Int)

I actually get an error, while

#eval 5 + (3 : Int)

actually works (as expected).

Am I misunderstanding something or does the above instance actually not work for mixed types?

Thanks!

[Kyle Miller]

set_option autoImplicit false can always be removed. It can be good practice when developing when you're not sure if you're accidentally introducing additional parameters.

[Kyle Miller]

5 + (3 : Int) works because of some elaboration magic for binary operators. If you go-to-def for + you'll see binop%, which triggers it.

That elaborator will get 5 to elaborate as an Int. You can hover over 5 in #check 5 + (3 : Int) to verify.

[Kyle Miller]

We need these special elaborators since heterogenous operators have elaboration issues — we want to be able to propagate the return value's type to the arguments, and from one argument to the other, when we can detect it's not heterogenous.

[Edward van de Meent]

i actually expected it to simply be coersion?

[Kyle Miller]

Anyway, the proximal error is that there's no HAdd Nat Int ?m.693 instance.

[Tom]

Thanks! Sorry - to be clear. I understand why "5 + (3 : Int)" works. However, the Adder example which @Edward van de Meent posted does not work for me with mixed types.

[Kyle Miller]

Yeah, that's what I'm addressing. The difference is that you have myAdd : MyAdd Nat

[Kyle Miller]

There's nothing here that will trigger a coercion

[Kyle Miller]

Even (5 : Nat) + (3 : Int) needs this binop% elaborator. Compare it to HAdd.hAdd (5 : Nat) (3 : Int), which fails.

[Kyle Miller]

Even if you use homogenous addition, there are elaboration gotchas. The first fails, but the second works:

#check Add.add (5 : Nat) (3 : Int)
#check Add.add (3 : Int) (5 : Nat)

[Edward van de Meent]

then what's going on here?

variable (x : Nat)

#check x + (3 : Int)

[Edward van de Meent]

ah, i think i've misunderstood you. i thought you said binop% was something to make number literals get cast to the right type, but it does the coersion in general

[Tom]

I see. I was just going off Ch 4. of FPiL, from which my understanding was that writing

#eval (5 : Nat) + (3 : Int)
#eval HAdd.hAdd (5 : Nat) (3 : Int)

are the same, because the former would only "desugar" to the latter. Seeing that the latter doesn't work is actually a surprise to me.

Hence why I was also confused about your comment about "coercion", because the only "coercion" I was looking for was the "CoeFun" to go from Adder a to something like `fun b => x.myval + b with [HAdd a b c] b -> c.

Clearly it's more complicated than that.