Stream: wg-traits

Topic: program-clauses callback


nikomatsakis (Oct 08 2018 at 19:28, on Zulip):

@scalexm ok, carry on :)

scalexm (Oct 08 2018 at 19:28, on Zulip):

if I try to call self.infcx.tcx.program_clauses_for_env(*environment); I get a compile error: "argument requires that 'tcx must outlive 'gcx"

scalexm (Oct 08 2018 at 19:28, on Zulip):

I don't understand why

nikomatsakis (Oct 08 2018 at 19:29, on Zulip):

can I see the diff maybe?

nikomatsakis (Oct 08 2018 at 19:29, on Zulip):

I'm guessing though it's because program_clause_for_env is a query, and hence the environment must be a ty::ParamEnv<'gcx>?

nikomatsakis (Oct 08 2018 at 19:29, on Zulip):

in effect

nikomatsakis (Oct 08 2018 at 19:29, on Zulip):

(is it a query?)

nikomatsakis (Oct 08 2018 at 19:30, on Zulip):

in any case the signature is:

crate fn program_clauses_for_env<'a, 'tcx>(
    tcx: TyCtxt<'a, 'tcx, 'tcx>,
    param_env: ty::ParamEnv<'tcx>,
) -> Clauses<'tcx> {
nikomatsakis (Oct 08 2018 at 19:30, on Zulip):

in particular TyCtxt<'a, 'tcx, 'tcx> seems like it would cause this problem

nikomatsakis (Oct 08 2018 at 19:30, on Zulip):

(to start, we might even just forego having it be a query)

scalexm (Oct 08 2018 at 19:30, on Zulip):

https://github.com/rust-lang/rust/compare/master...scalexm:program-clauses

nikomatsakis (Oct 08 2018 at 19:31, on Zulip):

yeah, ok, so that is the problem

nikomatsakis (Oct 08 2018 at 19:31, on Zulip):

usually what we do is to canonicalize the query key

scalexm (Oct 08 2018 at 19:31, on Zulip):

why the argument should be ty::ParamEnv<'gcx>?

nikomatsakis (Oct 08 2018 at 19:32, on Zulip):

well, it's a bit confusing because of our convention

nikomatsakis (Oct 08 2018 at 19:32, on Zulip):

that is, in the signature above, there is no 'gcx

nikomatsakis (Oct 08 2018 at 19:32, on Zulip):

so in that case 'tcx refers to the global arena

scalexm (Oct 08 2018 at 19:32, on Zulip):

ok

nikomatsakis (Oct 08 2018 at 19:32, on Zulip):

in particular you see TyCtxt<'_, 'tcx, 'tcx>

nikomatsakis (Oct 08 2018 at 19:32, on Zulip):

the second argument is the 'global lifetime'

nikomatsakis (Oct 08 2018 at 19:32, on Zulip):

by setting both the same, we force 'tcx to be the global lifetime

nikomatsakis (Oct 08 2018 at 19:32, on Zulip):

if it were TyCtxt<'_, '_, 'tcx> that would not be the case

nikomatsakis (Oct 08 2018 at 19:33, on Zulip):

but queries only operate on global data

scalexm (Oct 08 2018 at 19:33, on Zulip):

ah yeah ok

nikomatsakis (Oct 08 2018 at 19:33, on Zulip):

since the caches don't want to be tied to some particular inference step

scalexm (Oct 08 2018 at 19:33, on Zulip):

right

scalexm (Oct 08 2018 at 19:33, on Zulip):

indeed a TyCtxt<'_, 'gcx, 'gcx> naming convention would be less confusing I guess :)

nikomatsakis (Oct 08 2018 at 19:33, on Zulip):

anyway we could just make it not a query for now, or we can canonicalize the key — we could even just "lift" the key for now

nikomatsakis (Oct 08 2018 at 19:33, on Zulip):

indeed a TyCtxt<'_, 'gcx, 'gcx> naming convention would be less confusing I guess :)

yes

nikomatsakis (Oct 08 2018 at 19:34, on Zulip):

in practice, the param env at present is always going to be global

nikomatsakis (Oct 08 2018 at 19:34, on Zulip):

that won't always be true

nikomatsakis (Oct 08 2018 at 19:34, on Zulip):

once we want to support implication goals

scalexm (Oct 08 2018 at 19:34, on Zulip):

ok so just lift should work for now

nikomatsakis (Oct 08 2018 at 19:34, on Zulip):

but yeah for now we could do self.tcx.lift_to_global(param_env).unwrap()

nikomatsakis (Oct 08 2018 at 19:34, on Zulip):

and once we get to implication goals, we'll notice :)

scalexm (Oct 08 2018 at 19:34, on Zulip):

ok, so second problem comes with the contents of ParamEnv

scalexm (Oct 08 2018 at 19:35, on Zulip):

if we'd like to have implied bounds from types, it should somehow include the input types

nikomatsakis (Oct 08 2018 at 19:35, on Zulip):

(canonicalizing would possibly be better, of course, since it would equate various regions)

nikomatsakis (Oct 08 2018 at 19:35, on Zulip):

right so it needs something like WellFormed(T)?

scalexm (Oct 08 2018 at 19:35, on Zulip):

yes, so currently ParamEnv carries the "rustc-style" predicates

nikomatsakis (Oct 08 2018 at 19:36, on Zulip):

(oh, that reminds me that we were going to talk about chalk#176)

scalexm (Oct 08 2018 at 19:36, on Zulip):

e.g. ty::TraitPredicate etc

nikomatsakis (Oct 08 2018 at 19:36, on Zulip):

right right

nikomatsakis (Oct 08 2018 at 19:36, on Zulip):

I mean we have a WellFormed predicate but

nikomatsakis (Oct 08 2018 at 19:37, on Zulip):

it may or may not make sense to try and "split" into a new-style predicate, I guess?

nikomatsakis (Oct 08 2018 at 19:37, on Zulip):

is that what you are thinking?

scalexm (Oct 08 2018 at 19:37, on Zulip):

yes

nikomatsakis (Oct 08 2018 at 19:37, on Zulip):

basically make DomainGoal and Goal

nikomatsakis (Oct 08 2018 at 19:37, on Zulip):

in rustc

nikomatsakis (Oct 08 2018 at 19:38, on Zulip):

instead of re-using ty::Predicate as DomainGoal (is that what we do now?)

nikomatsakis (Oct 08 2018 at 19:38, on Zulip):

we already have Goal obviously

scalexm (Oct 08 2018 at 19:38, on Zulip):

well the only thing I need right now is for program_clauses_for_env to compute the correct set of rules coming from the environment

scalexm (Oct 08 2018 at 19:38, on Zulip):

so currently program_clauses_for_env just uses def ids it finds in the rustc-style predicates

nikomatsakis (Oct 08 2018 at 19:39, on Zulip):

hmm

nikomatsakis (Oct 08 2018 at 19:39, on Zulip):

maybe we should modify the input to that

nikomatsakis (Oct 08 2018 at 19:40, on Zulip):

well anyway neither here nor there

nikomatsakis (Oct 08 2018 at 19:40, on Zulip):

(e.g., to be a BTreeSet<DefId> or something)

nikomatsakis (Oct 08 2018 at 19:40, on Zulip):

seems like an ungreat idea

nikomatsakis (Oct 08 2018 at 19:40, on Zulip):

well the only thing I need right now is for program_clauses_for_env to compute the correct set of rules coming from the environment

are you saying the WF question can wait?

scalexm (Oct 08 2018 at 19:41, on Zulip):

not exactly, I was just thinking that indeed we could add ty::WellFormed(T) to the ParamEnv and then program_clauses_for_env would find the correct def ids from that =)

scalexm (Oct 08 2018 at 19:41, on Zulip):

but definitely not the cleanest way :p

nikomatsakis (Oct 08 2018 at 19:42, on Zulip):

maybe I was confused

nikomatsakis (Oct 08 2018 at 19:42, on Zulip):

what def-ids does it need to find

nikomatsakis (Oct 08 2018 at 19:43, on Zulip):

ah, I guess you mean it would find the def-ids of the types

scalexm (Oct 08 2018 at 19:43, on Zulip):

yes sorry

nikomatsakis (Oct 08 2018 at 19:43, on Zulip):

and we would use some query or other to get the WF reverse rules there?

scalexm (Oct 08 2018 at 19:43, on Zulip):

yes we basically just call program_clauses_for(def_id)

nikomatsakis (Oct 08 2018 at 19:43, on Zulip):

I see

scalexm (Oct 08 2018 at 19:43, on Zulip):

so if def_id refers to a type, we get the wanted implied bounds

nikomatsakis (Oct 08 2018 at 19:43, on Zulip):

well that does make sense

nikomatsakis (Oct 08 2018 at 19:44, on Zulip):

I'm a bit nervous about adding new things into the param env

nikomatsakis (Oct 08 2018 at 19:44, on Zulip):

I guess we could gate it in on -Zchalk or something

nikomatsakis (Oct 08 2018 at 19:44, on Zulip):

I'm not really sure what would go wrong, tbh

scalexm (Oct 08 2018 at 19:44, on Zulip):

yeah probably

nikomatsakis (Oct 08 2018 at 19:44, on Zulip):

that won't work across crates

scalexm (Oct 08 2018 at 19:48, on Zulip):

maybe we could, for now, use a new ParamEnv type

nikomatsakis (Oct 08 2018 at 19:48, on Zulip):

we could

nikomatsakis (Oct 08 2018 at 19:48, on Zulip):

it would sort of go along with moving away from Predicate

nikomatsakis (Oct 08 2018 at 19:48, on Zulip):

basically build up a "parallel" system

scalexm (Oct 08 2018 at 19:48, on Zulip):

yes

nikomatsakis (Oct 08 2018 at 19:49, on Zulip):

Predicate isn't a great fit, seeing as it has binders at each step etc

nikomatsakis (Oct 08 2018 at 19:49, on Zulip):

we'd have to encode this stuff in metadata, or else just recompute them on the fly from other metadata things

scalexm (Oct 08 2018 at 19:49, on Zulip):

yes and I don't think that we can easily replace it with the binders at the root instead of at the leafs

nikomatsakis (Oct 08 2018 at 19:49, on Zulip):

but encoding in metadata isn't that hard

scalexm (Oct 08 2018 at 19:51, on Zulip):

also actually the program_clauses callback is quite simple after all

scalexm (Oct 08 2018 at 19:52, on Zulip):

even the naive version I wrote seems good already, the worst thing it does is running over all impls for a given trait

nikomatsakis (Oct 08 2018 at 19:52, on Zulip):

seems good

scalexm (Oct 08 2018 at 20:03, on Zulip):

ok then I think I'll be tackling the new ParamEnv thing to start with

scalexm (Oct 08 2018 at 20:08, on Zulip):

while we're at it, I see that there is a add_clauses callback which should add clauses to the environment

scalexm (Oct 08 2018 at 20:08, on Zulip):

so I guess this new ParamEnv should have some form of mutability

scalexm (Oct 08 2018 at 20:08, on Zulip):

(in contrast with the existing one)

nikomatsakis (Oct 08 2018 at 20:09, on Zulip):

well

nikomatsakis (Oct 08 2018 at 20:10, on Zulip):

that is used for the A => B goals

nikomatsakis (Oct 08 2018 at 20:10, on Zulip):

we could make it "in place" mutable potentially

nikomatsakis (Oct 08 2018 at 20:10, on Zulip):

we could also just "re-intern" the new set

scalexm (Oct 09 2018 at 13:19, on Zulip):

@nikomatsakis I'm wondering whether we might need a more fine-grained way of retrieving the clauses for something

scalexm (Oct 09 2018 at 13:19, on Zulip):

currently the only thing we have is program_clauses_for(def_id)

scalexm (Oct 09 2018 at 13:20, on Zulip):

but for example, in program_clauses_for_env, the only clauses we care about are those of the form ... :- FromEnv(...)

scalexm (Oct 09 2018 at 13:20, on Zulip):

conversely if I want to prove for example WellFormed(Self: Trait), I don't care about all the clauses of the form ... :- FromEnv(...)

scalexm (Oct 09 2018 at 13:23, on Zulip):

basically I'm currently changing chalk integration to using a new type Environment<'tcx> instead of ParamEnv<'tcx>, which just consists in a list of Clause<'tcx>

scalexm (Oct 09 2018 at 13:24, on Zulip):

and I'm reluctant to continue with the approach "just find every def_id appearing in the list of clauses and call program_clauses_for(def_id)" in program_clauses_for_env

scalexm (Oct 09 2018 at 13:26, on Zulip):

basically I fear that we would add too much useless clauses and that the computed set would be really big

nikomatsakis (Oct 09 2018 at 13:46, on Zulip):

I think I expected to refine it at some point, yes

nikomatsakis (Oct 09 2018 at 13:46, on Zulip):

I was expecting to even take into account "simplified" types and the like

nikomatsakis (Oct 09 2018 at 13:47, on Zulip):

though of course we could move some of that logic into chalk-engine instead

nikomatsakis (Oct 09 2018 at 13:47, on Zulip):

maybe it makes sense to do some of that sooner rather than later

scalexm (Oct 09 2018 at 13:48, on Zulip):

I think we should at least separate different forms of clauses for now

scalexm (Oct 09 2018 at 13:48, on Zulip):

I propose that we somehow "tag" them

scalexm (Oct 09 2018 at 13:49, on Zulip):

basically there would be three categories, "implied bounds", "well formed" and "other"

scalexm (Oct 09 2018 at 13:49, on Zulip):

we keep the program_clauses_for(...) but we can filter on the tag before passing them to chalk-engine

nikomatsakis (Oct 09 2018 at 13:51, on Zulip):

I see

nikomatsakis (Oct 09 2018 at 13:51, on Zulip):

that seems good

Last update: Nov 12 2019 at 16:55UTC