Iltotore/iron

Subtype relationship for union of constraints: implication needed?

Closed this issue · 2 comments

Hello, @Iltotore thanks for a great library, it's a real pleasure to use iron.

I have a case where I want a string validated as composed of only certain characters, which I define as a union of constraints, but I'm having a tough time getting a value refined by a particular constraint in that union to be recognised as satisfying the union of constraints.

This came up originally when creating a org.scalacheck.Arbitrary instance for the narrower type, but here's a reduced example after some tinkering in the REPL...

import io.github.iltotore.iron.:|
import io.github.iltotore.iron.constraint.any.StrictEqual
import io.github.iltotore.iron.constraint.char.{ Digit, Letter }
import io.github.iltotore.iron.scalacheck.char.given

// I want only alphanumeric or a common field delimited.
type GoodChar = Digit | Letter | StrictEqual["_"] | StrictEqual["-"]

// compiles
val hyphen: Char :| StrictEqual['-'] = {
    import io.github.iltotore.iron.autoRefine
    '-'
}

// compiles
val listOfHyphen: List[Char :| StrictEqual['-']] = List(hyphen, hyphen)

// doesn't compile
val listOfGoodChar: List[Char :| GoodChar] = {
    import io.github.iltotore.iron.autoRefine
    listOfHyphen
}

// compiles
val letterA: Char :| Letter = {
    import io.github.iltotore.iron.autoRefine
    'A'
}

// doesn't compile
val widerA: Char :| GoodChar = letterA

My thought was that I perhaps need an Implication in scope relating the wider, union constraint to one of its individual, component constraints, but I wasn't sure if this...
a) should already be automatic
b) requires additional import(s)
c) requires manual definition of the implication relation
d) none of the above
?

Ah, it was autoCastIron that was missing. With that imported, I get the expected subtyping relation with the union and one of its components. Sorry for the noise.