Required type annotation using Array

Stream: lean4

[Paul Chisholm]

The following function type checks as expected

def rowStr : Array Bool → String := Array.foldr (fun (b:Bool) s => s ++ (if b then "#" else " ")) ""

However, if the type annotation is removed

def rowStr : Array Bool → String := Array.foldr (fun b s => s ++ (if b then "#" else " ")) ""

This error is thrown

failed to synthesize instance
  Decidable b

The equivalent function on lists (without type annotation) is fine

def rowStr : List Bool → String := List.foldr (fun b s => s ++ (if b then "#" else " ")) ""

Is this expected, and if so, why is the type annotation required?

Using the Lean 4 2021-09-30 nightly.

[Chris B]

Both of these work, which is interesting:

def rowStr : Array Bool → String := Array.foldr (fun b (s) => s ++ (if b then "#" else " ")) ""
def rowStr' : Array Bool → String := Array.foldr (fun (b) s => s ++ (if b then "#" else " ")) ""

[Leonardo de Moura]

There is no short answer to this question. Elaboration process has several moving pieces that sometimes interact in unexpected ways. I will try to give some context

• The if-then-else takes a Prop (+ implicit argument saying it is decidable) instead of a Bool. When a Bool is used, we need to apply a coercion.
• The elaborator propates typing constraints.

When elaborating if b then x else y without knowing bs type, the elaborator will assume the type is Prop. In the array example, this is exactly what happens, and it infers that b : Prop since no typing information was available, and then fails trying to show it is decidable.
The List example works because the elaborator succeeds in inferring the type of b before it tries to elaborate the if-then-else. Note that Array.foldr has extra parameters with default values which slightly affect the elaboration order.
Any tiny change in the elaboration order may trigger the failure above. I will try to address this issue by using a custom elaborator for if-then-else terms.

Note that, if we use a foldr for Array that is similar to List.foldr, then it will work

def foldr' (f : α → β → β) (init : β) (as : Array α) : β :=
  as.foldr f init

def rowStr : Array Bool → String := foldr' (fun b s => s ++ (if b then "#" else " ")) ""

The following variant of the List.foldr example doesn't work because the type of b is now not inferred before we elaborate the if-then-else.

def rowStr' : List Bool → String := fun bs => List.foldr (fun b s => if b then "#" else " ") "" bs

That is, very small changes in the elaboration order trigger the problem.

@Chris B Your two examples work because Lean 4 has support for patterns in fun (i.e., we can write fun (a, b) => ...), and it interpreting (b) as a pattern, which then affects the elaboration order, and allows the elaborator to succeed.

By adding a custom elaborator for if-then-else that waits for the type of the condition, I think we will make the process more robust, and all of the variants above will work.

[Chris B]

Interesting, thanks for the breakdown.

[Paul Chisholm]

Thanks, interesting how such seemingly small changes lead to subtle and complex considerations, but a great deal is going on here.

[Leonardo de Moura]

I improved the if-then-else elaborator. Now, all examples above are elaborated correctly.
https://github.com/leanprover/lean4/commit/2546a2cf7e23bf1c39ca9f7738af25bc7ffcc468