Beef up infer-mut-hack

[ranjitjhala]

(To avoid it getting "confused" be extraneous Constr)

[nilehmann]

@ranjitjhala

We already have Ty::unconstr which is a more general version of this.

[ranjitjhala]

Interesting -- didn't know about it!

But, not really, replacing

let ty = SkipConstr.fold_ty(ty);

with

 let (ty, _) = ty.unconstr();

Doesn't seem to work -- looks like unconstr is not "deep": it expects the Constr at the very top?

[ranjitjhala]

Looks like unconstr just peels away all the "topmost" Constr -- the moment it hits something else it stops.

So it won't work with

#[flux::sig(fn (xs: &mut { [i32][@n] | n > 1}))]
fn lib1(_xs: &mut [i32]) {}

[nilehmann]

You first need to match on the &mut T and then unconstr the T

 if let rty::Ref!(_, deref_ty, Mutability::Mut) = ty.kind()
    && let (deref_ty, _) = deref_ty.unconstr()
    && let TyKind::Indexed(..) = inner_ty.kind()

I wonder though if there's a clean way to handle this during canonicalization (the thing unpack is implementing on top of). It is always safe to turn an &mut {T | p} into {&mut T | p} so we could get rid of it during unpack

[ranjitjhala]

This is why I have two tests -- the other one flips the order which fails your method

#[flux::sig(fn (xs: &mut { [i32][@n] | n > 1}))]
fn lib1(_xs: &mut [i32]) {}

#[flux::sig(fn (xs: { &mut  [i32][@n] | n > 1}))]
fn lib2(_xs: &mut [i32]) {}

But yes, if you had canonicalized presumably lib1 gets turned into lib2?

[nilehmann]

ah yeah, you'd need to unconstr twice

let (ty, _) = ty.unconstr();
if let rty::Ref!(_, deref_ty, Mutability::Mut) = ty.kind() 
    && let (deref_ty, _) = deref_ty.unconstr() 
    && let TyKind::Indexed(..) = inner_ty.kind()

I still think there has to be a nice way in which we can canonicalize types before pattern matching on them. The canonicalize infra is almost there...