Type error when @extern method's result widens ADT value

[vkuncak]

This:

import stainless.annotation.*
object Branching:

  sealed trait Tree
  case class Node() extends Tree

  extension (tree: Tree)
    def nodesGood: Boolean = true

  @extern
  def myTree1: Tree = {
    Node()    
  } ensuring(_.nodesGood)

end Branching

gives:

[  Info  ] Preprocessing the symbols...                             
[ Error  ] TypeCheckBug.scala:11:23: Type error: {
[ Error  ]   <empty tree>[Tree]
[ Error  ] } ensuring {
[ Error  ]   nodesGood
[ Error  ] }, expected Tree,
[ Error  ] found <untyped>
[ Error  ] 
[ Error  ] Typing explanation:
[ Error  ] {
[ Error  ]   <empty tree>[Tree]
[ Error  ] } ensuring {
[ Error  ]   nodesGood
[ Error  ] } is of type <untyped>
[ Error  ]   <empty tree>[Tree] is of type Tree
[ Error  ]   nodesGood is of type (Node) => Boolean
[ Error  ]     nodesGood(_$1) is of type Boolean
[ Error  ]       _$1 is of type Node because nodesGood was instantiated with  with type (Tree) => Boolean
             def myTree1: Tree = {
                                 ^...
[ Fatal  ] Well-formedness check failed after extraction

in Stainless Version: 0.9.8.7-14-g7fd69e2

[vkuncak]

The workaround is to explicitly type the result of the closure given to ensuring ,

  @extern
  def myTree1: Tree = {
    Node()    
  } ensuring((res: Tree) => res.nodesGood)

[mario-bucev]

Or explicitly widen the resulting expression:

@extern
def myTree1: Tree = {
  Node() : Tree
} (_.nodesGood)