Operator follows same abstraction principle as NAryType

src/main/scala/inox/ast/ExprOps.scala

@@ -32,7 +32,7 @@ trait ExprOps extends GenTreeOps {
   type Source = Expr
   type Target = Expr
 
-  val Deconstructor = Operator
+  lazy val Deconstructor = Operator
 
   /** Replaces bottom-up variables by looking up for them in a map */
   def replaceFromSymbols[V <: VariableSymbol](substs: Map[V, Expr], expr: Expr)(implicit ev: VariableConverter[V]): Expr = {

src/main/scala/inox/ast/Extractors.scala

@@ -239,11 +239,23 @@ trait Extractors { self: Trees =>
     * tools for performing tree transformations that are very predictable, if
     * one need to simplify the tree, it is easy to write/call a simplification
     * function that would simply apply the corresponding constructor for each node.
+    *
+    * XXX: ideally, we would want [[Operator]] to be defined as
+    * {{{
+    *   val Operator: ExprDeconstructor {
+    *     val s: self.type
+    *     val t: self.type
+    *   }
+    * }}}
+    * however the Scala compiler seems to have some bug with this and reports
+    * wrong errors when we define it this way...
+    * @see https://issues.scala-lang.org/browse/SI-9247
     */
-
-  object Operator extends ExprDeconstructor {
-    val s: self.type = self
-    val t: self.type = self
+  val Operator: TreeExtractor {
+    val s: self.type
+    val t: self.type
+    type Source = self.Expr
+    type Target = self.Expr
   }
 
   object TopLevelOrs { // expr1 OR (expr2 OR (expr3 OR ..)) => List(expr1, expr2, expr3)

src/main/scala/inox/ast/Types.scala

@@ -85,6 +85,10 @@ trait Types { self: Trees =>
     def tcd(implicit s: Symbols): TypedClassDef = s.getClass(id, tps)
   }
 
+  /** NAryType extractor to extract any Type in a consistent way.
+    *
+    * @see [[Extractors.Operator]] about why we can't have nice(r) things
+    */
   val NAryType: TreeExtractor {
     val s: self.type
     val t: self.type

src/main/scala/inox/package.scala

 /* Copyright 2009-2016 EPFL, Lausanne */
 
-import inox.ast.TypeDeconstructor
-
 /** Core package of the Inox solving interface
   *
   * == Structure ==
@@ -45,10 +43,15 @@ package object inox {
 
   object trees extends ast.Trees {
 
+    object Operator extends {
+      protected val s: trees.type = trees
+      protected val t: trees.type = trees
+    } with ast.ExprDeconstructor
+
     object NAryType extends {
       protected val s: trees.type = trees
       protected val t: trees.type = trees
-    } with TypeDeconstructor
+    } with ast.TypeDeconstructor
 
     class Symbols(
       val functions: Map[Identifier, FunDef],