preliminary model for "opaque types" where hidden types are known

[nikomatsakis]

The goal here is to model Rust's impl Trait. For now the starting plan is to have a version where chalk is given both the opaque type declaration and the hidden type:

opaque type T<..>: Bounds = HiddenTy;

Note that opaque types can be generic.

We will model opaque types as an special kind of alias. Like associated types aliases, when an opaque type alias T is equated with some other type U, we will generate an AliasEq(T = U) goal.

The difference is that the two clauses for AliasEq goals work a bit differently. In particular, the "normalization" rule requires a special goal, Reveal, to be in the environment:

AliasEq(T = HiddenTy) :- Reveal.

AliasEq(T = !T).

There are also special rules for the !T placeholder:

Implemented(!T: Bounds). // from the declaration

// for auto traits:
Implemented(!T: AutoTrait) :- Implemented(HiddenTy: AutoTrait).

[nikomatsakis]

Let's create a check-list of details to take care of

(edit: checklist moved by detrumi to keep it updated)

[flodiebold]

(@flodiebold do you have an example test?)

How about this (comment in the require_send line to cause a cycle)?

[detrumi]

Checklist

• Add syntax for testing (Implement Impl Trait #324)
• Check that, without reveal, we can prove that the bounds are true but not other things (Implement Impl Trait #324)
• Cleanup debug output for impl traits (Improve opaque type debug output #400)
• Add tests for generic opaque types like type Foo<X> = impl Iterator<Item = X> (Opaque Type Generics #464)
• Generate clauses for auto traits (Generate auto trait clauses for opaque type goals #468)
• Check that, without reveal, we can prove that auto-traits hold if they hold for hidden type (Generate auto trait clauses for opaque type goals #468)
• Check that, with reveal, we can prove equality and also prove all trait bounds we need to prove
• Extend so that the hidden type is lazily accessed -- this is needed to permit cyclic dependencies in cases where we don't need to prove that $T: Send, which rustc apparently supports (Request hidden opaque types lazily #478)
• Extend with support for "where clauses" (Support where clauses on opaque types #563)
• Add well-formedness checking rules for the definition (must prove that the hidden type implements the required bounds, assuming the where clauses) (Check well-formedness of opaque type declarations #579)
• Document opaque types in the chalk book (document opaque types #559)
• Extend WF rules for implied bounds interactions

(moved the checklist to my own comment to avoid "nikomatsakis mentioned ..." messages when editing the checklist to refer to PRs)

[detrumi]

Only one task left: extend WF rules for implied bounds interactions. I can't quite remember what we meant with that, but I think it's something along these lines:

Given this program:

trait Clone { }
trait Iterator where Self: Clone { type Item; }
struct Struct { }
struct Ty { }

opaque type O: Iterator<Item = Struct> = Ty;

Using implied bounds, this can prove the following (see the implied_bounds test):

forall<T> {
    if (T: Iterator<Item = Struct>) {
        T: Clone
    }
}

The same should hold for opaque types, but doesn't:

if (Reveal) {
    O: Clone
}

We might be missing some more WF checks around opaque types, since the program above fails to prove the goal, but only does the WF check once you add impl Iterator for Ty {} (then it fails with "opaque type declaration O does not meet well-formedness requirements")