"warning: dynamic type predicate ignored (not yet supported)" is the precise message
Yeah, I hope that they will be in the next edition.
SPARK GPL 2015 introduced ghost code, which is great.
It's just a shame that I have to wait another year :)
There are ways of working around it though. Mainly by adding preconditions/postconditions onto the subprograms which use the type, but it's really ugly.
And adds a burden onto other code which use the subprograms.