This blog post will highlight what happens during implicit resolution using an Aux type on a type level proof when the proof has not been properly constructed. To show this, I'm going to revisit the approach taken in a previous blog post proving that a type was a member of a collection of types at compile time. By adding a few small tweaks I will try to achieve both inclusion and exclusion, where as before I could only get inclusion. Finally, I'll show how to build the proof just right and enjoy the reuse of code for multiple purposes but on the type level.
Like in other posts, I'm going to assume some knowledge about Scala and it's type system. First, I'll assume you understand implicit parameters and you're familiar with the type class pattern found in Scala. Secondly, you're familiar with the Aux type pattern or type refinements (which the Aux pattern is.) Finally, I'll assume you've had some exposure to implicit resolution order.
Revisited
For a refresher, let's take a look at the definition that proved some type exists within a collection of types:
I won't go into specifics here; you can read them in that blog post. Just know that if the type does not exist and we attempt to find the implicit through regular implicit resolution it'll fail compilation. Hence, this only ever allows us to prove something true and not the negation of the hypothesis.
To begin to prove both, I'll modify the definition of OneOf by adding an extra type member. I'll also add some types representing true/false and define an Aux type to compliment our new OneOf. In fact, so as not to confuse the situation, I'll rename it:
Next we'll define the proof to allow both inclusion and exclusion:
Here, we're using the implicit resolution order to force the compiler to search first through the recursive case, exploring the group of types completely before we allow it to reach the false condition. Once the false condition is reached, however, it will be carried all the way back up through the recursive stack to yield a final value of False.
The problem here is that we've failed to properly construct the proof. It's subtle but evidences itself through use of the type definitions we made using the Aux type. Try running this through the repl:
If we were to see if a String type compiles in the "contains" check, it would fail. However, the last case does compile when we would expect it to not compile.
The reason is simple. Normally when we construct a proof, we construct it in such a way as to only compile when the condition is matched. In this case, by over constraining the Aux type, we've told the compiler not to search the proof as we've written it but instead to search to find if there is any implicit which satisfies the condition that the type member is False. There is nothing to stop or signal to the compiler that it can't use the very last, completely unguarded implicit to complete the search.
What we have to do is use a dirty trick, cause an implicit divergence by allowing two mutually inclusive definitions to exist at the same search level:
Now, instead of compiling, the very last example used in the repl session would fail.
Conclusion
In this post I went over why an Aux type is both useful and dangerous at the same time. It is useful to get more mileage out of a the scaffolding of a type level proof. Allowing us to reuse logic for multiple conditions. At the same time, it is dangerous because it imposes an extra burden on the author. If care is not taken in the proof's construction unexpected result will highlight a discrepancy or any hole in the logic.
Due note that this blog post was written for educational purposes and it lacks the level of completeness and power a library might contains. If you enjoy these types of things have a gander at several libraries which use type level tricks to implement deeply powerful patterns: Miles' ever wonderful Shapless, my own AutoLifts or Stew's type level turning machine Scatur.