Better sort checking for constructors

[vrindisbacher]

Right now, the following fails:

use flux_rs::*;

#[flux::refined_by(start: T, end: T)]
struct Range<T> {
    #[flux::field(T[start])]
    pub start: T,
    #[flux::field(T[end])]
    pub end: T,
}

#[flux::sig(fn(r: Range<i32>{v: Range { start: 0, end: 1 } == v }))]
fn foo2(_r: Range<i32>) {}

Result:

  --> ../example.rs:11:33
   |
11 | #[flux::sig(fn(r: Range<i32>{v: Range { start: 0, end: 1 } == v }))]
   |                                 ^^^^^^^^^^^^^^^^^^^^^^^^^^ expected `?1s`, found constructor

A nice solution for this would be (from @nilehmann):

The nice solution for this problem is whenever we check Range { ... } against a sort s we unify it against Range<?1s> (for a fresh ?1s). And then check fields assuming ?1s . If s is Range<int> we will learn Range<?1s> = Range<int> ==> ?1s = int and consequently check fields against int. If s is ?0s we only learn ?0s = Range<?1s> and will check fields against ?1s.

[vrindisbacher]

Hey @nilehmann - I'm interested in taking a stab at this but I'm not really sure where to start. I'm assuming that this will happen when checking constructor's in wf/sortck?

I would imagine we need a case for when the expected sort is an inferred sort (after trying to resolve params)? i.e. something like:

if let rty::Sort::App(rty::SortCtor::Adt(sort_def), sort_args) = expected {
    let expected_def_id = sort_def.did();
    if let Some(path) = path {
        let path_def_id = match path.res {
            ExprRes::Struct(def_id) | ExprRes::Enum(def_id) => def_id,
            _ => span_bug!(expr.span, "unexpected path in constructor"),
        };
        if path_def_id != expected_def_id {
            return Err(self.emit_err(errors::SortMismatchFoundOmitted::new(
                path.span,
                expected.clone(),
            )));
        }
    } else {
        self.wfckresults
            .record_ctors_mut()
            .insert(expr.fhir_id, sort_def.did());
    }
    self.check_field_exprs(expr.span, sort_def, sort_args, field_exprs, spread, expected)?;
    Ok(())
} else if /* snip - expected is an inferred sort */ {
    //  Stuff above
} else {
    Err(self.emit_err(errors::UnexpectedConstructor::new(expr.span, expected)))
}

is that right?

[nilehmann]

This need a bit more design. We should meet. I'd also like to get @ranjitjhala input.

[vrindisbacher]

Cool - I'll be in today if you want to chat.

[ranjitjhala]

I'm around till noon at least.