Stream: general

Topic: help with the delta_instance derive handler

Scott Morrison (Apr 20 2020 at 01:53):

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 (Apr 20 2020 at 01:54):

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 (Apr 20 2020 at 01:54):

However in this example inst.collect_univ_params returns [].

Mario Carneiro (Apr 20 2020 at 01:56):

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

Ah, okay.

Scott Morrison (Apr 20 2020 at 01:58):

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

Scott Morrison (Apr 20 2020 at 01:58):

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

Mario Carneiro (Apr 20 2020 at 01:58):

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

Or am I doomed?

Scott Morrison (Apr 20 2020 at 01:58):

Sounds like I'm not doomed. :-)

Mario Carneiro (Apr 20 2020 at 01:59):

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

Scott Morrison (Apr 20 2020 at 01:59):

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

great.

Mario Carneiro (Apr 20 2020 at 01:59):

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

Scott Morrison (Apr 20 2020 at 02:01):

How are universe metavariables represented in an expr?

Scott Morrison (Apr 20 2020 at 02:02):

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

Scott Morrison (Apr 20 2020 at 02:03):

I see, there's level.mvar.

Scott Morrison (Apr 20 2020 at 02:05):

@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 (Apr 20 2020 at 02:11):

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

Scott Morrison (Apr 20 2020 at 02:12):

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 (Apr 20 2020 at 02:13):

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 (Apr 20 2020 at 02:32):

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 (Apr 20 2020 at 02:33):

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

Scott Morrison (Apr 20 2020 at 02:37):

Okay, I'll investigate, thanks!

Scott Morrison (Apr 20 2020 at 02:37):

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

Mario Carneiro (Apr 20 2020 at 02:38):

same as it does for expr

Mario Carneiro (Apr 20 2020 at 02:38):

metavariables are assigned to make them equal

Mario Carneiro (Apr 20 2020 at 02:39):

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 (Apr 20 2020 at 02:39):

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

Oh!

Scott Morrison (Apr 20 2020 at 02:45):

Hooray, problem solved!

Scott Morrison (Apr 20 2020 at 02:45):

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

Scott Morrison (Apr 20 2020 at 03:20):

#2463

Last updated: May 08 2021 at 09:11 UTC