# A good bad idea: use a constraint solver to proove \`when\` exhaustiveness

**URL:** <https://discuss.kotlinlang.org/t/a-good-bad-idea-use-a-constraint-solver-to-proove-when-exhaustiveness/5632>\
**Category:** Uncategorized\
**Created:** [November 30, 2017, 11:26pm UTC](https://discuss.kotlinlang.org/t/a-good-bad-idea-use-a-constraint-solver-to-proove-when-exhaustiveness/5632 "2017-11-30T23:26:36Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![Groostav](https://avatars.discourse-cdn.com/v4/letter/g/85f322/32.png) [@Groostav](https://discuss.kotlinlang.org/u/Groostav)\
**Post date:** [November 30, 2017, 11:26pm UTC](https://discuss.kotlinlang.org/t/a-good-bad-idea-use-a-constraint-solver-to-proove-when-exhaustiveness/5632/1 "2017-11-30T23:26:36Z")

</div>

Hey Guys,

It may or may not surprise you to know

```kt
val x = when { 
  true -> "testing!"
}

```

does not compile, because _the when statement is not exhaustive_, when, of course, it obviously is.

Rephrased, the compiler refuses to investigate anything other than sealed class hierarchies with respect to their exhasustiveness of a when statement. the compiler itself only considers 3 classes of when statements, those with an `else` clause, those without an `else` clause, and those on a sealed class hierarchy. The first is always non-exhaustive, the second is always exhaustive, the last is exhaustive iff every sealed class member exists as a clause.

I feel like its worth mentioning that this is probably the single most direct application of _SAT/SMT solvers_ I have ever seen in compilers.

So lets make this a language feature request and merge it into kotlin! We can evolve it to make it increasingly general purpose, and then dump this problem of _what is an exhaustive when expression_ onto a community that has a great deal of expertise proofing equations just like this. For example, it would be relatively trivial to transform

```kt
val x = when(someNullableInteger){
  null -> A()
  in Int.MIN_VALUE .. 0 -> B()
  in 1 .. Int.MAX_VALUE -> C()
}

```

which effectively has the compiler asking the question

> is the the universe of all possible `Int?` equal to { `null`, `MIN_VALUE .. 0`, `1 .. MAX_VALUE` }?

which can be rephrased as

> does there exist a value that is an `Int?` that is not in { `null`, `MIN_VALUE .. 0`, `1 .. MAX_VALUE` }?

transformed into smt-lib2 expression:

```lisp
(declare-const nullableInt Int)

(assert (! (= nullableInt [null])))
(assert
  (! 
    (and
      (>= nullableInt -2147483648)   
      (<= nullableInt 0)    
    )
  ) 
)
(assert
  (! 
    (and
      (>= nullableInt 1)
      (<= nullableInt 2147483647)
    )
  )
)

```

[link to live running code](https://rise4fun.com/Z3/8Fmk)

for which Z3 will _in fairly quick time_ come back with `UNSAT`, meaning it can generate a proof that there is no value outside of your when expressions, IE that your when statement is exhaustive.

So can we bolt this on to the kotlin compiler now?

The answer is almost certainly no. While SMT solvers will advertise that they work in the general case (and indeed, Z3 is used by pex in many very general cases), they have very little in terms of time-complexity guarantees. The Z3 solver effectively reserves the right to spin the CPU asking questions that it will never finish asking, in effect stalling the calling-compiler. So thats no good.

But this has me asking the question: what kinds of performance guarantees would the kotlin compiler team need to consider such an idea?

On the one end we have the go-lang guys who have deliberately structured their language such that its easy to parse, and then we have the scala guys who have a language riddled with complex ambiguity and sophisticated resolution rules but many more language features. What do you guys think kotlin should aim for?

I personally would really like more features around the _exhaustive-when_ as is this is one of very few language options where you can explicitly introduce a compiler error when somebody makes a change that your code likely isnt prepared for, which is an enormously powerful tool, in my eyes.

---

<div class="post-metadata">

**Author:** ![solidsnack](https://sea1.discourse-cdn.com/flex019/user_avatar/discuss.kotlinlang.org/solidsnack/32/1500_2.png) [@solidsnack](https://discuss.kotlinlang.org/u/solidsnack)\
**Post date:** [December 2, 2017, 10:10pm UTC](https://discuss.kotlinlang.org/t/a-good-bad-idea-use-a-constraint-solver-to-proove-when-exhaustiveness/5632/2 "2017-12-02T22:10:37Z")

</div>

Right now it seems like this feature is pretty predictable: if you want case coverage for the constructors of a union type it works, otherwise it doesn’t. If the feature were to grow general solving powers, but we still want some limit on compile times, it seems like the feature would be more useful but less predictable: sometimes you would add a branch and the compiler would give up, saying “solver timeout (200ms)”. Maybe on a faster computer it might work.

If the language/tools were to provide support for external verification, I wonder what that would look like? It seems like you’d want to have a pass where the compiler provided as much type information as it could, then a second pass whether the verifier looked at all the ill-typed or ill-formed expressions that remain, and then a pass that used that information to finalise the types.

---

<div class="post-metadata">

**Author:** ![mikehearn](https://sea1.discourse-cdn.com/flex019/user_avatar/discuss.kotlinlang.org/mikehearn/32/1424_2.png) [@mikehearn](https://discuss.kotlinlang.org/u/mikehearn)\
**Post date:** [December 4, 2017, 7:47pm UTC](https://discuss.kotlinlang.org/t/a-good-bad-idea-use-a-constraint-solver-to-proove-when-exhaustiveness/5632/3 "2017-12-04T19:47:02Z")

</div>

You would need to find a solver that supported deterministically limited queries, i.e. not wall clock time limited but number-of-operations limited.