Debugging coercions

Stream: new members

[Adomas Baliuka]

How do I find out where a coercion happens and what it does? For example, Mathlib seems to have a coercion from Nat to Nat -> Bool, which seems to always return true. (There is also one to Bool -> Nat, apparently constant function returning the coerced number). I tried synthesizing the Coe instances but it didn't work. How can I find out what is happening?

import Mathlib

#eval (5 : Nat → Bool) 1 -- true for all inputs?
#synth (Coe Nat (Nat → Bool))  -- fails
#synth (CoeFun Nat (fun _ => Nat → Bool))  -- fails

I found this after some time debugging why my program crashed when I unfortunately mixed up List.findIdx?and List.indexOf? and assumed it can't be wrong because "surely that would be a type error". (I'm still not sure why this crashes but the coercion is at fault)

import Mathlib

def argmaxValOfSum (l : List (List ℕ))
    : Option (ℕ × ℕ)
    :=
        let sums := l.map List.sum
        let maximum? := sums.maximum?
        match maximum? with
        | none => none
        | some maximum =>
            --dbg_trace "sums {sums}"
            --dbg_trace "maximum {maximum}"
            let argmax := sums.findIdx? maximum
            match argmax with
            | some amax => some (amax, maximum)
            | _ => none

#eval argmaxValOfSum  [[10000]]

[Yaël Dillies]

Does it return true for 0 : ℕ?

[Alex J. Best]

When you type (5 : T) whats happening isn't really a coercion from Nat to T. Instead Lean is looking for an instance OfNat T 5.

[Adomas Baliuka]

Yaël Dillies said:

Does it return true for 0 : ℕ?

Indeed, it does not.

[Adomas Baliuka]

Is there a way to "print whatever conversion is happening" without having to individually check Coe, CoeFun, OfNat, (maybe a lot more things?!...)?

[Kevin Buzzard]

Sure -- just hover over the 5 in the infoview.

import Mathlib

#check (5 : Nat → Bool)

[Adomas Baliuka]

That helps a lot, thanks. I never noticed that one can actually chain hover-tooltips in the infoview, i.e., get tooltips for terms in tooltips of tooltips...

To stay with my example and hopefully provide some content to this thread meriting the title, I tried to find out where this "conversion" (what's the most general term for what happens in (x : T)?) is defined:

• write #check (5 : Bool → Nat) and hover over the 5 in the infoview. This gives @OfNat.ofNat (Bool → ℕ) 5 instOfNat : Bool → ℕ.
• click oninstOfNat to see the instance definition.
• It 's instance instOfNat [NatCast R] [Nat.AtLeastTwo n] : OfNat R n := ... where R : Type*
• Now assume (non-automatic step!) that I need NatCast (Bool → ℕ)
• #synth NatCast (Bool → ℕ) gives instance natCast : NatCast (∀ a, π a) := { natCast := fun n _ ↦ n }, which looks like it will give the constant function _ => 5.

Is there a better way to do this? Some kind of stack-trace for what functions are called when doing (5 : Bool → Nat)? I'm not sure this process is guaranteed to give me what I want in all cases (and some of the steps are prone to error if I misunderstand the code I'm reading, although that might be quite a lot harder to address)

Another question: can one turn off some rarer implicit conversions? Type stability is useful for finding errors and implicit conversions (often considered problematic in some other programming languages) make that harder. This is what tripped me up in the "crash" example above. Lean wholeheartedly embraces implicit conversions, which probably makes a lot of sense given its aims and applications, but there still might be some tools to manage that.

[Kyle Miller]

OfNat isn't generally considered to be a conversion -- it's the mechanism that implements how natural number literals are interpreted with respect to a particular type.

Mathlib's putting an OfNat instance on Bool seems suspect... (0 : Bool) is false and (1 : Bool) is true, but then (2 : Bool) is false again -- it's whether the natural number is odd. It goes against a convention in many programming languages that 0 represents false and anything non-zero is true.

If you do fun (n : Nat) => (n : Bool) then you can see an actual coercion from Nat to Bool. It has the same properties.

[Kyle Miller]

You can see a trace of all instance problems by setting an option:

set_option trace.Meta.synthInstance true
#eval (fun (n : Nat) => (n : Bool)) 2

[Kyle Miller]

Lean wholeheartedly embraces implicit conversions

I wouldn't say it's wholehearted. If there is a canonical function from one type to another, mathlib is generally happy to have a Coe instance for it.

I think a problem you're experiencing is that Bool has a semiring structure put on it, and semirings have a canonical function from Nat, so mathlib has a coercion. Mathematically, this is the right thing to do, but in your context you are not viewing Bool as being a semiring -- it's just meant to represent a truth value. It makes me wonder whether mathlib should have a different Bool that's the boolean ring, leaving the Lean 4 core Bool for programming.

[Adomas Baliuka]

Is there a difference between implicit and explicit conversions/coercions in Lean? I would call (x : T) "explicit"and for f : X -> Y, and x : Z which can be coerced into X, I would call f x "implicit". I'm mostly worried about the implicit ones. In modern C++ programming, for example, implicit casts (too many terms used loosely here) are often "considered evil" across the board, and for good reason (although I personally don't agree with a blanket ban).

Are there ways to locally turn off some of these implicit conversions (without manually purging each individual instance, which apparently can have a wide variety of names)? Or to define a specific conversion/coercion as opt-in or explicit-only?

[Kyle Miller]

I think right now the only thing you can do is turning off instances one at a time (or getting support to change the library itself).

It's worth considering that in mathlib definitions don't come without accompanying theorems, so while these coercions that might be "evil" in C++, where nothing's proved, they turn out to be fine in mathlib. It can be frustrating though if you're just trying to write a program.

[Kyle Miller]

You might also consider importing just the parts of mathlib you need, which helps a bit with reducing the number of instances you need to be aware of. Mathlib developers don't recommend importing all of mathlib in general, even for mathematical applications.

[Kyle Miller]

It might be worth figuring out a design to get the coercion system be able to differentiate between explicit and implicit coercions. One way would be for there to be two typeclasses, with the implicit coercions typeclass providing all its instances to the explicit one, and then functions like elabTermEnsuringType could take an additional parameter for whether when ensuring the type it's OK to use explicit coercions.