help with the `delta_instance` derive handler

Stream: general

[Scott Morrison]

I'm failing to use the delta_instance derive handler. In particular, here's the MWE:

import algebra.category.Mon.basic

open category_theory

set_option formatter.hide_full_terms false
set_option pp.all true

attribute [derive large_category] Mon

This correctly finds the instance it wants, but fails to add the declaration with the error message:

failed to add declaration 'Mon.large_category_1' to environment, type has metavariables
  category_theory.large_category.{?l_1} Mon.{?l_1}

[Scott Morrison]

I can see that delta_instance looks for the universe parameters in the instance it has found, using inst.collect_univ_params, and passes those to add_decl, so I'd hoped that would cover this situation.

[Scott Morrison]

However in this example inst.collect_univ_params returns [].

[Mario Carneiro]

The issue might be that there are free universe metavariables, not free universe variables

[Scott Morrison]

Ah, okay.

[Scott Morrison]

Because we're in category theory land, and there's an undetermined universe...

[Scott Morrison]

So it this something I can fix, by constructing new universe variables and substituting?

[Mario Carneiro]

hopefully there is a similar function for collecting universe metavariables? If not, it's not hard to write

[Scott Morrison]

Or am I doomed?

[Scott Morrison]

Sounds like I'm not doomed. :-)

[Mario Carneiro]

Once you have the list of metavariables, you can just create fresh universe names and substitute

[Scott Morrison]

But is that the general idea? I collect the universe metavariables, for each one unify with a fresh ...

[Scott Morrison]

great.

[Mario Carneiro]

that's what lean does whenever you use things like Type*

[Scott Morrison]

How are universe metavariables represented in an expr?

[Scott Morrison]

They must be either expr.mvar of a special variety, or expr.sort with some special variety of level?

[Scott Morrison]

I see, there's level.mvar.

[Scott Morrison]

@Simon Hudon, do you know if there's anything existing in tactic.core that replaces all universe metavariables in an expression with fresh universe variables?

[Scott Morrison]

I guess I don't understand how the unification step is meant to happen here.

[Scott Morrison]

If I have a level.mvar, what do I replace it with? And how? I guess I have to build a new level.param for each, with a mk_fresh_name. But then do I have to traverse the expression myself replacing level.mvars with level.params by hand?

[Scott Morrison]

I see the built-in function expr.instantiate_univ_params, but that seems to be for replacing level.params, not replacing level.mvars.

[Simon Hudon]

You can use these functions to enumerate all the level mvar:

open expr

namespace level

meta def fold_mvar {α} : level → (name → α → α) → α → α
| zero f := id
| (succ a) f := fold_mvar a f
| (param a) f := id
| (mvar a) f := f a
| (max a b) f := fold_mvar a f ∘ fold_mvar b f
| (imax a b) f := fold_mvar a f ∘ fold_mvar b f

end level


namespace expr

meta def collect_meta_univ (e : expr) : list name :=
native.rb_set.to_list $ e.fold native.mk_rb_set $ λ e' i s,
match e' with
| (sort u) := u.fold_mvar (flip native.rb_set.insert) s
| (const _ ls) := ls.foldl (λ s' l, l.fold_mvar (flip native.rb_set.insert) s') s
| _ := s
end

end expr

[Simon Hudon]

You create a new level.param for each and unify them with the variables to assign to them

[Scott Morrison]

Okay, I'll investigate, thanks!

[Scott Morrison]

I don't understand what unification means for level, however.

[Mario Carneiro]

same as it does for expr

[Mario Carneiro]

metavariables are assigned to make them equal

[Mario Carneiro]

In this case it would be more convenient to just have a metavariable assignment API, but I don't think one is exposed

[Simon Hudon]

And you can use unify (sort u) (sort u') to make the assignment

[Scott Morrison]

Oh!

[Scott Morrison]

Hooray, problem solved!

[Scott Morrison]

Thanks, @Mario Carneiro and @Simon Hudon, PR on its way.

[Scott Morrison]

#2463