Error: value does not satisfy subset constraints of T

The error “value does not satisfy subset constraints of T” for some type name T arises when a value is trying to be converted to a subset type T, and the value cannot be proved to satisfy the predicate that defines the subset type.

This is pretty clear when one is trying to assign, say an int to a nat, but is more complex when using generic types.

This example

type neg = r : real | r <= 0.0

datatype formula<T> = 
   | Var(z: T)
   | Plus(x: formula<T>, y: formula<T>) 
   | Minus(x: formula<T>, y: formula<T>) 
   | Mult(x: formula<T>, y: formula<T>)
   | Divide(x: formula<T>, y: formula<T>)

function method toReal(x: formula<real>) : real
{
   match x
   case Var(z) => z
   case Plus(y, z) => toReal(y) + toReal(z)
   case Minus(y, z) => toReal(y) - toReal(z)
   case Mult(y, z) => toReal(y) * toReal(z)
   case Divide(y, z) => 
      if toReal(z) == 0.0 then 42.0 else 43.0
}

datatype ChildLineItem = ChildLineItem(negChargeAmount: formula<neg>)

predicate isValidChildLineItem(l: ChildLineItem) 
{ toReal(l.negChargeAmount) <= 0.0 }

produces

ERROR_Covariance.dfy(24,11): Error: value does not satisfy the subset constraints of 'formula<real>'

Dafny program verifier finished with 2 verified, 1 error

The problem is that the code is trying to convert a formula<neg> to a formula<real>. While a neg is a subtype of real, that does not imply a subtype relationship between formula<neg> and formula<real>. That relationship must be declared in the definition of formula. By default, the definition of a generic type is non-variant, meaning there is no subtype relationship between formula<T> and formula<U> when T is a subtype of U. What is wanted here is for formula to be covariant, so that formula<T> is a subtype of formula<U> when T is a subtype of U. For that, use the declaration formula<+T>.

To declare formula as contravariant use formula<-T>. Then formula<U> is a subtype of formula<T> when T is a subtype of U.

Type parameter characteristics are discussed in the reference manual