type Emp is Data:

type D is Type:
  K{f: D -> Emp}

def un(x: D) -> D -> Emp:
  match x:
    case K{f}:
      f

@unsafe
def dl(+x: D) -> Emp:
  un(x)(x)

@unsafe
def dlw(x: D) -> Emp:
  dl(x)

def w() -> D:
  K{dlw}

def boom() -> Emp:
  dlw(w())