Zulip Chat Archive

Stream: lean4

Topic: Guidelines on coercion instances


view this post on Zulip Gabriel Ebner (Apr 01 2021 at 15:34):

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

view this post on Zulip Gabriel Ebner (Apr 01 2021 at 15:35):

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

view this post on Zulip Daniel Selsam (Apr 01 2021 at 15:58):

@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.

view this post on Zulip Daniel Selsam (Apr 01 2021 at 16:04):

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

view this post on Zulip Daniel Selsam (Apr 01 2021 at 16:25):

(deleted)

view this post on Zulip Joe Hendrix (Apr 01 2021 at 16:58):

@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.

view this post on Zulip Daniel Selsam (Apr 01 2021 at 17:11):

@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

view this post on Zulip Joe Hendrix (Apr 01 2021 at 17:21):

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.

view this post on Zulip Gabriel Ebner (Apr 01 2021 at 17:36):

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.

view this post on Zulip Daniel Selsam (Apr 01 2021 at 17:41):

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


Last updated: May 07 2021 at 13:21 UTC