Coo L'Hibou
Coo L'Hibou

Reputation: 1

In scala 3, how to implement an implicit conversion over a type refined by iron?

Here is a minimal not working example of what I am trying to do : Let

import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.string.*

case class User(name: String)
type Username = String :| StartWith["@"]
def name2user(usern : Username) : User = User(usern)

I want to implements an implicit conversion so that :

val user : User = "@john" //compile
val user : User = "!john" //not compile

Here what I've tried so far

given name2user: Conversion[Username, User] = User(_)
val user1 : User = name2user("@john") // 
val user2 : User = "@john" //does not compile because "@john" is a String

and

implicit def name2user[S <: String](n: S)(implicit
   ev: S <:< Username
): User = User(n)
val user1: User = name2user2("@john") // cannot prove that String <:< Username
val user2: User = "@john" // does not compile because "@john" is a String

Once again this is a minimal example to illustrate as simply as possible my objective to integrate Iron's refinements and Scala 3 implicit conversions.

Thank you in anticipation for your help

Upvotes: 0

Views: 55

Answers (1)

Coo L&#39;Hibou
Coo L&#39;Hibou

Reputation: 1

Answering, you should inline and typelevel programming using good old implicits :

implicit inline def name2user(inline n: String)
(implicit inline ev: Username = n): User = User(n)   

val user3: User = name2user("@john") // compile   
val user4: User = "@john" // compile  
val user5: User = "#john" // does not compile as it should 

An interesting variation is to declare

case class User(name: Username)
implicit inline def name2user(inline n: String)
(implicit inline ev: Username = n): User = User(ev)   

This guarantee User is always well formed while authorizing a compile time automatic construction of it from well formed strings.

Upvotes: 0

Related Questions