Why does my constrained type fail to compile with 'no value can satisfy this constraint'?

← Advanced Type System · Ref: Q1376

The constraint you wrote cannot be satisfied by ANY value of the base type, so every construction of it would Panic and no variable of it could ever hold a value. EK9 proves this at the declaration (E08261) rather than leaving it to fail at runtime.

The usual cause is strict operators on a WHOLE-NUMBER base:

  defines type
    Wrong as Integer constrain as
      > 0 and < 1          //E08261 - nothing lies between 0 and 1

    Right as Integer constrain as
      >= 0 and <= 1        //admits 0 and 1

Discreteness matters: '> 0.0 and < 1.0' over Float is perfectly fine because 0.5 satisfies it. The same shape is empty over Integer and populated over Float.

The other causes are bounds written in the wrong order ('>= 10 and <= 5'), 'and' used where 'or' was meant, and an '==' beside a clause that contradicts it ('== 5 and > 10' - the '==' pins the only candidate there is, so any other clause can only take it away).

Only PROVABLE cases are reported. An 'or' anywhere, a regex, or a base whose ordering is not modelled is left to the runtime check.

See Q257 for constrained types. See Q1185 for a Percentage range and E08260.

Example

defines module qa.advancedtypes.unsatisfiableconstraint

  defines type

    //Inclusive bounds - admits 0 through 9. The strict form '> 0 and < 1' would be E08261.
    Digit as Integer constrain as
      >= 0 and <= 9

    //Bounds may meet at a single value: this admits exactly 5, and is NOT empty.
    ExactlyFive as Integer constrain as
      >= 5 and <= 5

    //🔑 Discreteness matters. This is the SAME shape that is impossible over Integer, and it is
    //perfectly satisfiable over Float because values lie between the bounds.
    Fraction as Float constrain as
      > 0.0 and < 1.0

    //Values on either side of a gap need 'or' - an 'and' here would admit nothing.
    Outlier as Integer constrain as
      <= 10 or >= 90

    //A lone '==' is fine; it is only contradicted when another clause excludes the pinned value.
    Answer as Integer constrain as
      == 42

    //Suffixed bounds must share ONE suffix. A Money varies along TWO axes - magnitude AND currency -
    //and only the magnitude may move, so bounds in different currencies admit nothing.
    Budget as Money constrain as
      > 330#GBP and < 450#GBP

  defines program

    UnsatisfiableConstraintDemo()
      stdout <- Stdout()

      //Inclusive bounds admit both ends
      low <- Digit(0)
      high <- Digit(9)
      stdout.println(`Digit 0 set: ${low?}`)
      stdout.println(`Digit 9 set: ${high?}`)

      //A single-value range still admits its one value
      five <- ExactlyFive(5)
      stdout.println(`ExactlyFive set: ${five?}`)

      //The continuous case: nothing lies between 0 and 1 for an Integer, but plenty does for a Float
      half <- Fraction(0.5)
      stdout.println(`Fraction 0.5 set: ${half?}`)

      //'or' admits both sides of the gap
      lowSide <- Outlier(5)
      highSide <- Outlier(95)
      stdout.println(`Outlier 5 set: ${lowSide?}`)
      stdout.println(`Outlier 95 set: ${highSide?}`)

      //The pinned value satisfies its own constraint
      answer <- Answer(42)
      stdout.println(`Answer set: ${answer?}`)

      //Out of range values use the fallible factory rather than a bare constructor
      tooBig <- Digit().of(10)
      stdout.println(`Digit 10 set: ${tooBig?}`)

Common mistakes

E08261 — Over a whole-number base the strict operators exclude the bounds themselves, so '> 0 and < 1' leaves nothing at all between them. Use the inclusive '>=' and '<=' when the bounds are the values you mean to allow. Note the same shape over a Float base is fine - '> 0.0 and < 1.0' admits 0.5 - because a continuous type has values between the bounds. See ek9 -h E08261 for details.

Incorrect:

Digit as Integer constrain as
      > 0 and < 1

Correct:

Digit as Integer constrain as
      >= 0 and <= 9

E08261 — The bounds are the right shape but the wrong way round, so the lower bound sits above the upper one and the range is empty. Read the two clauses as a range and check the smaller value is the one with '>='. See ek9 -h E08261 for details.

Incorrect:

ExactlyFive as Integer constrain as
      >= 5 and <= 4

Correct:

ExactlyFive as Integer constrain as
      >= 5 and <= 5

E08261 — 'and' means both clauses must hold at once, which nothing outside a single range can do. To allow values on either side of a gap use 'or' - that is a union of two ranges rather than an impossible intersection. See ek9 -h E08261 for details.

Incorrect:

Outlier as Integer constrain as
      >= 90 and <= 10

Correct:

Outlier as Integer constrain as
      <= 10 or >= 90

E08261 — An '==' pins the only candidate the type can ever hold, so every other clause can only take that value away. Either drop the '==' and use a range, or drop the clause that contradicts it. See ek9 -h E08261 for details.

Incorrect:

Answer as Integer constrain as
      == 42 and > 100

Correct:

Answer as Integer constrain as
      == 42

E08262 — A suffixed value has two parts and only one of them is a magnitude - '330#GBP' is an amount AND a currency. EK9 does not order values across the suffix, so a cross-currency comparison is UNSET, and an unset result never satisfies a constraint. The same applies to units of measure: '>= 500mm and <= 90cm' mixes two units and they do not convert automatically. Express every bound in one currency or one unit. See ek9 -h E08262 for details.

Incorrect:

Budget as Money constrain as
      > 330#GBP and < 450#USD

Correct:

Budget as Money constrain as
      > 330#GBP and < 450#GBP

Coming from another language?

Java: Bean Validation @Min/@Max are runtime annotations - a contradictory pair is never detected. Python: no type-level constraints at all. Rust: a newtype's validation is hand-written, so an impossible condition compiles and always returns Err. Kotlin: a value class init check with contradictory requires compiles and always throws. EK9: the constraint is part of the TYPE, so an unsatisfiable one is a compile error at the declaration.

Keywords: empty range, discrete, constrained, bounds, impossible, unsatisfiable, E08261, constrain as