This is necessary for Dafny 4.3 and higher, as Dafny no longer adds this method on reference types. The explicit construction of the right kind of TypeDescriptor (which works both before and after 4.3) was already implemented for other shapes in typeDescriptor(ShapeId), so I just tweaked the case identification, and scoped the default case more explicitly to shapes we know it works for, and now raise an exception for unrecognized shape types.
Description of changes:
This is necessary for Dafny 4.3 and higher, as Dafny no longer adds this method on reference types. The explicit construction of the right kind of TypeDescriptor (which works both before and after 4.3) was already implemented for other shapes in
typeDescriptor(ShapeId), so I just tweaked the case identification, and scoped the default case more explicitly to shapes we know it works for, and now raise an exception for unrecognized shape types.Unfortunately not covered by any TestModels (which is why #301 didn't fix this as well), but tested on MPL: https://github.com/aws/aws-cryptographic-material-providers-library/pull/195
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.