"Could not check well-formedness of type: <untyped>" when pattern matching covariant ADTs

[mario-bucev]

The following:

object CovariantPatmat {
  sealed abstract class Option[+T]
  case class Some[+T](value: T) extends Option[T]
  case object None extends Option[Nothing]

  trait Animal
  case class Cow(id: BigInt) extends Animal

  def test(an: Option[Animal]): BigInt = an match {
    case None => 0 // problematic
    case Some(_) => 42
  }
}

causes the following error:

[ Fatal  ] Could not check well-formedness of type: <untyped> (class inox.ast.Types$Untyped$)
[ Fatal  ] in context:
[ Fatal  ] Kind: type-checking
[ Fatal  ] Check SAT: false
[ Fatal  ] Emit VCs: true
[ Fatal  ] Functions: isSome$0, isOption$0, isEmpty$4, isNone$0, get$5, None$4, InstanceOf$0
[ Fatal  ] ADTs: Object$0, Animal$0, Option$4
[ Fatal  ] Type Variables: 
[ Fatal  ] Term Variables:
[ Fatal  ]   an$1: { x$101: Object$0 | (isOption$0(x$101, (x$102: Object$0) => x$102.isInstanceOf[Animal$1] && true)): @dropConjunct  }
[ Fatal  ]   scrut$1: Object$0
[ Fatal  ]   scrut$1 == an$1
[ Fatal  ]   !(!isEmpty$4[{ x$116: Object$0 | (isNone$0(x$116)): @dropConjunct  }](InstanceOf$0[{ x$114: Object$0 | (isOption$0(x$114, (x$115: Object$0) => x$115.isInstanceOf[Animal$1] && true)): @dropConjunct  }, { x$116: Object$0 | (isNone$0(x$116)): @dropConjunct  }](isNone$0, (x$110: { x$108: Object$0 | (isOption$0(x$108, (x$109: Object$0) => x$109.isInstanceOf[Animal$1] && true)): @dropConjunct  }) => x$110, scrut$1)) && !isEmpty$4[{ v$22: Object$0 | v$22.isInstanceOf[None$2] }](None$4(get$5[{ x$116: Object$0 | (isNone$0(x$116)): @dropConjunct  }](InstanceOf$0[{ x$114: Object$0 | (isOption$0(x$114, (x$115: Object$0) => x$115.isInstanceOf[Animal$1] && true)): @dropConjunct  }, { x$116: Object$0 | (isNone$0(x$116)): @dropConjunct  }](isNone$0, (x$110: { x$108: Object$0 | (isOption$0(x$108, (x$109: Object$0) => x$109.isInstanceOf[Animal$1] && true)): @dropConjunct  }) => x$110, scrut$1)))))
[ Fatal  ]   !scrut$1.isInstanceOf[Some$2]

With --debug=trees --debug-phases=TypeEncoding, we get to know a bit more:

[ Debug  ] Ensuring well-formedness after phase TypeEncoding...
[ Error  ] CovariantPatmat.scala:9:42: Type error: an$0 match {
[ Error  ]   case isNone$0.((x$110: { x$108: Object$0 | @dropConjunct isOption$0(x$108, (x$109: Object$0) => x$109 is Animal$1 && true) }) => x$110).InstanceOf$0(None$4()) =>
[ Error  ]     0
[ Error  ]   case Some$2(_) =>
[ Error  ]     42
[ Error  ] }, expected BigInt,
[ Error  ] found <untyped>
[ Error  ] 
[ Error  ] Typing explanation:
[ Error  ] an$0 match {
[ Error  ]   case isNone$0.((x$110: { x$108: Object$0 | @dropConjunct isOption$0(x$108, (x$109: Object$0) => x$109 is Animal$1 && true) }) => x$110).InstanceOf$0(None$4()) =>
[ Error  ]     0
[ Error  ]   case Some$2(_) =>
[ Error  ]     42
[ Error  ] } is of type <untyped>
[ Error  ]   an$0 is of type Object$0
[ Error  ]   0 is of type BigInt
[ Error  ]   isNone$0 is of type (Object$0) => Boolean
[ Error  ]     isNone$0(x$107) is of type Boolean
[ Error  ]       x$107 is of type Object$0 because isNone was instantiated with  with type (Object$0) => Boolean
[ Error  ]   (x$110: { x$108: Object$0 | @dropConjunct isOption$0(x$108, (x$109: Object$0) => x$109 is Animal$1 && true) }) => x$110 is of type (Object$0) => Object$0
[ Error  ]     x$110 is of type Object$0
[ Error  ]   42 is of type BigInt
             def test(an: Option[Animal]): BigInt = an match {
                                                    ^^^^^^^^^^...
[ Fatal  ] Well-formedness check failed after phase TypeEncoding