dot notation and typeclasses

Stream: general

[Sebastien Gouezel]

In #13179, I change the definition of monotone to require has_le instead of preorder. This breaks some uses of dot notation, as you can see from the log:

type mismatch at application
    (function.monotone_eval a).mem_upper_bounds_image
  term
    function.monotone_eval a
  has type
    monotone (function.eval a)
  but is expected to have type
    monotone ?m_5

I can fix those, sure, but I don't understand why this makes a difference. Any idea?

[Eric Wieser]

I think dot notation forces the argument to be fully unified before resolving the rest of the expression

[Eric Wieser]

If you add a type annotation inside the parens before applying the dot notation, does it work?

[Kyle Miller]

The key part of the error message that suggests Eric is right is "switched to simple application elaboration procedure because failed to use expected type to elaborate it." I think the simple elaboration procedure also has some bugs when it comes to dot notation, inserting arguments into the wrong places, but I haven't looked too deeply into that.

[Yaël Dillies]

Yeah I already tried to make this work and stopped because I wanted to keep dot notation working.