Issues with extension and pretty printer

[nilehmann]

I found a couple of issues with the extension when trying the following (note that you need to save without running rustfmt)

#[flux::sig(fn(c: Option<bool>) -> Option<i32{v:0 <= v}>)]
pub fn test0(c: Option<bool>) -> Option<i32> {
    c.map(|b| 
        if b { 
            1 
        } else { 
            2 
        }
    )
}

Type with no indices has confusing formatting

As shown in the image, Option is pretty printed as Option<λb0. bool[b0]>[{..}] . I find the ellipsis confusing because Option has no indices so there's nothing to expand (or rather it is indexed by a unit sort). I think we should show it as Option<λb0. bool[b0]> (I'm not worried about the lambda here, but we can discuss that)

The extension shows trace data from the shape phase

As shown below, the extension shows a hole (i.e., *) as part of the constraints which indicates it is not filtering out the trace data coming from the shape phase (related to #916)

[ranjitjhala]

Btw, what is the relevance of rustfmt here?

[nilehmann]

If you run rustfmt on save everything is collapsed in one line so you can't put the cursor inside the closure to get the behavior.