"Unreachable case" pattern matching with an Option of List

[avella2409]

Hello, I've started to play with Iron to learn more about refinement types, but I've encountered an error that I cannot understand the cause.

When I pattern match on an Option of List like Option[List[Int] :| ForAll[Greater[1]]], I get the following compilation error: Unreachable case.
When I replace the List with a Set or a Seq, it works perfectly. The following code shows how to reproduce it (Scala 3.3.1):

object UnreachableCodeExample {

    def example(): Unit =
        
        // Using List: Compile error: Unreachable case 
        val optionList: Option[List[Int] :| ForAll[Greater[1]]] =
            List(2, 3).refineOption

        optionList match
            case Some(value) => ??? // Compile error: Unreachable case 
            case None => ???


        // Using Seq: Everything work
        val optionSeq: Option[Seq[Int] :| ForAll[Greater[1]]] =
            Seq(2, 3).refineOption

        optionSeq match
            case Some(value) => ??? // No compile error
            case None => ???


        // Using Set: Everything work
        val optionSet: Option[Set[Int] :| ForAll[Greater[1]]] =
            Set(2, 3).refineOption

        optionSet match
            case Some(value) => ??? // No compile error
            case None => ???
}

What do you think I am missing?

[Iltotore]

Hello.

Can you send the full error message? IIRC the compiler gives additional information about why the case is unreachable.

[avella2409]

Sadly, there is nothing more than "Unreachable case."

In my scalac options, I have the -Werror flag, so in fact Unreachable case is a warning (that was converted to an error by the flag). But when I run the program, it works correctly; the code is reachable.

I have no idea why the compiler throws this warning.

[Iltotore]

Looks weird indeed. Looks more like a Scala bug than Iron to me but I will investigate this issue once available.

[Iltotore]

It is indeed a compiler bug. I opened an issue with a minimal example: scala/scala3#19275