has_coe_to_fun instance search

Stream: general

[Sebastien Gouezel]

While investigating the timeouts in #15078, @Frédéric Dupuis noticed that this was due to a weird instance search. Here is a mwe showing the behavior:

import analysis.normed_space.basic
variables {α : Type}

set_option trace.class_instances true

lemma wtf (A : set (set α)) (a : A) : true :=
begin
  have : (a : set α) = a := rfl,
  have : (a : set α) = a := rfl,
  trivial
end

If you put the cursor on the first have keyword in the proof, you will see that Lean goes on a wild hunt to find a has_coe_to_fun instance for the subtype ↥A. And of course fails. The instance search starts with

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_5 : has_coe_to_fun ↥A ?x_4 := @continuous_linear_equiv.has_coe_to_fun ?x_6 ?x_7 ?x_8 ?x_9 ?x_10 ?x_11 ?x_12 ?x_13 ?x_14 ?x_15 ?x_16 ?x_17 ?x_18 ?x_19
  ?x_20
  ?x_21
failed is_def_eq
[class_instances] (0) ?x_5 : has_coe_to_fun ↥A ?x_4 := @continuous_linear_map.to_fun ?x_22 ?x_23 ?x_24 ?x_25 ?x_26 ?x_27 ?x_28 ?x_29 ?x_30 ?x_31 ?x_32 ?x_33 ?x_34
failed is_def_eq

There are two things I don't understand here: first, why does the system look for a has_coe_to_fun instance? And second, why doesn't it cache the failure? (You can look at the instance search trace on the second have, it is just as long as for the first one). @Gabriel Ebner , do you have some ideas?

In such a short proof, it's not a real problem, but in a longer proof it makes things really really slow!

[Kyle Miller]

For type ascriptions, when there's a type mismatch the elaborator will eventually get to this line https://github.com/leanprover-community/lean/blob/master/src/frontends/lean/elaborator.cpp#L675

It checks the weak head normal form of the expected type to see if it's a pi type. And in this case, set α is a pi type, so it appears to make a go at it!

At least, this is what I think is happening. One test would be to create a version of set that's a structure to see if it avoids this behavior.

[Kyle Miller]

It might seem inconsistent that the typeclass inference starts with has_coe_to_fun ↥A ?x_4 (with a metavariable at the expected type) but mk_coercion_to_fn doesn't take an expected type and it uses inference to infer the resulting type. Maybe this metavariable is why the instance failure isn't cached? (I don't know how the cache works.)

[Sebastien Gouezel]

Thanks for the explanations, they're very convincing. I'm not sure why it doesn't use the expected type, though (and of course set shouldn't be considered a pi type to start with...)

[Kyle Miller]

A quick hack would be to tell the elaborator to not consider set to be a pi type when looking for coercions. I'm not sure if that's principled enough of a design...

[Kyle Miller]

Sebastien Gouezel said:

I'm not sure why it doesn't use the expected type, though

I think I get why -- when you have (a : X) you are happy if a coerces to something that has a type defeq to X, but if you give typeclass inference X then it'll force it to find something that's syntactically X.