🔬 model open vs closed world about chalk

[nikomatsakis]

cc @Garogolun -- you had expressed interest in this

[nikomatsakis]

My hope was that we could model this without touching the core solver. Roughly speaking my idea was to build on the notion of external types/traits that @lqd added in #86.

Let's posit that we have a External(Type) predicate that is true if the given type is external, and that we have a special OpenWorld domain goal (along with the existing, special CannotProve domain goal).

Then, during lowering, for each external trait like Iterator, maybe we define a program clause like this one:

forall<T> {
  Implemented(T: Iterator) :-
    OpenWorld,
    External(T),
    CannotProve
}

Now if we go to prove String: Iterator, we will neither fail nor succeed, but get back an ambiguos result (same with Not { String: Iterator }).

[nikomatsakis]

@Garogolun plans to hack on this!

[nikomatsakis]

cc @Garogolun -- I haven't heard from you, I think @sunjay is going to take a few steps here though.

[nikomatsakis]

OK, so. @sunjay, in terms of background reading, I would recommend RFC 1023, which covers the basic idea and rationale here.

It appears that we have already a field external that marks structs or traits:

https://github.com/rust-lang-nursery/chalk/blob/b953f83c81d6737d5f717a45fde6c6f212751a35/chalk-parse/src/ast.rs#L35-L37

We need to add a new kind of goal (actually, maybe two) that is like IsLocal(Ty) and IsLocal(TraitRef). Presumably that means adding variants to DomainGoal:

https://github.com/rust-lang-nursery/chalk/blob/b953f83c81d6737d5f717a45fde6c6f212751a35/src/ir/mod.rs#L504-L508

And then we need to add some rules into lowering for proving

For some struct S that is not marked as external, we would have:

forall<T> { IsLocal(S<T>). }

(Actually, we need a #[fundamental] tag too, but let's ignore that for now.)

For some trait ref like T: Trait, if the trait is not external, then there is a rule:

forall<T> {
  IsLocal(T: Trait)
}

If the trait is marked external, then it is local only if the types are local:

forall<T> {
  IsLocal(T: Trait) :- IsLocal(T)
}

We'll have to play with these rules, I haven't captured the full subtleties, but it's a start. =)

[sunjay]

@nikomatsakis I think this is completely done now. 🎉 😄