Investigate dependent refinements

[W95Psp]

What would it take to allow dependent refinement in (1) function inputs (2) function outputs (3) let bindings.

[W95Psp]

For now I came up with something like this, but that's not OK, we want to be able to refine nested types (ie a slice of refined something)

#[hax_lib::define_named_refinement]
fn NamedRefinement(x: u8, limit: usize) -> bool { x < limit }

#[hax_lib::attributes]
fn f(limit: Refine<u8, {x < 50}>, x: Refine<NamedRefinement<limit>>) {}


// WOULD DESUGAR TO:
macro_rules! NamedRefinement {
    (type) => {
        u8
    },
    (refinement, $x:expr, $limit:expr) => {
        $x < $limit
    }
}

#[_hax::refinement(arg 0: limit < 50)]
#[_hax::refinement(arg 1: NamedRefinement!(refinement, limit, x))]
fn f(limit: u8, x: u8) {
    
}

To have nested refinement types, we could use type synonym and a marker RefinementMarker type, that would be indexed by both it's inner type and an index.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[W95Psp]

I think we should still aim at those refinements on specific places. Let's keep this open for now.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[github-actions[bot]]

This issue has been closed due to a lack of activity since being marked as stale. If you believe this issue is still relevant, please reopen it with an update or comment.

[W95Psp]

I think this is still something we want to chat about