Some tests on ADTs with Scala 3

Logic.scala

import scala.compiletime.constValue

object Logic extends App:

  // Definitions

  enum Formula:
    case Variable[Id <: String & Singleton](val id: Id) extends Formula
    case True extends Formula
    case False extends Formula
    case And[L <: Formula, R <: Formula](left: L, right: R) extends Formula
    case Or[L <: Formula, R <: Formula](left: L, right: R) extends Formula
    case Not[F <: Formula](formula: F) extends Formula

  // Sugar

  import Formula._

  object Variable:
    inline given apply[Id <: String & Singleton]: Variable[Id] = new Variable[Id](constValue[Id])

  import Variable.apply

  type True = True.type
  type False = False.type

  type &&[L <: Formula, R <: Formula] = And[L, R]
  type ||[L <: Formula, R <: Formula] = Or[L, R]
  type ![F <: Formula] = Not[F]

  extension [L <: Formula](left: L)
    def &&[R <: Formula](right: R): L && R = And(left, right)
    def ||[R <: Formula](right: R): L || R = Or(left, right)
    def unary_! : ![L] = Not(left)

  given [L <: Formula, R <: Formula](using left: L, right: R): (L && R) = left && right
  given [L <: Formula, R <: Formula](using left: L, right: R): (L || R) = left || right
  given [F <: Formula](using formula: F): ![F] = !formula
  given True: Formula.True.type = True
  given False: Formula.False.type = False

  def $[T <: Formula](using T): T = summon[T]

  // Tests

  val a: (Variable["a"] && True) || ![False] = $

  assert(a == ((Variable["a"] && True) || !False))

  println($: False)