Proof failure when deconstructing nested types

[sonmarcho]

I get an error when trying to deconstruct types in an assignment, in the presence of type aliases.

datatype Value = Value_

datatype Wrapper<A> = | Wrap(ret: A)

// We need to use an alias for the inner type
type Alias<A> = Wrapper<A>

// Using a match works
lemma Test1(res: Wrapper<Alias<Value>>)
{
  match res {
    case Wrap(Wrap(v)) => {}
  }
}

// Not using an alias type works
lemma Test2(res: Wrapper<Wrapper<Value>>)
{
  var Wrap(Wrap(v)) := res;
}

// Replacing `Value` with a type parameter works
lemma Test3<T>(res: Wrapper<Alias<T>>)
{
  var Wrap(Wrap(v)) := res;
}

// This doesn't work
lemma Test4(res: Wrapper<Alias<Value>>)
{
  // "Error: value does not satisfy the subset constraints of 'Value'"
  //           VVV
  var Wrap(Wrap(v)) := res;
}

[MikaelMayer]

Interestingly, if you add an intermediate variable, it works:

var Wrap(unwrapped) := res;
  var Wrap(v) := unwrapped;

But otherwise this is clearly a bug.