irrefutable pattern.md

inspired by a question my colleague asked me.

Given a list of option of Ints:

val list = List(Some(1),None,Some(2))

desugar the for comprehension give us: nothing special here

@ desugar{ for { x <- list } yield x } 
res5: Desugared = ammonite.$sess.cmd4.list.map[Option[Int], Any](((x: Option[Int]) => x))(scala.collection.immutable.List.canBuildFrom[Option[Int]])

but if we desugar the for comprehension which also has pattern match inside:

@ desugar{ for (Some(x) <- list) yield x } 
res8: Desugared = ammonite.$sess.cmd4.list.withFilter(((check$ifrefutable$1: Option[Int]) => (check$ifrefutable$1: @scala.unchecked) match {
  case scala.Some((x @ _)) => true
  case _ => false
})).map[Int, Any](((x$1: Option[Int]) => (x$1: @scala.unchecked) match {
  case scala.Some((x @ _)) => x
}))(scala.collection.immutable.List.canBuildFrom[Int])

where the withFilter stuff come from? consult the spec:

The translation scheme is as follows. In a first step, every generator p <- e, where
p is not irrefutable (§8.1) for the type of e is replaced by
p <- e.withFilter { case p => true; case _ => false }

so what is irrefutable?

8.1.14 Irrefutable Patterns
A pattern p is irrefutable for a type T , if one of the following applies:
1. p is a variable pattern,
2. p is a typed pattern x : T, and T <: T
3. p is a constructor pattern c(p1, ..., pn), the type T is an instance of class c, the
primary constructor (§5.3) of type T has argument types T1, ..., Tn, and each
pi is irrefutable for Ti

I don't understand that so I am looking for Haskell document: https://www.haskell.org/tutorial/patterns.html

Patterns such as formal parameters that never fail to match are said to be irrefutable, in contrast to refutable patterns which may fail to match.

alternatively:

@ desugar{ for (x <- list if x.isDefined) yield x } 
res9: Desugared = ammonite.$sess.cmd4.list.withFilter(((x: Option[Int]) => x.isDefined)).map[Option[Int], Any](((x: Option[Int]) => x))(scala.collection.immutable.List.canBuildFrom[Option[Int]])