Skip to content

Instantly share code, notes, and snippets.

@nicolasstucki
Last active March 15, 2021 09:21
Show Gist options
  • Save nicolasstucki/1ab19828fff43ff1e57889d33c181571 to your computer and use it in GitHub Desktop.
Save nicolasstucki/1ab19828fff43ff1e57889d33c181571 to your computer and use it in GitHub Desktop.

Example implementation: safe type constraint =:=

In this example we will see how to reimplement =:= using phantom types and in the process fix a vulnerability that it has. It is a simplified version of TypeConstraint which also implements <:<.

=:= in Scala 2.x

Type constraints =:= gives an evidence that two generic types are in fact equal and provides a mechanism to safely cast one type to the other. In the following example we want to assign an x: X to an ys: Array[Y] where we don't know if it is possible (this will be known at call site). Therefore we use an implicit evidence ev: X =:= Y to know that they are equal and ev(x) to cast x form X to Y.

def putInHead[X, Y](x: X, ys: Array[Y])(implicit ev: X =:= Y): Unit = { 
  ys(0) = ev(x) 
} 
  
val array = Array[Int](1) 
putInHead(3, array) // implicit evidence `Int =:= Int` is constructed from `=:=.tpEquals[Int]` 

If we try to call the method with parameters that do not have the same type the compiler will tell us that this call cannot be done.

putInHead('5', array) // as expected this will not compile as it does not fine an evidence that `Char =:= Int` 

The implementation of Predef.=:= in Scala 2.x is as follows:

sealed abstract class =:=[From, To] extends (From => To) with Serializable 
  
private[this] final val singleton_=:= = new =:=[Any,Any] { def apply(x: Any): Any = x } 
  
object =:= { 
   implicit def tpEquals[A]: A =:= A = singleton_=:=.asInstanceOf[A =:= A] 
} 

This implementation is defines three things:

  • =:= as a type that can not be instantiated by the user (sealed abstract class)
  • An apply on an instance of type =:= that acts as a safe cast from type From to type To
  • A way to instantiate type evidences with implicit def tpEquals[A]: A =:= A

Issues with =:= in Scala 2.x

Unfortunately it is easy to trick the compiler using runtime casts because generic types are erased. Therefore the it is possible to create wrong code that will be assumed to be coherent and the fail at runtime on the pseudo-safe cast.

putInHead('5', array)(=:=.tpEquals.asInstanceOf[Char =:= Int]) 
// java.lang.ClassCastException: java.lang.Character cannot be cast to java.lang.Integer 
//  at scala.runtime.BoxesRunTime.unboxToInt(BoxesRunTime.java:101) 
//  at scala.runtime.ScalaRunTime$.array_update(ScalaRunTime.scala:92) 
//  at .putInHead(<console>:12) 

Even worse, if the ev.apply would not be called and it is just there as a sanity check (e.i. user should not call the method with different types), it would not crash and just run the method that it should not. Hence bug might not be detected for a while causing unforeseen sidefects.

Creating a safer type constraint with phantoms

To create our version to type evidences with phantom we will first create object TypeConstraint extends Phantom to define the phantom type. Now we can define the type =:=, tpEquals and apply inside of it.

  • The =:= type definition becomes a simple phantom type definition as type =:=[From, To] <: this.Any
  • The tpEquals can be trivially implemented by a assume as implicit def tpEquals[A]: A =:= A = assume
  • As it is not possible to declare the apply method on phantom types we will instead define a cast method that will receive the evidence implicitly as def cast[From, To](x: From)(implicit ev: From =:= To): To = x.asInstanceOf[To].

Putting everything together we get:

object TypeConstraint extends Phantom { 
   
  type =:=[From, To] <: this.Any 
   
  implicit def tpEquals[A]: A =:= A = assume 
   
  def cast[From, To](x: From)(implicit ev: From =:= To): To = x.asInstanceOf[To] 
} 

Now we can use this version of =:= in our putInHead example. Now it is not possible to fake evidences and hence the cast is always safe.

import TypeConstraint._ 
def putInHead[X, Y](x: X, ys: Array[Y])(implicit ev: X =:= Y): Unit = { 
  ys(0) = cast(x) 
} 
  
val array = Array[Int](1) 
putInHead(3, array) // implicit evidence `Int =:= Int` is constructed from TypeConstraint.tpEquals[Int]` 
  
putInHead('5', array) // as expected this will not compile as it does not fine an evidence that `Char =:= Int` 
  
putInHead('5', array)(tpEquals.asInstanceOf[Char =:= Int]) // will fail at compile time as `=:=` has no method `asInstanceOf` 

It also adds some additional inline to remove completely the overhead on the cast and the implicit call to tpEquals.

object TypeConstraint extends Phantom { 
   
  type =:=[From, To] <: this.Any 
   
  implicit inline def tpEquals[A]: A =:= A = assume 
   
  inline def cast[From, To](x: From)(implicit ev: From =:= To): To = x.asInstanceOf[To] 
}
@nicolasstucki
Copy link
Author

Newer version

import scala.annotation.implicitNotFound

/**
* An instance of `A <::< B` witnesses that `A` is a subtype of `B`.
* Requiring an implicit argument of the type `A <::< B` encodes
* the generalized constraint `A <: B`.
*
* To constrain any abstract type T that's in scope in a method's
* argument list (not just the method's own type parameters) simply
* add an implicit argument of type `T <::< U`, where `U` is the required
* upper bound; or for lower-bounds, use: `L <::< T`, where `L` is the
* required lower bound.
*
* In part contributed by Jason Zaugg.
* Adapted to phantom types by Nicolas Stucki.
*/
@implicitNotFound(msg = "Cannot prove that ${From} <::< ${To}.")
type <::<[-From, +To]

/** An instance of `A =::= B` witnesses that the types `A` and `B` are equal.
  *
  * @see `<::<` for expressing subtyping constraints
  */
@implicitNotFound(msg = "Cannot prove that ${From} =::= ${To}.")
type =::=[From, To] <: (From <::< To)

erased given [X]: (X =::= X) = scala.compiletime.erasedValue

object Cast:
  extension [From](x: From)
    inline def cast[To](using From <::< To): To = x.asInstanceOf[To] // Safe cast because we know `From <:< To`

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment