Guidelines on coercion instances

Stream: lean4

[Gabriel Ebner]

In Lean 3, we had pretty strict restrictions on possible coercion instances. For example, has_coe α t was always forbidden. Otherwise you easily ran into nontermination.
I thought that the new type-class synthesis algorithm in Lean 4 solved these nontermination issues in a more principled way, but I've just ran into this at first glance unrelated error with a seemingly innocent coercion:

def Cached {α : Type _} (a : α) := { b // b = a }

instance {a : α} : Coe (Cached a) α where
  coe x := x.1

def foo (a b : List Nat) := a ++ b -- times out

[Gabriel Ebner]

Replacing Coe by either CoeHead or CoeTail fixes the issue, but of course restricts the coercion.

[Daniel Selsam]

@Gabriel Ebner Tabling only prevents cycles under the bounded-term-size hypothesis, which means that the terms do not grow arbitrarily big. In your example, the instance effectively says "whenever you are trying to prove any goal α, try to prove the bigger goal @Cached α a". The trace shows this:

[Meta.synthInstance.newSubgoal] Coe (List Nat) (List Nat)
...
[Meta.synthInstance.newSubgoal] Coe (List Nat) (@Cached (List Nat) _tc.0)
...
[Meta.synthInstance.newSubgoal] Coe (List Nat) (@Cached (@Cached (List Nat) _tc.0) _tc.1)
...
[Meta.synthInstance.newSubgoal] Coe (List Nat) (@Cached (@Cached (@Cached (List Nat) _tc.0) _tc.1) _tc.2)
...

We don't have a great solution to this problem in general, though this instance seems like an ideal candidate for a head/tail restriction. I know Leo has thought about this problem a lot recently, and played with many heuristics for detecting "bad traces", but I don't know what his current thoughts are. There are many other options (e.g. iterative deepening) but no silver bullet yet AFAIK.

[Daniel Selsam]

There are a few other funny things about this example. The identity coercion should probably have maximum priority:

def Cached (α : Type _) (a : α) := { b // b = a }

instance {a : α} : Coe (Cached α a) α where
  coe x := x.1

instance : Coe α α where
  coe x := x

def foo (a b : List Nat) := a ++ b -- works now, since the coercion becomes id

[Daniel Selsam]

(deleted)

[Joe Hendrix]

@Daniel Selsam I just realized that I've had an implicitly operational interpretation of coercions as trying to convert a value to match an argument type (e.g., starting from the type of the value and trying to find an coercion to the argument type).

Are coercisions searches fully bidirectional? Would it be useful/feasible to have oriented coercisions (or perhaps more generally triggered instances) that require a specific Coe form to apply? There may be similarities with SMT heuristics for instantiating universally quantified variables.

[Daniel Selsam]

@Joe Hendrix Currently, coercions are handled by the typeclass mechanism, so the search is effectively defined by the typeclass instances, most of which are defined in https://github.com/leanprover/lean4/blob/master/src/Init/Coe.lean

[Joe Hendrix]

Thanks. It looks like it could be pretty programmable, maybe the Cached coercision above could use CoeHead or one of the more restricted type classes.

[Gabriel Ebner]

In your example, the instance effectively says "whenever you are trying to prove any goal α, try to prove the bigger goal @Cached α a

This is not a property of type-class inference itself, but of the way that the *Coe* instances are set up. (The type class instance itself says "whenever you prove Coe (Cached a) α, you need to prove nothing else".) This particular instance also seems to have changed since Lean 3. Coe (Foo α) α used to be okay while Coe α (Foo α) was forbidden. Now it seems to be the other way around.
It's good to know that the Lean 3 issues with transitive coercions are still there, and need similar workarounds. I won't push the issue if the coercion design is still subject to change anyhow. I don't think this pathological type class encoding (i.e., encoding a transitive predicate as a typeclass) is used for anything else either.

[Daniel Selsam]

This is not a property of type-class inference itself, but of the way that the Coe instances are set up.

Yes, my response was poorly worded. FYI here is the Lean4 instance in question: https://github.com/leanprover/lean4/blob/master/src/Init/Coe.lean#L70 as you said, the corresponding Lean3 one goes in the other direction: https://github.com/leanprover-community/lean/blob/master/library/init/coe.lean#L95