Specifying instance for ite.

Stream: lean4

[Jun Yoshida]

I found the following code producing an error around ite.

#eval ite (α:=Nat) (c:=1=2) (h:=inferInstance) 3 5  -- OK
#eval ite (α:=Nat) (1=2) (h:=inferInstance) 3 5     -- error
/-
application type mismatch
  ite ?m.2520 (1 = 2)
argument
  1 = 2
has type
  Prop : Type
but is expected to have type
  ℕ : Type
-/

Could you tell me what happens here?
I'd also like to know the best way to specify an instance of Decidable c to ite or if-then-else.

[Kevin Buzzard]

The best way to specify an instance of Decidable c is to make sure the type class inference system knows about it and then let it do the work for you.

[Kevin Buzzard]

docs4#ite

[Kevin Buzzard]

I don't understand the error though

[Max Nowak 🐉]

My best guess is, since in the second eval you don't have a continuous sequence of (_ := _) named args, it gets confused about the argument order?

[František Silváši 🦉]

This has to do with the way that you're specifying \alpha which is implicit. The '... is expected to have type \N' means that it's trying to resolve it as the first argument following the instance of Decidable.

E.g. this will work:

#eval @ite Nat (1=2) inferInstance 3 5

[Kevin Buzzard]

Right -- that's what's happening, and that's a workaround, but at the end of the day this still looks like a bug? This doesn't work either (same error):

#eval ite (α:=Nat) (h:=inferInstance) (1=2) 3 5

[Jun Yoshida]

Thanks for a lot of comments.
In contrast to the ordinary math project, I have several instances of Decidable p which depend on different sets of axioms. So it is convenient having a way to specify instances explicitly in addition to the type-class inference system. @František Silváši 🦉 's method looks neat to me; moving from Lean 3, I have nearly forgot about @ notation.

[Jun Yoshida]

Max Nowak 🐺 said:

My best guess is, since in the second eval you don't have a continuous sequence of (_ := _) named args, it gets confused about the argument order?

That makes sense, but writing (h:=_) first looks ugly to me since it is a dependent argument.

[Jun Yoshida]

Besides, the error message doesn't make sense or at least isn't helpful.

[Jun Yoshida]

Here is MWE from scratch.

class IsThree (n : Nat)
instance inst3 : IsThree 3 := .mk

def test (n : Nat) [h : IsThree n] : Nat := 0

#eval test 3                         -- OK
#eval test 3 (h:=inferInstance)      -- error
#eval test (h:=inferInstance) 3      -- error
/-
function expected at
  test ?m.10077
term has type
  ℕ
-/
#eval test (n:=3) (h:=inferInstance) -- OK
#eval test (h:=inst3)                -- OK (?!)

I was surprised that the last one compiles successfully. Is it an expected behavior?