How to define a given clause using singleton type as the type parameter?

Question
1

Hi,

I defined DepType for exercising the dependent product type.

import scala.compiletime.ops.int.

type Nat = Int

sealed trait DepType[N <: Nat]:
  type T
  def apply(x: N): T
 
given depType0: DepType[0] with
  type T = Int
  override def apply(x: 0) = 10
 
given depType1: DepType[1] with
  type T = String
  override def apply(x: 1) = "abc"
 
given depTypeN[N <: Nat]: DepType[S[S[N]]] with
  type T = Boolean
  override def apply(x: S[S[N]]) = true

object DepFunction:
  def apply[N <: Nat](x: N)(using depType: DepType[N]): depType.T = depType(x)

val _0: 0 = 0
val _1: 1 = 1
val _2: 2 = 2
val _3: 3 = 3

For the following code:

val x: Int = DepFunction(_0)         
val y: String = DepFunction(_1)
val z: Boolean = DepFunction(_2)

The compiler show the error messages liking:

No given instance of type deps.v2.DepType[Int] was found for parameter depType of method apply in object DepFunction

For the first line, for example, why does the compiler not use the instance of the DepType[0]?

How to fix it?

Thanks for your help!

Guofeng

2

the key is in the error message:

No given instance of type deps.v2.DepType[Int] was found

This means that N was widened from 0 to Int. To prevent widening, you can use the Singleton upper bound on the type parameter, e.g. [N <: Nat & Singleton]

3

Solved it by followin your advice (using N <: Nat & Singleton as the type parameter ).

It is strange that the following usage cannot solve the issue:

type Nat = Int & Singleton

Thanks again.