Zulip Chat Archive

Stream: general

Topic: help with the `delta_instance` derive handler


view this post on Zulip 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}

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Apr 20 2020 at 01:54):

However in this example inst.collect_univ_params returns [].

view this post on Zulip Mario Carneiro (Apr 20 2020 at 01:56):

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

view this post on Zulip Scott Morrison (Apr 20 2020 at 01:57):

Ah, okay.

view this post on Zulip Scott Morrison (Apr 20 2020 at 01:58):

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

view this post on Zulip Scott Morrison (Apr 20 2020 at 01:58):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Apr 20 2020 at 01:58):

Or am I doomed?

view this post on Zulip Scott Morrison (Apr 20 2020 at 01:58):

Sounds like I'm not doomed. :-)

view this post on Zulip Mario Carneiro (Apr 20 2020 at 01:59):

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

view this post on Zulip 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 ...

view this post on Zulip Scott Morrison (Apr 20 2020 at 01:59):

great.

view this post on Zulip Mario Carneiro (Apr 20 2020 at 01:59):

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

view this post on Zulip Scott Morrison (Apr 20 2020 at 02:01):

How are universe metavariables represented in an expr?

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Apr 20 2020 at 02:03):

I see, there's level.mvar.

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Apr 20 2020 at 02:11):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Apr 20 2020 at 02:37):

Okay, I'll investigate, thanks!

view this post on Zulip Scott Morrison (Apr 20 2020 at 02:37):

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

view this post on Zulip Mario Carneiro (Apr 20 2020 at 02:38):

same as it does for expr

view this post on Zulip Mario Carneiro (Apr 20 2020 at 02:38):

metavariables are assigned to make them equal

view this post on Zulip 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

view this post on Zulip Simon Hudon (Apr 20 2020 at 02:39):

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

view this post on Zulip Scott Morrison (Apr 20 2020 at 02:39):

Oh!

view this post on Zulip Scott Morrison (Apr 20 2020 at 02:45):

Hooray, problem solved!

view this post on Zulip Scott Morrison (Apr 20 2020 at 02:45):

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

view this post on Zulip Scott Morrison (Apr 20 2020 at 03:20):

#2463


Last updated: May 08 2021 at 09:11 UTC