sir-wabbit

trait Data { type Value }
final case class Value[N <: Data](value: N#Value) extends AnyVal

abstract class Nat protected () extends Data { type Value = Int }
final class Z extends Nat
final class S[N <: Nat] extends Nat

object Nat {
  implicit val zValue: Value[Z] = 
    Value[Z](0)

sir-wabbit

sealed abstract class BoundedLeibniz[-L <: AnyKind, +H >: L <: AnyKind, A >: L <: H, B >: L <: H] private[BoundedLeibniz] () { ab =>
  def subst[F[_ >: L <: H]](fa: F[A]): F[B]
  final def coerce(a: A): B = {
    type f[a] = a
    subst[f](a)
  }
}

sir-wabbit

package catz.base

import catz.base.BasePackage.{<~<, ===, Ξ}
import Liskov._

/**
  * Liskov substitutability: A better `<:<`.
  *
  * `Liskov[A, B]` witnesses that `A` can be used in any negative context
  * that expects a `B`. (e.g. if you could pass an `A` into any function

sir-wabbit

def coerce[U, V](u: U): V = {
  trait F { type R }
  trait X extends F { type R = U }
  trait Y extends F { type R = V }
  final case class T[A <: F](value: A#R)

  val a: T[X with Y] = new T[Y with X](u) 
  a.value
}

sir-wabbit

object Main {
  def imp[T](implicit t: T): t.type {} = t

  trait Value[T] {
    type Type
    def value: Type
  }
  object Value {
    type Aux[T, V] = Value[T] { type Type = V }

sir-wabbit

object Main {
  type Nat
  object Nat {
    type Z <: Nat
    type S[N <: Nat] <: Nat
  }

  object Church {
    object List {
      type Nil

sir-wabbit

// Type-level pairs.
final class Pair[a, b] { type Cata[g[_, _]] = g[a, b] }
type Fst[t[_[_, _]]] = t[({type l[a, b] = a})#l]
type Snd[t[_[_, _]]] = t[({type l[a, b] = b})#l]

// Bounded equality.
sealed abstract class EqT[+H, A <: H, B <: H] {
  def subst[F[_ <: H]](fa: F[A]): F[B]
}
object EqT {

sir-wabbit

sealed abstract class Leibniz[-L, +H >: L, A >: L <: H, B >: L <: H] {
  def subst[F[_ >: L <: H]](fa: F[A]): F[B]
  
  def flip: Leibniz[L, H, B, A] = {
    type f[a >: L <: H] = Leibniz[L, H, a, A]
    subst[f](Leibniz.refl[A])
  }
}
object Leibniz {
  def refl[A]: Leibniz[A, A, A, A] = new Leibniz[A, A, A, A] {

sir-wabbit

import cats.Applicative
import cats.instances.list._
import cats.instances.option._
import cats.syntax.functor._
import cats.Id

trait Instance[TC[_]] {
  type Type
  def value: Type
  def typeclass: TC[Type]

sir-wabbit

import cats.Show
import cats.instances.int._

implicit def hnil: HNil = HNil()
implicit def hcons[H, T <: HList](implicit h: H, t: T): H :: T = new ::[H, T](h, t)

trait HList
final case class HNil() extends HList
final case class ::[H, T <: HList](head: H, tail: T) extends HList