RFC: coercion resolution

[leodemoura]

We currently use type class resolution to implement coercion resolution. The type classes are defined in the following file https://github.com/leanprover/lean/blob/master/library/init/coe.lean The resolution process is described in Section 10.6 at https://leanprover.github.io/theorem_proving_in_lean/

On top of that, we have the following two hacks/extensions.

1- A coercion from Prop to bool for decidable propositions. This is harded coded in the elaborator. So, it doesn't participate in the type class resolution process.

We cannot define this coercion as an instance of has_coe because the coercion from Prop to bool depends on the argument p : Prop. In the current approach, we cannot redefine the has_coe type classes, and allow dependencies on the input argument. Reason: the input argument usually contains several metavariables at coercion resolution time.

The current hack addresses this limitation by just checking whether the types are Prop and bool, and putting the decidable instance on the todo set for type class resolution.

2- By default coercion resolution is only fired if the types are know when the type mismatch was detected. However, there is an exception for monads. Given, an unification failure of the form

              M a =?= N ?m

where M and N are monads, we assign ?m := a and then try to find a coercion from M a to N a. This hack is used all the time when we are lifting tactics (from tactic to smt_tactic, and tactic to solver).

We can try to avoid this hack by adding has_coe (M a) (N ?m) to the type class resolution todo set, and assume the instance can eventually be synthesized. One potential drawback is weird error messages about failures to synthesize has_coe instances instead of a clear "type mismatch error".

We also have a list of pending features requested by users

1- Coercions C from T to function space are only used when the term of type T is used as a function. Example:

           f : T
           (f a)  -- Coercion C will be considered here

Users also want us to consider this kind of coercion when elaborating higher-order functions. Example:

           g : (nat -> nat) -> nat
           f : T
           C : has_coe_to_fun T

           g f   -- Coercion C is used here

This one is relatively easy to implement.

2- Backtrack when considering coercions from a type T to the function space. The user may have defined multiple coercions from T to the function space. They want the lean elaborator to trie all of them. Example.

           C1 : has_coe_to_fun T -- to nat -> nat
           C2 : has_coe_to_fun T -- to bool -> bool -> bool
           f  : T

           check f 10    -- uses C1
           check f tt tt -- uses C2

This one can be done too.

3- Coercions from a type T to a subtype {x : T // p x} We would need to invoke some tactic to synthesize a proof of p x.

Coercions from A to B using cast when we can synthesize a proof for A = B.

The main issue here is performance. If we allow type class resolution to invoke arbitrary tactics, then all caching infrastructure will have to be disabled. One option is to have a special kind of type class that allows this kind of dependency and caching is disabled for this new kind. In this way, we would be able to use the cache for type classes such as has_add, monoid, group, semiring, ... There is another problem, we often need to invoke type class resolution during unification. We would have to disable this feature for type classes that depend on tactics.

Another option is to implement coercion resolution using a tactic that can be extended by the user. The simplest way to extend the tactic is by adding has_coe instances. Recall that type class resolution is just backward chaining which is trivial to implement using tactics. We would be able to remove the current hacks from elaborator.cpp and embed them in the default tactic. We would also be able to avoid the auxiliary has_coe_t and has_lift_t used to "implement" transitive closure. In this approach, the function coe would be defined as

    def {u v} coe {α : Type u} {β : Type v} (a : α) (fn : α → β . mk_coe) := 
    fn a

where mk_coe is the tactic for synthesizing coercions. Note that the notation (fn : α → β . mk_coe) for "auto parameters" is already supported in 3.1.0

[avigad]

How does the last option interact with caching? Can user extensions decide whether it is safe to use the cache?

[leodemoura]

How does the last option interact with caching?

In last option, the system would not use any cache for coercions. We would rely on the fact that the number of coercions needed to elaborate a file is linear on the size of the file. The coercions are only introduced on terms that were "typed by the user".

Note that the same is not true for type class resolution. For example, when we execute simp or cc they generate many type class resolution problems.

Can user extensions decide whether it is safe to use the cache?

I think it would be tricky to trust they are not making mistakes. The problem is that a mistake here would affect other users.

[gebner]

The main issue here is performance. If we allow type class resolution to invoke arbitrary tactics, then all caching infrastructure will have to be disabled.

If I see this correctly, we could register tactics to be run during type class resolution without disabling the cache, it just wouldn't help us with coercions. We'd just need to run the tactic in a fresh tactic state that only depends on the environment.

We want coercions to be resolved even when the types have metavariables, but we don't want typeclass instances to be resolved when there are metavariables. It doesn't really fit into the out_param framework either. From that point of view, they need to do something different, so it seems reasonable to implement coercion resolution as a separate tactic. How would bootstrapping work? Is coercion only available after the tactic has been defined?

[leodemoura]

If I see this correctly, we could register tactics to be run during type class resolution without disabling the cache, it just wouldn't help us with coercions. We'd just need to run the tactic in a fresh tactic state that only depends on the environment.

There are two issues with this suggestion: 1- We often need access to the local context to be able to access local instances. If the fresh tactic state does not depend on it, type class resolution will fail. 2- Before reusing cached values, we make sure the reducibility annotations did not change nor the [instance] annotations. This is sufficient because the type class resolution code only depends on these two attributes. However, if we can run arbitrary tactics, this check is not sufficient anymore since we don't really know which attributes and/or evironment extensions the tactic depends on.

How would bootstrapping work? Is coercion only available after the tactic has been defined?

Yes, this would be the easy solution. I think we can survive without coercions until the tactic framework is defined.

[leodemoura]

At #1674, we are considering a new elaborator which maps syntax to expr. It will be a good opportunity to implement this issue.

[gebner]

I have just implemented feature request number one. (Apply to-function and to-sort coercion in function arguments.)

For completeness, I'd like to add the following feature request as well: to-function coercions where the type contains metavariables. I think this would just work with the tactics-based coercions:

structure isomorphism (A B : Type)
def identity {A} : isomorphism A A := ...
example := identity 5

I'm not entirely clear on the design of the tactics, though. If we didn't have transitivity, then it would be clear: we just have functions that take the given expression and the expected type, and potentially return a result. With transitivity, I think we need to start searching at one end and ignore the other. Something like the following, maybe?

/-- Takes an expression, and returns all possible one-step coercion results.  -/
meta def coe_handler := expr → tactic (list expr)

I think we need to start from the given expression in order to have a finitely branching search space. (There are infinitely many terms that can coerce into bool.) Even though this would break transitivity, maybe coe_handler should take an extra argument for the expected type so that we can do into-subtype coercion (i.e., feature request 3).

[leodemoura]

@gebner I'm trying to get back to Lean. I want to focus on other pending problems. It would be a big distraction for me a PR for this RFC.