scala - Why is it ok to pass a Compare type without parameters here? -

i studying code example type level programming in scala:

object typelevel {    sealed trait true extends bool {     type if[t <: up, f <: up, up] = t   }    sealed trait false extends bool {     type if[t <: up, f <: up, up] = f   }    sealed trait bool {     type if[t <: up, f <: up, up] <:   }    object bool {     type &&[a <: bool, b <: bool] = a#if[b, false, bool]     type ||[a <: bool, b <: bool] = a#if[true, b, bool]     type not[a <: bool] = a#if[false, true, bool]   }    case class boolrep[b <: bool](val value: boolean)    def toboolean[b <: bool](implicit b: boolrep[b]) = b.value    implicit val falserep: boolrep[false] = boolrep[false](false)   implicit val truerep: boolrep[true] = boolrep[true](true)    sealed trait comparison {     type match[iflt <: up, ifeq <: up, ifgt <: up, up] <:     type gt = match[false, false, true, bool]     type lt = match[true, false, false, bool]     type eq = match[false, true, false, bool]     type le = match[true, true, false, bool]     type ge = match[false, true, true, bool]   }    sealed trait gt extends comparison {     type match[iflt <: up, ifeq <: up, ifgt <: up, up] = ifgt   }    sealed trait lt extends comparison {     type match[iflt <: up, ifeq <: up, ifgt <: up, up] = iflt   }    sealed trait eq extends comparison {     type match[iflt <: up, ifeq <: up, ifgt <: up, up] = ifeq   }    sealed trait nat {     type match[nonzero[n <: nat] <: up, ifzero <: up, up] <:      type compare[n <: nat] <: comparison   }    sealed trait _0 extends nat {     type match[nonzero[n <: nat] <: up, ifzero <: up, up] = ifzero      type compare[n <: nat] =     n#match[constlt, eq, comparison]      type constlt[a] = lt   }    sealed trait succ[n <: nat] extends nat {     type match[nonzero[n <: nat] <: up, ifzero <: up, up] = nonzero[n]      type compare[o <: nat] = o#match[n#compare, gt, comparison]   }    type _1 = succ[_0]   type _2 = succ[_1]   type _3 = succ[_2]   type _4 = succ[_1]    type is0[a <: nat] = a#match[constfalse, true, bool]   type constfalse[a] = false   type consttrue[a] = true    def printall(strings: string*): unit = {     println(strings.mkstring("\n"))   }    def main(args: array[string]) {     import bool.{&&, ||, not}     printall(       toboolean[true && false || not[false]].tostring,       toboolean[is0[_0]].tostring,       toboolean[_0#compare[_0]#eq].tostring,       toboolean[_1#compare[_0]#gt] tostring,       toboolean[_0#compare[_1]#lt] tostring,       toboolean[_1#compare[_2]#lt] tostring     )   } } 

this allows compare natural numbers @ compile time. can trace how _1#compare[_2]#lt works:

• succ[_0]#compare[_2]#lt
• _2#match[_0#compare, gt, comparison]#lt

here lost. signature of compare in _0

type compare[n <: nat] = n#match[constlt, eq, comparison] 

so needs 1 parameter, , definition of type relies on parameter n. _0#compare doesn't make sense. explain how works here?

i figured out:

→ _1#compare[_2]#lt

→ succ[_0]#compare[_2]#lt

→ _2#match[_0#compare, gt, comparison]#lt

→ succ[_1]#match[_0#compare[_1], gt, comparison]#lt ……… _1 in _0#compare[_1] inferred.

→ _0#compare[_1]#lt

→ lt#lt

→ true