Skip to content

opaque type universal args cannot depend on member constraints #16

Open
@lcnr

Description

@lcnr
#[derive(Copy, Clone)]
struct Inv<'a>(*mut &'a ());
fn mk<'a>() -> Inv<'a> {
    loop {}
}

fn scope<'a, 'b, 'c>(
    a: Inv<'a>,
    b: Inv<'b>,
    c: Inv<'c>,
) -> (impl Sized + use<'c>, impl Sized + use<'a, 'b>) {
    loop {
        let _0 = mk();
        let _1 = mk();
        // small: opaque1<'b>
        // big: opaque2<'a, '0>
        let (mut small, mut big) = scope(a, _0, b);
        // opaque1<'b> = Inv<'0>
        // member constraint DOES NOT equate '0 with 'b
        // it only adds 'b to the region value of '0
        small = _0;
        // opaque2<'a, '0> = Inv<'1>;
        // when checking whether an arg is universal we first
        // check whether its scc representative is a free region.
        big = a;
    }
    scope(a, b, c)
}

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions