From a5a80503a066d5aa7617e7ed4bb46c3ede5c0be2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= <jonas.fiala@inf.ethz.ch>
Date: Mon, 5 Feb 2024 11:19:32 +0100
Subject: [PATCH] Tests pass

---
 src/main/scala/viper/silver/ast/Program.scala |  29 +-
 .../ast/utility/QuantifiedPermissions.scala   |   4 +-
 .../ast/utility/rewriter/Rewritable.scala     |  33 +-
 .../ast/utility/rewriter/Strategy.scala       |   1 +
 .../viper/silver/parser/FastParser.scala      |  57 +-
 .../viper/silver/parser/MacroExpander.scala   |  19 +-
 .../scala/viper/silver/parser/ParseAst.scala  | 463 +++++++---
 .../viper/silver/parser/ParseAstKeyword.scala |  39 +-
 .../viper/silver/parser/ParseAstLsp.scala     |  21 +-
 .../scala/viper/silver/parser/Resolver.scala  | 790 +++++++++---------
 .../viper/silver/parser/Transformer.scala     | 160 ----
 .../viper/silver/parser/Translator.scala      |  38 +-
 .../standard/adt/AdtPASTExtension.scala       | 370 ++++----
 .../plugin/standard/adt/AdtPlugin.scala       |  25 +-
 .../PredicateInstancePASTExtension.scala      |  22 +-
 .../PredicateInstancePlugin.scala             |   2 +-
 .../plugin/standard/refute/RefutePlugin.scala |   2 +-
 .../termination/TerminationPlugin.scala       |  33 +-
 src/test/resources/all/basic/syntax.vpr       |   3 +-
 src/test/resources/all/issues/carbon/0364.vpr |   4 +-
 .../resources/all/issues/silicon/0291.vpr     |   4 +-
 src/test/resources/all/issues/silver/0039.vpr |   8 +-
 src/test/resources/all/issues/silver/0069.vpr |  10 +-
 .../resources/all/issues/silver/0106-1.vpr    |   6 +-
 src/test/resources/all/issues/silver/0120.vpr |   4 +-
 src/test/resources/all/issues/silver/0164.vpr |   2 +-
 .../resources/all/issues/silver/0175b.vpr     |   2 +-
 src/test/resources/all/issues/silver/0469.vpr |   2 +-
 src/test/resources/all/issues/silver/0697.vpr |   8 +-
 src/test/resources/all/issues/silver/0720.vpr |   2 +-
 .../resources/all/parsing/assign_ambig.vpr    |   7 +
 .../all/parsing/typed_call_ambig2.vpr         |   2 +
 .../permission_introspection/forpermCheck.vpr |   8 +-
 .../wands/regression/consistency.vpr          |  16 -
 .../wands/regression/consistency2.vpr         |  22 +
 src/test/scala/ASTTransformationTests.scala   |  10 +-
 src/test/scala/PluginTests.scala              |   3 +-
 src/test/scala/SemanticAnalysisTests.scala    |   4 +-
 38 files changed, 1152 insertions(+), 1083 deletions(-)
 delete mode 100644 src/main/scala/viper/silver/parser/Transformer.scala
 create mode 100644 src/test/resources/all/parsing/assign_ambig.vpr
 create mode 100644 src/test/resources/wands/regression/consistency2.vpr

diff --git a/src/main/scala/viper/silver/ast/Program.scala b/src/main/scala/viper/silver/ast/Program.scala
index c12616c80..b46953b99 100644
--- a/src/main/scala/viper/silver/ast/Program.scala
+++ b/src/main/scala/viper/silver/ast/Program.scala
@@ -214,18 +214,20 @@ case class Program(domains: Seq[Domain], fields: Seq[Field], functions: Seq[Func
     }
 
     def checkNamesInScope(currentScope: Scope, dMap: immutable.HashMap[String, Declaration]) : Seq[ConsistencyError] = {
-      var declarationMap = dMap
+      var newMap = immutable.HashMap.empty[String, Declaration]
       var s: Seq[ConsistencyError] = Seq.empty[ConsistencyError]
       //check name declarations
       currentScope.scopedDecls.foreach(l=> {
         if(!Consistency.validUserDefinedIdentifier(l.name))
           s :+= ConsistencyError(s"${l.name} is not a valid identifier.", l.pos)
 
-        declarationMap.get(l.name) match {
-          case Some(_: Declaration) => s :+= ConsistencyError(s"Duplicate identifier ${l.name} found.", l.pos)
-          case None => declarationMap += (l.name -> l)
+        newMap.get(l.name) match {
+          case Some(_: Declaration) => s :+= ConsistencyError(s"Duplicate identifier `${l.name}` found.", l.pos)
+          case None => newMap += (l.name -> l)
         }
       })
+      // Override duplicate keys in old map
+      val declarationMap = dMap ++ newMap
 
       //check name uses
       Visitor.visitOpt(currentScope.asInstanceOf[Node], Nodes.subnodes){ n => {
@@ -409,11 +411,13 @@ case class Method(name: String, formalArgs: Seq[LocalVarDecl], formalReturns: Se
   }
 
   def deepCollectInBody[A](f: PartialFunction[Node, A]): Seq[A] = body match {
+    case null => Nil
+    case None => Nil
     case Some(actualBody) => actualBody.deepCollect(f)
-    case None => Seq()
   }
 
-  val scopedDecls: Seq[Declaration] = formalArgs ++ formalReturns
+  def labels: Seq[Label] = deepCollectInBody { case l: Label => l }
+  val scopedDecls: Seq[Declaration] = formalArgs ++ formalReturns ++ labels
 
   override lazy val check: Seq[ConsistencyError] =
     pres.flatMap(Consistency.checkPre) ++
@@ -444,19 +448,6 @@ case class Method(name: String, formalArgs: Seq[LocalVarDecl], formalReturns: Se
   def toCfg(simplify: Boolean = true, detect: Boolean = true): SilverCfg = CfgGenerator.methodToCfg(this, simplify, detect)
 }
 
-object MethodWithLabelsInScope {
-  def apply(name: String, formalArgs: Seq[LocalVarDecl], formalReturns: Seq[LocalVarDecl], pres: Seq[Exp], posts: Seq[Exp], body: Option[Seqn])
-                 (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): Method = {
-    val newBody = body match {
-      case Some(actualBody) =>
-        val newScopedDecls = actualBody.scopedSeqnDeclarations ++ actualBody.deepCollect({case l: Label => l})
-        Some(actualBody.copy(scopedSeqnDeclarations = newScopedDecls)(actualBody.pos, actualBody.info, actualBody.errT))
-      case _ => body
-    }
-    Method(name, formalArgs, formalReturns, pres, posts, newBody)(pos, info, errT)
-  }
-}
-
 /** A function declaration */
 case class Function(name: String, formalArgs: Seq[LocalVarDecl], typ: Type, pres: Seq[Exp], posts: Seq[Exp], body: Option[Exp])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Member with FuncLike with Contracted {
   override lazy val check : Seq[ConsistencyError] =
diff --git a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
index 763baca44..5d99d4e62 100644
--- a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
+++ b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
@@ -141,9 +141,9 @@ object QuantifiedPermissions {
       val currentRoot = toVisit.dequeue()
 
       val relevantNodes: Seq[Node] = currentRoot match {
-        case m@Method(_, _, _, pres, posts, _) if m != root =>
+        case m: Method if m != root =>
           // use only specification of called methods
-          pres ++ posts
+          m.pres ++ m.posts
         case f@Function(_, _, _, pres, posts, _) if f != root =>
           // use only specification of called functions
           pres ++ posts
diff --git a/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala b/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala
index 0be8156d9..78c250b9d 100644
--- a/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala
+++ b/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala
@@ -6,11 +6,18 @@
 
 package viper.silver.ast.utility.rewriter
 
-import viper.silver.parser.Transformer.ParseTreeDuplicationError
+import viper.silver.parser.PNode
 import viper.silver.ast.{AtomicType, BackendFuncApp, DomainFuncApp, ErrorTrafo, FuncApp, Info, Node, Position}
 
 import scala.reflect.runtime.{universe => reflection}
 
+trait HasExtraValList {
+  def getExtraVals: Seq[Any]
+}
+trait HasExtraVars {
+  def copyExtraVars(from: Any): Unit
+}
+
 /**
   * Trait Rewritable provides an interface that specifies which methods are required for the rewriter to work with.
   * For classes that implement product (especially case classes) everything is already implemented here and one only has to extend this base class
@@ -39,8 +46,8 @@ trait Rewritable extends Product {
         val firstArgList = children
         var secondArgList = Seq.empty[Any]
         import viper.silver.ast.{DomainType, DomainAxiom, FuncApp, DomainFunc, DomainFuncApp}
-        import viper.silver.parser.{PAxiom, PDomainFunction, PDomainType, PNode}
         this match {
+          // TODO: remove the following cases by implementing `HasExtraValList` on the respective classes
           case dt: DomainType => secondArgList = Seq(dt.typeParameters)
           case da: DomainAxiom => secondArgList = Seq(da.pos, da.info, da.domainName, da.errT)
           case fa: FuncApp => secondArgList = Seq(fa.pos, fa.info, fa.typ, fa.errT)
@@ -48,9 +55,14 @@ trait Rewritable extends Product {
           case df: DomainFuncApp => secondArgList = Seq(df.pos, df.info, df.typ, df.domainName, df.errT)
           case ba: BackendFuncApp => secondArgList = Seq(ba.pos, ba.info, ba.typ, ba.interpretation, ba.errT)
           case no: Node => secondArgList = no.getMetadata
-          case pa: PAxiom => secondArgList = Seq(pa.domainName) ++ Seq(pos.getOrElse(pa.pos))
-          case pd: PDomainFunction => secondArgList = Seq(pd.domainName) ++ Seq(pos.getOrElse(pd.pos))
-          case pn: PNode => secondArgList = Seq(pos.getOrElse(pn.pos))
+
+          case evl: HasExtraValList => {
+            secondArgList = evl.getExtraVals.map(ev => {
+              // Replace positions with the new one
+              val replace = pos.isDefined && ev.isInstanceOf[(_, _)] && ev.asInstanceOf[(_, _)]._1.isInstanceOf[Position] && ev.asInstanceOf[(_, _)]._2.isInstanceOf[Position]
+              if (replace) pos.get else ev
+            })
+          }
           case _ =>
         }
 
@@ -62,9 +74,9 @@ trait Rewritable extends Product {
         }
 
         // Copy member values, as they aren't in the parameters' list.
-        this match {
-          case dt: PDomainType =>
-            newNode.asInstanceOf[PDomainType].kind = dt.kind
+        newNode match {
+          case ev: HasExtraVars =>
+            ev.copyExtraVars(this)
           case _ =>
         }
 
@@ -109,4 +121,9 @@ trait Rewritable extends Product {
       newNode.asInstanceOf[this.type]
     }
   }
+
+  def initProperties(): Unit = ()
 }
+
+case class ParseTreeDuplicationError(original: PNode, newChildren: Seq[Any])
+    extends RuntimeException(s"Cannot duplicate $original with new children $newChildren")
diff --git a/src/main/scala/viper/silver/ast/utility/rewriter/Strategy.scala b/src/main/scala/viper/silver/ast/utility/rewriter/Strategy.scala
index 170f43609..39048aee4 100644
--- a/src/main/scala/viper/silver/ast/utility/rewriter/Strategy.scala
+++ b/src/main/scala/viper/silver/ast/utility/rewriter/Strategy.scala
@@ -356,6 +356,7 @@ class Strategy[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag, C
       case Traverse.Innermost => rewriteInnermost(node, contextUsed)
     }
     changed = !(result eq node)
+    result.initProperties()
     result
   }
 
diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index 24844c188..7588a8961 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -41,7 +41,7 @@ object FastParserCompanion {
   def identStarts[$: P] = CharIn("A-Z", "a-z", "$_")
   def identContinues[$: P] = CharIn("0-9", "A-Z", "a-z", "$_")
 
-  type Pos = (Position, Position)
+  type Pos = (FilePosition, FilePosition)
   import scala.language.implicitConversions
   implicit def LeadingWhitespaceStr[$: P](p: String): LeadingWhitespace[Unit] = new LeadingWhitespace(() => P(p))
   implicit def LeadingWhitespace[T](p: => P[T]) = new LeadingWhitespace(() => p)
@@ -62,7 +62,7 @@ object FastParserCompanion {
     def ~~~[$: P, V, R](other: LW[V])(implicit s: Implicits.Sequencer[T, V, R]): P[R] = (p() ~~ other.p()).asInstanceOf[P[R]]
     def ~~~/[$: P, V, R](other: LW[V])(implicit s: Implicits.Sequencer[T, V, R]): P[R] = (p() ~~/ other.p()).asInstanceOf[P[R]]
   }
-  class PositionParsing[T](val p: () => P[((Position, Position)) => T]) extends AnyVal {
+  class PositionParsing[T](val p: () => P[((FilePosition, FilePosition)) => T]) extends AnyVal {
     def pos(implicit ctx: P[Any], lineCol: LineCol, _file: Path): P[T] = {
       // TODO: switch over to this?
       // Index ~~ p() ~~ Index map { case (start, f, end) => {
@@ -71,7 +71,7 @@ object FastParserCompanion {
       //   f((FilePosition(_file, startPos._1, startPos._2), FilePosition(_file, finishPos._1, finishPos._2)))
       // }}
       val startPos = lineCol.getPos(ctx.index)
-      val res: P[((Position, Position)) => T] = p()
+      val res: P[((FilePosition, FilePosition)) => T] = p()
       val finishPos = lineCol.getPos(ctx.index)
       res.map(_((FilePosition(_file, startPos._1, startPos._2), FilePosition(_file, finishPos._1, finishPos._2))))
     }
@@ -286,7 +286,7 @@ class FastParser {
           j += 1
         }
       }
-      PProgram(imports, macros, domains, fields, functions, predicates, methods, extensions, errors)(p.pos)
+      PProgram(imports, macros, domains, fields, functions, predicates, methods, extensions)(p.pos, errors)
     }
 
 
@@ -304,7 +304,7 @@ class FastParser {
           case _ =>
             SourcePosition(_file, 0, 0)
         }
-        PProgram(Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Seq(ParseError(msg, location)))((NoPosition, NoPosition))
+        PProgram(Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)((NoPosition, NoPosition), Seq(ParseError(msg, location)))
     }
   }
 
@@ -517,9 +517,9 @@ class FastParser {
 
   def idnuse[$: P]: P[PIdnUseExp] = P(ident map (PIdnUseExp.apply _)).pos
 
-  def idnref[$: P]: P[PIdnRef] = P(ident map (PIdnRef.apply _)).pos
+  def idnref[$: P, T <: PDeclarationInner](implicit ctag: scala.reflect.ClassTag[T]): P[PIdnRef[T]] = P(ident map (PIdnRef.apply[T] _)).pos
 
-  def oldLabel[$: P]: P[PLabelUse] = P((P(PKw.Lhs) map (PLhsLabel.apply _)).pos | idnuse)
+  def oldLabel[$: P]: P[Either[PKw.Lhs, PIdnRef[PLabel]]] = P((P(PKw.Lhs) map (Left(_))) | (idnref[$, PLabel] map (Right(_))))
 
   def old[$: P]: P[PKwOp.Old => Pos => POldExp] = P(oldLabel.brackets.? ~ exp.parens).map {
     case (lbl, g) => POldExp(_, lbl, g)
@@ -560,7 +560,7 @@ class FastParser {
       => SuffixedExpressionGenerator[PExp](e0 => PLookup(e0, l, e1, r)(e0.pos._1, pos._2)) })
 
   def fieldAccess[$: P]: P[SuffixedExpressionGenerator[PExp]] =
-    P(((!P(PSymOp.DotDot) ~~ PSymOp.Dot) ~ idnref) map { case (dot, id) => pos: Pos => SuffixedExpressionGenerator[PExp](e => PFieldAccess(e, dot, id)(e.pos._1, pos._2)) }).pos
+    P(((!P(PSymOp.DotDot) ~~ PSymOp.Dot) ~ idnref[$, PFieldDecl]) map { case (dot, id) => pos: Pos => SuffixedExpressionGenerator[PExp](e => PFieldAccess(e, dot, id)(e.pos._1, pos._2)) }).pos
 
   def sliceEnd[$: P]: P[((PSymOp.LBracket, PSymOp.RBracket)) => Pos => SuffixedExpressionGenerator[PExp]] =
     P((P(PSymOp.DotDot) ~ exp).map { case (d, n) => b => pos: Pos
@@ -617,9 +617,9 @@ class FastParser {
 
   def chainComp(op: PReserved[PBinaryOp], right: PExp)(pos: Pos)(from: PExp) = SuffixedExpressionGenerator(_ match {
       case left@PBinExp(_, op0, middle) if cmpOps.contains(op0.rs.token) && left != from =>
-        PBinExp(left, PReserved(PSymOp.AndAnd)(NoPosition, NoPosition), PBinExp(middle, op, right)(middle.pos._1, pos._2))(left.pos._1, pos._2)
+        PBinExp(left, PReserved(PSymOp.AndAnd)(NoPosition, NoPosition), PBinExp(middle.deepCopyAll.asInstanceOf[PExp], op, right)(middle.pos._1, pos._2))(left.pos._1, pos._2)
       case left@PBinExp(_, PReserved(PSymOp.AndAnd), PBinExp(_, op0, middle)) if cmpOps.contains(op0.rs.token) && left != from =>
-        PBinExp(left, PReserved(PSymOp.AndAnd)(NoPosition, NoPosition), PBinExp(middle, op, right)(middle.pos._1, pos._2))(left.pos._1, pos._2)
+        PBinExp(left, PReserved(PSymOp.AndAnd)(NoPosition, NoPosition), PBinExp(middle.deepCopyAll.asInstanceOf[PExp], op, right)(middle.pos._1, pos._2))(left.pos._1, pos._2)
       case left => PBinExp(left, op, right)(left.pos._1, pos._2)
   })
 
@@ -674,11 +674,7 @@ class FastParser {
     P(idndef ~ PSymOp.EqEq ~ parenthesizedExp ~ PKwOp.In ~ exp).map {
       case (id, eq, exp1, in, exp2) =>
         val nestedScope = PLetNestedScope(exp2)(exp2.pos)
-        k => pos => {
-          val let = PLet(k, id, eq, exp1, in, nestedScope)(pos)
-          nestedScope.outerLet = let
-          let
-        }
+        k => PLet(k, id, eq, exp1, in, nestedScope)(_)
     }
 
   def idndef[$: P]: P[PIdnDef] = P(ident map (PIdnDef.apply _)).pos
@@ -717,7 +713,7 @@ class FastParser {
 
   def typ[$: P]: P[PType] = P(typReservedKw | domainTyp | macroType)
 
-  def domainTyp[$: P]: P[PDomainType] = P((idnref ~~~ typeList(typ).lw.?) map (PDomainType.apply _).tupled).pos
+  def domainTyp[$: P]: P[PDomainType] = P((idnref[$, PTypeDeclaration] ~~~ typeList(typ).lw.?) map (PDomainType.apply _).tupled).pos
 
   def seqType[$: P]: P[PKw.Seq => Pos => PSeqType] = P(typ.brackets map { t => PSeqType(_, t) })
 
@@ -804,11 +800,15 @@ class FastParser {
 
   def newExp[$: P]: P[PKw.New => Pos => PNewExp] = P(newExpFields.parens map { n => PNewExp(_, n) })
 
-  def newExpFields[$: P]: P[Either[PSym.Star, PDelimited[PIdnUseExp, PSym.Comma]]] = P(P(PSym.Star).map(Left(_)) | P(idnuse.delimited(PSym.Comma).map(Right(_))))
+  def newExpFields[$: P]: P[Either[PSym.Star, PDelimited[PIdnRef[PFieldDecl], PSym.Comma]]] = P(P(PSym.Star).map(Left(_)) | P(idnref[$, PFieldDecl].delimited(PSym.Comma).map(Right(_))))
 
-  def funcApp[$: P]: P[PCall] = P((idnref ~ argList(exp)) map {
-    case (func, args) => PCall(func, args, None)(_)
-  }).pos
+  def funcApp[$: P]: P[PCall] = P(idnref[$, PGlobalCallable] ~~ " ".repX(1).map { _ => pos: Pos => pos }.pos.? ~~ argList(exp)).map {
+    case (func, space, args) =>
+      space.foreach { space =>
+        _warnings = _warnings :+ ParseWarning("Whitespace between a function identifier and the opening paren is deprecated, remove the spaces", SourcePosition(_file, space._1, space._2))
+      }
+      PCall(func, args, None)(_)
+  }.pos
 
   def maybeTypedFuncApp[$: P](bracketed: Boolean): P[PCall] = P(if (!bracketed) funcApp else (funcApp ~~~ (P(PSym.Colon) ~ typ).lw.?).map {
     case (func, typeGiven) => func.copy(typeAnnotated = typeGiven)(_)
@@ -905,13 +905,13 @@ class FastParser {
     P((nonEmptyIdnTypeList(PLocalVarDecl(_)) ~~~ (P(PSymOp.Assign) ~ exp).lw.?) map { case (a, i) => PVars(_, a, i) })
 
   def defineDecl[$: P]: P[PKw.Define => PAnnotationsPosition => PDefine] =
-    P((idndef ~~~/ NoCut(argList(idndef)).lw.? ~ (stmtBlock(false) | exp)) map {
+    P((idndef ~~~/ NoCut(argList((idndef map PDefineParam.apply).pos)).lw.? ~ (stmtBlock(false) | exp)) map {
       case (idn, args, body) => k => ap: PAnnotationsPosition => PDefine(ap.annotations, k, idn, args, body)(ap.pos)
     })
 
   def defineDeclStmt[$: P]: P[PKw.Define => Pos => PDefine] = P(defineDecl.map { f => k => pos: Pos => f(k)(PAnnotationsPosition(Nil, pos)) })
 
-  def goto[$: P]: P[PKw.Goto => Pos => PGoto] = P(idnuse map { i => PGoto(_, i) _ })
+  def goto[$: P]: P[PKw.Goto => Pos => PGoto] = P(idnref[$, PLabel] map { i => PGoto(_, i) _ })
 
   def label[$: P]: P[PKw.Label => Pos => PLabel] =
     P((idndef ~ semiSeparated(invariant)) map { case (i, inv) => k=> PLabel(k, i, inv) _ })
@@ -954,8 +954,7 @@ class FastParser {
         decls.collect { case p: PPredicate => p }, // Predicates
         decls.collect { case m: PMethod => m }, // Methods
         decls.collect { case e: PExtender => e }, // Extensions
-        warnings // Parse Warnings
-      )(_)
+      )(_, warnings) // Parse Warnings
     }
   }).pos
 
@@ -981,8 +980,8 @@ class FastParser {
       val members = block.inner.members
       val funcs1 = members collect { case m: PDomainFunction1 => m }
       val axioms1 = members collect { case m: PAxiom1 => m }
-      val funcs = funcs1 map (f => (PDomainFunction(f.annotations, f.unique, f.function, f.idndef, f.args, f.c, f.typ, f.interpretation)(PIdnRef(name.name)(name.pos))(f.pos), f.s))
-      val axioms = axioms1 map (a => (PAxiom(a.annotations, a.axiom, a.idndef, a.exp)(PIdnRef(name.name)(name.pos))(a.pos), a.s))
+      val funcs = funcs1 map (f => (PDomainFunction(f.annotations, f.unique, f.function, f.idndef, f.args, f.c, f.typ, f.interpretation)(f.pos), f.s))
+      val axioms = axioms1 map (a => (PAxiom(a.annotations, a.axiom, a.idndef, a.exp)(a.pos), a.s))
       val allMembers = block.update(PDomainMembers(PDelimited(funcs)(NoPosition, NoPosition), PDelimited(axioms)(NoPosition, NoPosition))(block.pos))
       k => ap: PAnnotationsPosition => PDomain(
         ap.annotations,
@@ -1000,11 +999,11 @@ class FastParser {
     case (unique, (function, idn, args, c, typ), interpretation, s) => ap: PAnnotationsPosition => PDomainFunction1(ap.annotations, unique, function, idn, args, c, typ, interpretation, s)(ap.pos)
   }
 
-  def domainFunctionSignature[$: P] = P(P(PKw.Function) ~ idndef ~ argList(formalArg | unnamedFormalArg) ~ PSym.Colon ~ typ)
+  def domainFunctionSignature[$: P] = P(P(PKw.Function) ~ idndef ~ argList(domainFunctionArg) ~ PSym.Colon ~ typ)
 
-  def formalArg[$: P]: P[PFormalArgDecl] = P(idnTypeBinding.map(PFormalArgDecl(_)))
+  def domainFunctionArg[$: P]: P[PDomainFunctionArg] = P(idnTypeBinding.map(PDomainFunctionArg(_)) | typ.map(PDomainFunctionArg(None, None, _) _).pos)
 
-  def unnamedFormalArg[$: P] = P(typ map (PUnnamedFormalArgDecl.apply _)).pos
+  def formalArg[$: P]: P[PFormalArgDecl] = P(idnTypeBinding map (PFormalArgDecl(_)))
 
   def bracedExp[$: P]: P[PBracedExp] = P(exp.braces map (PBracedExp(_) _)).pos
 
diff --git a/src/main/scala/viper/silver/parser/MacroExpander.scala b/src/main/scala/viper/silver/parser/MacroExpander.scala
index 910bd9325..1a48508a7 100644
--- a/src/main/scala/viper/silver/parser/MacroExpander.scala
+++ b/src/main/scala/viper/silver/parser/MacroExpander.scala
@@ -7,8 +7,7 @@
 package viper.silver.parser
 
 import viper.silver.ast.{FilePosition, Position, SourcePosition}
-import viper.silver.ast.utility.rewriter.{ContextA, PartialContextC, StrategyBuilder}
-import viper.silver.parser.Transformer.ParseTreeDuplicationError
+import viper.silver.ast.utility.rewriter.{ContextA, ParseTreeDuplicationError, PartialContextC, StrategyBuilder}
 import viper.silver.verifier.ParseWarning
 
 import scala.collection.mutable
@@ -63,7 +62,7 @@ object MacroExpander {
       val (replacer, freeVars) = makeReplacer()
       // Execute with empty replacer, thus no variables will be replaced but freeVars will be filled
       replacer.execute(define)
-      val parameters = define.parameters.map(_.inner.toSeq).getOrElse(Seq.empty[PIdnDef]).map(_.name).toSet
+      val parameters = define.parameters.map(_.inner.toSeq).getOrElse(Seq.empty).map(_.idndef.name).toSet
       val nonUsedParameter = parameters -- freeVars
 
       if (nonUsedParameter.nonEmpty) {
@@ -151,7 +150,7 @@ object MacroExpander {
       linearizeMethod(doExpandDefines(localMacros ++ globalMacros, methodWithoutMacros, p))
     })
 
-    PProgram(p.imports, p.macros, domains, p.fields, functions, predicates, methods, p.extensions, p.errors ++ warnings)(p.pos)
+    PProgram(p.imports, p.macros, domains, p.fields, functions, predicates, methods, p.extensions)(p.pos, p.errors ++ warnings)
   }
 
 
@@ -203,8 +202,8 @@ object MacroExpander {
     }
 
     // Create a map that maps the formal parameters to the actual arguments of a macro call
-    def mapParamsToArgs(params: Seq[PIdnDef], args: Seq[PExp]): Map[String, PExp] = {
-      params.map(_.name).zip(args).toMap
+    def mapParamsToArgs(params: Seq[PDefineParam], args: Seq[PExp]): Map[String, PExp] = {
+      params.map(_.idndef.name).zip(args).toMap
     }
 
     /* Abstraction over several possible `PNode`s that can represent macro applications */
@@ -427,17 +426,17 @@ object MacroExpander {
       // Variable use: macro parameters are replaced by their respective argument expressions
       case (varUse: PIdnUseExp, ctx) if !ctx.c.boundVars.contains(varUse.name) =>
         if (ctx.c.paramToArgMap.contains(varUse.name))
-          (ctx.c.paramToArgMap(varUse.name), ctx.updateContext(ctx.c.copy(paramToArgMap = ctx.c.paramToArgMap.empty)))
+          (ctx.c.paramToArgMap(varUse.name).deepCopyAll, ctx.updateContext(ctx.c.copy(paramToArgMap = ctx.c.paramToArgMap.empty)))
         else {
           freeVars += varUse.name
           (varUse, ctx)
         }
-      case (varUse: PIdnRef, ctx) if !ctx.c.boundVars.contains(varUse.name) =>
+      case (varUse: PIdnRef[_], ctx) if !ctx.c.boundVars.contains(varUse.name) =>
         if (ctx.c.paramToArgMap.contains(varUse.name)) {
-          val replacement = ctx.c.paramToArgMap(varUse.name)
+          val replacement = ctx.c.paramToArgMap(varUse.name).deepCopyAll
           if (replacement.isInstanceOf[PIdnUseExp]) {
             val repExp = replacement.asInstanceOf[PIdnUseExp]
-            (PIdnRef(repExp.name)(repExp.pos), ctx.updateContext(ctx.c.copy(paramToArgMap = ctx.c.paramToArgMap.empty)))
+            (PIdnRef(repExp.name)(repExp.pos)(varUse.ctag), ctx.updateContext(ctx.c.copy(paramToArgMap = ctx.c.paramToArgMap.empty)))
           } else
             throw ParseException(s"Macro expansion cannot substitute expression `${replacement.pretty}` in non-expression position at ${varUse.pos._1}.", replacement.pos)
         } else {
diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala
index 5b675073d..46ac168eb 100644
--- a/src/main/scala/viper/silver/parser/ParseAst.scala
+++ b/src/main/scala/viper/silver/parser/ParseAst.scala
@@ -8,7 +8,7 @@ package viper.silver.parser
 
 import java.util.concurrent.atomic.{AtomicInteger, AtomicLong}
 import viper.silver.ast.utility.Visitor
-import viper.silver.ast.utility.rewriter.{Rewritable, StrategyBuilder}
+import viper.silver.ast.utility.rewriter.{Rewritable, StrategyBuilder, HasExtraVars, HasExtraValList}
 import viper.silver.ast.{Exp, Member, NoPosition, Position, Stmt, Type}
 import viper.silver.parser.TypeHelper._
 import viper.silver.verifier.ParseReport
@@ -28,7 +28,7 @@ trait Where {
   * The root of the parser abstract syntax tree.  Note that we prefix all nodes with `P` to avoid confusion
   * with the actual Viper abstract syntax tree.
   */
-trait PNode extends Where with Product with Rewritable {
+trait PNode extends Where with Product with Rewritable with HasExtraValList {
 
   /* Should output something that can be displayed to the user. */
   def pretty: String
@@ -98,13 +98,22 @@ trait PNode extends Where with Product with Rewritable {
 
   private val _children = scala.collection.mutable.ListBuffer[PNode]()
 
+  def getParent: Option[PNode] = parent
+  def getAncestor[T](implicit ctag: scala.reflect.ClassTag[T]): Option[T] = {
+    var p = getParent
+    while (p.isDefined && !ctag.runtimeClass.isInstance(p.get))
+      p = p.get.getParent
+    p.map(_.asInstanceOf[T])
+  }
+  def getEnclosingScope: Option[PScope] = getAncestor[PScope]
+  def isDescendant[T](implicit ctag: scala.reflect.ClassTag[T]): Boolean = getAncestor[T].isDefined
 
-  var parent: Option[PNode] = None
+  private var parent: Option[PNode] = None
   var index: Int = -1
   var next: Option[PNode] = None
   var prev: Option[PNode] = None
 
-  def initProperties(): Unit = {
+  override def initProperties(): Unit = {
 
     var ind: Int = 0
     var prev: Option[PNode] = None
@@ -123,12 +132,7 @@ trait PNode extends Where with Product with Rewritable {
     }
   }
 
-  def getEnclosingScope: Option[PScope] = {
-    var p = parent
-    while (p.isDefined && !p.get.isInstanceOf[PScope])
-      p = p.get.parent
-    p.map(_.asInstanceOf[PScope])
-  }
+  override def getExtraVals: Seq[Any] = Seq(pos)
 }
 
 /** Marks that this class contains no PNodes and thus should not be traversed deeper. */
@@ -175,13 +179,55 @@ object TypeHelper {
   val Bool = PPrimitiv(PReserved.implied(PKw.Bool))(NoPosition, NoPosition)
   val Perm = PPrimitiv(PReserved.implied(PKw.Perm))(NoPosition, NoPosition)
   val Ref = PPrimitiv(PReserved.implied(PKw.Ref))(NoPosition, NoPosition)
-  val Wand = PWandType()(NoPosition, NoPosition)
+  val Impure = PBoolImpureType()
+  val Wand = PBoolWandType()
+  val Predicate = PBoolPredicateType()
   def MakeSet(typ: PType) = PSetType(PReserved.implied(PKw.Set), PGrouped.impliedBracket(typ))(NoPosition, NoPosition)
   def MakeSeq(typ: PType) = PSeqType(PReserved.implied(PKw.Seq), PGrouped.impliedBracket(typ))(NoPosition, NoPosition)
   def MakeMap(key: PType, value: PType) = PMapType(PReserved.implied(PKw.Map), PGrouped.impliedBracket(
       PPairArgument(key, PReserved.implied(PSym.Comma), value)(NoPosition, NoPosition)
     ))(NoPosition, NoPosition)
   def MakeMultiset(typ: PType) = PMultisetType(PReserved.implied(PKw.Multiset), PGrouped.impliedBracket(typ))(NoPosition, NoPosition)
+
+  def commonSupertype(a: PType, b: PType): Option[PType] = {
+    (a, b) match {
+      case _ if a == b => Some(a)
+      case (PFunctionType(args1, res1), PFunctionType(args2, res2)) if args1.length == args2.length =>
+        val args = args1.zip(args2).map(p => commonSubtype(p._1, p._2))
+        (args.forall(_.isDefined), commonSupertype(res1, res2)) match {
+          case (true, Some(res)) => Some(PFunctionType(args.map(_.get), res))
+          case _ => None
+        }
+      case _ => (a.umbrella, b.umbrella) match {
+        case (Some(au), Some(bu)) if au == bu => Some(au)
+        case (Some(au), None) if au == b => Some(au)
+        case (None, Some(bu)) if a == bu => Some(a)
+        case _ => None
+      }
+    }
+  }
+  def commonSubtype(a: PType, b: PType): Option[PType] = {
+    (a, b) match {
+      case _ if a == b => Some(a)
+      case (PFunctionType(args1, res1), PFunctionType(args2, res2)) if args1.length == args2.length =>
+        val args = args1.zip(args2).map(p => commonSupertype(p._1, p._2))
+        (args.forall(_.isDefined), commonSubtype(res1, res2)) match {
+          case (true, Some(res)) => Some(PFunctionType(args.map(_.get), res))
+          case _ => None
+        }
+      case _ => (a.umbrella, b.umbrella) match {
+        case (Some(au), None) if au == b => Some(a)
+        case (None, Some(bu)) if a == bu => Some(b)
+        case _ => None
+      }
+    }
+  }
+
+  /** Is type `sub` a subtype of type `sup` (i.e. `sub` can be used in a place where `sup` is expected) */
+  def isSubtype(sub: PType, sup: PType): Boolean = {
+    val commonSup = commonSupertype(sub, sup)
+    commonSup.isDefined && commonSup.get == sup
+  }
 }
 
 ///////////////////////////////////////////////////////////////////////////
@@ -195,15 +241,41 @@ trait PIdentifier extends PLeaf {
 case class PIdnDef(name: String)(val pos: (Position, Position)) extends PNode with PIdentifier
 
 trait PIdnUse extends PNode with PIdentifier {
-  var decl: Option[PDeclaration] = None
+  def decl: Option[PDeclarationInner]
+
   // Set for `x` when `x := ...`, set for `f` only when `x.f := ...`
   var assignUse: Boolean = false
 
   def rename(newName: String): PIdnUse
 }
-// Any `PIdnUse` which should have it's `decl` resolved by the `NameAnalyser`.
-sealed trait PIdnUseName extends PIdnUse
-case class PIdnUseExp(name: String)(val pos: (Position, Position)) extends PIdnUseName with PExp with PAssignTarget with PMaybeMacroExp with PLabelUse with PLspIdnUseExp {
+/** Any `PIdnUse` which should have it's `decl` resolved by the `NameAnalyser`. */
+sealed trait PIdnUseName[T <: PDeclarationInner] extends PIdnUse {
+  implicit def ctag: scala.reflect.ClassTag[T]
+
+  // Could refer to one of these decls
+  protected var _decls: Seq[PDeclarationInner] = Nil
+  private var _filters: Seq[T => Boolean] = Nil
+  def decls: Seq[T] = _decls.flatMap(_ match {
+      case d: T => Some(d)
+      case _ => None
+    }).filter(t => _filters.forall(_(t)))
+  override def decl: Option[T] = if (decls.length == 1) Some(decls.head) else None
+
+  def prependDecls(ds: Seq[PDeclarationInner]) = _decls = ds ++ _decls
+  def newDecl(d: PDeclarationInner) = _decls :+= d
+
+  /** Filters `decls` according to the given predicate, returns `true` if any are left. */
+  def filterDecls(f: T => Boolean): Boolean = {
+    _filters :+= f
+    decls.isEmpty
+  }
+}
+/** Any `PNode` which should be ignored (as well as it's children) by the `NameAnalyser`. */
+trait PNameAnalyserOpaque extends PNode
+
+case class PIdnUseExp(name: String)(val pos: (Position, Position)) extends PIdnUseName[PTypedVarDecl] with PExp with PAssignTarget with PMaybeMacroExp with PLspIdnUseExp {
+  override def ctag = scala.reflect.classTag[PTypedVarDecl]
+
   override def possibleMacro = Some(this)
   override def macroArgs: Seq[PExp] = Seq()
 
@@ -219,8 +291,15 @@ case class PIdnUseExp(name: String)(val pos: (Position, Position)) extends PIdnU
 
   override def rename(newName: String) = PIdnUseExp(newName)(pos)
 }
-case class PIdnRef(name: String)(val pos: (Position, Position)) extends PIdnUseName with PLspIdnUse {
-  override def rename(newName: String) = PIdnRef(newName)(pos)
+case class PIdnRef[T <: PDeclarationInner](name: String)(val pos: (Position, Position))(implicit val ctag: scala.reflect.ClassTag[T]) extends PIdnUseName[T] with PLspIdnUse {
+  override def rename(newName: String): PIdnUse = PIdnRef(newName)(pos)
+  /** Changes the type of declaration which is referenced, preserves all previously added `decls` but discards `filters`. */
+  def retype[U <: PDeclarationInner]()(implicit ctag: scala.reflect.ClassTag[U]): PIdnRef[U] = {
+    val newRef = PIdnRef(name)(pos)
+    newRef._decls = _decls
+    newRef
+  }
+  override def getExtraVals: Seq[Any] = Seq(pos, ctag)
 }
 
 ///////////////////////////////////////////////////////////////////////////
@@ -228,46 +307,49 @@ case class PIdnRef(name: String)(val pos: (Position, Position)) extends PIdnUseN
 
 trait PAnyFormalArgDecl extends PNode with PUnnamedTypedDeclaration with PPrettySubnodes
 
-case class PUnnamedFormalArgDecl(var typ: PType)(val pos: (Position, Position)) extends PAnyFormalArgDecl {
-  override def pretty = typ.pretty
+/** The declaration of an argument to a domain function. Not a `PDeclaration` as it will never clash. */
+case class PDomainFunctionArg(name: Option[PIdnDef], c: Option[PSym.Colon], typ: PType)(val pos: (Position, Position)) extends PAnyFormalArgDecl
+object PDomainFunctionArg {
+  def apply(d: PIdnTypeBinding): PDomainFunctionArg = PDomainFunctionArg(Some(d.idndef), Some(d.c), d.typ)(d.pos)
 }
 
 /** Any `var: Type` style binding, only useful during parsing and therefore not a `PNode`. */
 case class PIdnTypeBinding(idndef: PIdnDef, c: PSym.Colon, typ: PType)(val pos: (Position, Position))
 
 /** Anything that can be `PIdnUse`d as an expression (e.g. the receiver of a `PFieldAccess`). */
-trait PAnyVarDecl extends PTypedDeclaration with PLocalDeclaration with PPrettySubnodes {
+sealed trait PTypedVarDecl extends PTypedDeclaration with PDeclarationInner with PPrettySubnodes {
+  def idndef: PIdnDef
   def toIdnUse: PIdnUseExp = {
     val use = PIdnUseExp(idndef.name)(idndef.pos)
     use.typ = typ
-    use.decl = Some(this)
+    use.newDecl(this)
     use
   }
 }
 /** Anything that can be `PIdnUse`d as the target of a `PAssign`. */
-trait PAssignableVarDecl extends PAnyVarDecl
+sealed trait PAssignableVarDecl extends PTypedVarDecl
 
 /** Any argument to a method, function or predicate. */
-case class PFormalArgDecl(idndef: PIdnDef, c: PSym.Colon, typ: PType)(val pos: (Position, Position)) extends PAnyFormalArgDecl with PAnyVarDecl with PLspFormalArgDecl
+case class PFormalArgDecl(idndef: PIdnDef, c: PSym.Colon, typ: PType)(val pos: (Position, Position)) extends PAnyFormalArgDecl with PTypedVarDecl with PMemberDeclaration with PMemberUniqueDeclaration with PLspFormalArgDecl
 object PFormalArgDecl {
   def apply(d: PIdnTypeBinding): PFormalArgDecl = PFormalArgDecl(d.idndef, d.c, d.typ)(d.pos)
 }
 /** The return arguments of methods. */
-case class PFormalReturnDecl(idndef: PIdnDef, c: PSym.Colon, typ: PType)(val pos: (Position, Position)) extends PAssignableVarDecl with PLocalDeclaration with PLspFormalReturnDecl
+case class PFormalReturnDecl(idndef: PIdnDef, c: PSym.Colon, typ: PType)(val pos: (Position, Position)) extends PAssignableVarDecl with PMemberDeclaration with PMemberUniqueDeclaration with PLspFormalReturnDecl
 object PFormalReturnDecl {
   def apply(d: PIdnTypeBinding): PFormalReturnDecl = PFormalReturnDecl(d.idndef, d.c, d.typ)(d.pos)
 }
 
-case class PLogicalVarDecl(idndef: PIdnDef, c: PSym.Colon, typ: PType)(val pos: (Position, Position)) extends PAnyVarDecl with PLocalDeclaration with PLspLogicalVarDecl
+case class PLogicalVarDecl(idndef: PIdnDef, c: PSym.Colon, typ: PType)(val pos: (Position, Position)) extends PTypedVarDecl with PLocalDeclaration with PScopeUniqueDeclaration with PLspLogicalVarDecl
 object PLogicalVarDecl {
   def apply(d: PIdnTypeBinding): PLogicalVarDecl = PLogicalVarDecl(d.idndef, d.c, d.typ)(d.pos)
 }
 /** Declaration of a local variable. */
-case class PLocalVarDecl(idndef: PIdnDef, c: PSym.Colon, typ: PType)(val pos: (Position, Position)) extends PAssignableVarDecl with PLocalDeclaration with PLspLocalVarDecl
+case class PLocalVarDecl(idndef: PIdnDef, c: PSym.Colon, typ: PType)(val pos: (Position, Position)) extends PAssignableVarDecl with PLocalDeclaration with PScopeUniqueDeclaration with PLspLocalVarDecl
 object PLocalVarDecl {
   def apply(d: PIdnTypeBinding): PLocalVarDecl = PLocalVarDecl(d.idndef, d.c, d.typ)(d.pos)
 }
-case class PFieldDecl(idndef: PIdnDef, c: PSym.Colon, typ: PType)(val pos: (Position, Position)) extends PTypedDeclaration with PGlobalDeclaration with PLspFieldDecl {
+case class PFieldDecl(idndef: PIdnDef, c: PSym.Colon, typ: PType)(val pos: (Position, Position)) extends PTypedDeclaration with PGlobalDeclaration with PGlobalUniqueDeclaration with PLspFieldDecl {
   var decl: Option[PFields] = None
   override def annotations = decl.toSeq.flatMap(_.annotations)
   override def pretty = s"${idndef.pretty}: ${typ.pretty}"
@@ -285,6 +367,8 @@ trait PType extends PNode with PPrettySubnodes {
   def isGround: Boolean = true
   def substitute(ts: PTypeSubstitution): PType
   def subNodes: Seq[PType]
+  def isPure: Boolean = true
+  def umbrella: Option[PType] = None
 
   //If we add type quantification or any type binders we need to modify this
   def freeTypeVariables: Set[String] =
@@ -293,6 +377,8 @@ trait PType extends PNode with PPrettySubnodes {
         case pdt: PDomainType if pdt.isTypeVar && PTypeVar.isFreePTVName(pdt.domain.name) => Set(pdt.genericName)
         case _ => Set()
       })
+
+  override def toString(): String = pretty
 }
 
 
@@ -300,11 +386,12 @@ case class PPrimitiv[T <: PKeywordType](name: PReserved[T])(val pos: (Position,
   override def isValidOrUndeclared = true
   override def substitute(ts: PTypeSubstitution): PType = this
   override val subNodes = Seq()
+  override def umbrella: Option[PType] = if (name.rs == PKw.Bool) Some(TypeHelper.Impure) else None
 
   override def pretty = name.pretty
 }
 
-case class PDomainType(domain: PIdnRef, args: Option[PDelimited.Comma[PSym.Bracket, PType]])(val pos: (Position, Position)) extends PGenericType with PLspDomainType {
+case class PDomainType(domain: PIdnRef[PTypeDeclaration], args: Option[PDelimited.Comma[PSym.Bracket, PType]])(val pos: (Position, Position)) extends PGenericType with PLspDomainType with HasExtraVars {
   val genericName = domain.name
   override val typeArguments = typeArgs
   var kind: PDomainTypeKinds.Kind = PDomainTypeKinds.Unresolved
@@ -348,6 +435,8 @@ case class PDomainType(domain: PIdnRef, args: Option[PDelimited.Comma[PSym.Brack
 
   override def withTypeArguments(s: Seq[PType]): PDomainType =
     if (s.length == 0 && args.isEmpty) this else copy(args = Some(args.get.update(s)))(pos)
+
+  override def copyExtraVars(from: Any): Unit = this.kind = from.asInstanceOf[PDomainType].kind
 }
 
 object PDomainTypeKinds {
@@ -483,30 +572,43 @@ case class PMacroType(use: PCall) extends PType {
   * the type of any expression whose value is meaningful in the translation.
   */
 sealed trait PInternalType extends PType {
-  override val subNodes = Seq()
+  override val pos: (Position, Position) = (NoPosition, NoPosition)
+  override val subNodes: Seq[PType] = Seq()
   override def substitute(ts: PTypeSubstitution) = this
 }
 
 // for resolving if something cannot be typed
-case class PUnknown()(val pos: (Position, Position) = (NoPosition, NoPosition)) extends PInternalType {
+case class PUnknown() extends PInternalType {
   override def isValidOrUndeclared = false
   override def pretty = "<error>"
 }
 
-case class PWandType()(val pos: (Position, Position)) extends PInternalType {
+case class PBoolImpureType() extends PInternalType {
+  override def isValidOrUndeclared = true
+  override def isPure: Boolean = false
+  override def pretty = "Bool (Impure)"
+}
+case class PBoolWandType() extends PInternalType {
+  override def isValidOrUndeclared = true
+  override def isPure: Boolean = false
+  override def umbrella: Option[PType] = Some(TypeHelper.Impure)
+  override def pretty = "Bool (Wand)"
+}
+case class PBoolPredicateType() extends PInternalType {
   override def isValidOrUndeclared = true
-  override def pretty = "Bool"
+  override def isPure: Boolean = false
+  override def umbrella: Option[PType] = Some(TypeHelper.Impure)
+  override def pretty = "Bool (Predicate)"
 }
 
 /** The type of a `PIdnUse` which refers to a function. Ensures that we get a
  * typecheck error if we try to use a function as a value.
  */
-case class PFunctionType(argTypes: Seq[PType], resultType: PType) extends PType {
-  override val pos: (Position, Position) = resultType.pos
+case class PFunctionType(argTypes: Seq[PType], resultType: PType) extends PInternalType {
   override def isValidOrUndeclared: Boolean = subNodes.forall(_.isValidOrUndeclared)
-  override def substitute(ts: PTypeSubstitution): PType =
+  override def substitute(ts: PTypeSubstitution): PFunctionType =
     PFunctionType(argTypes.map(_.substitute(ts)), resultType.substitute(ts))
-  override def subNodes: Seq[PType] = argTypes ++ Seq(resultType)
+  override val subNodes: Seq[PType] = argTypes ++ Seq(resultType)
   override def pretty = {
     val argsPretty = argTypes.map(_.pretty).mkString("(", ", ", ")")
     s"$argsPretty: ${resultType.pretty}"
@@ -519,9 +621,18 @@ case class PFunctionType(argTypes: Seq[PType], resultType: PType) extends PType
 // The argument types are unified with the (fresh versions of) types  are
 trait PExp extends PNode with PPrettySubnodes {
   var brackets: Option[PGrouped[PSym.Paren, PExp]] = None
-  var typ: PType = PUnknown()()
+  var typ: PType = PUnknown()
 
   def typeSubstitutions: scala.collection.Seq[PTypeSubstitution]
+  /** Rule out e.g. `Impure && Impure` if `Bool && Bool` is an option (since `Bool <: Impure`). */
+  def typeSubsDistinct: scala.collection.Seq[PTypeSubstitution] = {
+    val all = typeSubstitutions.distinct.zipWithIndex
+    all.filter { case (sub, i) => all.forall {
+      case (sup, j) => i == j || !sub.m.forall {
+        case (name, t) => sup.m.contains(name) && isSubtype(sup.m(name), t)
+      }
+    }} map (_._1)
+  }
 
   def forceSubstitution(ts: PTypeSubstitution): Unit
 
@@ -536,15 +647,82 @@ case class PAnnotatedExp(annotation: PAnnotation, e: PExp)(val pos: (Position, P
   override def forceSubstitution(ts: PTypeSubstitution): Unit = e.forceSubstitution(ts)
 }
 
-case class PTypeSubstitution(m: Map[String, PType]) //extends Map[String,PType]()
+trait PSubstitutionMap[S <: PSubstitutionMap[S]] {
+  /** Add a new substitution from `a` to `b`. */
+  def add[T <: PSubstitutionMap[T]](a: PType, b: PType, default: T): Either[(PType, PType), T]
+  /** Insert a substitution which does not yet exist. Should not be called directly. */
+  def insert(name: String, t: PType): Either[(PType, PType), S]
+  /** Replace a substitution which already exists. Should not be called directly. */
+  def replace(name: String, t: PType): S
+}
+
+/** An internal map which is temporarily used for construction a substitution for an expression before being `collapse`d. Uses two `PTypeSubstitution` maps,
+ * one which is the composition of all maps of subexpressions and the other which is for the signature of the current expression (and `canGeneralise`). */
+case class PTypeSubstitutionInternal(m: PTypeSubstitution, added: PTypeSubstitution = PTypeSubstitution(Map(), true)) extends PSubstitutionMap[PTypeSubstitutionInternal] {
+  require(!m.canGeneralise && added.canGeneralise)
+  def keySet: Set[String] = m.keySet ++ added.keySet
+  def get(key: String): Option[PType] = added.get(key).orElse(m.get(key))
+
+  def compose(other: PTypeSubstitution): Either[(PType, PType), PTypeSubstitutionInternal] = {
+    val sharedKeys = this.m.keySet.intersect(other.keySet)
+    if (sharedKeys.exists(p => this.m.get(p).get != other.get(p).get)) {
+      /* no composed substitution if input substitutions do not match */
+      val nonMatchingKey = sharedKeys.find(p => this.m.get(p).get != other.get(p).get).get
+      return Left((this.m.get(nonMatchingKey).get, other.get(nonMatchingKey).get))
+    }
+
+    val newSub = new PTypeSubstitution(
+      this.m.map({ case (s: String, pt: PType) => s -> pt.substitute(other) }) ++
+        other.map({ case (s: String, pt: PType) => s -> pt.substitute(this.m) }))
+    Right(PTypeSubstitutionInternal(newSub, added))
+  }
+
+  override def insert(name: String, t: PType): Either[(PType, PType), PTypeSubstitutionInternal] = {
+    val newAdded = added.add(name, t)
+    if (newAdded.toOption.isDefined)
+      Right(PTypeSubstitutionInternal(m, newAdded.toOption.get))
+    else
+      Left(newAdded.swap.toOption.get)
+  }
+  override def replace(name: String, t: PType): PTypeSubstitutionInternal = PTypeSubstitutionInternal(m.replace(name, t), added)
+
+  // The expected call sequence is `m.add` -> `this.insert` -> `added.add` -> `added.insert/replace`. We need to call `add` on both
+  // sub-maps to ensure that we also `add` any generics with the match case of `PGenericType`.
+  override def add[T <: PSubstitutionMap[T]](a: PType, b: PType, default: T = this): Either[(PType, PType), T] =
+    m.add(a, b, default)
+
+  def collapse: PTypeSubstitution =
+    added.m.foldLeft(m)({
+      case (s, (a, b)) => s.substitute(a, b).insert(a, b.substitute(s)).toOption.get
+    })
+}
+
+/** If `!canGeneralise` this is a substitution map which supports basic add, where we can check if an expression corresponds to some expected type.
+ * This is done by calling `add(a, b)` where `a` is the type of the expression and `b` is the expected type of the slot. For example, one might call
+ * `add(Int, Bool)` if they see `3 ? ... : ...` and get an error (Left) since `3` is not a subtype of the expected `Bool`.
+ * 
+ * On the other hand if `canGeneralise` is true, then this is a substitution map which supports generalisation. This means that a call to `add(a, b)`
+ * is symmetric in `a` and `b`. For example, one might call `add(Wand, Bool)` if they see `... ? ... --* ... : true` (or more likely will have called
+ * `add(#T0, Wand)` and `add(#T0, Bool)` where the second call is turned into `add(Wand, Bool)`) where the type is generalised to `Impure` without error.
+ */
+case class PTypeSubstitution(m: Map[String, PType], canGeneralise: Boolean = false) extends PSubstitutionMap[PTypeSubstitution]
 {
-  require(m.values.forall(_.isValidOrUndeclared))
+  require(m.values.forall(_.isValidOrUndeclared), s"Invalid type substitution: $m (${m.map(kv => kv._1 -> kv._2.isValidOrUndeclared)})")
+
+  override def insert(name: String, t: PType): Either[(PType, PType), PTypeSubstitution] = {
+    require(!m.contains(name))
+    Right(substitute(name, t) + (name -> t))
+  }
+  override def replace(name: String, t: PType): PTypeSubstitution = {
+    assert(m.contains(name) && canGeneralise)
+    PTypeSubstitution(m + (name -> t), canGeneralise)
+  }
 
-  def -(key: String) = new PTypeSubstitution(m.-(key))
+  def -(key: String) = new PTypeSubstitution(m.-(key), canGeneralise)
 
   def get(key: String): Option[PType] = m.get(key)
 
-  private def +(kv: (String, PType)): PTypeSubstitution = new PTypeSubstitution(m + kv)
+  private def +(kv: (String, PType)): PTypeSubstitution = new PTypeSubstitution(m + kv, canGeneralise)
 
   def iterator: Iterator[(String, PType)] = m.iterator
 
@@ -552,7 +730,7 @@ case class PTypeSubstitution(m: Map[String, PType]) //extends Map[String,PType](
 
   def keySet: Set[String] = m.keySet
 
-  def restrict(s: Set[String]) = PTypeSubstitution(m.filter(s contains _._1))
+  def restrict(s: Set[String]) = PTypeSubstitution(m.filter(s contains _._1), canGeneralise)
 
   def map[B](f: ((String, PType)) => B): Seq[B] =
     m.map(f).toSeq
@@ -562,9 +740,9 @@ case class PTypeSubstitution(m: Map[String, PType]) //extends Map[String,PType](
   def contains(key: String): Boolean = get(key).nonEmpty
 
   def substitute(a: String, b: PType): PTypeSubstitution = {
-    require(!contains(a))
+    require(!contains(a), s"Substituting $a -> $b into $this")
     val ts = PTypeSubstitution(Map(a -> b))
-    PTypeSubstitution(m.map(kv => kv._1 -> kv._2.substitute(ts)))
+    PTypeSubstitution(m.map(kv => kv._1 -> kv._2.substitute(ts)), canGeneralise)
   }
 
   // The following methods all return a type substitution if successful,
@@ -577,20 +755,46 @@ case class PTypeSubstitution(m: Map[String, PType]) //extends Map[String,PType](
 
   def add(a: String, b: PType): Either[(PType, PType), PTypeSubstitution] = add(PTypeVar(a), b)
 
-  def add(a: PType, b: PType): Either[(PType, PType), PTypeSubstitution] = {
+  /** If `!canGeneralise` then `a` is the type of the expression being used, `b` is the expected type of the slot */
+  override def add[T <: PSubstitutionMap[T]](a: PType, b: PType, default: T = this): Either[(PType, PType), T] = {
     val as = a.substitute(this)
     val bs = b.substitute(this)
+    if (as == bs) return Right(default)
+    val sup = commonSupertype(as, bs)
+
+    // Try to generalise the substitution
+    if (canGeneralise) {
+      var generalised: Option[T] = None
+      a match {
+        // The current value in the map (`as`) is less general than the common supertype.
+        case PTypeVar(name) if PTypeVar.isFreePTVName(name) && sup.isDefined && sup.get != as =>
+          generalised = Some(generalised.getOrElse(default).replace(name, sup.get))
+        case _ =>
+      }
+      b match {
+        // The current value in the map (`bs`) is less general than the common supertype.
+        case PTypeVar(name) if PTypeVar.isFreePTVName(name) && sup.isDefined && sup.get != bs =>
+          generalised = Some(generalised.getOrElse(default).replace(name, sup.get))
+        case _ =>
+      }
+      if (generalised.isDefined)
+        return Right(generalised.get)
+    }
+    // Could not generalise
     (as, bs) match {
-      case (aa, bb) if aa == bb => Right(this)
+      // The slot type is more general than the expression type (all is good)
+      case _ if sup.isDefined && sup.get == bs => Right(default)
+      // The already present type is the more general one
+      case _ if canGeneralise && sup.isDefined && sup.get == as => Right(default)
       case (PTypeVar(name), t) if PTypeVar.isFreePTVName(name) =>
-        assert(!contains(name))
-        Right(substitute(name, t) + (name -> t))
-      case (_, PTypeVar(name)) if PTypeVar.isFreePTVName(name) => add(bs, as)
+        default.insert(name, t)
+      case (t, PTypeVar(name)) if PTypeVar.isFreePTVName(name) =>
+        default.insert(name, t)
       case (gt1: PGenericType, gt2: PGenericType) if gt1.genericName == gt2.genericName =>
         val zippedArgs = gt1.typeArguments zip gt2.typeArguments
-        (zippedArgs.foldLeft[Either[(PType, PType), PTypeSubstitution]](Right(this))
-          ((ss: Either[(PType, PType), PTypeSubstitution], p: (PType, PType)) => ss match {
-            case Right(sss) => sss.add(p._1, p._2) match {
+        (zippedArgs.foldLeft[Either[(PType, PType), T]](Right(default))
+          ((ss: Either[(PType, PType), T], p: (PType, PType)) => ss match {
+            case Right(sss) => sss.add(p._1, p._2, sss) match {
               case l@Left(pair) =>
                 val problemArg = zippedArgs.zipWithIndex.find(_._1 == pair)
                 problemArg match {
@@ -609,19 +813,8 @@ case class PTypeSubstitution(m: Map[String, PType]) //extends Map[String,PType](
 
   }
 
-  //  def apply(key:PDomainType) = apply(key.domain.name)
-  //  def apply(key:String) = get(key)
-
-  //  def getOrId(key:String) : String = this(key) match{ case Some(if (contains(key)) get(key) else key
   def this(s: Seq[(String, PType)]) = this(s.toMap)
 
-  //  def this(m:Map[PDomainType,PType]) = this(m.map (kv=>kv._1.domain.name->kv._2))
-
-  //  implicit def this(m:Map[String,PType]) = this(m.map (kv=>kv._1->kv._2))
-
-  //  implicit def fromMap(m:Map[String,PType]) = new PTypeSubstitution(m)
-  //  private def this() = this(Map())
-
   def isFullyReduced =
     m.values.forall(pt => (pt.freeTypeVariables intersect m.keySet).isEmpty)
 
@@ -654,6 +847,8 @@ class PTypeRenaming(val mm: Map[String, String])
 
 trait POpApp extends PExp {
   def args: Seq[PExp]
+  /** Which `args` must be pure? Enforced at type checking. */
+  def requirePure: Seq[PExp] = Nil
 
   private val _typeSubstitutions = new scala.collection.mutable.ArrayDeque[PTypeSubstitution]()
 
@@ -701,7 +896,7 @@ trait PCallLike extends POpApp {
   def callArgs: PDelimited.Comma[PSym.Paren, PExp]
 }
 
-case class PCall(idnref: PIdnRef, callArgs: PDelimited.Comma[PSym.Paren, PExp], typeAnnotated: Option[(PSym.Colon, PType)])(val pos: (Position, Position))
+case class PCall(idnref: PIdnRef[PGlobalCallable], callArgs: PDelimited.Comma[PSym.Paren, PExp], typeAnnotated: Option[(PSym.Colon, PType)])(val pos: (Position, Position))
   extends PCallLike with PLocationAccess with PAccAssertion with PAssignTarget with PMaybeMacroExp with PLspCall {
   override def possibleMacro = if (typeAnnotated.isEmpty) Some(idnref) else None
   override def macroArgs = args
@@ -712,19 +907,19 @@ case class PCall(idnref: PIdnRef, callArgs: PDelimited.Comma[PSym.Paren, PExp],
     case Some(pf: PFunction) if pf.formalArgs.size == args.size => List(
         (args.indices.map(i => POpApp.pArgS(i) -> pf.formalArgs(i).typ) :+ (POpApp.pResS -> pf.typ.resultType)).toMap
       )
-    case Some(pdf: PDomainFunction) if pdf.formalArgs.size == args.size => List(
+    case Some(pdf: PDomainFunction) if pdf.formalArgs.size == args.size && domainTypeRenaming.isDefined => List(
         (args.indices.map(i => POpApp.pArgS(i) -> pdf.formalArgs(i).typ.substitute(domainTypeRenaming.get)) :+
             (POpApp.pResS -> pdf.typ.resultType.substitute(domainTypeRenaming.get))).toMap
       )
     case Some(pp: PPredicate) if pp.formalArgs.size == args.size => List(
-        (args.indices.map(i => POpApp.pArgS(i) -> pp.formalArgs(i).typ) :+ (POpApp.pResS -> Bool)).toMap
+        (args.indices.map(i => POpApp.pArgS(i) -> pp.formalArgs(i).typ) :+ (POpApp.pResS -> pp.resultType)).toMap
       )
     // this case is handled in Resolver.scala (- method check) which generates the appropriate error message
     case _ => Nil
   })
 
-  var funcDecl: Option[PAnyFunction] = None
-  var methodDecl: Option[PMethod] = None
+  def funcDecl: Option[PAnyFunction] = idnref.decl.filter(_.isInstanceOf[PAnyFunction]).map(_.asInstanceOf[PAnyFunction])
+  def methodDecl: Option[PMethod] = idnref.decl.filter(_.isInstanceOf[PMethod]).map(_.asInstanceOf[PMethod])
   // def formalArgs: Option[Seq[PFormalArgDecl]] = decl.map(_.formalArgs)
 
   override def extraLocalTypeVariables = _extraLocalTypeVariables
@@ -734,6 +929,7 @@ case class PCall(idnref: PIdnRef, callArgs: PDelimited.Comma[PSym.Paren, PExp],
 
   def isDomainFunction = domainTypeRenaming.isDefined
   def isPredicate = funcDecl.map(_.isInstanceOf[PPredicate]).getOrElse(false)
+  def isMethod = methodDecl.isDefined
 
   var domainSubstitution: Option[PTypeSubstitution] = None
 
@@ -765,7 +961,8 @@ class PBinExp(val left: PExp, val op: PReserved[PBinaryOp], val right: PExp)(val
   override val args = Seq(left, right)
 
   override val extraLocalTypeVariables = if (op.rs.isInstanceOf[PCollectionOp]) Set(PCollectionOp.infVar) else Set()
-  val signatures: List[PTypeSubstitution] = op.rs.signatures
+  override def requirePure = if (op.rs.requirePureArgs) args else Nil
+  override def signatures: List[PTypeSubstitution] = op.rs.signatures
 
   override def canEqual(that: Any): Boolean = that.isInstanceOf[PBinExp]
 
@@ -848,7 +1045,7 @@ trait PLocationAccess extends PResourceAccess {
   def idnref: PIdnUse
 }
 
-case class PFieldAccess(rcv: PExp, dot: PSymOp.Dot, idnref: PIdnRef)(val pos: (Position, Position)) extends PLocationAccess with PAssignTarget with PLspExpRef {
+case class PFieldAccess(rcv: PExp, dot: PSymOp.Dot, idnref: PIdnRef[PFieldDecl])(val pos: (Position, Position)) extends PLocationAccess with PAssignTarget with PLspExpRef {
   override final val args = Seq(rcv)
 
   override def signatures = idnref.decl match {
@@ -862,13 +1059,13 @@ case class PFieldAccess(rcv: PExp, dot: PSymOp.Dot, idnref: PIdnRef)(val pos: (P
 case class PUnfolding(unfolding: PKwOp.Unfolding, acc: PAccAssertion, in: PKwOp.In, exp: PExp)(val pos: (Position, Position)) extends PHeapOpApp with PLspExp {
   override val args = Seq(acc, exp)
   override val signatures: List[PTypeSubstitution] =
-    List(Map(POpApp.pArgS(0) -> Bool, POpApp.pResS -> POpApp.pArg(1)))
+    List(Map(POpApp.pArgS(0) -> Predicate, POpApp.pResS -> POpApp.pArg(1)))
 }
 
 case class PApplying(applying: PKwOp.Applying, wand: PExp, in: PKwOp.In, exp: PExp)(val pos: (Position, Position)) extends PHeapOpApp with PLspExp {
   override val args = Seq(wand, exp)
   override val signatures: List[PTypeSubstitution] =
-    List(Map(POpApp.pArgS(0) -> Bool, POpApp.pResS -> POpApp.pArg(1)))
+    List(Map(POpApp.pArgS(0) -> Wand, POpApp.pResS -> POpApp.pArg(1)))
 }
 
 sealed trait PBinder extends PExp with PScope with PLspExp {
@@ -929,8 +1126,8 @@ case class PLet(l: PKwOp.Let, variable: PIdnDef, eq: PSymOp.EqEq, exp: PExp, in:
   }
 }
 
-case class PLetNestedScope(body: PExp)(val pos: (Position, Position)) extends PAnyVarDecl with PLocalDeclaration with PLspLogicalVarDecl {
-  var outerLet: PLet = null
+case class PLetNestedScope(body: PExp)(val pos: (Position, Position)) extends PTypedVarDecl with PLocalDeclaration with PScopeUniqueDeclaration with PLspLogicalVarDecl {
+  def outerLet: PLet = getAncestor[PLet].get
   override def idndef: PIdnDef = outerLet.variable
   override def typ: PType = outerLet.exp.typ
 }
@@ -940,7 +1137,8 @@ case class PInhaleExhaleExp(l: PSymOp.LBracket, in: PExp, c: PSymOp.Comma, ex: P
   override val args = Seq(in, ex)
 
   val signatures: List[PTypeSubstitution] = List(
-    Map(POpApp.pArgS(0) -> Bool, POpApp.pArgS(1) -> Bool, POpApp.pResS -> Bool)
+    Map(POpApp.pArgS(0) -> Bool, POpApp.pArgS(1) -> Bool, POpApp.pResS -> Bool),
+    Map(POpApp.pArgS(0) -> Impure, POpApp.pArgS(1) -> Impure, POpApp.pResS -> Impure),
   )
 }
 
@@ -985,21 +1183,17 @@ sealed trait PAccAssertion extends PExp with PLspExp {
 
 case class PAccPred(op: PKwOp.Acc, amount: PGrouped[PSym.Paren, PMaybePairArgument[PLocationAccess, PExp]])(val pos: (Position, Position)) extends PCallKeyword with PAccAssertion {
   override val signatures: List[PTypeSubstitution] = List(
-    Map(POpApp.pArgS(1) -> Perm, POpApp.pResS -> Bool))
+    Map(POpApp.pArgS(0) -> Predicate, POpApp.pArgS(1) -> Perm, POpApp.pResS -> Predicate),
+    Map(POpApp.pArgS(1) -> Perm, POpApp.pResS -> Impure),
+  )
   def loc = amount.inner.first
   def perm = amount.inner.second.map(_._2).getOrElse(PFullPerm.implied())
   override val args = Seq(loc, perm)
 }
 
-sealed trait PLabelUse extends PNode {
-  def name: String
-}
-case class PLhsLabel(k: PKw.Lhs)(val pos: (Position, Position)) extends PNode with PLabelUse with PPrettySubnodes {
-  override def name = k.rs.keyword
-}
-
-case class POldExp(op: PKwOp.Old, label: Option[PGrouped[PSym.Bracket, PLabelUse]], e: PGrouped[PSym.Paren, PExp])(val pos: (Position, Position)) extends PCallKeyword with PHeapOpApp {
+case class POldExp(op: PKwOp.Old, label: Option[PGrouped[PSym.Bracket, Either[PKw.Lhs, PIdnRef[PLabel]]]], e: PGrouped[PSym.Paren, PExp])(val pos: (Position, Position)) extends PCallKeyword with PHeapOpApp {
   override val args = Seq(e.inner)
+  override def requirePure = args
   override val signatures: List[PTypeSubstitution] = List(Map(POpApp.pResS -> POpApp.pArg(0)))
 
   // override def getSemanticHighlights: Seq[SemanticHighlight] = label.toSeq.flatMap(RangePosition(_).map(sp => SemanticHighlight(sp, TokenType.Event)))
@@ -1048,7 +1242,7 @@ sealed trait PExplicitCollectionLiteral extends PCollectionLiteral {
 }
 
 sealed trait PSeqLiteral extends PCollectionLiteral {
-  def pCollectionType(pType: PType) = if (pType.isUnknown) PUnknown()() else MakeSeq(pType)
+  def pCollectionType(pType: PType) = if (pType.isUnknown) PUnknown() else MakeSeq(pType)
 }
 
 case class PEmptySeq(op: PKwOp.Seq, pAnnotatedType: Option[PGrouped[PSym.Bracket, PType]], callArgs: PDelimited.Comma[PSym.Paren, Nothing])(val pos: (Position, Position)) extends PSeqLiteral with PEmptyCollectionLiteral
@@ -1123,7 +1317,7 @@ case class PSize(l: PSymOp.Or, seq: PExp, r: PSymOp.Or)(val pos: (Position, Posi
 }
 
 sealed trait PSetLiteral extends PCollectionLiteral {
-  def pCollectionType(pType: PType) = if (pType.isUnknown) PUnknown()() else MakeSet(pType)
+  def pCollectionType(pType: PType) = if (pType.isUnknown) PUnknown() else MakeSet(pType)
 }
 
 case class PEmptySet(op: PKwOp.Set, pAnnotatedType: Option[PGrouped[PSym.Bracket, PType]], callArgs: PDelimited.Comma[PSym.Paren, Nothing])(val pos: (Position, Position)) extends PSetLiteral with PEmptyCollectionLiteral
@@ -1131,7 +1325,7 @@ case class PEmptySet(op: PKwOp.Set, pAnnotatedType: Option[PGrouped[PSym.Bracket
 case class PExplicitSet(op: PKwOp.Set, callArgs: PDelimited.Comma[PSym.Paren, PExp])(val pos: (Position, Position)) extends PSetLiteral with PExplicitCollectionLiteral
 
 sealed trait PMultiSetLiteral extends PCollectionLiteral {
-  def pCollectionType(pType: PType) = if (pType.isUnknown) PUnknown()() else MakeMultiset(pType)
+  def pCollectionType(pType: PType) = if (pType.isUnknown) PUnknown() else MakeMultiset(pType)
 }
 
 case class PEmptyMultiset(op: PKwOp.Multiset, pAnnotatedType: Option[PGrouped[PSym.Bracket, PType]], callArgs: PDelimited.Comma[PSym.Paren, Nothing])(val pos: (Position, Position)) extends PMultiSetLiteral with PEmptyCollectionLiteral
@@ -1149,7 +1343,7 @@ sealed trait PMapLiteral extends POpApp with PLspExp {
   def pValueType: PType
 
   def pMapType(keyType: PType, valueType: PType): PType =
-    if (keyType.isUnknown || valueType.isUnknown) PUnknown()()
+    if (keyType.isUnknown || valueType.isUnknown) PUnknown()
     else MakeMap(keyType, valueType)
 }
 
@@ -1268,27 +1462,26 @@ case class PVars(keyword: PKw.Var, vars: PDelimited[PLocalVarDecl, PSym.Comma],
   def assign: Option[PAssign] = init map (i => PAssign(vars.update(vars.toSeq.map(_.toIdnUse)), Some(i._1), i._2)(pos))
 }
 
-case class PLabel(label: PKw.Label, idndef: PIdnDef, invs: PDelimited[PSpecification[PKw.InvSpec], Option[PSym.Semi]])(val pos: (Position, Position)) extends PStmt with PLocalDeclaration {
+case class PLabel(label: PKw.Label, idndef: PIdnDef, invs: PDelimited[PSpecification[PKw.InvSpec], Option[PSym.Semi]])(val pos: (Position, Position)) extends PStmt with PMemberDeclaration with PBackwardDeclaration {
   override def completionScope: Map[SuggestionScope,Byte] = Map(LabelScope -> 0, StatementScope -> -50)
   override def completionKind: CompletionKind.CompletionKind = CompletionKind.Event
   override def tokenType = TokenType.Event
   override def symbolKind: SymbolKind.SymbolKind = SymbolKind.Event
-  override def hint = {
-    val firstLine = s"${label.pretty} ${idndef.pretty}"
-    val invsStr = invs.toSeq.map(i => s"\n  ${i.pretty}").mkString
-    firstLine + invsStr
-  }
   override def description: String = "Label"
+  override def hint: String = this.pretty
 }
 
-case class PGoto(goto: PKw.Goto, target: PIdnUseExp)(val pos: (Position, Position)) extends PStmt with HasSemanticHighlights {
+case class PGoto(goto: PKw.Goto, target: PIdnRef[PLabel])(val pos: (Position, Position)) extends PStmt with HasSemanticHighlights {
   override def getSemanticHighlights: Seq[SemanticHighlight] = RangePosition(target).map(sp => SemanticHighlight(sp, TokenType.Event)).toSeq
   // override def getHoverHints: Seq[HoverHint] = target.hoverHint(RangePosition(target))
 }
 
-case class PTypeVarDecl(idndef: PIdnDef)(val pos: (Position, Position)) extends PLocalDeclaration with PPrettySubnodes {
+// Should this be sealed?
+sealed trait PTypeDeclaration extends PDeclarationInner
+
+case class PTypeVarDecl(idndef: PIdnDef)(val pos: (Position, Position)) extends PMemberDeclaration with PTypeDeclaration with PPrettySubnodes {
   override def symbolKind: SymbolKind.SymbolKind = SymbolKind.TypeParameter
-  override def hint: String = idndef.pretty
+  override def hint: String = this.pretty
   override def completionScope: Map[SuggestionScope,Byte] = Map(TypeScope -> 0)
   override def completionKind: CompletionKind.CompletionKind = CompletionKind.TypeParameter
   override def completionChars: Option[Map[Char, Byte]] = Some(Map(':' -> 50))
@@ -1303,7 +1496,7 @@ case class PQuasihavoc(quasihavoc: PKw.Quasihavoc, lhs: Option[(PExp, PSymOp.Imp
 case class PQuasihavocall(quasihavocall: PKw.Quasihavocall, vars: PDelimited[PLogicalVarDecl, PSym.Comma], colons: PSym.ColonColon, lhs: Option[(PExp, PSymOp.Implies)], e: PExp)(val pos: (Position, Position)) extends PStmt with PScope
 
 /* new(f1, ..., fn) or new(*) */
-case class PNewExp(keyword: PKw.New, fields: PGrouped[PSym.Paren, Either[PSym.Star, PDelimited[PIdnUseExp, PSym.Comma]]])(val pos: (Position, Position)) extends PExp with PLspExp {
+case class PNewExp(keyword: PKw.New, fields: PGrouped[PSym.Paren, Either[PSym.Star, PDelimited[PIdnRef[PFieldDecl], PSym.Comma]]])(val pos: (Position, Position)) extends PExp with PLspExp {
   override final val typeSubstitutions = Seq(PTypeSubstitution.id)
   def forceSubstitution(ts: PTypeSubstitution) = {}
   // override def getHoverHints: Seq[HoverHint] = fields.toSeq.flatMap(_.flatMap(ir => ir.hoverHint(RangePosition(ir))))
@@ -1344,26 +1537,49 @@ sealed trait PAssignTarget
 /** An entity is a declaration (named) or an error node */
 sealed trait PEntity
 
-trait PDeclaration extends PNode with PEntity with PLspDeclaration {
+trait PDeclarationInner extends PNode with PLspDeclaration {
   def idndef: PIdnDef
 }
 
+sealed trait PDeclaration extends PDeclarationInner with PEntity
+
+sealed trait PUniqueDeclaration
+
+// Unique within contained `PProgram`, can only be attached to `PGlobalDeclaration`
+trait PGlobalUniqueDeclaration extends PUniqueDeclaration
+
+// Unique within contained `PMember`
+trait PMemberUniqueDeclaration extends PUniqueDeclaration
+
+// Unique within contained `PScope` (but not necessarily parent or child scopes)
+trait PScopeUniqueDeclaration extends PUniqueDeclaration
+
+// Can be referenced before declaration
+trait PBackwardDeclaration
+
+// A declaration which shadows any previous declarations with the same name
+trait POverridesDeclaration
+
 sealed trait PUnnamedTypedDeclaration extends PNode {
   def typ: PType
 }
 
-trait PGlobalDeclaration extends PDeclaration with PAnnotated with PLspGlobalDeclaration
+// Can be referenced from anywhere within the `PProgram` (needs `PBackwardDeclaration` since PProgram reorders declarations)
+trait PGlobalDeclaration extends PDeclaration with PBackwardDeclaration with PAnnotated with PLspGlobalDeclaration
 
-trait PLocalDeclaration extends PDeclaration with HasCompletionProposals
+// Can be referenced from anywhere within the containing `PMember`
+trait PMemberDeclaration extends PDeclaration
 
-trait PUniversalDeclaration extends PDeclaration
+// Can be referenced from anywhere within the containing `PScope`
+trait PLocalDeclaration extends PDeclaration with HasCompletionProposals
 
-sealed trait PTypedDeclaration extends PDeclaration with PUnnamedTypedDeclaration
+trait PTypedDeclaration extends PUnnamedTypedDeclaration
 
 case class PBracedExp(e: PGrouped[PSym.Brace, PExp])(val pos: (Position, Position)) extends PNode {
   override def pretty = s" ${e.l.pretty}\n  ${e.inner.pretty}\n${e.r.pretty}"
 }
 
+// Maybe we can lift the `PGlobalUniqueDeclaration` restriction?
 trait PGlobalCallable extends PGlobalDeclaration {
   def args: PDelimited.Comma[PSym.Paren, PAnyFormalArgDecl]
   def formalArgs: Seq[PAnyFormalArgDecl] = args.inner.toSeq
@@ -1383,11 +1599,11 @@ trait PMember extends PScope with PAnnotated {
 }
 
 /** Anything that is a PMember and declares only a single thing (itself) */
-trait PSingleMember extends PMember with PGlobalDeclaration {
+trait PSingleMember extends PMember with PGlobalDeclaration with PGlobalUniqueDeclaration {
   override def declares = Seq(this)
 }
 
-sealed trait PAnyFunction extends PSingleMember with PGlobalDeclaration with PTypedDeclaration with PGlobalCallable with PLspAnyFunction {
+trait PAnyFunction extends PScope with PTypedDeclaration with PGlobalCallable with PLspAnyFunction {
   def resultType: PType
   override def typ: PFunctionType = PFunctionType(formalArgs.map(_.typ), resultType)
 }
@@ -1395,11 +1611,12 @@ sealed trait PAnyFunction extends PSingleMember with PGlobalDeclaration with PTy
 ///////////////////////////////////////////////////////////////////////////
 // Program Members
 
-case class PProgram(imports: Seq[PImport], macros: Seq[PDefine], domains: Seq[PDomain], fields: Seq[PFields], functions: Seq[PFunction], predicates: Seq[PPredicate], methods: Seq[PMethod], extensions: Seq[PExtender], errors: Seq[ParseReport])(val pos: (Position, Position)) extends PNode with PLspProgram {
+case class PProgram(imports: Seq[PImport], macros: Seq[PDefine], domains: Seq[PDomain], fields: Seq[PFields], functions: Seq[PFunction], predicates: Seq[PPredicate], methods: Seq[PMethod], extensions: Seq[PExtender])(val pos: (Position, Position), val errors: Seq[ParseReport]) extends PNode with PLspProgram {
   override def pretty =  {
     val all = Seq(imports, macros, domains, fields, functions, predicates, methods, extensions).filter(_.length > 0)
     all.map(_.map(_.pretty).mkString("\n")).mkString("\n")
   }
+  override def getExtraVals: Seq[Any] = Seq(pos, errors)
 }
 
 case class PImport(annotations: Seq[PAnnotation], imprt: PKw.Import, file: PStringLiteral)(val pos: (Position, Position)) extends PNode with PPrettySubnodes with PLspDocumentSymbol {
@@ -1414,12 +1631,14 @@ case class PImport(annotations: Seq[PAnnotation], imprt: PKw.Import, file: PStri
   }
 }
 
-case class PDefine(annotations: Seq[PAnnotation], define: PKw.Define, idndef: PIdnDef, parameters: Option[PDelimited.Comma[PSym.Paren, PIdnDef]], body: PNode)(val pos: (Position, Position)) extends PSingleMember with PStmt with PAnnotated with PGlobalDeclaration {
+case class PDefineParam(idndef: PIdnDef)(val pos: (Position, Position)) extends PNode with PLocalDeclaration with PPrettySubnodes with PLspAnyVarDecl {
+  override def typeMaybe: Option[PType] = None
+  override def description: String = "Macro Parameter"
+  override def tokenType: TokenType.TokenType = TokenType.Parameter
+}
+
+case class PDefine(annotations: Seq[PAnnotation], define: PKw.Define, idndef: PIdnDef, parameters: Option[PDelimited.Comma[PSym.Paren, PDefineParam]], body: PNode)(val pos: (Position, Position)) extends PSingleMember with PStmt with PNameAnalyserOpaque {
   override def symbolKind: SymbolKind.SymbolKind = SymbolKind.Function
-  override def hint: String = {
-    val params = parameters.map(_.pretty).getOrElse("")
-    s"${define.pretty} ${idndef.pretty}$params"
-  }
   override def completionScope: Map[SuggestionScope,Byte] = body match {
     case _: PExp => Map(ExpressionScope -> 0, TypeScope -> 0, StatementScope -> -50)
     case _: PStmt => Map(StatementScope -> 0)
@@ -1428,10 +1647,11 @@ case class PDefine(annotations: Seq[PAnnotation], define: PKw.Define, idndef: PI
   override def completionKind: CompletionKind.CompletionKind = CompletionKind.Snippet
   override def tokenType = TokenType.Macro
   override def description: String = "Macro"
+  override def hint: String = this.pretty
 }
 
 case class PDomain(annotations: Seq[PAnnotation], domain: PKw.Domain, idndef: PIdnDef, typVars: Option[PDelimited.Comma[PSym.Bracket, PTypeVarDecl]], interpretations: Option[PDomainInterpretations], members: PGrouped[PSym.Brace, PDomainMembers])
-                  (val pos: (Position, Position)) extends PSingleMember with PGlobalDeclaration with PPrettySubnodes with HasFoldingRanges with HasSuggestionScopeRanges {
+                  (val pos: (Position, Position)) extends PSingleMember with PTypeDeclaration with PPrettySubnodes with HasFoldingRanges with HasSuggestionScopeRanges {
   def typVarsSeq: Seq[PTypeVarDecl] = typVars.map(_.inner.toSeq).getOrElse(Nil)
 
   override def tokenType = TokenType.Interface
@@ -1452,9 +1672,10 @@ case class PDomain(annotations: Seq[PAnnotation], domain: PKw.Domain, idndef: PI
 case class PDomainFunctionInterpretation(k: PKw.Interpretation, i: PStringLiteral)(val pos: (Position, Position)) extends PNode with PPrettySubnodes {
   override def pretty = s"\n  ${super.pretty}"
 }
-case class PDomainFunction(annotations: Seq[PAnnotation], unique: Option[PKw.Unique], function: PKw.Function, idndef: PIdnDef, args: PDelimited.Comma[PSym.Paren, PAnyFormalArgDecl], c: PSym.Colon, resultType: PType, interpretation: Option[PDomainFunctionInterpretation])
-                          (val domainName: PIdnRef)(val pos: (Position, Position)) extends PAnyFunction with PPrettySubnodes {
-
+trait PDomainMember extends PScope {
+  def domain: PDomain = getAncestor[PDomain].get
+}
+case class PDomainFunction(annotations: Seq[PAnnotation], unique: Option[PKw.Unique], function: PKw.Function, idndef: PIdnDef, args: PDelimited.Comma[PSym.Paren, PDomainFunctionArg], c: PSym.Colon, resultType: PType, interpretation: Option[PDomainFunctionInterpretation])(val pos: (Position, Position)) extends PSingleMember with PAnyFunction with PDomainMember with PPrettySubnodes {
   override def keyword = function
   override def pres = PDelimited.empty
   override def posts = PDelimited.empty
@@ -1462,7 +1683,7 @@ case class PDomainFunction(annotations: Seq[PAnnotation], unique: Option[PKw.Uni
   override def description: String = "Domain Function"
 }
 
-case class PAxiom(annotations: Seq[PAnnotation], axiom: PKw.Axiom, idndef: Option[PIdnDef], exp: PBracedExp)(val domainName: PIdnRef)(val pos: (Position, Position)) extends PScope with PPrettySubnodes with HasFoldingRanges {
+case class PAxiom(annotations: Seq[PAnnotation], axiom: PKw.Axiom, idndef: Option[PIdnDef], exp: PBracedExp)(val pos: (Position, Position)) extends PDomainMember with PPrettySubnodes with HasFoldingRanges {
 
   override def getFoldingRanges: Seq[FoldingRange] = RangePosition(exp).map(FoldingRange(_)).toSeq
 }
@@ -1480,7 +1701,7 @@ case class PDomainInterpretations(k: PReserved[PKeywordLang], m: PDelimited.Comm
 }
 
 trait PDomainMember1 extends PNode with PPrettySubnodes
-case class PDomainFunction1(annotations: Seq[PAnnotation], unique: Option[PKw.Unique], function: PKw.Function, idndef: PIdnDef, args: PDelimited.Comma[PSym.Paren, PAnyFormalArgDecl], c: PSym.Colon, typ: PType, interpretation: Option[PDomainFunctionInterpretation], s: Option[PSym.Semi])(val pos: (Position, Position)) extends PDomainMember1
+case class PDomainFunction1(annotations: Seq[PAnnotation], unique: Option[PKw.Unique], function: PKw.Function, idndef: PIdnDef, args: PDelimited.Comma[PSym.Paren, PDomainFunctionArg], c: PSym.Colon, typ: PType, interpretation: Option[PDomainFunctionInterpretation], s: Option[PSym.Semi])(val pos: (Position, Position)) extends PDomainMember1
 case class PAxiom1(annotations: Seq[PAnnotation], axiom: PKw.Axiom, idndef: Option[PIdnDef], exp: PBracedExp, s: Option[PSym.Semi])(val pos: (Position, Position)) extends PDomainMember1
 case class PDomainMembers1(members: Seq[PDomainMember1])(val pos: (Position, Position)) extends PNode with PPrettySubnodes
 
@@ -1494,7 +1715,7 @@ case class PSpecification[+T <: PKw.Spec](k: PReserved[PKw.Spec], e: PExp)(val p
 }
 
 case class PFunction(annotations: Seq[PAnnotation], function: PKw.Function, idndef: PIdnDef, args: PDelimited.Comma[PSym.Paren, PFormalArgDecl], c: PSym.Colon, resultType: PType, pres: PDelimited[PSpecification[PKw.PreSpec], Option[PSym.Semi]], posts: PDelimited[PSpecification[PKw.PostSpec], Option[PSym.Semi]], body: Option[PBracedExp])
-                    (val pos: (Position, Position)) extends PAnyFunction with PGlobalCallableNamedArgs with PPrettySubnodes {
+                    (val pos: (Position, Position)) extends PSingleMember with PAnyFunction with PGlobalCallableNamedArgs with PPrettySubnodes {
   def deepCopy(annotations: Seq[PAnnotation] = this.annotations, function: PKw.Function = this.function, idndef: PIdnDef = this.idndef, args: PDelimited.Comma[PSym.Paren, PFormalArgDecl] = this.args, c: PSym.Colon = this.c, resultType: PType = this.resultType, pres: PDelimited[PSpecification[PKw.PreSpec], Option[PSym.Semi]] = this.pres, posts: PDelimited[PSpecification[PKw.PostSpec], Option[PSym.Semi]] = this.posts, body: Option[PBracedExp] = this.body): PFunction = {
     StrategyBuilder.Slim[PNode]({
       case p: PFunction => PFunction(annotations, function, idndef, args, c, resultType, pres, posts, body)(p.pos)
@@ -1507,9 +1728,9 @@ case class PFunction(annotations: Seq[PAnnotation], function: PKw.Function, idnd
 }
 
 case class PPredicate(annotations: Seq[PAnnotation], predicate: PKw.Predicate, idndef: PIdnDef, args: PDelimited.Comma[PSym.Paren, PFormalArgDecl], body: Option[PBracedExp])(val pos: (Position, Position))
-  extends PAnyFunction with PGlobalCallableNamedArgs with PPrettySubnodes {
+  extends PSingleMember with PAnyFunction with PGlobalCallableNamedArgs with PPrettySubnodes {
   override def c = PReserved.implied(PSym.Colon)
-  override def resultType = Bool
+  override def resultType = Predicate
 
   override def returnString: Option[String] = None
 
@@ -1614,6 +1835,4 @@ trait PExtender extends PNode {
   def translateExp(t: Translator): Exp = ???
 
   def translateType(t: Translator): Type = ???
-
-  def transformExtension(t: Transformer.type): PNode = ???
 }
diff --git a/src/main/scala/viper/silver/parser/ParseAstKeyword.scala b/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
index 866bd1e78..7fa16659a 100644
--- a/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
+++ b/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
@@ -333,6 +333,7 @@ object PSym {
 /** Anything that can act as an operator. */
 trait POperator extends PReservedString with PLspOperator {
   def operator: String
+  def requirePureArgs = false
   override def token = operator
   override def documentationAsHint: Boolean = false
 }
@@ -362,6 +363,7 @@ trait PLogicalOp extends PBinaryOp {
   override def signatures = List(Map(POpApp.pArgS(0) -> Bool, POpApp.pArgS(1) -> Bool, POpApp.pResS -> Bool))
 }
 trait PEqOp extends PBinaryOp {
+  override def requirePureArgs = true
   override def signatures = List(Map(POpApp.pArgS(1) -> POpApp.pArg(0), POpApp.pResS -> Bool))
 }
 trait PCollectionOp extends PBinaryOp
@@ -372,10 +374,8 @@ object PCollectionOp {
 object PSymOp {
   case object Wand    extends PSym("--*") with PSymbolOp with PBinaryOp {
     override def signatures = List(
-      Map(POpApp.pArgS(0) -> Bool, POpApp.pArgS(1) -> Bool, POpApp.pResS -> TypeHelper.Wand),
-      Map(POpApp.pArgS(0) -> Bool, POpApp.pArgS(1) -> Bool, POpApp.pResS -> Bool),
-      Map(POpApp.pArgS(0) -> Bool, POpApp.pArgS(1) -> TypeHelper.Wand, POpApp.pResS -> TypeHelper.Wand),
-      Map(POpApp.pArgS(0) -> Bool, POpApp.pArgS(1) -> TypeHelper.Wand, POpApp.pResS -> Bool))
+      Map(POpApp.pArgS(0) -> Impure, POpApp.pArgS(1) -> Impure, POpApp.pResS -> TypeHelper.Wand),
+    )
   }
   type Wand = PReserved[Wand.type]
 
@@ -386,24 +386,38 @@ object PSymOp {
   case object Ge      extends PSym(">=")  with PSymbolOp with PBinaryOp with PCmpOp
   case object Lt      extends PSym("<")   with PSymbolOp with PBinaryOp with PCmpOp
   case object Gt      extends PSym(">")   with PSymbolOp with PBinaryOp with PCmpOp
-  case object AndAnd  extends PSym("&&")  with PSymbolOp with PBinaryOp with PLogicalOp
+  case object AndAnd  extends PSym("&&")  with PSymbolOp with PBinaryOp {
+    override def signatures = List(
+      Map(POpApp.pArgS(0) -> Bool, POpApp.pArgS(1) -> Bool, POpApp.pResS -> Bool),
+      Map(POpApp.pArgS(0) -> Impure, POpApp.pArgS(1) -> Impure, POpApp.pResS -> Impure),
+    )
+  }
   case object OrOr    extends PSym("||")  with PSymbolOp with PBinaryOp with PLogicalOp
-  case object Implies extends PSym("==>") with PSymbolOp with PBinaryOp with PLogicalOp
+  case object Implies extends PSym("==>") with PSymbolOp with PBinaryOp {
+    override def signatures = List(
+      Map(POpApp.pArgS(0) -> Bool, POpApp.pArgS(1) -> Bool, POpApp.pResS -> Bool),
+      Map(POpApp.pArgS(0) -> Bool, POpApp.pArgS(1) -> Impure, POpApp.pResS -> Impure),
+    )
+  }
   type Implies = PReserved[Implies.type]
   case object Iff    extends PSym("<==>") with PSymbolOp with PBinaryOp with PLogicalOp
   case object Mul     extends PSym("*")   with PSymbolOp with PBinaryOp {
     override def signatures = List(
       Map(POpApp.pArgS(0) -> Perm, POpApp.pArgS(1) -> Perm, POpApp.pResS -> Perm),
+      // The following two are not necessary if `Int` is a subtype of `Perm`
       Map(POpApp.pArgS(0) -> Int, POpApp.pArgS(1) -> Perm, POpApp.pResS -> Perm),
       Map(POpApp.pArgS(0) -> Perm, POpApp.pArgS(1) -> Int, POpApp.pResS -> Perm),
-      Map(POpApp.pArgS(0) -> Int, POpApp.pArgS(1) -> Int, POpApp.pResS -> Int))
+      Map(POpApp.pArgS(0) -> Int, POpApp.pArgS(1) -> Int, POpApp.pResS -> Int),
+    )
   }
   case object Div     extends PSym("/")   with PSymbolOp with PBinaryOp {
     override def signatures = List(
+      // The following two are not necessary if `Int` is a subtype of `Perm`
       Map(POpApp.pArgS(0) -> Int, POpApp.pArgS(1) -> Int, POpApp.pResS -> Perm),
       Map(POpApp.pArgS(0) -> Perm, POpApp.pArgS(1) -> Int, POpApp.pResS -> Perm),
+      Map(POpApp.pArgS(0) -> Int, POpApp.pArgS(1) -> Int, POpApp.pResS -> Int),
       Map(POpApp.pArgS(0) -> Perm, POpApp.pArgS(1) -> Perm, POpApp.pResS -> Perm),
-      Map(POpApp.pArgS(0) -> Int, POpApp.pArgS(1) -> Int, POpApp.pResS -> Int))
+    )
   }
   case object ArithDiv extends PSym("\\") with PSymbolOp with PBinaryOp with PIntOp
   case object Mod     extends PSym("%")   with PSymbolOp with PBinaryOp with PIntOp
@@ -411,7 +425,8 @@ object PSymOp {
   case object Minus   extends PSym("-")   with PSymbolOp with PBinaryOp with PArithOp
   case object Append  extends PSym("++")  with PSymbolOp with PBinaryOp with PCollectionOp {
     override def signatures = List(
-      Map(POpApp.pArgS(0) -> MakeSeq(PCollectionOp.infVar), POpApp.pArgS(1) -> MakeSeq(PCollectionOp.infVar), POpApp.pResS -> MakeSeq(PCollectionOp.infVar)))
+      Map(POpApp.pArgS(0) -> MakeSeq(PCollectionOp.infVar), POpApp.pArgS(1) -> MakeSeq(PCollectionOp.infVar), POpApp.pResS -> MakeSeq(PCollectionOp.infVar)),
+    )
   }
 
   case object Neg     extends PSym("-")   with PSymbolOp with PUnaryOp {
@@ -448,20 +463,20 @@ object PSymOp {
 // Use the token type from `PLspKeyword`
 trait POperatorKeyword extends PKeyword with POperator with PLspKeyword
 
-trait PSetToSetOp extends PBinaryOp {
+trait PSetToSetOp extends PBinaryOp with PCollectionOp {
   override def signatures = List(
     Map(POpApp.pArgS(0) -> MakeSet(PCollectionOp.infVar), POpApp.pArgS(1) -> MakeSet(PCollectionOp.infVar), POpApp.pResS -> MakeSet(PCollectionOp.infVar)),
     Map(POpApp.pArgS(0) -> MakeMultiset(PCollectionOp.infVar), POpApp.pArgS(1) -> MakeMultiset(PCollectionOp.infVar), POpApp.pResS -> MakeMultiset(PCollectionOp.infVar))
   )
 }
-trait PInOp extends PBinaryOp {
+trait PInOp extends PBinaryOp with PCollectionOp {
   override def signatures = List(
     Map(POpApp.pArgS(1) -> MakeSet(POpApp.pArg(0)), POpApp.pResS -> Bool),
     Map(POpApp.pArgS(1) -> MakeSeq(POpApp.pArg(0)), POpApp.pResS -> Bool),
     Map(POpApp.pArgS(1) -> MakeMultiset(POpApp.pArg(0)), POpApp.pResS -> Int),
     Map(POpApp.pArgS(1) -> MakeMap(POpApp.pArg(0), PCollectionOp.infVar), POpApp.pResS -> Bool))
 }
-trait PSubsetOp extends PBinaryOp {
+trait PSubsetOp extends PBinaryOp with PCollectionOp {
   override def signatures = List(
     Map(POpApp.pArgS(0) -> MakeSet(PCollectionOp.infVar), POpApp.pArgS(1) -> MakeSet(PCollectionOp.infVar), POpApp.pResS -> Bool),
     Map(POpApp.pArgS(0) -> MakeMultiset(PCollectionOp.infVar), POpApp.pArgS(1) -> MakeMultiset(PCollectionOp.infVar), POpApp.pResS -> Bool))
diff --git a/src/main/scala/viper/silver/parser/ParseAstLsp.scala b/src/main/scala/viper/silver/parser/ParseAstLsp.scala
index f73ba0b38..89c208935 100644
--- a/src/main/scala/viper/silver/parser/ParseAstLsp.scala
+++ b/src/main/scala/viper/silver/parser/ParseAstLsp.scala
@@ -68,7 +68,7 @@ trait PLspHoverHintBoth extends PLspHoverHint with PLspHoverHintRef {
 // Identifiers (uses and definitions)
 ////
 trait PLspIdnUse extends PNode with PLspTokenModifiers with HasSemanticHighlights with HasGotoDefinitions with HasReferenceTos {
-  def decl: Option[PDeclaration]
+  def decl: Option[PDeclarationInner]
   def assignUse: Boolean
 
   override def tokenModifiers = (if (assignUse) Seq(TokenModifier.Modification) else Nil)
@@ -133,29 +133,33 @@ trait PLspOperator extends PLspReservedString {
 // Variable declarations
 ////
 trait PLspAnyVarDecl extends PLspDeclaration {
-  def typ: PType
+  def typeMaybe: Option[PType]
   override def hint = pretty
-  override def detail = Some(typ.pretty)
+  override def detail = typeMaybe.map(_.pretty)
   override def symbolKind = SymbolKind.Variable
   override def completionScope = Map(ExpressionScope -> 0, StatementScope -> -50)
   override def completionKind = CompletionKind.Variable
 }
+trait PLspTypedVarDecl extends PLspAnyVarDecl {
+  def typ: PType
+  override def typeMaybe = Some(typ)
+}
 
-trait PLspFormalArgDecl extends PLspDeclaration with PLspAnyVarDecl {
+trait PLspFormalArgDecl extends PLspDeclaration with PLspTypedVarDecl {
   override def tokenType = TokenType.Parameter
   override def description = "Argument Binding"
   override def tokenModifiers = Seq(TokenModifier.Readonly)
 }
-trait PLspFormalReturnDecl extends PLspDeclaration with PLspAnyVarDecl {
+trait PLspFormalReturnDecl extends PLspDeclaration with PLspTypedVarDecl {
   override def tokenType = TokenType.Variable
   override def description = "Return Variable"
 }
-trait PLspLogicalVarDecl extends PLspDeclaration with PLspAnyVarDecl {
+trait PLspLogicalVarDecl extends PLspDeclaration with PLspTypedVarDecl {
   override def tokenType = TokenType.Parameter
   override def description = "Logical Binding"
   override def tokenModifiers = Seq(TokenModifier.Readonly)
 }
-trait PLspLocalVarDecl extends PLspDeclaration with PLspAnyVarDecl {
+trait PLspLocalVarDecl extends PLspDeclaration with PLspTypedVarDecl {
   override def tokenType = TokenType.Variable
   override def description = "Local Variable"
 }
@@ -216,7 +220,8 @@ trait PLspCall extends PLspExpRef with HasInlayHints {
     parts.head == d || parts.last == d
   }
   override def getInlayHints: Seq[InlayHint] = formalArgs.zip(args).flatMap {
-    case (_: PUnnamedFormalArgDecl, _) => None
+    case (PDomainFunctionArg(None, _, _), _) => None
+    case (PDomainFunctionArg(Some(decl), _, _), PIdnUseExp(use)) if idnUseMatchesArg(decl.name, use) => None
     case (PFormalArgDecl(decl, _, _), PIdnUseExp(use)) if idnUseMatchesArg(decl.name, use) => None
     case (PFormalArgDecl(decl, _, _), arg) => (RangePosition(decl), RangePosition(arg)) match {
       case (Some(declRp), Some(argRp)) => {
diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala
index 399b15441..9e6514b4a 100644
--- a/src/main/scala/viper/silver/parser/Resolver.scala
+++ b/src/main/scala/viper/silver/parser/Resolver.scala
@@ -7,10 +7,8 @@
 package viper.silver.parser
 
 import viper.silver.FastMessaging
-import viper.silver.ast.LabelledOld
 
 import scala.collection.mutable
-import scala.reflect._
 
 /**
   * A resolver and type-checker for the intermediate Viper AST.
@@ -55,6 +53,7 @@ case class TypeChecker(names: NameAnalyser) {
   var curMember: PScope = null
   var curFunction: PFunction = null
   var resultAllowed: Boolean = false
+  var permBan: Option[String] = None
 
   /** to record error messages */
   var messages: FastMessaging.Messages = Nil
@@ -92,13 +91,6 @@ case class TypeChecker(names: NameAnalyser) {
     p.functions foreach checkBody
     p.predicates foreach checkBody
     p.methods foreach checkBody
-
-
-    /* Report any domain type that couldn't be resolved */
-    /* Alex suggests replacing *all* these occurrences by one arbitrary type */
-    p visit {
-      case dt: PDomainType if dt.isUndeclared => messages ++= FastMessaging.message(dt, s"found undeclared type ${dt.domain.name}")
-    }
   }
 
   def checkMember(m: PScope)(fcheck: => Unit): Unit = {
@@ -116,8 +108,14 @@ case class TypeChecker(names: NameAnalyser) {
 
   def checkBody(m: PMethod): Unit = {
     checkMember(m) {
-      m.pres.toSeq foreach (p => check(p.e, Bool))
-      m.posts.toSeq foreach (p => check(p.e, Bool))
+      m.pres.toSeq foreach (p => {
+        check(p.e, Impure)
+        checkNoPermForpermExceptInhaleExhale(p.e)
+      })
+      m.posts.toSeq foreach (p => {
+        check(p.e, Impure)
+        checkNoPermForpermExceptInhaleExhale(p.e)
+      })
       m.body.foreach(check)
     }
   }
@@ -136,9 +134,18 @@ case class TypeChecker(names: NameAnalyser) {
     checkMember(f) {
       assert(curFunction == null)
       curFunction = f
-      f.pres.toSeq foreach (p => check(p.e, Bool))
+      f.pres.toSeq foreach (p => {
+        check(p.e, Impure)
+        checkNoPermForpermExceptInhaleExhale(p.e)
+        checkNoMagicWands(p.e)
+      })
+      permBan = Some("function postconditions")
       resultAllowed = true
-      f.posts.toSeq foreach (p => check(p.e, Bool))
+      f.posts.toSeq foreach (p => {
+        check(p.e, Bool)
+        checkNoPermForpermExceptInhaleExhale(p.e, true)
+      })
+      permBan = None
       f.body.map(_.e.inner).foreach(check(_, f.typ.resultType)) //result in the function body gets the error message somewhere else
       resultAllowed = false
       curFunction = null
@@ -153,7 +160,10 @@ case class TypeChecker(names: NameAnalyser) {
 
   def checkBody(p: PPredicate): Unit = {
     checkMember(p) {
-      p.body.map(_.e.inner).foreach(check(_, Bool))
+      p.body.foreach(b => {
+        check(b.e.inner, Impure)
+        checkNoMagicWands(b.e.inner)
+      })
     }
   }
 
@@ -187,6 +197,10 @@ case class TypeChecker(names: NameAnalyser) {
   def check(f: PDomainFunction): Unit = {
     check(f.typ)
     f.formalArgs foreach (a => check(a.typ))
+    // This should probably be reported the name analyser instead
+    val idndefs = f.args.inner.toSeq.flatMap(_.name)
+    val duplicates = idndefs.groupBy(_.name).collect { case (_, v) if v.length > 1 => v }
+    duplicates.foreach(d => messages ++= FastMessaging.message(d.head, s"duplicate argument name `${d.last.name}`"))
   }
 
   def check(stmt: PStmt): Unit = {
@@ -199,10 +213,10 @@ case class TypeChecker(names: NameAnalyser) {
         }
       case PFold(_, e) =>
         acceptNonAbstractPredicateAccess(e, "abstract predicates cannot be folded")
-        check(e, Bool)
+        check(e, Predicate)
       case PUnfold(_, e) =>
         acceptNonAbstractPredicateAccess(e, "abstract predicates cannot be unfolded")
-        check(e, Bool)
+        check(e, Predicate)
       case PPackageWand(_, e, proofScript) =>
         check(e, Wand)
         checkMagicWand(e)
@@ -211,17 +225,21 @@ case class TypeChecker(names: NameAnalyser) {
         check(e, Wand)
         checkMagicWand(e)
       case PExhale(_, e) =>
-        check(e, Bool)
+        check(e, Impure)
+        if (e.typ == Bool)
+          messages ++= FastMessaging.message(stmt, "found `exhale` of pure boolean expression, use `assert` instead", error = false)
       case PAssert(_, e) =>
-        check(e, Bool)
+        check(e, Impure)
       case PInhale(_, e) =>
-        check(e, Bool)
+        check(e, Impure)
+        if (e.typ == Bool)
+          messages ++= FastMessaging.message(stmt, "found `inhale` of pure boolean expression, use `assume` instead", error = false)
       case PAssume(_, e) =>
-        check(e, Bool)
+        check(e, Impure)
       case assign: PAssign =>
         checkAssign(assign)
       case PLabel(_, _, invs) =>
-        invs.toSeq foreach (i => check(i.e, Bool))
+        invs.toSeq foreach (i => check(i.e, Impure))
       case PGoto(_, _) =>
       case PIf(_, cond, thn, els) =>
         check(cond, Bool)
@@ -231,7 +249,10 @@ case class TypeChecker(names: NameAnalyser) {
         check(els)
       case PWhile(_, cond, invs, body) =>
         check(cond, Bool)
-        invs.toSeq foreach (inv => check(inv.e, Bool))
+        invs.toSeq foreach (inv => {
+          check(inv.e, Impure)
+          checkNoPermForpermExceptInhaleExhale(inv.e)
+        })
         check(body)
       case v: PVars =>
         v.vars.toSeq foreach (v => check(v.typ))
@@ -262,46 +283,60 @@ case class TypeChecker(names: NameAnalyser) {
     stmt.targets.toSeq foreach {
       case idnuse: PIdnUseExp =>
         idnuse.assignUse = true
-        names.definition(curMember)(idnuse) match {
-          case Some(decl: PAssignableVarDecl) =>
-            check(idnuse, decl.typ)
-          case _ =>
-            messages ++= FastMessaging.message(idnuse, "expected an assignable identifier as lhs")
-        }
+        if (idnuse.decls.nonEmpty) {
+          idnuse.filterDecls(_.isInstanceOf[PAssignableVarDecl])
+          if (idnuse.decl.isDefined)
+            check(idnuse, idnuse.decl.get.typ)
+          else if (idnuse.decls.isEmpty)
+            messages ++= FastMessaging.message(idnuse, s"expected an assignable identifier `${idnuse.name}` as lhs")
+          else
+            messages ++= FastMessaging.message(idnuse, s"ambiguous identifier `${idnuse.name}`, expected single parameter or local variable")
+        } else
+          messages ++= FastMessaging.message(idnuse, s"undeclared identifier `${idnuse.name}`, expected parameter or local variable")
       case fa@PFieldAccess(_, _, field) =>
         field.assignUse = true
-        names.definition(curMember)(field, Some(PFields.getClass)) match {
-          case Some(PFieldDecl(_, _, typ)) =>
-            check(fa, typ)
-          case _ =>
-            messages ++= FastMessaging.message(field, "expected a field as lhs")
-        }
+        if (field.decl.isDefined)
+          check(fa, field.decl.get.typ)
+        else if (field.decls.length > 1)
+          messages ++= FastMessaging.message(field, s"ambiguous field `${field.name}`")
+        else
+          messages ++= FastMessaging.message(field, s"undeclared field `${field.name}`")
       case call: PCall => sys.error(s"Unexpected node $call found")
     }
     // Check rhs
     stmt match {
-      case PAssign(targets, _, c@PCall(func, _, _)) if names.definition(curMember)(func).get.isInstanceOf[PMethod] =>
-        val m = names.definition(curMember)(func).get.asInstanceOf[PMethod]
-        val formalArgs = m.formalArgs
-        val formalTargets = m.formalReturns
-        c.methodDecl = Some(m)
-        func.decl = Some(m)
-        formalArgs.foreach(fa => check(fa.typ))
-        if (formalArgs.length != c.args.length) {
-          messages ++= FastMessaging.message(stmt, "wrong number of arguments")
-        } else if (formalTargets.length != targets.length) {
-          messages ++= FastMessaging.message(stmt, "wrong number of targets")
-        } else {
+      case PAssign(targets, _, c@PCall(func, _, _)) if targets.length != 1 || func.decls.forall(!_.isInstanceOf[PAnyFunction]) =>
+        if (func.filterDecls(_.isInstanceOf[PMethod]))
+          messages ++= FastMessaging.message(func, s"undeclared call `${func.name}`, expected function or method")
+        else if (func.filterDecls(_.asInstanceOf[PMethod].formalArgs.length == c.args.length))
+          messages ++= FastMessaging.message(c, s"wrong number of arguments")
+        else if (func.filterDecls(_.asInstanceOf[PMethod].formalReturns.length == targets.length))
+          messages ++= FastMessaging.message(stmt, s"wrong number of targets")
+        else if (func.decl.isEmpty)
+          messages ++= FastMessaging.message(stmt, "ambiguous method call")
+        else {
+          val m = func.decl.get.asInstanceOf[PMethod]
+          val formalArgs = m.formalArgs
+          val formalTargets = m.formalReturns
+          formalArgs.foreach(fa => check(fa.typ))
           for ((formal, actual) <- (formalArgs zip c.args) ++ (formalTargets zip targets.toSeq)) {
             check(actual, formal.typ)
           }
         }
-      case PAssign(targets, _, PNewExp(_, fieldsOpt)) if targets.length == 1 =>
+      case PAssign(targets, _, PNewExp(_, fields)) if targets.length == 1 =>
         check(targets.head, Ref)
-        fieldsOpt.inner foreach (fds => acceptAndCheckTypedEntity[PFieldDecl, Nothing](fds.toSeq, "expected a field as argument"))
+        fields.inner match {
+          case Right(fields) => fields.toSeq foreach (f => {
+            if (f.decls.isEmpty)
+              messages ++= FastMessaging.message(f, s"undeclared field `${f.name}`")
+            else if (f.decls.length > 1)
+              messages ++= FastMessaging.message(f, s"ambiguous field `${f.name}`")
+          })
+          case Left(_) =>
+        }
       case PAssign(targets, _, rhs) if targets.length == 1 => check(rhs, targets.head.typ)
-      // Case `targets.length != 1`:
-      case _ => messages ++= FastMessaging.message(stmt, "expected a method call")
+      // Case `targets.length != 1 && !rhs.isInstanceOf[PCall]`:
+      case _ => messages ++= FastMessaging.message(stmt, "expected a method call when assigning to multiple targets")
     }
   }
 
@@ -315,12 +350,12 @@ case class TypeChecker(names: NameAnalyser) {
     e match {
       case _: PFieldAccess => checkTopTyped(e, None)
       case pc: PCall =>
-        check(e, Bool)
+        check(e, Impure)
         // make sure that this is in fact a predicate
         if (!pc.isPredicate) {
           messages ++= FastMessaging.message(stmt, havocError)
         }
-      case _: PMagicWandExp => check(e, Bool)
+      case _: PMagicWandExp => check(e, Impure)
       case _ => messages ++= FastMessaging.message(stmt, havocError)
     }
   }
@@ -334,12 +369,14 @@ case class TypeChecker(names: NameAnalyser) {
         messages ++= FastMessaging.message(exp, "expected predicate access")
         return
     }
-    val ad = names.definition(curMember)(call.idnref)
-    ad match {
-      case Some(predicate: PPredicate) =>
-        if (predicate.body.isEmpty) messages ++= FastMessaging.message(call.idnref, messageIfAbstractPredicate)
-      case _ => messages ++= FastMessaging.message(exp, "expected predicate access")
-    }
+    if (call.idnref.decls.isEmpty)
+      messages ++= FastMessaging.message(call.idnref, s"undeclared predicate `${call.idnref.name}`")
+    else if (call.idnref.filterDecls(_.isInstanceOf[PPredicate]))
+      messages ++= FastMessaging.message(call.idnref, s"expected predicate access `${call.idnref.name}")
+    else if (call.idnref.decl.isEmpty)
+      messages ++= FastMessaging.message(call.idnref, s"ambiguous predicate access `${call.idnref.name}")
+    else if (call.idnref.decl.get.asInstanceOf[PPredicate].body.isEmpty)
+      messages ++= FastMessaging.message(call.idnref, messageIfAbstractPredicate)
   }
 
   def checkMagicWand(e: PExp): Unit = e match {
@@ -348,60 +385,24 @@ case class TypeChecker(names: NameAnalyser) {
       messages ++= FastMessaging.message(e, "expected magic wand")
   }
 
-  /** This handy method checks if all passed `idnUses` refer to specific
-    * subtypes `TypedEntity`s when looked up in the current scope/lookup table.
-    * For each element in `idnUses`, if it refers an appropriate subtype, then
-    * `handle` is applied to the current element of `idnUses` and to the
-    * `TypedEntity` it refers to.
-    *
-    * If only a single subtype of `TypedEntity` is acceptable, pass `Nothing`
-    * as the second type argument.
-    *
-    * Caution is advised, however, since the method checks various
-    * type-relations only at runtime.
-    *
-    * @param idnUses      Identifier usages to check
-    * @param errorMessage Error message in case one of the identifiers usages
-    *                     does not refer to an appropriate subtype of
-    *                     `TypedEntity`
-    * @param handle       Handle pairs of current identifier usage and referenced
-    *                     `TypedEntity`
-    * @tparam T1 An accepted subtype of `TypedEntity`
-    * @tparam T2 Another accepted subtype of `TypedEntity`
-    *
-    *            TODO: Generalise the method to take ClassTags T1, ..., TN.
-    *            TODO: If only a single T is taken, let handle be (PIdnUse, T) => Unit
-    */
-  def acceptAndCheckTypedEntity[T1: ClassTag, T2: ClassTag]
-  (idnUses: Seq[PIdnUse], errorMessage: => String): Unit = {
-
-    /* TODO: Ensure that the ClassTags denote subtypes of TypedEntity */
-    val acceptedClasses = Seq[Class[_]](classTag[T1].runtimeClass, classTag[T2].runtimeClass)
-
-    idnUses.foreach { use =>
-      val decl = names.definition(curMember)(use)
-
-      if (decl.isDefined) {
-        acceptedClasses.find(_.isInstance(decl.get)) match {
-          case Some(_) =>
-            val td = decl.get.asInstanceOf[PTypedDeclaration]
-            if (use.isInstanceOf[PIdnUseExp])
-              use.asInstanceOf[PIdnUseExp].typ = td.typ
-            // TODO: is this necessary?
-            use.decl = Some(td)
-          case None =>
-            messages ++= FastMessaging.message(use, errorMessage)
-        }
-      } else {
-        assert(!names.success)
-      }
-    }
+  def checkNoPermForpermExceptInhaleExhale(e: PExp, skipForPerm: Boolean = false): Unit = {
+    val errors = e.shallowCollect({
+      case p: PCurPerm => Some(p)
+      case p: PForPerm if !skipForPerm => Some(p)
+      case _: PInhaleExhaleExp => None
+    }).flatten
+    errors.foreach(e => {
+      messages ++= FastMessaging.message(e, "preconditions, postconditions and invariants may only contain `perm` and `forperm` expressions inside of an inhale-exhale")
+    })
   }
 
+  def checkNoMagicWands(e: PExp): Unit =
+    e.shallowCollect({ case p: PMagicWandExp => p }).foreach(e => {
+      messages ++= FastMessaging.message(e, "magic wands are not supported in function preconditions or predicates")
+    })
+
   def check(typ: PType): Unit = {
     typ match {
-      case _: PWandType =>
-        sys.error("unexpected use of internal typ")
       case PPrimitiv(_) =>
       /* Nothing to type check (or resolve) */
       case dt@PDomainType(_, _) if dt.isResolved =>
@@ -411,14 +412,33 @@ case class TypeChecker(names: NameAnalyser) {
 
         args foreach (_.inner.toSeq foreach check)
 
-        names.definition(curMember)(domain) match {
-          case Some(PDomain(_, _, _, typVars, _, _)) =>
-            ensure(args.map(_.inner.length) == typVars.map(_.inner.length), typ, "wrong number of type arguments")
-            dt.kind = PDomainTypeKinds.Domain
-          case Some(PTypeVarDecl(_)) =>
-            dt.kind = PDomainTypeKinds.TypeVar
-          case _ =>
-            dt.kind = PDomainTypeKinds.Undeclared
+        dt.kind = PDomainTypeKinds.Undeclared
+
+        if (domain.decls.isEmpty) {
+          if (args.isDefined)
+            messages ++= FastMessaging.message(dt, s"undeclared type `${domain.name}`, expected domain")
+          else
+            messages ++= FastMessaging.message(dt, s"undeclared type `${domain.name}`")
+        } else {
+          if (args.isDefined) {
+            if (domain.filterDecls(d => d.isInstanceOf[PDomain] && d.asInstanceOf[PDomain].typVars.isDefined && d.asInstanceOf[PDomain].typVars.get.inner.length == args.get.inner.length))
+              messages ++= FastMessaging.message(dt, s"undeclared type `${domain.name}`, expected domain with ${args.get.inner.length} type argument${if (args.get.inner.length == 1) "" else "s"}")
+          } else {
+            if (domain.filterDecls(d => !d.isInstanceOf[PDomain] || (d.isInstanceOf[PDomain] && d.asInstanceOf[PDomain].typVars.isEmpty)))
+              messages ++= FastMessaging.message(dt, s"undeclared type `${domain.name}`, found domain with type arguments")
+          }
+
+          if (domain.decl.isEmpty) {
+            if (domain.decls.length > 1)
+              messages ++= FastMessaging.message(dt, s"ambiguous type `${domain.name}`")
+          } else domain.decl.get match {
+            case PDomain(_, _, _, typVars, _, _) =>
+              // Should never fail, checked above with `filterDecls`
+              ensure(args.map(_.inner.length) == typVars.map(_.inner.length), typ, "wrong number of type arguments")
+              dt.kind = PDomainTypeKinds.Domain
+            case PTypeVarDecl(_) =>
+              dt.kind = PDomainTypeKinds.TypeVar
+          }
         }
 
       case PSeqType(_, elemType) =>
@@ -436,64 +456,17 @@ case class TypeChecker(names: NameAnalyser) {
       case t: PExtender =>
         t.typecheck(this, names).getOrElse(Nil) foreach (message =>
           messages ++= FastMessaging.message(t, message))
-      case PUnknown() =>
-        messages ++= FastMessaging.message(typ, "expected concrete type, but found unknown type")
-    }
-  }
-
-  /**
-    * Are types 'a' and 'b' compatible?  Type variables are assumed to be unbound so far,
-    * and if they occur they are compatible with any type. PUnknown is also compatible with
-    * everything, as are undeclared PDomainTypes.
-    */
-  def isCompatible(a: PType, b: PType): Boolean = {
-    (a, b) match {
-      case _ if a == b => true
-      case (PUnknown(), _) | (_, PUnknown()) => true
-      case (dt: PDomainType, _) if dt.isUndeclared => true
-      case (_, dt: PDomainType) if dt.isUndeclared => true
-      case (PTypeVar(_), _) | (_, PTypeVar(_)) => true
-      case (Bool, PWandType()) => true
-      case (PSeqType(_, e1), PSeqType(_, e2)) => isCompatible(e1.inner, e2.inner)
-      case (PSetType(_, e1), PSetType(_, e2)) => isCompatible(e1.inner, e2.inner)
-      case (PMultisetType(_, e1), PMultisetType(_, e2)) => isCompatible(e1.inner, e2.inner)
-      case (m1: PMapType, m2: PMapType) => isCompatible(m1.keyType, m2.keyType) && isCompatible(m1.valueType, m2.valueType)
-      case (PDomainType(domain1, args1), PDomainType(domain2, args2))
-        if domain1 == domain2 && args1.map(_.inner.length) == args2.map(_.inner.length) =>
-        (args1.toSeq.flatMap(_.inner.toSeq) zip args2.toSeq.flatMap(_.inner.toSeq)) forall (x => isCompatible(x._1, x._2))
-
-      case (_: PExtender, _) => false // TBD: the equality function for two type variables
-      case (_, _: PExtender) => false // TBD: the equality function for two type variables
-
-      case _ => false
-    }
-  }
-
-  /**
-    * Type-check and resolve e and ensure that it has type expected.  If that is not the case, then an
-    * error should be issued.
-    */
-  def composeAndAdd(pts1: PTypeSubstitution, pts2: PTypeSubstitution, pt1: PType, pt2: PType): Either[(PType, PType), PTypeSubstitution] = {
-    val sharedKeys = pts1.keySet.intersect(pts2.keySet)
-    if (sharedKeys.exists(p => pts1.get(p).get != pts2.get(p).get)) {
-      /* no composed substitution if input substitutions do not match */
-      val nonMatchingKey = sharedKeys.find(p => pts1.get(p).get != pts2.get(p).get).get
-      return Left((pts1.get(nonMatchingKey).get, pts2.get(nonMatchingKey).get))
+      case _: PInternalType =>
+        sys.error("unexpected use of internal typ")
     }
-
-    //composed substitution before add
-    val cs = new PTypeSubstitution(
-      pts1.map({ case (s: String, pt: PType) => s -> pt.substitute(pts2) }) ++
-        pts2.map({ case (s: String, pt: PType) => s -> pt.substitute(pts1) }))
-    cs.add(pt1, pt2)
   }
 
   /*
    * Parameters:
    * rlts: local substitutions, refreshed
    * argData: a sequence of tuples, one per op arguments, where
-   *          _1 is the fresh local argument type
-   *          _2 is the type of the argument expression
+   *          _1 is the type of the argument expression
+   *          _2 is the fresh local argument type
    *          _3 is the set of substitutions of the argument expression
    *          _4 is the argument expression itself (used to extract a precise position)
    * Returns:
@@ -505,10 +478,11 @@ case class TypeChecker(names: NameAnalyser) {
   def unifySequenceWithSubstitutions(rlts: Seq[PTypeSubstitution],
                                      argData: scala.collection.immutable.Seq[(PType, PType, Seq[PTypeSubstitution], PExp)])
   : Either[(PType, PType, PExp), Seq[PTypeSubstitution]] = {
-    var pss = rlts
+    // Merge all the substitutions of all arguments
+    var pss = rlts.map(ts => PTypeSubstitutionInternal(ts.m))
     for (tri <- argData) {
       val current = (for (ps <- pss; aps <- tri._3)
-        yield composeAndAdd(ps, aps, tri._1, tri._2))
+        yield ps.compose(aps))
       val allBad = current.forall(e => e.isLeft)
       if (allBad) {
         val badMatch = current.find(e => e.isLeft)
@@ -517,22 +491,29 @@ case class TypeChecker(names: NameAnalyser) {
       }
       pss = current.flatMap(_.toOption)
     }
-    Right(pss)
-  }
 
-  def getParentAxiom(n: PNode): Option[PAxiom] = n match {
-    case a: PAxiom => Some(a)
-    case _ => n.parent.flatMap(getParentAxiom)
+    // Add in the signature -> argument type substitutions
+    for (tri <- argData) {
+      val current = (for (ps <- pss)
+        yield ps.add(tri._1, tri._2))
+      val allBad = current.forall(e => e.isLeft)
+      if (allBad) {
+        val badMatch = current.find(e => e.isLeft)
+        val badTypes = badMatch.get.swap.toOption.get
+        return Left(badTypes._1, badTypes._2, tri._4)
+      }
+      pss = current.flatMap(_.toOption)
+    }
+    Right(pss.map(_.collapse))
   }
 
   def ground(exp: PExp, pts: PTypeSubstitution): PTypeSubstitution = {
     pts.m.flatMap(kv => kv._2.freeTypeVariables &~ pts.m.keySet).foldLeft(pts)((ts, fv) => {
       var chosenType: PType = PTypeSubstitution.defaultType
-      getParentAxiom(curMember) match {
-        case Some(ax: PAxiom) if ax.parent.exists(p => p.isInstanceOf[PDomain]) =>
+      curMember.getAncestor[PDomain] match {
+        case Some(domain: PDomain) =>
           // If we are inside the domain that defines the type variable, then we choose the type variable itself
           // as the default.
-          val domain = ax.parent.get.asInstanceOf[PDomain]
           // The name pf domain function application type variables has the form
           // domainName + PTypeVar.domainNameSep + typeVarName + PTypeVar.sep + index
           if (fv.startsWith(domain.idndef.name + PTypeVar.domainNameSep)) {
@@ -549,7 +530,7 @@ case class TypeChecker(names: NameAnalyser) {
       }
       if (chosenType == PTypeSubstitution.defaultType) {
         messages ++= FastMessaging.message(exp,
-          s"Unconstrained type parameter, substituting default type ${PTypeSubstitution.defaultType}.", error = false)
+          s"unconstrained type parameter, substituting default type ${PTypeSubstitution.defaultType}", error = false)
       }
       ts.add(PTypeVar(fv), chosenType).toOption.get
     })
@@ -561,7 +542,7 @@ case class TypeChecker(names: NameAnalyser) {
   }
 
   def typeError(exp: PExp) = {
-    messages ++= FastMessaging.message(exp, s"Type error in the expression at ${exp.pos._1}")
+    messages ++= FastMessaging.message(exp, s"type error")
   }
 
   def check(exp: PExp, expected: PType) = exp match {
@@ -578,22 +559,22 @@ case class TypeChecker(names: NameAnalyser) {
         case Some(expected) if expected.isValidOrUndeclared => exp.typeSubstitutions.flatMap(_.add(exp.typ, expected).toOption)
         case _ => exp.typeSubstitutions
       }
+      var error = true
       if (etss.nonEmpty) {
         val ts = selectAndGroundTypeSubstitution(exp, etss)
         exp.forceSubstitution(ts)
-      } else {
-        oexpected match {
-          case Some(expected) =>
-            val reportedActual = if (exp.typ.isGround) {
-              exp.typ
-            } else {
-              exp.typ.substitute(selectAndGroundTypeSubstitution(exp, exp.typeSubstitutions))
-            }
-            messages ++= FastMessaging.message(exp,
-              s"Expected type ${expected.pretty}, but found ${reportedActual.pretty} at the expression at ${exp.pos._1}")
-          case None =>
-            typeError(exp)
-        }
+        error = oexpected.isDefined && !isSubtype(exp.typ, oexpected.get)
+      }
+      if (error) oexpected match {
+        case Some(expected) =>
+          val reportedActual = if (exp.typ.isGround) {
+            exp.typ
+          } else {
+            exp.typ.substitute(selectAndGroundTypeSubstitution(exp, exp.typeSubstitutions))
+          }
+          messages ++= FastMessaging.message(exp, s"found incompatible type `${reportedActual.pretty}`, expected `${expected.pretty}`")
+        case None =>
+          typeError(exp)
       }
     }
   }
@@ -621,7 +602,7 @@ case class TypeChecker(names: NameAnalyser) {
       * Sets an error type for 'exp' to suppress further warnings.
       */
     def setErrorType(): Unit = {
-      setType(PUnknown()())
+      setType(PUnknown())
     }
 
     def getFreshTypeSubstitution(tvs: Seq[PDomainType]): PTypeRenaming =
@@ -636,13 +617,6 @@ case class TypeChecker(names: NameAnalyser) {
       new PTypeSubstitution(ts map (kv => rts.rename(kv._1) -> kv._2.substitute(rts)))
     }
 
-    def inAxiomScope(s: Option[PNode]): Boolean =
-      s match {
-        case Some(_: PAxiom) => true
-        case Some(x) => inAxiomScope(x.parent)
-        case None => false
-      }
-
     var extraReturnTypeConstraint: Option[PType] = None
 
     exp match {
@@ -664,7 +638,7 @@ case class TypeChecker(names: NameAnalyser) {
             if (resultAllowed)
               setType(curFunction.typ.resultType)
             else
-              issueError(r, "'result' can only be used in function postconditions")
+              issueError(r, "`result` can only be used in function postconditions")
           case _ =>
         }
 
@@ -673,6 +647,9 @@ case class TypeChecker(names: NameAnalyser) {
           poa.args.foreach(checkInternal)
           var nestedTypeError = !poa.args.forall(a => a.typ.isValidOrUndeclared)
           if (!nestedTypeError) {
+            // Check purity of arguments
+            poa.requirePure.foreach(a => if (!a.typ.isPure) issueError(a, "argument is not pure"))
+
             poa match {
               case pfa@PCall(func, _, explicitType) =>
                 explicitType match {
@@ -682,48 +659,60 @@ case class TypeChecker(names: NameAnalyser) {
                   case None =>
                 }
 
-                if (!nestedTypeError) {
-                  val ad = names.definition(curMember)(func)
-                  ad match {
-                    case Some(fd: PAnyFunction) =>
-                      func.decl = Some(fd)
-                      pfa.funcDecl = Some(fd)
-                      ensure(fd.formalArgs.length == pfa.args.length, pfa, "wrong number of arguments")
-                      fd match {
-                        case pfn: PFunction =>
-                          checkMember(fd) {
-                            check(fd.typ)
-                            fd.formalArgs foreach (a => check(a.typ))
-                          }
-                          if (inAxiomScope(Some(pfa)) && pfn.pres.length != 0)
-                            issueError(func, s"Cannot use function ${func.name}, which has preconditions, inside axiom")
-
-                        case pdf: PDomainFunction =>
-                          val domain = names.definition(curMember)(pdf.domainName).get.asInstanceOf[PDomain]
-                          val typVars = domain.typVarsSeq
-                          val fdtv = PTypeVar.freshTypeSubstitution((typVars map (tv => tv.idndef.name)).distinct) //fresh domain type variables
-                          pfa.domainTypeRenaming = Some(fdtv)
-                          pfa._extraLocalTypeVariables = (typVars map (tv => PTypeVar(tv.idndef.name))).toSet
-                          extraReturnTypeConstraint = explicitType.map(_._2)
-                        case _: PPredicate =>
-                      }
-                    case _ =>
-                      issueError(func, "expected function or predicate ")
+                // Resolve the function name to a function declaration
+                if (func.decls.nonEmpty) {
+                  func.filterDecls(_.isInstanceOf[PAnyFunction])
+                  if (func.decls.isEmpty)
+                    issueError(func, "expected function or predicate")
+                  else if (func.decls.length > 1) {
+                    issueError(func, "ambiguous function or predicate")
+                  }
+                }
+                if (func.decls.isEmpty)
+                  issueError(func, s"undeclared call `${func.name}`, expected function or predicate")
+                else if (func.filterDecls(_.isInstanceOf[PAnyFunction]))
+                  issueError(func, s"invalid method call `${func.name}` in expression position, expected function or predicate")
+                else if (func.decl.isEmpty)
+                  issueError(func, s"ambiguous call `${func.name}`")
+                else {
+                  val fd = func.decl.get.asInstanceOf[PAnyFunction]
+                  ensure(fd.formalArgs.length == pfa.args.length, pfa, "wrong number of arguments")
+                  if (!nestedTypeError) {
+                    extraReturnTypeConstraint = explicitType.map(_._2)
+                    fd match {
+                      case pfn: PFunction =>
+                        checkMember(fd) {
+                          check(fd.typ)
+                          fd.formalArgs foreach (a => check(a.typ))
+                        }
+                        if (pfa.isDescendant[PAxiom] && pfn.pres.length != 0)
+                          issueError(func, s"Cannot use function ${func.name}, which has preconditions, inside axiom")
+
+                      case pdf: PDomainFunction =>
+                        val domain = pdf.domain
+                        val typVars = domain.typVarsSeq
+                        val fdtv = PTypeVar.freshTypeSubstitution((typVars map (tv => tv.idndef.name)).distinct, Some(domain.idndef.name)) //fresh domain type variables
+                        pfa.domainTypeRenaming = Some(fdtv)
+                        pfa._extraLocalTypeVariables = (typVars map (tv => PTypeVar(tv.idndef.name))).toSet
+                      case _: PPredicate =>
+                        if (explicitType.isDefined)
+                          issueError(pfa, "predicate call cannot have an explicit type")
+                    }
                   }
                 }
 
               case pu: PUnfolding =>
-                if (!isCompatible(pu.acc.loc.typ, Bool)) {
-                  messages ++= FastMessaging.message(pu, "expected predicate access")
-                }
                 acceptNonAbstractPredicateAccess(pu.acc, "abstract predicates cannot be unfolded")
 
               case PApplying(_, wand, _, _) =>
                 checkMagicWand(wand)
 
               // We checked that the `rcv` is valid above with `poa.args.foreach(checkInternal)`
-              case PFieldAccess(_, _, idnuse) =>
-                acceptAndCheckTypedEntity[PFieldDecl, Nothing](Seq(idnuse), "expected field")
+              case PFieldAccess(_, _, idnref) =>
+                if (idnref.decls.isEmpty)
+                  issueError(idnref, s"undeclared field `${idnref.name}`")
+                else if (idnref.decl.isEmpty)
+                  issueError(idnref, s"ambiguous field `${idnref.name}`")
 
               case acc: PAccPred =>
                 acc.loc match {
@@ -742,6 +731,10 @@ case class TypeChecker(names: NameAnalyser) {
                 if (!pem.pValueType.isValidOrUndeclared)
                   check(pem.pValueType)
 
+              case _: PCurPerm =>
+                if (permBan.isDefined)
+                  issueError(poa, s"${permBan.get} are not allowed to contain `perm` expressions")
+
               case _ =>
             }
           }
@@ -754,21 +747,18 @@ case class TypeChecker(names: NameAnalyser) {
             if (rlts.nonEmpty && poa.args.forall(_.typeSubstitutions.nonEmpty) && !nestedTypeError) {
               val flat = poa.args.indices map (i => POpApp.pArg(i).substitute(ltr)) //fresh local argument types
               // the quadruples below are: (fresh argument type, argument type as used in domain of substitutions, substitutions, expression)
-              val argData = flat.indices.map(i => (flat(i), poa.args(i).typ, poa.args(i).typeSubstitutions.distinct.toSeq, poa.args(i))) ++
-                (
-                  extraReturnTypeConstraint match {
-                    case None => Nil
-                    case Some(t) => Seq((rrt, t, List(PTypeSubstitution.id), poa))
-                  }
-                  )
+              val argData = flat.indices.map(i => (poa.args(i).typ, flat(i), poa.args(i).typeSubsDistinct.toSeq, poa.args(i))) ++
+                (extraReturnTypeConstraint match {
+                  case None => Nil
+                  case Some(t) => Seq((t, rrt, List(PTypeSubstitution.id), poa))
+                })
               val unifiedSequence = unifySequenceWithSubstitutions(rlts, argData)
               if (unifiedSequence.isLeft && poa.typeSubstitutions.isEmpty) {
                 val problem = unifiedSequence.left.toOption.get
-                messages ++= FastMessaging.message(problem._3,
-                  s"Expected type ${problem._1.pretty}, but found ${problem._2.pretty} at the expression at ${problem._3.pos._1}.")
+                messages ++= FastMessaging.message(problem._3, s"found incompatible type `${problem._1.pretty}`, expected `${problem._2.pretty}`")
               } else {
                 poa.typeSubstitutions ++= unifiedSequence.toOption.get
-                val ts = poa.typeSubstitutions.distinct
+                val ts = poa.typeSubsDistinct
                 poa.typ = if (ts.size == 1) rrt.substitute(ts.head) else rrt
               }
             } else {
@@ -779,13 +769,18 @@ case class TypeChecker(names: NameAnalyser) {
                 poa.typeSubstitutions += rlts.find(_.contains(rrt)).get
                 poa.typ = ts.head
               } else
-                poa.typ = PUnknown()()
+                poa.typ = PUnknown()
             }
           }
         }
 
-      case piu: PIdnUse =>
-        acceptAndCheckTypedEntity[PAnyVarDecl, Nothing](Seq(piu), "expected variable identifier")
+      case piu: PIdnUseExp =>
+        if (piu.decls.isEmpty)
+          issueError(piu, s"undeclared identifier `${piu.name}`")
+        else if (piu.decl.isEmpty)
+          issueError(piu, s"ambiguous identifier `${piu.name}`")
+        else
+          piu.typ = piu.decl.get.typ
 
       case pl@PLet(_, _, _, e, _, ns) =>
         val oldCurMember = curMember
@@ -796,10 +791,15 @@ case class TypeChecker(names: NameAnalyser) {
         curMember = oldCurMember
 
       case pq: PForPerm =>
+        if (permBan.isDefined)
+          issueError(pq, s"${permBan.get} are not allowed to contain `forperm` expressions")
         val oldCurMember = curMember
         curMember = pq
         pq.boundVars foreach (v => check(v.typ))
+        val oldPermBan = permBan
+        permBan = Some("forperm quantifier bodies")
         check(pq.body, Bool)
+        permBan = oldPermBan
         checkInternal(pq.accessRes.inner)
         pq.triggers foreach (_.exp.inner.toSeq foreach (tpe => checkTopTyped(tpe, None)))
         pq._typeSubstitutions = pq.body.typeSubstitutions.toList.distinct
@@ -810,10 +810,11 @@ case class TypeChecker(names: NameAnalyser) {
         val oldCurMember = curMember
         curMember = pq
         pq.boundVars foreach (v => check(v.typ))
-        check(pq.body, Bool)
+        val expected = if (pq.isInstanceOf[PForall]) Impure else Bool
+        check(pq.body, expected)
         pq.triggers foreach (_.exp.inner.toSeq foreach (tpe => checkTopTyped(tpe, None)))
         pq._typeSubstitutions = pq.body.typeSubstitutions.toList.distinct
-        pq.typ = Bool
+        pq.typ = pq.body.typ
         curMember = oldCurMember
 
       case pne: PNewExp => issueError(pne, s"unexpected use of `new` as an expression")
@@ -831,8 +832,101 @@ case class TypeChecker(names: NameAnalyser) {
   }
 }
 
+case class DeclarationMap(
+  decls: mutable.HashMap[String, mutable.Buffer[PDeclaration]] = mutable.HashMap.empty,
+  unique: mutable.HashMap[String, (Boolean, PDeclaration)] = mutable.HashMap.empty,
+  refs: mutable.HashMap[String, mutable.Buffer[PIdnUseName[_]]] = mutable.HashMap.empty,
+  isMember: Boolean,
+  isGlobal: Boolean = false,
+) {
+  def checkUnique(decl: PDeclaration, canUnique: Boolean): Option[PDeclaration] = {
+    val name = decl.idndef.name
+    val uniq = unique.get(name)
+    val uniqGlobal = uniq.map(u => u._1 && u._2.isInstanceOf[PGlobalUniqueDeclaration]).getOrElse(false)
+    val uniqMember = uniqGlobal || uniq.map(u => u._1 && u._2.isInstanceOf[PMemberUniqueDeclaration]).getOrElse(false)
+    val uniqScope = uniqMember || uniq.map(u => u._1 && u._2.isInstanceOf[PScopeUniqueDeclaration]).getOrElse(false)
+    decl match {
+      case _: PGlobalUniqueDeclaration if canUnique => unique.update(name, (canUnique, decl))
+      case _: PMemberUniqueDeclaration if !uniqGlobal && canUnique => unique.update(name, (canUnique, decl))
+      case _: PScopeUniqueDeclaration if !uniqMember && canUnique => unique.update(name, (canUnique, decl))
+      case _ if uniqScope =>
+      case _ =>
+        // Neither is unique, use last seen
+        unique.update(name, (canUnique, decl))
+        return None
+    }
+    uniq.map(_._2)
+  }
+  def newDecl(decl: PDeclaration) = {
+    val name = decl.idndef.name
+    // Backward references
+    if (decl.isInstanceOf[PBackwardDeclaration])
+      refs.get(name).foreach(_.foreach(_.newDecl(decl)))
+    // Add to declaration map
+    val buf = decls.getOrElseUpdate(name, mutable.Buffer.empty)
+    if (decl.isInstanceOf[POverridesDeclaration])
+      buf.clear()
+    buf += decl
+  }
+
+  def merge(map: DeclarationMap): Seq[(PDeclaration, PDeclaration)] = {
+    // Add outer decls to inner refs
+    map.refs.flatMap(r => decls.get(r._1).map(_ -> r._2)).foreach {
+      case (ds, rs) => rs
+        .filter(_.decls.forall(!_.isInstanceOf[POverridesDeclaration]))
+        .foreach(_.prependDecls(ds.toSeq))
+    }
+    // Save inner decls and add them to outer refs
+    map.decls.values.foreach(_.foreach(d => 
+        if (!d.isInstanceOf[PLocalDeclaration] &&
+          !(d.isInstanceOf[PMemberDeclaration] && map.isMember) &&
+          !(d.isInstanceOf[PGlobalDeclaration] && map.isGlobal)
+        ) newDecl(d)
+    ))
+    // Save inner refs
+    map.refs.foreach { case (k, rs) => refs.getOrElseUpdate(k, mutable.Buffer.empty) ++= rs }
+    // Propagate inner unique declarations to outer.
+    // Cannot simply use `decls` since we could miss an inner local declaration clashing with an outer unique one (or even a `PLocalDeclaration` which is `PGlobalUniqueDeclaration`)
+    map.unique.values.flatMap { case (inScope, d) => {
+      val canUnique = (d.isInstanceOf[PGlobalUniqueDeclaration] && !map.isGlobal) || (d.isInstanceOf[PMemberUniqueDeclaration] && !map.isMember)
+      checkUnique(d, inScope && canUnique).map((d, _))
+    }}.toSeq
+  }
+
+  def newRef(idnuse: PIdnUseName[_]) = {
+    // assert(idnuse.decls.isEmpty, s"Encountered new `PIdnUseName` which wasn't new (${idnuse.name} at ${idnuse.pos._1}). This can happen when PAst nodes are not properly copied (e.g. with `deepCopyAll`) but instead alias.")
+    decls.get(idnuse.name).toSeq.flatten.foreach(idnuse.newDecl)
+    refs.getOrElseUpdate(idnuse.name, mutable.Buffer.empty) += idnuse
+  }
+
+  def clear() = {
+    decls.clear()
+    unique.clear()
+    refs.clear()
+  }
+
+  def keys = decls.keys
+}
+
 /**
-  * Resolves identifiers to their declaration.
+  * Resolves identifiers to their declaration. The important traits that relate to this are:
+  * - `PDeclaration` marks a declaration of an identifier.
+  * - `PIdnUseName` marks a use of an identifier (should be resolved).
+  * 
+  * - `PScope` marks a scope.
+  * - `PMember <: PScope` marks a member scope.
+  * - `PLocalDeclaration`: a declaration that is visible within the containing scope.
+  * - `PMemberDeclaration`: a declaration that is visible within the containing member.
+  * - `PGlobalDeclaration`: a declaration that is visible within the program.
+  * 
+  * - `PBackwardDeclaration`: a declaration that can be referenced before it is declared.
+  * - `POverridesDeclaration`: a declaration that overrides any other previously seen declarations.
+  * 
+  * - `PScopeUniqueDeclaration`: marks a declaration as unique within the scope.
+  * - `PMemberUniqueDeclaration`: marks a declaration as unique within the member.
+  * - `PGlobalUniqueDeclaration`: marks a declaration as unique within the program.
+  * 
+  * - `PNameAnalyserOpaque` marks a scope as opaque (should not be traversed by the name analyser).
   */
 case class NameAnalyser() {
 
@@ -840,60 +934,18 @@ case class NameAnalyser() {
   var messages: FastMessaging.Messages = Nil
   def success: Boolean = messages.isEmpty || messages.forall(m => !m.error)
 
-  /** Resolves the declaration to which the given identifier `idnuse` refers.
-    *
-    * If `member` is not null then the identifier will first be looked up in
-    * the scope defined by the member. If it fails (or if the member is null),
-    * the wider scope will be considered.
-    *
-    * In order to resolve name clashes, e.g., if the identifier is expected to
-    * refer to a field, but there is a local variable with the same name in the
-    * member scope that shadows the field, then the `expected` class can be
-    * provided (e.g., `PFields`), with the result that the shadowing local
-    * variable will be ignored because its class (`PVars`) doesn't
-    * match.
-    *
-    * @param member   Current scope in which to start the resolving.
-    * @param idnuse   Identifier that is to be resolved.
-    * @param expected Expected class of the entity.
-    * @return Resolved entity of expected type, or None if no entity of that type was found.
+  /** Resolves the global declaration to which the given identifier `name` refers.
     */
-  def definition(member: PScope)(idnuse: PIdnUse, expected: Option[Class[_]] = None): Option[PDeclaration] = {
-    if (member == null) {
-      globalDeclarationMap.get(idnuse.name)
-    } else {
-      // lookup in method map first, and otherwise in the general one
-      val entity =
-        localDeclarationMaps.get(member.scopeId).get.get(idnuse.name) match {
-          case None =>
-            globalDeclarationMap.get(idnuse.name)
-          case Some(foundEntity) =>
-            if (expected.isDefined && foundEntity.getClass != expected.get) {
-              val globalResult = globalDeclarationMap.get(idnuse.name)
-              if (globalResult.isDefined && globalResult.get.getClass == expected.get) {
-                globalResult
-              } else {
-                // error will reported by caller.
-                None
-              }
-            } else {
-              Some(foundEntity)
-            }
-        }
-
-      entity
-    }
+  def globalDefinitions(name: String): Seq[PDeclaration] = {
+    globalDeclarationMap.decls.getOrElse(name, Nil).toSeq
   }
 
   def reset(): Unit = {
     globalDeclarationMap.clear()
     localDeclarationMaps.clear()
-    universalDeclarationMap.clear()
     namesInScope.clear()
   }
-
-  private val globalDeclarationMap = mutable.HashMap[String, PDeclaration]()
-  private val universalDeclarationMap = mutable.HashMap[String, PDeclaration]()
+  private val globalDeclarationMap = DeclarationMap(isMember = false, isGlobal = true)
 
   /* [2014-11-13 Malte] Changed localDeclarationMaps to be a map from PScope.Id
    * instead of from PScope directly. This was necessary in order to support
@@ -903,88 +955,45 @@ case class NameAnalyser() {
    * localDeclarationMaps because such that the value stored for scope cannot
    * be retrieved anymore.
    */
-  private val localDeclarationMaps = mutable.HashMap[PScope.Id, mutable.HashMap[String, PDeclaration]]()
+  private val localDeclarationMaps = mutable.HashMap[PScope.Id, DeclarationMap]()
 
   private val namesInScope = mutable.Set.empty[String]
 
-  private def clearUniversalDeclarationsMap(): Unit = {
-    universalDeclarationMap.map { k =>
-      globalDeclarationMap.put(k._1, k._2)
-      localDeclarationMaps.map { l =>
-        l._2.put(k._1, k._2)
-      }
-    }
-  }
-
-  private def check(n: PNode, target: Option[PNode]): Unit = {
-    var curMember: PScope = null
-
-    def getMap(d: PNode): mutable.HashMap[String, PDeclaration] =
-      d match {
-        case _: PUniversalDeclaration => universalDeclarationMap
-        case _: PGlobalDeclaration => globalDeclarationMap
-        case _ => getCurrentMap
-      }
-
-    def getCurrentMap: mutable.HashMap[String, PDeclaration] =
-      if (curMember == null) globalDeclarationMap else localDeclarationMaps.get(curMember.scopeId).get
+  private def check(g: PNode, target: Option[PNode]): Unit = {
+    var curScope: PScope = null
+    def getMap(): DeclarationMap = Option(curScope).map(_.scopeId).map(localDeclarationMaps.get(_).get).getOrElse(globalDeclarationMap)
 
     val scopeStack = mutable.Stack[PScope]()
+    var opaque = 0
 
     val nodeDownNameCollectorVisitor = new PartialFunction[PNode, Unit] {
       def apply(n: PNode) = {
         if (n == target.orNull)
-          namesInScope ++= getCurrentMap.map(_._1)
+          namesInScope ++= getMap().keys
         n match {
+          // Opaque
+          case _: PNameAnalyserOpaque =>
+            opaque += 1
+          case _ if opaque > 0 =>
+          // Regular
           case d: PDeclaration =>
-            val map = getMap(d)
-            map.get(d.idndef.name) match {
-              case Some(m: PMember) if d eq m =>
-              // We re-encountered a member we already looked at in the previous run.
-              // This is expected, nothing to do.
-              case Some(e: PDeclaration) =>
-                messages ++= FastMessaging.message(d.idndef, "Duplicate identifier `" + e.idndef.name + "' at " + e.idndef.pos._1 + " and at " + d.idndef.pos._1)
-              case None =>
-                globalDeclarationMap.get(d.idndef.name) match {
-                  case Some(e: PDeclaration) =>
-                    if (!(d.parent.isDefined && d.parent.get.isInstanceOf[PDomainFunction]))
-                      messages ++= FastMessaging.message(d.idndef, "Identifier shadowing `" + e.idndef.name + "' at " + e.idndef.pos._1 + " and at " + d.idndef.pos._1)
-                  case None =>
-                }
-                map.put(d.idndef.name, d)
-            }
-          case i: PIdnUseName =>
-            if (i.decl.isEmpty) {
-              // look up in both maps (if we are not in a method currently, we look in the same map twice, but that is ok)
-              val resolved = getCurrentMap.get(i.name).orElse(globalDeclarationMap.get(i.name)).map(_.asInstanceOf[PDeclaration])
-              i.decl = resolved
-            }
-            (i.parent, i.decl) match {
-              case (Some(parent), None) =>
-                if (!parent.isInstanceOf[PDomainType] && !parent.isInstanceOf[PGoto] &&
-                  !(parent.isInstanceOf[POldExp] && parent.asInstanceOf[POldExp].label.map(_ == i).getOrElse(false)) &&
-                  !(i.name == LabelledOld.LhsOldLabel && parent.isInstanceOf[POldExp] && parent.asInstanceOf[POldExp].label.isDefined)) {
-                  messages ++= FastMessaging.message(i, s"identifier ${i.name} not defined.")
-                }
-              // domain types can also be type variables, which need not be declared
-              // goto and state labels may exist out of scope (but must exist in method, this is checked in final AST in checkIdentifiers)
-              case (None, _) =>
-              case _ =>
-            }
+            // Add to declaration map
+            val localDecls = getMap()
+            localDecls.newDecl(d)
+            val clashing = localDecls.checkUnique(d, true)
+            if (clashing.isDefined)
+              messages ++= FastMessaging.message(d.idndef, s"duplicate identifier `${d.idndef.name}` at ${d.idndef.pos._1} and at ${clashing.get.idndef.pos._1}")
+          case i: PIdnUseName[_] if target.isEmpty =>
+            getMap().newRef(i)
           case _ =>
         }
 
         n match {
+          case _ if opaque > 0 =>
           case s: PScope =>
-            val localDeclarations =
-              if (curMember == null)
-                mutable.HashMap[String, PDeclaration]()
-              else
-                localDeclarationMaps.getOrElse(curMember.scopeId, mutable.HashMap[String, PDeclaration]()).clone()
-
-            localDeclarationMaps.put(s.scopeId, localDeclarations)
-            scopeStack.push(curMember)
-            curMember = s
+            localDeclarationMaps.put(s.scopeId, DeclarationMap(isMember = s.isInstanceOf[PMember]))
+            scopeStack.push(curScope)
+            curScope = s
           case _ =>
         }
       }
@@ -993,7 +1002,8 @@ case class NameAnalyser() {
         n match {
           case _: PDeclaration => true
           case _: PScope => true
-          case _: PIdnUseName => true
+          case _: PIdnUseName[_] => true
+          case _: PNameAnalyserOpaque => true
           case _ => target.isDefined
         }
       }
@@ -1002,8 +1012,20 @@ case class NameAnalyser() {
     val nodeUpNameCollectorVisitor = new PartialFunction[PNode, Unit] {
       def apply(n: PNode) = {
         n match {
+          // Opaque
+          case _: PNameAnalyserOpaque =>
+            opaque -= 1
+          case _ if opaque > 0 =>
+          // Regular
           case _: PScope =>
-            curMember = scopeStack.pop()
+            val popMap = localDeclarationMaps.get(curScope.scopeId).get
+            val newScope = scopeStack.pop()
+            curScope = newScope
+
+            val clashing = getMap().merge(popMap)
+            clashing.foreach { case (clashing, unique) =>
+              messages ++= FastMessaging.message(clashing.idndef, s"duplicate identifier `${clashing.idndef.name}` at ${clashing.idndef.pos._1} and at ${unique.idndef.pos._1}")
+            }
           case _ =>
         }
       }
@@ -1011,48 +1033,14 @@ case class NameAnalyser() {
       def isDefinedAt(n: PNode) = {
         n match {
           case _: PScope => true
+          case _: PNameAnalyserOpaque => true
           case _ => false
         }
       }
     }
 
-    n match {
-      case prog: PProgram =>
-        // find all global names first
-        for (d <- prog.domains) {
-          nodeDownNameCollectorVisitor(d)
-          d.members.inner.funcs.toSeq.foreach(f => {
-            nodeDownNameCollectorVisitor(f);
-            nodeUpNameCollectorVisitor(f)
-          })
-          nodeUpNameCollectorVisitor(d)
-        }
-        prog.fields.foreach(f => f.visit(nodeDownNameCollectorVisitor, nodeUpNameCollectorVisitor))
-        prog.functions.foreach(f => {
-          nodeDownNameCollectorVisitor(f);
-          nodeUpNameCollectorVisitor(f)
-        })
-        prog.predicates.foreach(f => {
-          nodeDownNameCollectorVisitor(f);
-          nodeUpNameCollectorVisitor(f)
-        })
-        prog.methods.foreach(m => {
-          nodeDownNameCollectorVisitor(m);
-          nodeUpNameCollectorVisitor(m)
-        })
-        prog.extensions.foreach(e => e.visit(nodeDownNameCollectorVisitor, nodeUpNameCollectorVisitor))
-
-        // now completely walk through all axioms, functions, predicates, and methods
-        prog.domains.foreach(d => d.visit(nodeDownNameCollectorVisitor, nodeUpNameCollectorVisitor))
-        prog.functions.foreach(f => f.visit(nodeDownNameCollectorVisitor, nodeUpNameCollectorVisitor))
-        prog.predicates.foreach(f => f.visit(nodeDownNameCollectorVisitor, nodeUpNameCollectorVisitor))
-        prog.methods.foreach(m => m.visit(nodeDownNameCollectorVisitor, nodeUpNameCollectorVisitor))
-
-      case _ =>
-        // find all declarations
-        n.visit(nodeDownNameCollectorVisitor, nodeUpNameCollectorVisitor)
-    }
-    clearUniversalDeclarationsMap()
+    // find all declarations
+    g.visit(nodeDownNameCollectorVisitor, nodeUpNameCollectorVisitor)
   }
 
   def run(p: PProgram): Boolean = {
@@ -1062,6 +1050,6 @@ case class NameAnalyser() {
 
   def namesInScope(n: PNode, target: Option[PNode] = None): Set[String] = {
     check(n, target)
-    (namesInScope ++ globalDeclarationMap.map(_._1)).toSet
+    (namesInScope ++ globalDeclarationMap.keys).toSet
   }
 }
diff --git a/src/main/scala/viper/silver/parser/Transformer.scala b/src/main/scala/viper/silver/parser/Transformer.scala
deleted file mode 100644
index 2ed867530..000000000
--- a/src/main/scala/viper/silver/parser/Transformer.scala
+++ /dev/null
@@ -1,160 +0,0 @@
-// This Source Code Form is subject to the terms of the Mozilla Public
-// License, v. 2.0. If a copy of the MPL was not distributed with this
-// file, You can obtain one at http://mozilla.org/MPL/2.0/.
-//
-// Copyright (c) 2011-2019 ETH Zurich.
-
-package viper.silver.parser
-
-object Transformer {
-//   /* Attention: You most likely want to call initTree on the transformed node. */
-//   def transform[A <: PNode](node: A,
-//                             pre: PartialFunction[PNode, PNode] = PartialFunction.empty)(
-//                              recursive: PNode => Boolean = !pre.isDefinedAt(_),
-//                              post: PartialFunction[PNode, PNode] = PartialFunction.empty,
-//                              allowChangingNodeType: Boolean = false,
-//                              resultCheck: PartialFunction[(PNode, PNode), Unit] = PartialFunction.empty): A = {
-
-//     @inline
-//     def go[B <: PNode](root: B): B = {
-//       transform(root, pre)(recursive, post, allowChangingNodeType, resultCheck)
-//     }
-//     @inline
-//     def goPair[B <: PNode, C <: PNode](root: (B, C)): (B, C) = {
-//       (go(root._1), go(root._2))
-//     }
-
-//     def recurse(parent: PNode): PNode = {
-//       val newNode = parent match {
-//         case _: PIdnDef => parent
-//         case _: PIdnUse => parent
-//         case _: PKeyword => parent
-//         case _: POperator => parent
-//         case p@PFormalArgDecl(idndef, typ) => PFormalArgDecl(go(idndef), go(typ))(p.pos)
-//         case p@PFormalReturnDecl(idndef, typ) => PFormalReturnDecl(go(idndef), go(typ))(p.pos)
-//         case p@PLogicalVarDecl(idndef, typ) => PLogicalVarDecl(go(idndef), go(typ))(p.pos)
-//         case p@PLocalVarDecl(idndef, typ) => PLocalVarDecl(go(idndef), go(typ))(p.pos)
-//         case p@PFieldDecl(idndef, typ) => PFieldDecl(go(idndef), go(typ))(p.pos)
-//         case p@PTypeVarDecl(idndef) => PTypeVarDecl(go(idndef))(p.pos)
-//         case p@PPrimitiv(keyword) => PPrimitiv(go(keyword))(p.pos)
-//         case pdt@PDomainType(domain, args) =>
-//           val newPdt = PDomainType(go(domain), args map go)(pdt.pos)
-//           newPdt.kind = pdt.kind
-//           newPdt
-//         case p@PSeqType(seq, elementType) => PSeqType(go(seq), go(elementType))(p.pos)
-//         case p@PSetType(set, elementType) => PSetType(go(set), go(elementType))(p.pos)
-//         case p@PMultisetType(multiset, elementType) => PMultisetType(go(multiset), go(elementType))(p.pos)
-//         case p@PMapType(map, keyType, valueType) => PMapType(map, go(keyType), go(valueType))(p.pos)
-//         case _: PUnknown => parent
-//         case _: PWandType => parent
-//         case PFunctionType(argTypes, resultType) => PFunctionType(argTypes map go, go(resultType))
-//         case p@PMagicWandExp(left, op, right) => PMagicWandExp(go(left), go(op), go(right))(p.pos)
-//         case p@PBinExp(left, op, right) => PBinExp(go(left), go(op), go(right))(p.pos)
-//         case p@PUnExp(op, exp) => PUnExp(go(op), go(exp))(p.pos)
-//         case _: PIntLit => parent
-//         case p@PResultLit(result) => PResultLit(go(result))(p.pos)
-//         case p@PBoolLit(keyword, b) => PBoolLit(go(keyword), b)(p.pos)
-//         case p@PNullLit(nul) => PNullLit(go(nul))(p.pos)
-//         case p@PFieldAccess(rcv, dot, idnuse) => PFieldAccess(go(rcv), go(dot), go(idnuse))(p.pos)
-//         case p@PCall(func, l, args, r, explicitType) =>
-//           PCall(go(func), go(l), args map go, go(r), explicitType match {
-//             case Some(t) => Some(go(t))
-//             case None => None
-//           })(p.pos)
-
-
-//         case p@PUnfolding(unfolding, acc, in, exp) => PUnfolding(go(unfolding), go(acc), go(in), go(exp))(p.pos)
-//         case p@PApplying(applying, wand, in, exp) => PApplying(go(applying), go(wand), go(in), go(exp))(p.pos)
-
-//         case p@PExists(exists, vars, cs, triggers, exp) => PExists(go(exists), vars map go, go(cs), triggers map go, go(exp))(p.pos)
-//         case p@PForall(forall, vars, cs, triggers, exp) => PForall(go(forall), vars map go, go(cs), triggers map go, go(exp))(p.pos)
-//         case p@PTrigger(exp) => PTrigger(exp map go)(p.pos)
-//         case p@PForPerm(forperm, vars, res, cs, exp) => PForPerm(go(forperm), vars map go, go(res), go(cs), go(exp))(p.pos)
-//         case p@PCondExp(cond, q, thn, c, els) => PCondExp(go(cond), go(q), go(thn), go(c), go(els))(p.pos)
-//         case p@PInhaleExhaleExp(l, in, c, ex, r) => PInhaleExhaleExp(go(l), go(in), go(c), go(ex), go(r))(p.pos)
-//         case p@PCurPerm(k, l, loc, r) => PCurPerm(go(k), go(l), go(loc), go(r))(p.pos)
-//         case _: PNoPerm => parent
-//         case _: PFullPerm => parent
-//         case _: PWildcard => parent
-//         case _: PEpsilon => parent
-//         case p@PAccPred(acc, loc, perm) => PAccPred(go(acc), go(loc), go(perm))(p.pos)
-//         case p@POldExp(k, lbl, l, e, r) => POldExp(go(k), lbl map go, go(l), go(e), go(r))(p.pos)
-//         case p@PEmptySeq(k, t, l, r) => PEmptySeq(go(k), go(t), go(l), go(r))(p.pos)
-//         case p@PExplicitSeq(k, l, elems, r) => PExplicitSeq(go(k), go(l), elems map go, go(r))(p.pos)
-//         case p@PRangeSeq(l, low, ds, high, r) => PRangeSeq(go(l), go(low), go(ds), go(high), go(r))(p.pos)
-//         case p@PSeqSlice(seq, l, s, ds, e, r) => PSeqSlice(go(seq), go(l), s map go, go(ds), e map go, go(r))(p.pos)
-//         case p@PSize(seq) => PSize(go(seq))(p.pos)
-//         case p@PEmptySet(k, t, l, r) => PEmptySet(go(k), go(t), go(l), go(r))(p.pos)
-//         case p@PLookup(seq, l, idx, r) => PLookup(go(seq), go(l), go(idx), go(r))(p.pos)
-//         case p@PUpdate(seq, l, idx, a, elem, r) => PUpdate(go(seq), go(l), go(idx), go(a), go(elem), go(r))(p.pos)
-//         case p@PExplicitSet(k, l, elems, r) => PExplicitSet(go(k), go(l), elems map go, go(r))(p.pos)
-//         case p@PEmptyMultiset(k, t, l, r) => PEmptyMultiset(go(k), go(t), go(l), go(r))(p.pos)
-//         case p@PExplicitMultiset(k, l, elems, r) => PExplicitMultiset(go(k), go(l), elems map go, go(r))(p.pos)
-
-//         case p@PSeqn(ss) => PSeqn(ss map go)(p.pos)
-//         case p@PFold(fold, e) => PFold(go(fold), go(e))(p.pos)
-//         case p@PUnfold(unfold, e) => PUnfold(go(unfold), go(e))(p.pos)
-//         case p@PPackageWand(pckg, e, proofScript) => PPackageWand(go(pckg), go(e), go(proofScript))(p.pos)
-//         case p@PApplyWand(apply, e) => PApplyWand(go(apply), go(e))(p.pos)
-//         case p@PExhale(exhale, e) => PExhale(go(exhale), go(e))(p.pos)
-//         case p@PAssert(assert, e) => PAssert(go(assert), go(e))(p.pos)
-//         case p@PAssume(assume, e) => PAssume(go(assume), go(e))(p.pos)
-//         case p@PInhale(inhale, e) => PInhale(go(inhale), go(e))(p.pos)
-//         case p@PQuasihavoc(quasihavoc, lhs, e) =>
-//           PQuasihavoc(go(quasihavoc), lhs map goPair, go(e))(p.pos)
-//         case p@PQuasihavocall(quasihavocall, vars, cc, lhs, e) =>
-//           PQuasihavocall(go(quasihavocall), vars map go, go(cc), lhs map goPair, go(e))(p.pos)
-//         case p@PEmptyMap(k, keyType, valueType, l, r) => PEmptyMap(go(k), go(keyType), go(valueType), go(l), go(r))(p.pos)
-//         case p@PExplicitMap(k, l, exprs, r) => PExplicitMap(go(k), go(l), exprs map go, go(r))(p.pos)
-//         case p@PMaplet(key, value) => PMaplet(go(key), go(value))(p.pos)
-//         case p@PMapDomain(op, base) => PMapDomain(go(op), go(base))(p.pos)
-//         case p@PMapRange(op, base) => PMapRange(go(op), go(base))(p.pos)
-//         case p@PNewExp(k, fields) => PNewExp(go(k), fields map (_.map(go)))(p.pos)
-//         case p@PAssign(targets, op, rhs) => PAssign(targets map go, op map go, go(rhs))(p.pos)
-//         case p@PIf(keyword, cond, thn, elsKw, els) => PIf(go(keyword), go(cond), go(thn), elsKw map go, go(els))(p.pos)
-//         case p@PWhile(keyword, cond, invs, body) => PWhile(go(keyword), go(cond), invs map goPair, go(body))(p.pos)
-//         case p@PVars(keyword, vars, init) => PVars(go(keyword), vars map go, init map goPair)(p.pos)
-//         case p@PLabel(label, idndef, invs) => PLabel(go(label), go(idndef), invs map goPair)(p.pos)
-//         case p@PGoto(goto, target) => PGoto(go(goto), go(target))(p.pos)
-//         case p@PDefine(anns, define, idndef, optArgs, exp) => PDefine(anns map go, go(define), go(idndef), optArgs map (_ map go) , go(exp))(p.pos)
-//         case p@PLet(op, idndef, eq, exp, in, nestedScope) => PLet(go(op), go(idndef), go(eq), go(exp), go(in), go(nestedScope))(p.pos)
-//         case p@PLetNestedScope(body) => PLetNestedScope(go(body))(p.pos)
-//         case _: PSkip => parent
-
-//         case p@PProgram(files, macros, domains, fields, functions, predicates, methods, extensions, errors) => PProgram(files, macros map go, domains map go, fields map go, functions map go, predicates map go, methods map go, extensions map go, errors)(p.pos)
-//         case p@PImport(anns, imprt, local, file) => PImport(anns map go, go(imprt), local, go(file))(p.pos)
-//         case p@PMethod(anns, k, idndef, formalArgs, returns, formalReturns, pres, posts, body) => PMethod(anns map go, go(k), go(idndef), formalArgs map go, returns map go, formalReturns map go, pres map goPair, posts map goPair, body map go)(p.pos)
-//         case p@PDomain(anns, k, idndef, typVars, members, interp) => PDomain(anns map go, go(k), go(idndef), typVars map go, go(members), interp)(p.pos)
-//         case p@PDomainMembers(funcs, axioms) => PDomainMembers(funcs map go, axioms map go)(p.pos)
-//         case p@PFields(anns, k, fields) => PFields(anns map go, go(k), fields map go)(p.pos)
-//         case p@PFunction(anns, k, idndef, formalArgs, typ, pres, posts, body) => PFunction(anns map go, go(k), go(idndef), formalArgs map go, go(typ), pres map goPair, posts map goPair, body map go)(p.pos)
-//         case pdf@PDomainFunction(anns, unique, k, idndef, formalArgs, typ, interp) => PDomainFunction(anns map go, unique map go, go(k), go(idndef), formalArgs map go, go(typ), interp)(domainName = pdf.domainName)(pdf.pos)
-//         case p@PPredicate(anns, k, idndef, formalArgs, body) => PPredicate(anns map go, go(k), go(idndef), formalArgs map go, body map go)(p.pos)
-//         case pda@PAxiom(anns, k, idndef, exp) => PAxiom(anns map go, go(k), idndef map go, go(exp))(domainName = pda.domainName)(pda.pos)
-//         case p@PBlock(inner) => PBlock(go(inner))(p.pos)
-//         case pe:PExtender => pe.transformExtension(this)
-//       }
-
-//       if (!allowChangingNodeType)
-//         assert(newNode.getClass == parent.getClass, "Transformer is not expected to change type of nodes.")
-
-//       newNode
-//     }
-
-
-
-//     val beforeRecursion = pre.applyOrElse(node, identity[PNode])
-
-//     resultCheck.applyOrElse((node, beforeRecursion), identity[(PNode, PNode)])
-
-//     val afterRecursion = if (recursive(node)) {
-//       recurse(beforeRecursion)
-//     } else {
-//       beforeRecursion
-//     }
-//     post.applyOrElse(afterRecursion, identity[PNode]).asInstanceOf[A]
-//   }
-
-  case class ParseTreeDuplicationError(original: PNode, newChildren: Seq[Any])
-      extends RuntimeException(s"Cannot duplicate $original with new children $newChildren")
-}
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index 5a3ee4a60..5ef98bec4 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -30,7 +30,7 @@ case class Translator(program: PProgram) {
     // assert(TypeChecker.messagecount == 0, "Expected previous phases to succeed, but found error messages.") // AS: no longer sharing state with these phases
 
     program match {
-      case PProgram(_, _, pdomains, pfields, pfunctions, ppredicates, pmethods, pextensions, _) =>
+      case PProgram(_, _, pdomains, pfields, pfunctions, ppredicates, pmethods, pextensions) =>
 
         /* [2022-03-14 Alessandro] Domain signatures need no be translated first, since signatures of other declarations
          * like domain functions, and ordinary functions might depend on the domain signature. Especially this is the case
@@ -80,12 +80,7 @@ case class Translator(program: PProgram) {
     case PMethod(_, _, idndef, _, _, pres, posts, body) =>
       val m = findMethod(idndef)
 
-      val newBody = body.map(actualBody => {
-        val b = stmt(actualBody).asInstanceOf[Seqn]
-        val newScopedDecls = b.scopedSeqnDeclarations ++ b.deepCollect {case l: Label => l}
-
-        b.copy(scopedSeqnDeclarations = newScopedDecls)(b.pos, b.info, b.errT)
-      })
+      val newBody = body.map(actualBody => stmt(actualBody).asInstanceOf[Seqn])
 
       val finalMethod = m.copy(pres = pres.toSeq map (p => exp(p.e)), posts = posts.toSeq map (p => exp(p.e)), body = newBody)(m.pos, m.info, m.errT)
 
@@ -105,9 +100,9 @@ case class Translator(program: PProgram) {
 
   private def translate(a: PAxiom): DomainAxiom = a match {
     case pa@PAxiom(anns, _, Some(name), e) =>
-      NamedDomainAxiom(name.name, exp(e.e.inner))(a, Translator.toInfo(anns, pa), domainName = pa.domainName.name)
+      NamedDomainAxiom(name.name, exp(e.e.inner))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name)
     case pa@PAxiom(anns, _, None, e) =>
-      AnonymousDomainAxiom(exp(e.e.inner))(a, Translator.toInfo(anns, pa), domainName = pa.domainName.name)
+      AnonymousDomainAxiom(exp(e.e.inner))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name)
   }
 
   private def translate(f: PFunction): Function = f match {
@@ -148,7 +143,7 @@ case class Translator(program: PProgram) {
       case pf@PFunction(_, _, _, _, _, typ, _, _, _) =>
         Function(name, pf.formalArgs map liftArgDecl, ttyp(typ), null, null, null)(pos, Translator.toInfo(p.annotations, pf))
       case pdf@PDomainFunction(_, unique, _, _, _, _, typ, interp) =>
-        DomainFunc(name, pdf.formalArgs map liftAnyArgDecl, ttyp(typ), unique.isDefined, interp.map(_.i.grouped.inner))(pos, Translator.toInfo(p.annotations, pdf),pdf.domainName.name)
+        DomainFunc(name, pdf.formalArgs map liftAnyArgDecl, ttyp(typ), unique.isDefined, interp.map(_.i.grouped.inner))(pos, Translator.toInfo(p.annotations, pdf), pdf.domain.idndef.name)
       case pd@PDomain(_, _, _, typVars, interp, _) =>
         Domain(name, null, null, typVars map (_.inner.toSeq map (t => TypeVar(t.idndef.name))) getOrElse Nil, interp.map(_.interps))(pos, Translator.toInfo(p.annotations, pd))
       case pp: PPredicate =>
@@ -355,7 +350,7 @@ case class Translator(program: PProgram) {
     pexp match {
       case piu @ PIdnUseExp(name) =>
         piu.decl match {
-          case Some(_: PAnyVarDecl) => LocalVar(name, ttyp(pexp.typ))(pos, info)
+          case Some(_: PTypedVarDecl) => LocalVar(name, ttyp(pexp.typ))(pos, info)
           // A malformed AST where a field, function or other declaration is used as a variable.
           // Should have been caught by the type checker.
           case _ => sys.error("should not occur in type-checked program")
@@ -470,12 +465,8 @@ case class Translator(program: PProgram) {
         IntLit(i)(pos, info)
       case p@PResultLit(_) =>
         // find function
-        var par: PNode = p.parent.get
-        while (!par.isInstanceOf[PFunction]) {
-          if (par == null) sys.error("cannot use 'result' outside of function")
-          par = par.parent.get
-        }
-        Result(ttyp(par.asInstanceOf[PFunction].typ.resultType))(pos, info)
+        val func = p.getAncestor[PFunction].get
+        Result(ttyp(func.typ.resultType))(pos, info)
       case bool: PBoolLit =>
         if (bool.b) TrueLit()(pos, info) else FalseLit()(pos, info)
       case PNullLit(_) =>
@@ -552,7 +543,7 @@ case class Translator(program: PProgram) {
         }
       case POldExp(_, lbl, e) =>
         val ee = exp(e.inner)
-        lbl.map(l => LabelledOld(ee, l.inner.name)(pos, info)).getOrElse(Old(ee)(pos, info))
+        lbl.map(l => LabelledOld(ee, l.inner.fold(_.rs.keyword, _.name))(pos, info)).getOrElse(Old(ee)(pos, info))
       case PCondExp(cond, _, thn, _, els) =>
         CondExp(exp(cond), exp(thn), exp(els))(pos, info)
       case PCurPerm(_, res) =>
@@ -597,8 +588,8 @@ case class Translator(program: PProgram) {
 
       case PSeqSlice(seq, _, s, _, e, _) =>
         val es = exp(seq)
-        val ss = s.map(exp).map(SeqTake(es, _)(pos, info)).getOrElse(es)
-        e.map(exp).map(SeqDrop(ss, _)(pos, info)).getOrElse(ss)
+        val ss = e.map(exp).map(SeqTake(es, _)(pos, info)).getOrElse(es)
+        s.map(exp).map(SeqDrop(ss, _)(pos, info)).getOrElse(ss)
 
       case PUpdate(base, _, key, _, value, _) => base.typ match {
         case _: PSeqType => SeqUpdate(exp(base), exp(key), exp(value))(pos, info)
@@ -645,7 +636,8 @@ case class Translator(program: PProgram) {
   def liftAnyArgDecl(formal: PAnyFormalArgDecl) =
     formal match {
       case f: PFormalArgDecl => liftArgDecl(f)
-      case u: PUnnamedFormalArgDecl => UnnamedLocalVarDecl(ttyp(u.typ))(u.typ)
+      case PDomainFunctionArg(Some(idndef), _, typ) => LocalVarDecl(idndef.name, ttyp(typ))(idndef)
+      case PDomainFunctionArg(None, _, typ) => UnnamedLocalVarDecl(ttyp(typ))(typ)
     }
 
   /** Takes a `PFormalArgDecl` and turns it into a `LocalVarDecl`. */
@@ -696,7 +688,9 @@ case class Translator(program: PProgram) {
           assert(typ.typeArgs.isEmpty)
           TypeVar(name.name) // not a domain, i.e. it must be a type variable
       }
-    case PWandType() => Wand
+    case TypeHelper.Wand => Wand
+    case TypeHelper.Predicate => Bool
+    case TypeHelper.Impure => Bool
     case t: PExtender => t.translateType(this)
     case PUnknown() =>
       sys.error("unknown type unexpected here")
diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala
index 5824317df..1e8decf5a 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala
@@ -13,9 +13,8 @@ import viper.silver.parser._
 import viper.silver.plugin.standard.adt.PAdtConstructor.findAdtConstructor
 
 import scala.annotation.unused
-import scala.util.{Success, Try}
-// import viper.silver.ast.utility.lsp.GotoDefinition
 import viper.silver.ast.utility.lsp.SymbolKind
+import viper.silver.ast.utility.rewriter.HasExtraVars
 
 /**
   * Keywords used to define ADT's
@@ -32,32 +31,8 @@ case class PAdt(annotations: Seq[PAnnotation], adt: PReserved[PAdtKeyword.type],
   override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = {
     t.checkMember(this) {
       constructors foreach (_.typecheck(t, n))
+      derive foreach (_.typecheck(t, n))
     }
-    // Check that formalArg identifiers among all constructors are unique
-    val allFormalArgs = constructors flatMap (_.formalArgs collect { case fad: PFormalArgDecl => fad })
-    val duplicateArgs = allFormalArgs.groupBy(_.idndef.name).collect { case (_, ys) if ys.size > 1 => ys.tail }.toSeq
-    t.messages ++= duplicateArgs.flatMap { args => args.flatMap { arg =>
-      FastMessaging.message(arg.idndef, "Duplicate argument identifier `" + arg.idndef.name + "' among adt constructors at " + arg.idndef.pos._1)
-    }}
-
-    // Check validity blocklisted identifiers
-    derive.foreach(_.derivingInfos.inner.foreach { di =>
-      val diff = di.without.map(without => {
-        val possibleFields =  allFormalArgs.map(_.toIdnUse.name).toSet
-        without.blockList.toSeq.filterNot(blockedField => possibleFields(blockedField.name))
-      }).getOrElse(Nil)
-      if (diff.nonEmpty) {
-        t.messages ++= FastMessaging.message(diff.head, "Invalid identifier `" + diff.head.name + "' at " + diff.head.pos._1)
-      }
-    })
-    // Check duplicate deriving infos
-    val duplicateDerivingInfo = derive.toSeq.flatMap(_.derivingInfos.inner.groupBy(_.idnuse).collect { case (_, ys) if ys.size > 1 => ys.head })
-    t.messages ++= duplicateDerivingInfo.flatMap { di =>
-      FastMessaging.message(di.idnuse, "Duplicate derivation of function `" + di.idnuse.name + "' at " + di.idnuse.pos._1)
-    }
-
-    derive.foreach(_.typecheck(t, n))
-
     None
   }
 
@@ -69,7 +44,7 @@ case class PAdt(annotations: Seq[PAnnotation], adt: PReserved[PAdtKeyword.type],
       typVarsSeq map (t => TypeVar(t.idndef.name)),
       derive.toSeq.flatMap(_.derivingInfos.inner.map { a =>
         val without = a.without.toSet
-        (a.idnuse.name, (if (a.param.nonEmpty) Some(t.ttyp(a.param.get.inner)) else None, without.flatMap(_.blockList.toSeq.map(_.name))))
+        (a.idndef.name, (if (a.param.nonEmpty) Some(t.ttyp(a.param.get.inner)) else None, without.flatMap(_.blockList.toSeq.map(_.name))))
       }).toMap
     )(t.liftPos(this), Translator.toInfo(this.annotations, this))
   }
@@ -99,6 +74,7 @@ case class PAdt(annotations: Seq[PAnnotation], adt: PReserved[PAdtKeyword.type],
       typeVar.kind = PDomainTypeKinds.TypeVar
       typeVar
     })))(NoPosition, NoPosition)
+    adtType.adt.newDecl(this)
     adtType.kind = PAdtTypeKinds.Adt
     adtType
   }
@@ -110,20 +86,6 @@ case class PAdt(annotations: Seq[PAnnotation], adt: PReserved[PAdtKeyword.type],
     s"${adt.pretty}${idndef.pretty}$tvsPretty"
   }
   override def getFoldingRanges: Seq[FoldingRange] = RangePosition(this).map(FoldingRange(_)).toSeq
-  // override def withChildren(children: Seq[Any], pos: Option[(Position, Position)] = None, forceRewrite: Boolean = false): this.type = {
-  //   if (!forceRewrite && this.children == children && pos.isEmpty)
-  //     this
-  //   else {
-  //     assert(children.length == 6, s"PAdt : expected length 6 but got ${children.length}")
-  //     val first = children(0).asInstanceOf[Seq[PAnnotation]]
-  //     val second = children(1).asInstanceOf[PReserved[PAdtKeyword.type]]
-  //     val third = children(2).asInstanceOf[PIdnDef]
-  //     val fourth = children(3).asInstanceOf[Option[PDelimited.Comma[PSym.Bracket, PTypeVarDecl]]]
-  //     val fifth = children(4).asInstanceOf[PAdtSeq[PAdtConstructor]]
-  //     val sixth = children(5).asInstanceOf[Option[PAdtDeriving]]
-  //     PAdt(first, second, third, fourth, fifth, sixth)(pos.getOrElse(this.pos)).asInstanceOf[this.type]
-  //   }
-  // }
   override def completionScope: Map[SuggestionScope,Byte] = Map(TypeScope -> 0)
   override def completionKind: CompletionKind.CompletionKind = CompletionKind.Enum
   override def description: String = "Adt"
@@ -141,34 +103,42 @@ object PAdt {
 
 }
 
+trait PAdtChild extends PNode {
+  def adt: PAdt = getAncestor[PAdt].get
+}
+
 case class PAdtSeq[T <: PNode](seq: PGrouped[PSym.Brace, Seq[T]])(val pos: (Position, Position)) extends PExtender {
   def inner: Seq[T] = seq.inner
   override def pretty = s"${seq.l.pretty}\n  ${seq.inner.map(_.pretty).mkString("  \n")}\n${seq.r.pretty}"
 }
 
-case class PAdtConstructor(annotations: Seq[PAnnotation], idndef: PIdnDef, args: PDelimited.Comma[PSym.Paren, PFormalArgDecl])
-                          (var adt: PAdt)(val pos: (Position, Position)) extends PExtender with PSingleMember with PGlobalCallableNamedArgs with PPrettySubnodes with PLspAnyFunction {
-  def adtName: PIdnRef = PIdnRef(adt.idndef.name)(adt.idndef.pos)
+/** Any argument to a method, function or predicate. */
+case class PAdtFieldDecl(idndef: PIdnDef, c: PSym.Colon, typ: PType)(val pos: (Position, Position)) extends PAnyFormalArgDecl with PTypedDeclaration with PGlobalDeclaration with PMemberUniqueDeclaration with PAdtChild with PLspFormalArgDecl {
+  def constructor: PAdtConstructor = getAncestor[PAdtConstructor].get
+  def annotations: Seq[PAnnotation] = Nil
+}
+object PAdtFieldDecl {
+  def apply(d: PIdnTypeBinding): PAdtFieldDecl = PAdtFieldDecl(d.idndef, d.c, d.typ)(d.pos)
+}
+
+case class PAdtConstructor(annotations: Seq[PAnnotation], idndef: PIdnDef, args: PDelimited.Comma[PSym.Paren, PAdtFieldDecl])(val pos: (Position, Position)) extends PExtender with PAnyFunction with PGlobalUniqueDeclaration with PPrettySubnodes with PAdtChild with PLspAnyFunction {
+  def fieldDecls: Seq[PAdtFieldDecl] = this.args.inner.toSeq
   override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = {
     this.formalArgs foreach (a => t.check(a.typ))
-
     // Check if there are name clashes for the corresponding discriminator, if so we raise a type-check error
-    Try {
-      n.definition(t.curMember)(PIdnRef("is" + idndef.name)(idndef.pos))
-    } match {
-      case Success(Some(decl)) =>
-        t.messages ++= FastMessaging.message(idndef, "corresponding adt discriminator identifier `" + decl.idndef.name + "' at " + idndef.pos._1 + " is shadowed at " + decl.idndef.pos._1)
-      case _ =>
+    val discClashes = t.names.globalDefinitions("is" + idndef.name)
+    if (discClashes.nonEmpty) {
+      val decl = discClashes.head
+      t.messages ++= FastMessaging.message(idndef, "corresponding adt discriminator identifier `" + decl.idndef.name + "` at " + idndef.pos._1 + " is shadowed at " + decl.idndef.pos._1)
     }
     None
   }
 
   override def translateMemberSignature(t: Translator): AdtConstructor = {
-    val adt = PAdt.findAdt(adtName, t)
     AdtConstructor(
-      adt,
+      PAdt.findAdt(adt.idndef, t),
       idndef.name,
-      formalArgs map { arg => LocalVarDecl(arg.idndef.name, t.ttyp(arg.typ))(t.liftPos(arg.idndef)) }
+      formalArgs map (_.asInstanceOf[PAdtFieldDecl]) map { arg => LocalVarDecl(arg.idndef.name, t.ttyp(arg.typ))(t.liftPos(arg.idndef)) }
     )(t.liftPos(this), Translator.toInfo(annotations, this))
   }
 
@@ -176,18 +146,6 @@ case class PAdtConstructor(annotations: Seq[PAnnotation], idndef: PIdnDef, args:
     findAdtConstructor(idndef, t)
   }
 
-  override def withChildren(children: Seq[Any], pos: Option[(Position, Position)] = None, forceRewrite: Boolean = false): this.type = {
-    if (!forceRewrite && this.children == children && pos.isEmpty)
-      this
-    else {
-      assert(children.length == 3, s"PAdtConstructor : expected length 3 but got ${children.length}")
-      val first = children(0).asInstanceOf[Seq[PAnnotation]]
-      val second = children(1).asInstanceOf[PIdnDef]
-      val third = children(2).asInstanceOf[PDelimited.Comma[PSym.Paren, PFormalArgDecl]]
-      PAdtConstructor(first, second, third)(this.adt)(pos.getOrElse(this.pos)).asInstanceOf[this.type]
-    }
-  }
-
   override def c: PSym.Colon = PReserved.implied(PSym.Colon)
   override def resultType: PType = adt.getAdtType
 
@@ -219,27 +177,45 @@ object PAdtConstructor {
 }
 
 case class PAdtConstructors1(seq: PGrouped[PSym.Brace, Seq[PAdtConstructor1]])(val pos: (Position, Position))
-case class PAdtConstructor1(annotations: Seq[PAnnotation], idndef: PIdnDef, args: PDelimited.Comma[PSym.Paren, PFormalArgDecl], s: Option[PSym.Semi])(val pos: (Position, Position))
+case class PAdtConstructor1(annotations: Seq[PAnnotation], idndef: PIdnDef, args: PDelimited.Comma[PSym.Paren, PAdtFieldDecl], s: Option[PSym.Semi])(val pos: (Position, Position))
 
-case class PAdtDeriving(k: PReserved[PDerivesKeyword.type], derivingInfos: PAdtSeq[PAdtDerivingInfo])(val pos: (Position, Position)) extends PExtender with PPrettySubnodes {
+case class PAdtDeriving(k: PReserved[PDerivesKeyword.type], derivingInfos: PAdtSeq[PAdtDerivingInfo])(val pos: (Position, Position)) extends PExtender with PPrettySubnodes with PAdtChild {
   override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = {
-    derivingInfos.inner.foreach(_.typecheck(t, n))
+    derivingInfos.inner foreach (_.typecheck(t, n))
+
+    // Check duplicate deriving infos
+    val duplicateDerivingInfo = derivingInfos.inner.groupBy(_.idndef.name).collect { case (_, ys) if ys.size > 1 => ys.head }
+    t.messages ++= duplicateDerivingInfo.flatMap { di =>
+      FastMessaging.message(di.idndef, s"duplicate derivation of function `${di.idndef.name}`")
+    }
+
     None
   }
 }
 
-case class PAdtWithout(k: PReserved[PWithoutKeyword.type], blockList: PDelimited[PAdtFieldRef, PSym.Comma])(val pos: (Position, Position)) extends PExtender with PPrettySubnodes
+case class PAdtWithout(k: PReserved[PWithoutKeyword.type], blockList: PDelimited[PIdnRef[PAdtFieldDecl], PSym.Comma])(val pos: (Position, Position)) extends PExtender with PPrettySubnodes with PAdtChild {
+  override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = {
+    blockList.toSeq.foreach(idnref => {
+      if (idnref.filterDecls(_.constructor.adt.scopeId == adt.scopeId))
+        t.messages ++= FastMessaging.message(idnref, s"undeclared adt field `${idnref.name}`, expected field in containing adt")
+      else if (idnref.decl.isEmpty)
+        t.messages ++= FastMessaging.message(idnref, s"ambiguous adt field `${idnref.name}`")
+    })
+    None
+  }
+}
 
-case class PAdtDerivingInfo(idnuse: PIdnRef, param: Option[PGrouped[PSym.Bracket, PType]], without: Option[PAdtWithout])(val pos: (Position, Position)) extends PExtender with PPrettySubnodes {
+case class PAdtDerivingInfo(idndef: PIdnDef, param: Option[PGrouped[PSym.Bracket, PType]], without: Option[PAdtWithout])(val pos: (Position, Position)) extends PExtender with PPrettySubnodes {
 
   override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = {
-    param.map(_.inner).foreach(t.check)
+    param.map(_.inner) foreach (t.check)
+    without map (_.typecheck(t, n))
     None
   }
 }
 
-case class PAdtType(adt: PIdnRef, args: Option[PDelimited.Comma[PSym.Bracket, PType]])
-                   (val pos: (Position, Position)) extends PExtender with PGenericType with HasSemanticHighlights {
+case class PAdtType(adt: PIdnRef[PAdt], args: Option[PDelimited.Comma[PSym.Bracket, PType]])
+                   (val pos: (Position, Position)) extends PExtender with PGenericType with HasSemanticHighlights with HasExtraVars {
 
   var kind: PAdtTypeKinds.Kind = PAdtTypeKinds.Unresolved
 
@@ -273,19 +249,22 @@ case class PAdtType(adt: PIdnRef, args: Option[PDelimited.Comma[PSym.Bracket, PT
 
         typeArgs foreach t.check
 
-        var x: Any = null
-
-        try {
-          x = t.names.definition(t.curMember)(adt).get
-        } catch {
-          case _: Throwable =>
-        }
+        at.kind = PAdtTypeKinds.Undeclared
 
-        x match {
-          case PAdt(_, _, _, typVars, _, _) =>
-            t.ensure(args.map(_.inner.length) == typVars.map(_.inner.length), this, "wrong number of type arguments")
-            at.kind = PAdtTypeKinds.Adt
+        if (adt.decls.isEmpty)
+          Some(Seq(s"undeclared type `${at.adt.name}`, expected adt"))
+        else if (adt.decl.isEmpty)
+          Some(Seq(s"ambiguous adt type `${at.adt.name}`"))
+        else {
+          at.kind = PAdtTypeKinds.Adt
+          val x: PAdt = adt.decl.get.asInstanceOf[PAdt]
+          t.ensure(args.map(_.inner.length) == x.typVars.map(_.inner.length), this, "wrong number of type arguments")
             None
+            None
+          case _ =>
+            at.kind = PAdtTypeKinds.Undeclared
+            Option(Seq(s"found undeclared type ${at.adt.name}"))
+          None
           case _ =>
             at.kind = PAdtTypeKinds.Undeclared
             Option(Seq(s"found undeclared type ${at.adt.name}"))
@@ -310,6 +289,8 @@ case class PAdtType(adt: PIdnRef, args: Option[PDelimited.Comma[PSym.Bracket, PT
 
   override def getSemanticHighlights: Seq[SemanticHighlight] =
     RangePosition(adt).map(sp => SemanticHighlight(sp, TokenType.Enum)).toSeq
+
+  override def copyExtraVars(from: Any): Unit = this.kind = from.asInstanceOf[PAdtType].kind
 }
 
 object PAdtTypeKinds {
@@ -325,7 +306,6 @@ object PAdtTypeKinds {
 /** Common trait for ADT operator applications * */
 sealed trait PAdtOpApp extends PExtender with POpApp {
   // Following fields are set during resolving, respectively in the typecheck method below
-  var adt: PAdt = null
   var adtTypeRenaming: Option[PTypeRenaming] = None
   var adtSubstitution: Option[PTypeSubstitution] = None
   var _extraLocalTypeVariables: Set[PDomainType] = Set()
@@ -338,7 +318,6 @@ sealed trait PAdtOpApp extends PExtender with POpApp {
   }
 
   override def forceSubstitution(ots: PTypeSubstitution): Unit = {
-
     val ts = adtTypeRenaming match {
       case Some(dtr) =>
         val s3 = PTypeSubstitution(dtr.mm.map(kv => kv._1 -> (ots.get(kv._2) match {
@@ -381,105 +360,121 @@ object PAdtOpApp {
     if (poa.typeSubstitutions.isEmpty) {
       poa.args.foreach(t.checkInternal)
       var nestedTypeError = !poa.args.forall(a => a.typ.isValidOrUndeclared)
-      if (!nestedTypeError) {
-        poa match {
-          case pcc@PConstructorCall(constr, _, typeAnnotated) =>
-            typeAnnotated match {
-              case Some((_, ta)) =>
-                t.check(ta)
-                if (!ta.isValidOrUndeclared) nestedTypeError = true
-              case None =>
-            }
-
-            if (!nestedTypeError) {
-              val ac = t.names.definition(t.curMember)(constr).get.asInstanceOf[PAdtConstructor]
-              pcc.constructor = ac
-              t.ensure(ac.formalArgs.size == pcc.args.size, pcc, "wrong number of arguments")
-              val adt = t.names.definition(t.curMember)(ac.adtName).get.asInstanceOf[PAdt]
-              pcc.adt = adt
-              val fdtv = PTypeVar.freshTypeSubstitution((adt.typVarsSeq map (tv => tv.idndef.name)).distinct) //fresh domain type variables
-              pcc.adtTypeRenaming = Some(fdtv)
-              pcc._extraLocalTypeVariables = (adt.typVarsSeq map (tv => PTypeVar(tv.idndef.name))).toSet
-              extraReturnTypeConstraint = pcc.typeAnnotated.map(_._2)
-            }
-
-          case pdc@PDestructorCall(_, _, name) =>
-            pdc.args.head.typ match {
-              case at: PAdtType =>
-                val adt = t.names.definition(t.curMember)(at.adt).get.asInstanceOf[PAdt]
-                pdc.adt = adt
-                val matchingConstructorArgs: Seq[PFormalArgDecl] = adt.constructors flatMap (c => c.formalArgs.collect { case fad@PFormalArgDecl(idndef, _, _) if idndef.name == name.name => fad })
-                if (matchingConstructorArgs.nonEmpty) {
-                  pdc.matchingConstructorArg = matchingConstructorArgs.head
-                  name.decl = Some(matchingConstructorArgs.head)
+      poa match {
+        case pcc@PConstructorCall(_, _, typeAnnotated) =>
+          if (pcc.idnref.decls.isEmpty) {
+            nestedTypeError = true
+            t.messages ++= FastMessaging.message(pcc.idnref, s"undefined adt constructor `${pcc.idnref.name}`")
+          }
+          typeAnnotated match {
+            case Some((_, ta)) =>
+              t.check(ta)
+              if (!ta.isValidOrUndeclared) nestedTypeError = true
+              if (!nestedTypeError) {
+                val adtName = ta.asInstanceOf[PAdtType].adt.name
+                if (pcc.idnref.filterDecls(_.adt.idndef.name == adtName)) {
+                  nestedTypeError = true
+                  t.messages ++= FastMessaging.message(pcc.idnref, s"undefined constructor `${pcc.idnref.name}` in adt `$adtName`")
+                } else if (pcc.idnref.decls.length > 1) {
+                  nestedTypeError = true
+                  t.messages ++= FastMessaging.message(pcc.idnref, s"ambiguous adt constructor `${pcc.idnref.name}` in adt `$adtName`")
+                }
+              }
+            case None =>
+              if (pcc.idnref.decls.length > 1) {
+                nestedTypeError = true
+                t.messages ++= FastMessaging.message(pcc.idnref, s"ambiguous adt constructor `${pcc.idnref.name}`")
+              }
+          }
+          if (!nestedTypeError) {
+            val ac = pcc.constructor.get
+            t.ensure(ac.formalArgs.size == pcc.args.size, pcc, "wrong number of arguments")
+            val adt = ac.adt
+            val fdtv = PTypeVar.freshTypeSubstitution((adt.typVarsSeq map (tv => tv.idndef.name)).distinct) //fresh domain type variables
+            pcc.adtTypeRenaming = Some(fdtv)
+            pcc._extraLocalTypeVariables = (adt.typVarsSeq map (tv => PTypeVar(tv.idndef.name))).toSet
+            extraReturnTypeConstraint = pcc.typeAnnotated.map(_._2)
+          }
+
+        case pdc@PDestructorCall(rcv, _, name) =>
+          rcv.typ match {
+            case at: PAdtType =>
+              // Otherwise error already reported by `PAdtType.typecheck`
+              if (!nestedTypeError && at.adt.decl.isDefined) {
+                val adt = at.adt.decl.get.asInstanceOf[PAdt]
+                if (name.filterDecls(_.constructor.adt.idndef.name == adt.idndef.name)) {
+                  nestedTypeError = true
+                  t.messages ++= FastMessaging.message(pdc, s"undefined adt field `${name.name}` when destructing, in adt `${adt.idndef.name}`")
+                } else if (name.decl.isEmpty) {
+                  nestedTypeError = true
+                  t.messages ++= FastMessaging.message(pdc, s"ambiguous adt field `${name.name}` when destructing, in adt `${adt.idndef.name}`")
+                } else {
                   val fdtv = PTypeVar.freshTypeSubstitution((adt.typVarsSeq map (tv => tv.idndef.name)).distinct) //fresh domain type variables
                   pdc.adtTypeRenaming = Some(fdtv)
                   pdc._extraLocalTypeVariables = (adt.typVarsSeq map (tv => PTypeVar(tv.idndef.name))).toSet
-                } else {
-                  nestedTypeError = true
-                  t.messages ++= FastMessaging.message(pdc, "no matching destructor found")
                 }
-              case _ =>
-                nestedTypeError = true
-                t.messages ++= FastMessaging.message(pdc, "expected an adt as receiver")
-            }
+              }
+            case typ =>
+              nestedTypeError = true
+              t.messages ++= FastMessaging.message(pdc, s"found incompatible receiver type `${typ.pretty}` when destructing adt field `${name.name}`, expected an adt")
+          }
+
+        case pdc@PDiscriminatorCall(_, _, is, name) =>
+          if (name.decls.isEmpty) {
+            nestedTypeError = true
+            t.messages ++= FastMessaging.message(pdc, s"undefined adt constructor `${name.name}` when checking `${is.pretty}${name.name}`")
+          } else if (name.decl.isEmpty) {
+            nestedTypeError = true
+            t.messages ++= FastMessaging.message(pdc, s"ambiguous adt constructor `${name.name}` when checking `${is.pretty}${name.name}`")
+          } else if (!nestedTypeError) {
+            val ac = name.decl.get.asInstanceOf[PAdtConstructor]
+            val adt = ac.adt
+            val fdtv = PTypeVar.freshTypeSubstitution((adt.typVarsSeq map (tv => tv.idndef.name)).distinct) //fresh domain type variables
+            pdc.adtTypeRenaming = Some(fdtv)
+            pdc._extraLocalTypeVariables = (adt.typVarsSeq map (tv => PTypeVar(tv.idndef.name))).toSet
+          }
+
+        case _ => sys.error("PAdtOpApp#typecheck: unexpectable type")
+      }
 
-          case pdc@PDiscriminatorCall(_, _, _, name) =>
-            t.names.definition(t.curMember)(name) match {
-              case Some(ac: PAdtConstructor) =>
-                val adt = t.names.definition(t.curMember)(ac.adtName).get.asInstanceOf[PAdt]
-                pdc.adt = adt
-                val fdtv = PTypeVar.freshTypeSubstitution((adt.typVarsSeq map (tv => tv.idndef.name)).distinct) //fresh domain type variables
-                pdc.adtTypeRenaming = Some(fdtv)
-                pdc._extraLocalTypeVariables = (adt.typVarsSeq map (tv => PTypeVar(tv.idndef.name))).toSet
-              case _ =>
-                nestedTypeError = true
-                t.messages ++= FastMessaging.message(pdc, "invalid adt discriminator")
+      if (!nestedTypeError && poa.signatures.nonEmpty && poa.args.forall(_.typeSubstitutions.nonEmpty)) {
+        val ltr = getFreshTypeSubstitution(poa.localScope.toList) //local type renaming - fresh versions
+        val rlts = poa.signatures map (ts => refreshWith(ts, ltr)) //local substitutions refreshed
+        assert(rlts.nonEmpty)
+        val rrt: PDomainType = POpApp.pRes.substitute(ltr).asInstanceOf[PDomainType] // return type (which is a dummy type variable) replaced with fresh type
+        val flat = poa.args.indices map (i => POpApp.pArg(i).substitute(ltr)) //fresh local argument types
+        // the tuples below are: (fresh argument type, argument type as used in domain of substitutions, substitutions, the argument itself)
+        poa.typeSubstitutions ++= t.unifySequenceWithSubstitutions(rlts, flat.indices.map(i => (poa.args(i).typ, flat(i), poa.args(i).typeSubsDistinct.toSeq, poa.args(i))) ++
+          (
+            extraReturnTypeConstraint match {
+              case None => Nil
+              case Some(t) => Seq((t, rrt, List(PTypeSubstitution.id), poa))
             }
-
-          case _ => sys.error("PAdtOpApp#typecheck: unexpectable type")
-        }
-
-        if (poa.signatures.nonEmpty && poa.args.forall(_.typeSubstitutions.nonEmpty) && !nestedTypeError) {
-          val ltr = getFreshTypeSubstitution(poa.localScope.toList) //local type renaming - fresh versions
-          val rlts = poa.signatures map (ts => refreshWith(ts, ltr)) //local substitutions refreshed
-          assert(rlts.nonEmpty)
-          val rrt: PDomainType = POpApp.pRes.substitute(ltr).asInstanceOf[PDomainType] // return type (which is a dummy type variable) replaced with fresh type
-          val flat = poa.args.indices map (i => POpApp.pArg(i).substitute(ltr)) //fresh local argument types
-          // the tuples below are: (fresh argument type, argument type as used in domain of substitutions, substitutions, the argument itself)
-          poa.typeSubstitutions ++= t.unifySequenceWithSubstitutions(rlts, flat.indices.map(i => (flat(i), poa.args(i).typ, poa.args(i).typeSubstitutions.distinct.toSeq, poa.args(i))) ++
-            (
-              extraReturnTypeConstraint match {
-                case None => Nil
-                case Some(t) => Seq((rrt, t, List(PTypeSubstitution.id), poa))
-              }
-              )
-          ).getOrElse(Seq())
-          val ts = poa.typeSubstitutions.distinct
-          if (ts.isEmpty)
-            t.typeError(poa)
-          poa.typ = if (ts.size == 1) rrt.substitute(ts.head) else rrt
-        } else {
-          poa.typeSubstitutions.clear()
-          poa.typ = PUnknown()()
-        }
+            )
+        ).getOrElse(Seq())
+        val ts = poa.typeSubsDistinct
+        if (ts.isEmpty)
+          t.typeError(poa)
+        poa.typ = if (ts.size == 1) rrt.substitute(ts.head) else rrt
+      } else {
+        poa.typeSubstitutions.clear()
+        poa.typ = PUnknown()
       }
     }
     None
   }
 }
 
-case class PConstructorCall(idnref: PIdnRef, callArgs: PDelimited.Comma[PSym.Paren, PExp], typeAnnotated: Option[(PSym.Colon, PType)])
+case class PConstructorCall(idnref: PIdnRef[PAdtConstructor], callArgs: PDelimited.Comma[PSym.Paren, PExp], typeAnnotated: Option[(PSym.Colon, PType)])
                            (val pos: (Position, Position) = (NoPosition, NoPosition)) extends PAdtOpApp with PCallLike with PLocationAccess with HasSemanticHighlights with PLspCall {
-  // Following field is set during resolving, respectively in the typecheck method inherited from PAdtOpApp
-  var constructor: PAdtConstructor = null
-
+  def constructor: Option[PAdtConstructor] = idnref.decl.filter(_.isInstanceOf[PAdtConstructor]).map(_.asInstanceOf[PAdtConstructor])
+  def adt: Option[PAdt] = constructor.map(_.adt)
   override def signatures: List[PTypeSubstitution] = {
-    if (adt != null && constructor != null && constructor.formalArgs.size == args.size) {
+    if (adt.isDefined && constructor.get.formalArgs.size == args.size) {
       List(
         new PTypeSubstitution(
-          args.indices.map(i => POpApp.pArg(i).domain.name -> constructor.formalArgs(i).typ.substitute(adtTypeRenaming.get)) :+
-            (POpApp.pRes.domain.name -> adt.getAdtType.substitute(adtTypeRenaming.get)))
+          args.indices.map(i => POpApp.pArg(i).domain.name -> constructor.get.formalArgs(i).typ.substitute(adtTypeRenaming.get)) :+
+            (POpApp.pRes.domain.name -> adt.get.getAdtType.substitute(adtTypeRenaming.get)))
       )
     } else List()
   }
@@ -504,24 +499,17 @@ case class PConstructorCall(idnref: PIdnRef, callArgs: PDelimited.Comma[PSym.Par
     RangePosition(idnref).map(sp => SemanticHighlight(sp, TokenType.EnumMember)).toSeq
 }
 
-// Cannot reuse `PIdnRef` because it implements `PIdnUseName` but the name analyser doesn't work for field references.
-case class PAdtFieldRef(name: String)(val pos: (Position, Position)) extends PIdnUse with PLspIdnUse {
-  override def rename(newName: String) = PIdnRef(newName)(pos)
-}
-
-case class PDestructorCall(rcv: PExp, dot: PReserved[PDiscDot.type], idnref: PAdtFieldRef)
+case class PDestructorCall(rcv: PExp, dot: PReserved[PDiscDot.type], idnref: PIdnRef[PAdtFieldDecl])
                           (val pos: (Position, Position) = (NoPosition, NoPosition)) extends PAdtOpApp with HasSemanticHighlights with PLspExpRef {
-  // Following field is set during resolving, respectively in the typecheck method inherited from PAdtOpApp
-  var matchingConstructorArg: PFormalArgDecl = null
+  def field: Option[PAdtFieldDecl] = idnref.decl.filter(_.isInstanceOf[PAdtFieldDecl]).map(_.asInstanceOf[PAdtFieldDecl])
+  def adt: Option[PAdt] = field.map(_.constructor.adt)
 
-  // override def opName: String = name.name
-
-  override def signatures: List[PTypeSubstitution] = if (adt != null && matchingConstructorArg != null) {
+  override def signatures: List[PTypeSubstitution] = if (adt.isDefined && adtTypeRenaming.isDefined) {
     assert(args.length == 1, s"PDestructorCall: Expected args to be of length 1 but was of length ${args.length}")
     List(
       new PTypeSubstitution(
-        args.indices.map(i => POpApp.pArg(i).domain.name -> adt.getAdtType.substitute(adtTypeRenaming.get)) :+
-          (POpApp.pRes.domain.name -> matchingConstructorArg.typ.substitute(adtTypeRenaming.get)))
+        args.indices.map(i => POpApp.pArg(i).domain.name -> adt.get.getAdtType.substitute(adtTypeRenaming.get)) :+
+          (POpApp.pRes.domain.name -> field.get.typ.substitute(adtTypeRenaming.get)))
     )
   } else List()
 
@@ -535,7 +523,7 @@ case class PDestructorCall(rcv: PExp, dot: PReserved[PDiscDot.type], idnref: PAd
     }
     so match {
       case Some(s) =>
-        val adt = t.getMembers()(this.adt.idndef.name).asInstanceOf[Adt]
+        val adt = t.getMembers()(this.adt.get.idndef.name).asInstanceOf[Adt]
         assert(s.keys.toSet == adt.typVars.toSet)
         AdtDestructorApp(adt, idnref.name, actualRcv, s)(t.liftPos(this))
       case _ => sys.error("type unification error - should report and not crash")
@@ -551,15 +539,15 @@ case object PIsKeyword extends PKwOp("is") {
 }
 case object PDiscDot extends PSym(".") with PSymbolOp
 
-case class PDiscriminatorCall(rcv: PExp, dot: PReserved[PDiscDot.type], is: PReserved[PIsKeyword.type], idnref: PIdnRef)
+case class PDiscriminatorCall(rcv: PExp, dot: PReserved[PDiscDot.type], is: PReserved[PIsKeyword.type], idnref: PIdnRef[PAdtConstructor])
                              (val pos: (Position, Position) = (NoPosition, NoPosition)) extends PAdtOpApp with HasSemanticHighlights with PLspExpRef {
-  // override def opName: String = "is" + name.name
-
-  override def signatures: List[PTypeSubstitution] = if (adt != null) {
+  def constructor: Option[PAdtConstructor] = idnref.decl.filter(_.isInstanceOf[PAdtConstructor]).map(_.asInstanceOf[PAdtConstructor])
+  def adt: Option[PAdt] = constructor.map(_.adt)
+  override def signatures: List[PTypeSubstitution] = if (adt.isDefined) {
     assert(args.length == 1, s"PDiscriminatorCall: Expected args to be of length 1 but was of length ${args.length}")
     List(
       new PTypeSubstitution(
-        args.indices.map(i => POpApp.pArg(i).domain.name -> adt.getAdtType.substitute(adtTypeRenaming.get)) :+
+        args.indices.map(i => POpApp.pArg(i).domain.name -> adt.get.getAdtType.substitute(adtTypeRenaming.get)) :+
           (POpApp.pRes.domain.name -> TypeHelper.Bool))
     )
   } else List()
@@ -574,7 +562,7 @@ case class PDiscriminatorCall(rcv: PExp, dot: PReserved[PDiscDot.type], is: PRes
     }
     so match {
       case Some(s) =>
-        val adt = t.getMembers()(this.adt.idndef.name).asInstanceOf[Adt]
+        val adt = t.getMembers()(this.adt.get.idndef.name).asInstanceOf[Adt]
         assert(s.keys.toSet == adt.typVars.toSet)
         AdtDiscriminatorApp(adt, idnref.name, actualRcv, s)(t.liftPos(this))
       case _ => sys.error("type unification error - should report and not crash")
diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
index 25dd30f2d..78f38695f 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
@@ -20,7 +20,7 @@ class AdtPlugin(@unused reporter: viper.silver.reporter.Reporter,
                 config: viper.silver.frontend.SilFrontendConfig,
                 fp: FastParser) extends SilverPlugin with ParserPluginTemplate {
 
-  import fp.{annotation, argList, formalArg, idndef, idnref, typ, typeList, domainTypeVarDecl, ParserExtension, lineCol, _file}
+  import fp.{annotation, argList, idnTypeBinding, idndef, idnref, typ, typeList, domainTypeVarDecl, ParserExtension, lineCol, _file}
   import FastParserCompanion.{ExtendedParsing, LeadingWhitespace, PositionParsing, reservedKw, reservedSym, whitespace}
 
   /**
@@ -71,27 +71,25 @@ class AdtPlugin(@unused reporter: viper.silver.reporter.Reporter,
     P(P(PAdtKeyword) ~ idndef ~ typeList(domainTypeVarDecl).? ~ adtConstructorDecl.rep.braces.map(PAdtConstructors1.apply _).pos ~~~ adtDerivesDecl.lw.?).map {
       case (k, name, typparams, c, dec) =>
         ap: PAnnotationsPosition => {
-          val adt = PAdt(
+          PAdt(
             ap.annotations,
             k,
             name,
             typparams,
-            PAdtSeq(c.seq.update(c.seq.inner map (c => PAdtConstructor(c.annotations, c.idndef, c.args)(null)(c.pos))))(c.pos),
+            PAdtSeq(c.seq.update(c.seq.inner map (c => PAdtConstructor(c.annotations, c.idndef, c.args)(c.pos))))(c.pos),
             dec,
           )(ap.pos)
-          adt.c.seq.inner.toSeq.foreach(_.adt = adt)
-          adt
         }
     }
 
   def adtDerivesDecl[$: P] = P((P(PDerivesKeyword) ~ adtDerivingDeclBody.rep.braces.map(PAdtSeq.apply _).pos) map (PAdtDeriving.apply _).tupled).pos
 
-  def adtWithout[$: P]: P[PAdtWithout] = P((P(PWithoutKeyword) ~ idnref.map(i => PAdtFieldRef(i.name)(i.pos)).delimited(PSym.Comma, min = 1)) map (PAdtWithout.apply _).tupled).pos
+  def adtWithout[$: P]: P[PAdtWithout] = P((P(PWithoutKeyword) ~ idnref[$, PAdtFieldDecl].delimited(PSym.Comma, min = 1)) map (PAdtWithout.apply _).tupled).pos
 
   def adtDerivingDeclBody[$: P]: P[PAdtDerivingInfo] =
-    P((idnref ~~~ typ.brackets.lw.? ~~~ adtWithout.lw.?) map ((PAdtDerivingInfo.apply _).tupled)).pos
+    P((idndef ~~~ typ.brackets.lw.? ~~~ adtWithout.lw.?) map ((PAdtDerivingInfo.apply _).tupled)).pos
 
-  def adtConstructorDecl[$: P]: P[PAdtConstructor1] = P((annotation.rep ~ idndef ~ argList(formalArg) ~~~ P(PSym.Semi).lw.?) map (PAdtConstructor1.apply _).tupled).pos
+  def adtConstructorDecl[$: P]: P[PAdtConstructor1] = P((annotation.rep ~ idndef ~ argList(idnTypeBinding.map(PAdtFieldDecl(_))) ~~~ P(PSym.Semi).lw.?) map (PAdtConstructor1.apply _).tupled).pos
 
   override def beforeResolve(input: PProgram): PProgram = {
     if (deactivated) {
@@ -102,21 +100,22 @@ class AdtPlugin(@unused reporter: viper.silver.reporter.Reporter,
     val declaredAdtNames = input.extensions.collect { case a: PAdt => a.idndef.name }.toSet
     val declaredConstructorNames = input.extensions.collect { case a: PAdt => a.constructors.map(c => c.idndef) }.flatten.toSet
     val declaredConstructorArgsNames = input.extensions.collect { case a: PAdt =>
-      a.constructors flatMap (c => c.formalArgs collect { case PFormalArgDecl(idndef, _, _) => idndef.name })
+      a.constructors flatMap (_.fieldDecls map (_.idndef.name))
     }.flatten.toSet
 
     def transformStrategy[T <: PNode](input: T): T = StrategyBuilder.Slim[PNode]({
       // If derives import is missing deriving info is ignored
       case pa@PAdt(anns, adt, idndef, typVars, constructors, _) if !derivesImported => PAdt(anns, adt, idndef, typVars, constructors, None)(pa.pos)
-      case pa@PDomainType(idnuse, args) if declaredAdtNames.contains(idnuse.name) => PAdtType(idnuse, args)(pa.pos)
-      case pc@PCall(idnuse, args, typeAnnotated) if declaredConstructorNames.exists(_.name == idnuse.name) => PConstructorCall(idnuse, args, typeAnnotated)(pc.pos)
+      case pa@PDomainType(idnuse, args) if declaredAdtNames.contains(idnuse.name) => PAdtType(idnuse.retype(), args)(pa.pos)
+      case pc@PCall(idnuse, args, typeAnnotated) if declaredConstructorNames.exists(_.name == idnuse.name) => PConstructorCall(idnuse.retype(), args, typeAnnotated)(pc.pos)
       // A destructor call or discriminator call might be parsed as left-hand side of a field assignment, which is illegal. Hence in this case
       // we simply treat the calls as an ordinary field access, which results in an identifier not found error.
       case pfa@PAssign(PDelimited(fieldAcc: PFieldAccess), op, rhs) if declaredConstructorArgsNames.contains(fieldAcc.idnref.name) ||
         declaredConstructorNames.exists("is" + _.name == fieldAcc.idnref.name) =>
         PAssign(pfa.targets.update(Seq(fieldAcc.copy(rcv = transformStrategy(fieldAcc.rcv))(fieldAcc.pos))), op, transformStrategy(rhs))(pfa.pos)
-      case pfa@PFieldAccess(rcv, dot, idnuse) if declaredConstructorArgsNames.contains(idnuse.name) => PDestructorCall(rcv, PReserved(PDiscDot)(dot.pos), PAdtFieldRef(idnuse.name)(idnuse.pos))(pfa.pos)
-      case pfa@PFieldAccess(rcv, dot, idnuse) if declaredConstructorNames.exists("is" + _.name == idnuse.name) => {
+      case pfa@PFieldAccess(rcv, dot, idnuse) if declaredConstructorArgsNames.contains(idnuse.name) =>
+        PDestructorCall(rcv, PReserved(PDiscDot)(dot.pos), idnuse.retype())(pfa.pos)
+      case pfa@PFieldAccess(rcv, dot, idnuse) if idnuse.decls.forall(!_.isInstanceOf[PFieldDecl]) && declaredConstructorNames.exists("is" + _.name == idnuse.name) => {
         val middlePos = idnuse.pos._1.deltaColumn(2)
         PDiscriminatorCall(rcv, PReserved(PDiscDot)(dot.pos), PReserved(PIsKeyword)(idnuse.pos._1, middlePos), PIdnRef(idnuse.name.substring(2))(middlePos, idnuse.pos._2))(pfa.pos)
       }
diff --git a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePASTExtension.scala
index 7b45056bd..eea61fb61 100644
--- a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePASTExtension.scala
+++ b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePASTExtension.scala
@@ -18,7 +18,7 @@ case object PPredicateInstanceKeyword extends PKw("PredicateInstance") with PKey
  */
 case object PMarkerSymbol extends PSym("#") with PSymbolLang
 
-case class PPredicateInstance(m: PReserved[PMarkerSymbol.type], idnuse: PIdnRef, args: PDelimited.Comma[PSym.Paren, PExp])(val pos: (Position, Position)) extends PExtender with PExp {
+case class PPredicateInstance(m: PReserved[PMarkerSymbol.type], idnuse: PIdnRef[PPredicate], args: PDelimited.Comma[PSym.Paren, PExp])(val pos: (Position, Position)) extends PExtender with PExp {
 
   typ = PPrimitiv(PReserved(PPredicateInstanceKeyword)(NoPosition, NoPosition))(NoPosition, NoPosition)
 
@@ -28,16 +28,16 @@ case class PPredicateInstance(m: PReserved[PMarkerSymbol.type], idnuse: PIdnRef,
   override def forceSubstitution(ts: PTypeSubstitution): Unit = {}
 
   override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = {
-    // TODO: Don't know if this is correct
-    // check that idnuse is the id of a predicate
-    n.definition(member = null)(idnuse) match {
-      case Some(p: PPredicate) =>
-        // type checking should be the same as for PPredicateAccess nodes
-        val predicateAccess = PCall(idnuse, args, None)(p.pos)
-        predicateAccess.funcDecl = Some(p)
-        t.checkInternal(predicateAccess)
-        None
-      case _ => Some(Seq("expected predicate"))
+    if (idnuse.decls.isEmpty)
+      // Already reported by name analyser
+      return None
+    if (idnuse.decls.size > 1)
+      Some(Seq("predicate instance is ambiguous"))
+    else {
+      // type checking should be the same as for PPredicateAccess nodes
+      val predicateAccess = PCall(idnuse.retype(), args, None)(pos)
+      t.checkInternal(predicateAccess)
+      None
     }
   }
 
diff --git a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
index b9c6a53e6..b8816e3b0 100644
--- a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
@@ -32,7 +32,7 @@ class PredicateInstancePlugin(@unused reporter: viper.silver.reporter.Reporter,
    *
    */
   def predicateInstance[$: P]: P[PPredicateInstance] = P((P(PMarkerSymbol) ~ predAcc).map {
-    case (m, p) => PPredicateInstance(m, p.idnref, p.callArgs)(_)
+    case (m, p) => PPredicateInstance(m, p.idnref.retype(), p.callArgs)(_)
   }).pos
 
   /** Called before any processing happened.
diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
index 611760813..ea3bae391 100644
--- a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
@@ -59,7 +59,7 @@ class RefutePlugin(@unused reporter: viper.silver.reporter.Reporter,
             Seq(nonDetLocalVarDecl)
           )(r.pos)
       }).recurseFunc({
-        case Method(_, _, _, _, _, body) => Seq(body)
+        case method: Method => Seq(method.body)
       }).execute[Method](method)
     })
     Program(input.domains, input.fields, input.functions, input.predicates, transformedMethods, input.extensions)(input.pos, input.info, input.errT)
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
index b10b75e03..4afe109b4 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -78,9 +78,9 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
     val transformPredicateInstances = StrategyBuilder.Slim[PNode]({
       case pc@PCall(idnUse, args, None) if input.predicates.exists(_.idndef.name == idnUse.name) =>
         // PCall represents the predicate access before the translation into the AST
-        PPredicateInstance(PReserved.implied(PMarkerSymbol), idnUse, args)(pc.pos)
+        PPredicateInstance(PReserved.implied(PMarkerSymbol), idnUse.retype(), args)(pc.pos)
       case PAccPred(_, PGrouped(_, PMaybePairArgument(pc@PCall(idnUse, args, None), _), _)) if input.predicates.exists(_.idndef.name == idnUse.name) =>
-        PPredicateInstance(PReserved.implied(PMarkerSymbol), idnUse, args)(pc.pos)
+        PPredicateInstance(PReserved.implied(PMarkerSymbol), idnUse.retype(), args)(pc.pos)
       case d => d
     }).recurseFunc({
       case PUnfolding(_, _, _, exp) => // ignore predicate access when it is used for unfolding
@@ -95,18 +95,18 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
     // Apply the predicate access to instance transformation only to decreases clauses.
     val newProgram: PProgram = StrategyBuilder.Slim[PNode]({
       case dt: PDecreasesTuple =>
-        decreasesClauses = decreasesClauses :+ dt
-        transformPredicateInstances.execute(dt): PDecreasesTuple
+        val transformedDt = transformPredicateInstances.execute(dt): PDecreasesTuple
+        decreasesClauses = decreasesClauses :+ transformedDt
+        transformedDt
       case dc : PDecreasesClause =>
         decreasesClauses = decreasesClauses :+ dc
         dc
       case d => d
     }).recurseFunc({ // decreases clauses can only appear in functions/methods pres, posts and methods bodies
-      case PProgram(_, _, _, _, functions, _, methods, _, _) => Seq(functions, methods)
+      case PProgram(_, _, _, _, functions, _, methods, _) => Seq(functions, methods)
       case PFunction(_, _, _, _, _, _, pres, posts, _) => Seq(pres, posts)
       case PMethod(_, _, _, _, _, pres, posts, body) => Seq(pres, posts, body)
     }).execute(input)
-
     newProgram
   }
 
@@ -118,7 +118,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
       if (!(c.idnref.name == "decreases" || c.idnref.name == "bounded"))
         return false
       c.funcDecl match {
-        case Some(df: PDomainFunction) => df.domainName.name == "WellFoundedOrder"
+        case Some(df: PDomainFunction) => df.domain.idndef.name == "WellFoundedOrder"
         case _ => false
       }
     }
@@ -155,14 +155,13 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
       return input
 
     var usesPredicate = false
-    val allClauseTypes: Set[Any] = decreasesClauses.flatMap{
-      case PDecreasesTuple(Seq(), _) => Nil
-      case PDecreasesTuple(exps, _) => exps.toSeq.map(e => e.typ match {
-        case PUnknown() if e.isInstanceOf[PCall] =>
-          usesPredicate = usesPredicate || e.asInstanceOf[PCall].funcDecl.map(_.isInstanceOf[PPredicate]).getOrElse(false)
-          Nil
-        case _ => e.typ
-      })
+    val allClauseTypes: Set[PType] = decreasesClauses.flatMap {
+      case PDecreasesTuple(exps, _) => exps.toSeq.flatMap(_ match {
+          case _: PPredicateInstance =>
+            usesPredicate = true
+            None
+          case e => Some(e.typ)
+        })
       case _ => Seq()
     }.toSet
     val presentDomains = input.domains.map(_.idndef.name).toSet
@@ -196,7 +195,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
       val importPProgram = PAstProvider.generateViperPAst(importOnlyProgram)
       val mergedDomains = input.domains.filter(_.idndef.name != "WellFoundedOrder") ++ importPProgram.get.domains
 
-      val mergedProgram = input.copy(domains = mergedDomains)(input.pos)
+      val mergedProgram = input.copy(domains = mergedDomains)(input.pos, input.errors)
       super.beforeTranslate(mergedProgram)
     } else {
       super.beforeTranslate(input)
@@ -359,7 +358,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
       }
   }).recurseFunc({
     case Program(_, _, functions, _, methods, _) => Seq(functions, methods)
-    case Method(_, _, _, _, _, body) => Seq(body)
+    case method: Method => Seq(method.body)
   })
 
   /**
diff --git a/src/test/resources/all/basic/syntax.vpr b/src/test/resources/all/basic/syntax.vpr
index 3e749dc7a..b6a865ab3 100644
--- a/src/test/resources/all/basic/syntax.vpr
+++ b/src/test/resources/all/basic/syntax.vpr
@@ -36,9 +36,10 @@ method m(this : Ref)
     y := df(this.g)
 }
 
-  //:: ExpectedOutput(typechecker.error)
+//:: ExpectedOutput(typechecker.error)
 method m54(this:Ref)  returns (this:Ref)
 {    
+    //:: ExpectedOutput(typechecker.error)
     this := this
 }
 
diff --git a/src/test/resources/all/issues/carbon/0364.vpr b/src/test/resources/all/issues/carbon/0364.vpr
index 9a5eb7fdb..5ddbc256c 100644
--- a/src/test/resources/all/issues/carbon/0364.vpr
+++ b/src/test/resources/all/issues/carbon/0364.vpr
@@ -6,12 +6,12 @@ field val: Int
 define wandA(a) acc(a.val) --* acc(a.val)
 
 function reqA(a: Ref): Int
-  //:: ExpectedOutput(consistency.error)
+  //:: ExpectedOutput(typechecker.error)
   requires wandA(a)
 
 predicate predA(a: Ref)
 {
-  //:: ExpectedOutput(consistency.error)
+  //:: ExpectedOutput(typechecker.error)
   wandA(a)
 }
 
diff --git a/src/test/resources/all/issues/silicon/0291.vpr b/src/test/resources/all/issues/silicon/0291.vpr
index 480b9e763..8a5c9f1f6 100644
--- a/src/test/resources/all/issues/silicon/0291.vpr
+++ b/src/test/resources/all/issues/silicon/0291.vpr
@@ -5,8 +5,8 @@ field f : Int
 field g : Int
 
 function f1(x: Ref) : Int
-  //:: ExpectedOutput(consistency.error)
+  //:: ExpectedOutput(typechecker.error)
   requires(perm(x.f) == perm(x.g))
-  //:: ExpectedOutput(consistency.error)
+  //:: ExpectedOutput(typechecker.error)
   ensures(forperm r: Ref [r.f] :: false)
 { 2 }
diff --git a/src/test/resources/all/issues/silver/0039.vpr b/src/test/resources/all/issues/silver/0039.vpr
index 346b0ba9b..27f0d3fe2 100644
--- a/src/test/resources/all/issues/silver/0039.vpr
+++ b/src/test/resources/all/issues/silver/0039.vpr
@@ -20,15 +20,15 @@ method m(this:Ref,b1:Bool)
     assert acc(this.f)
     assert acc(old(this).f)
     assert acc(old(this.f).f)
-//:: ExpectedOutput(consistency.error)
+//:: ExpectedOutput(typechecker.error)
     assert old(acc(this.f))
 
     var b : Bool
     b := fun(this,b)
- //:: ExpectedOutput(consistency.error)
+ //:: ExpectedOutput(typechecker.error)
    b := fun(this,acc(this.f))
-//:: ExpectedOutput(consistency.error)
+//:: ExpectedOutput(typechecker.error)
     assert df(acc(this.f))>0
-//:: ExpectedOutput(consistency.error)
+//:: ExpectedOutput(typechecker.error)
     m(this,acc(this.f))
 }
diff --git a/src/test/resources/all/issues/silver/0069.vpr b/src/test/resources/all/issues/silver/0069.vpr
index f9d8e92f4..d1f489f90 100644
--- a/src/test/resources/all/issues/silver/0069.vpr
+++ b/src/test/resources/all/issues/silver/0069.vpr
@@ -5,7 +5,7 @@ field f : Int
 
 function g(x:Ref) : Int
   requires acc(x.f,write)
-  //:: ExpectedOutput(consistency.error)
+  //:: ExpectedOutput(typechecker.error)
   ensures acc(x.f,write)
 { 0 }
 
@@ -19,7 +19,7 @@ field val:Ref
 
 function f1(x:Ref):Int
   requires acc(x.val) && 1==1
-  //:: ExpectedOutput(consistency.error)
+  //:: ExpectedOutput(typechecker.error)
   ensures acc(x.val) && 2==3
 
 predicate P(x: Ref) { true }
@@ -29,12 +29,12 @@ function f2(x: Ref): Int
   ensures unfolding acc(P(x), 1/2) in true
 
 function f3(x: Ref): Int
-  //:: ExpectedOutput(consistency.error)
+  //:: ExpectedOutput(typechecker.error)
   requires true --* true
-  //:: ExpectedOutput(consistency.error)
+  //:: ExpectedOutput(typechecker.error)
   ensures true --* true
 
 function f4(x: Ref): Int
-  //:: ExpectedOutput(consistency.error)
+  //:: ExpectedOutput(typechecker.error)
   requires true --* true
   ensures applying (true --* true) in true
diff --git a/src/test/resources/all/issues/silver/0106-1.vpr b/src/test/resources/all/issues/silver/0106-1.vpr
index ce5dd7a5a..19986d0f5 100644
--- a/src/test/resources/all/issues/silver/0106-1.vpr
+++ b/src/test/resources/all/issues/silver/0106-1.vpr
@@ -5,21 +5,21 @@ field f: Int
 field g: Int
 
 method m1(x: Ref)
-  //:: ExpectedOutput(consistency.error)
+  //:: ExpectedOutput(typechecker.error)
   requires perm(x.f) == perm(x.g)
   //this is fine because perm occurs in inhale/exhale
   requires [perm(x.f) > perm(x.g), true]
 {}
 
 function f1(x: Ref): Bool
-  //:: ExpectedOutput(consistency.error)
+  //:: ExpectedOutput(typechecker.error)
   requires forperm r: Ref [r.f] :: true
   //this is fine because perm occurs in inhale/exhale
   requires [forperm r: Ref [r.f] :: true, true]
 
 method invariant_test(x: Ref) {
   while (true)
-    //:: ExpectedOutput(consistency.error)
+    //:: ExpectedOutput(typechecker.error)
     invariant perm(x.f) == perm(x.g)
     //this is fine because perm occurs in inhale/exhale
     invariant [perm(x.f) > perm(x.g), true]
diff --git a/src/test/resources/all/issues/silver/0120.vpr b/src/test/resources/all/issues/silver/0120.vpr
index 84509a98c..dc2b8b162 100644
--- a/src/test/resources/all/issues/silver/0120.vpr
+++ b/src/test/resources/all/issues/silver/0120.vpr
@@ -7,13 +7,13 @@ predicate p(r: Ref) {true}
 
 method m(c: Ref, b: Bool)
 {
-    //:: ExpectedOutput(consistency.error)
+    //:: ExpectedOutput(typechecker.error)
 	assert forperm r: Ref [r.f] :: acc(r.f, 1/2)
 }
 
 method m2(c: Ref, b: Bool)
 {
-    //:: ExpectedOutput(consistency.error)
+    //:: ExpectedOutput(typechecker.error)
 	assert forperm r: Ref [r.f] :: acc(p(r), 1/2)
 }
 
diff --git a/src/test/resources/all/issues/silver/0164.vpr b/src/test/resources/all/issues/silver/0164.vpr
index 2e48df016..ebb71dc1f 100644
--- a/src/test/resources/all/issues/silver/0164.vpr
+++ b/src/test/resources/all/issues/silver/0164.vpr
@@ -7,6 +7,6 @@ method ff ()
 {
     var r : Ref;
     var b : Bool;
-    //:: ExpectedOutput(consistency.error)
+    //:: ExpectedOutput(typechecker.error)
     b := (4 == 4 ? acc(r.f, write) : 4 == 4)
 }
\ No newline at end of file
diff --git a/src/test/resources/all/issues/silver/0175b.vpr b/src/test/resources/all/issues/silver/0175b.vpr
index 0767ac4e9..e2115aae1 100644
--- a/src/test/resources/all/issues/silver/0175b.vpr
+++ b/src/test/resources/all/issues/silver/0175b.vpr
@@ -4,6 +4,6 @@
 field f: Int
 
 method test(xs: Set[Ref], ys: Seq[Ref])
-  //:: ExpectedOutput(consistency.error)
+  //:: ExpectedOutput(typechecker.error)
   requires forall x: Ref :: ((x in xs) && (forall i: Int :: i in [0..|ys|) ==> acc(ys[i].f))) ==> acc(x.f)
 {}
\ No newline at end of file
diff --git a/src/test/resources/all/issues/silver/0469.vpr b/src/test/resources/all/issues/silver/0469.vpr
index 888b2e609..1d0d6c615 100644
--- a/src/test/resources/all/issues/silver/0469.vpr
+++ b/src/test/resources/all/issues/silver/0469.vpr
@@ -6,6 +6,6 @@ field b: Bool
 method t(l: Seq[Int], x: Ref, cond: Bool)
   requires |l| == 3 && forall i: Int :: (0 <= i && i < |l|) ==> l[i] == 4
 {
-  //:: ExpectedOutput(consistency.error)
+  //:: ExpectedOutput(typechecker.error)
   assert l[(acc(x.b) && x.b) ? 1 : 2] == 4;
 }
diff --git a/src/test/resources/all/issues/silver/0697.vpr b/src/test/resources/all/issues/silver/0697.vpr
index a1db01682..82eead36d 100644
--- a/src/test/resources/all/issues/silver/0697.vpr
+++ b/src/test/resources/all/issues/silver/0697.vpr
@@ -19,14 +19,14 @@ method main1(b: Bool)
 method main2(b: Bool)
 {
     if (b) {
-        //:: ExpectedOutput(consistency.error)
         var x: Int
         x := 45
         assert x > 34
     }
 
-      var x: Int
-      x := 45
-      assert x > 34
+    //:: ExpectedOutput(typechecker.error)
+    var x: Int
+    x := 45
+    assert x > 34
 
 }
\ No newline at end of file
diff --git a/src/test/resources/all/issues/silver/0720.vpr b/src/test/resources/all/issues/silver/0720.vpr
index 8402a5973..78012d204 100644
--- a/src/test/resources/all/issues/silver/0720.vpr
+++ b/src/test/resources/all/issues/silver/0720.vpr
@@ -4,6 +4,6 @@
 predicate p(flag: Bool)
 
 method client() {
-    //:: ExpectedOutput(consistency.error)
+    //:: ExpectedOutput(typechecker.error)
     inhale p(p(false))
 }
diff --git a/src/test/resources/all/parsing/assign_ambig.vpr b/src/test/resources/all/parsing/assign_ambig.vpr
new file mode 100644
index 000000000..f4ae6ebb5
--- /dev/null
+++ b/src/test/resources/all/parsing/assign_ambig.vpr
@@ -0,0 +1,7 @@
+field f: Bool
+method bar(a: Bool, b: Seq[Ref])
+    requires |b| > 0 && acc(b[0].f)
+{
+  assume a
+  (b[..1][0]).f := a
+}
diff --git a/src/test/resources/all/parsing/typed_call_ambig2.vpr b/src/test/resources/all/parsing/typed_call_ambig2.vpr
index c54bfd926..ff8873555 100644
--- a/src/test/resources/all/parsing/typed_call_ambig2.vpr
+++ b/src/test/resources/all/parsing/typed_call_ambig2.vpr
@@ -1,3 +1,5 @@
+//:: IgnoreFile(/Carbon/issue/488/)
+
 domain huh {
     function myfun(b: Bool): Bool
 }
diff --git a/src/test/resources/all/permission_introspection/forpermCheck.vpr b/src/test/resources/all/permission_introspection/forpermCheck.vpr
index 2ef01d6a6..42af00310 100644
--- a/src/test/resources/all/permission_introspection/forpermCheck.vpr
+++ b/src/test/resources/all/permission_introspection/forpermCheck.vpr
@@ -4,25 +4,25 @@
 field f1: Int
 
 function permInPost(x: Ref): Int
-  //:: ExpectedOutput(consistency.error)
+  //:: ExpectedOutput(typechecker.error)
   ensures [perm(x.f1) == none, true]
 
 method permUse()
 {
   var r1: Ref
-  //:: ExpectedOutput(consistency.error)
+  //:: ExpectedOutput(typechecker.error)
   assert forperm r: Ref [r.f1] :: perm(r.f1) > none
 }
 
 method nestedForperm() {
     var x: Ref
-    //:: ExpectedOutput(consistency.error)
+    //:: ExpectedOutput(typechecker.error)
     assert forperm r: Ref [r.f1] :: (forperm r1: Ref [r1.f1] :: true)
 }
 
 method nonPureBody() {
     var x: Ref
-    //:: ExpectedOutput(consistency.error)
+    //:: ExpectedOutput(typechecker.error)
     assert forperm r: Ref [r.f1] :: p(r)
 }
 
diff --git a/src/test/resources/wands/regression/consistency.vpr b/src/test/resources/wands/regression/consistency.vpr
index 22c03de4e..abf5f4cb9 100644
--- a/src/test/resources/wands/regression/consistency.vpr
+++ b/src/test/resources/wands/regression/consistency.vpr
@@ -48,22 +48,6 @@ method test03() {
   assert unfolding Pair(p) in acc(Pair(p))
 }
 
-
-/* Applying/packaging must occur inside wands */
-
-function foobar(x: Ref): Int
-  //:: ExpectedOutput(consistency.error)
-  requires true --* acc(x.f)
-{
-  applying (true --* acc(x.f)) in x.f
-}
-
-predicate test18(x: Ref) {
-  //:: ExpectedOutput(consistency.error)
-  acc(x.f) && (acc(x.f) --* acc(x.g)) && applying (acc(x.f) --* acc(x.g)) in true
-}
-
-
 /* Ghost operations on the left of a wand are not supported (and not
  * necessary, they could be performed outside of the wand)
  */
diff --git a/src/test/resources/wands/regression/consistency2.vpr b/src/test/resources/wands/regression/consistency2.vpr
new file mode 100644
index 000000000..bde7840a8
--- /dev/null
+++ b/src/test/resources/wands/regression/consistency2.vpr
@@ -0,0 +1,22 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+/* Consistency checks (performed on the real Silver AST, not the parser AST) */
+/* These checks are now also performed by the resolver during typechecking */
+
+field f: Int
+field g: Int
+
+/* Applying/packaging must occur inside wands */
+
+function foobar(x: Ref): Int
+  //:: ExpectedOutput(typechecker.error)
+  requires true --* acc(x.f)
+{
+  applying (true --* acc(x.f)) in x.f
+}
+
+predicate test18(x: Ref) {
+  //:: ExpectedOutput(typechecker.error)
+  acc(x.f) && (acc(x.f) --* acc(x.g)) && applying (acc(x.f) --* acc(x.g)) in true
+}
diff --git a/src/test/scala/ASTTransformationTests.scala b/src/test/scala/ASTTransformationTests.scala
index ef98765e0..bbb9caeb7 100644
--- a/src/test/scala/ASTTransformationTests.scala
+++ b/src/test/scala/ASTTransformationTests.scala
@@ -84,11 +84,11 @@ class ASTTransformationTests extends AnyFunSuite {
      val p = (NoPosition, NoPosition)
      val binExp1 = PBinExp(PIntLit(1)(p), PReserved.implied(PSymOp.EqEq), PIntLit(1)(p))(p)
      val method1 = PMethod(Seq(), PReserved.implied(PKw.Method), PIdnDef("m")(p), PGrouped.impliedParen(PDelimited.empty), None, PDelimited.empty, PDelimited.empty, Some(PSeqn(PDelimited.impliedBlock(Seq(PAssert(PReserved.implied(PKw.Assert), binExp1)(p))))(p)))(p)
-     val original = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(), Seq(), Seq(method1), Seq(), Seq())(p)
+     val original = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(), Seq(), Seq(method1), Seq())(p, Seq())
 
      val binExp2 = PBinExp(PIntLit(3)(p), PReserved.implied(PSymOp.EqEq), PIntLit(3)(p))(p)
      val method2 = PMethod(Seq(), PReserved.implied(PKw.Method), PIdnDef("m")(p), PGrouped.impliedParen(PDelimited.empty), None, PDelimited.empty, PDelimited.empty, Some(PSeqn(PDelimited.impliedBlock(Seq(PAssert(PReserved.implied(PKw.Assert), binExp2)(p))))(p)))(p)
-     val target = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(), Seq(), Seq(method2),  Seq(), Seq())(p)
+     val target = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(), Seq(), Seq(method2),  Seq())(p, Seq())
 
      case class Context(increment: Int)
 
@@ -124,11 +124,11 @@ class ASTTransformationTests extends AnyFunSuite {
     val function = PFunction(Seq(), PReserved.implied(PKw.Function), PIdnDef("f")(p), commaParen(Seq(PFormalArgDecl(PIdnDef("x")(p), PReserved.implied(PSym.Colon), TypeHelper.Int)(p), PFormalArgDecl(PIdnDef("y")(p), PReserved.implied(PSym.Colon), TypeHelper.Int)(p))), PReserved.implied(PSym.Colon), TypeHelper.Int, PDelimited.empty, PDelimited.empty, None)(p)
     val assume1 = PAssume(PReserved.implied(PKw.Assume), PBinExp(PCall(PIdnRef("f")(p), commaParen(Seq(PIntLit(1)(p), PIntLit(1)(p))), None)(p), PReserved.implied(PSymOp.EqEq), PCall(PIdnRef("f")(p), commaParen(Seq(PIntLit(1)(p), PCall(PIdnRef("f")(p), commaParen(Seq(PIntLit(1)(p), PCall(PIdnRef("f")(p), commaParen(Seq(PIntLit(1)(p), PIntLit(1)(p))), None)(p))), None)(p))), None)(p))(p))(p)
     val method1 = PMethod(Seq(), PReserved.implied(PKw.Method), PIdnDef("m")(p), PGrouped.impliedParen(PDelimited.empty), None, PDelimited.empty, PDelimited.empty, Some(PSeqn(PDelimited.impliedBlock(Seq(assume1)))(p)))(p)
-    val original = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(function), Seq(), Seq(method1),  Seq(), Seq())(p)
+    val original = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(function), Seq(), Seq(method1),  Seq())(p, Seq())
 
     val assume2 = PAssume(PReserved.implied(PKw.Assume), PBinExp(PCall(PIdnRef("f")(p), commaParen(Seq(PIntLit(2)(p), PIntLit(1)(p))), None)(p), PReserved.implied(PSymOp.EqEq), PCall(PIdnRef("f")(p), commaParen(Seq(PIntLit(2)(p), PCall(PIdnRef("f")(p), commaParen(Seq(PIntLit(3)(p), PCall(PIdnRef("f")(p), commaParen(Seq(PIntLit(4)(p), PIntLit(1)(p))), None)(p))), None)(p))), None)(p))(p))(p)
     val method2 = PMethod(Seq(), PReserved.implied(PKw.Method), PIdnDef("m")(p), PGrouped.impliedParen(PDelimited.empty), None, PDelimited.empty, PDelimited.empty, Some(PSeqn(PDelimited.impliedBlock(Seq(assume2)))(p)))(p)
-    val target = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(function), Seq(), Seq(method2),  Seq(), Seq())(p)
+    val target = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(function), Seq(), Seq(method2),  Seq())(p, Seq())
 
     case class Context(increment: Int)
 
@@ -149,7 +149,7 @@ class ASTTransformationTests extends AnyFunSuite {
     val p = (NoPosition, NoPosition)
     val requires = PForall(PReserved.implied(PKw.Forall), PDelimited.implied(Seq(PLogicalVarDecl(PIdnDef("y")(p), PReserved.implied(PSym.Colon), TypeHelper.Int)(p)), PReserved.implied(PSym.Comma)), PReserved.implied(PSym.ColonColon), Seq(), PBinExp(PIdnUseExp("y")(p), PReserved.implied(PSymOp.EqEq), PIdnUseExp("y")(p))(p))(p)
     val function = PFunction(Seq(), PReserved.implied(PKw.Function), PIdnDef("f")(p), PDelimited.impliedParenComma(Seq(PFormalArgDecl(PIdnDef("x")(p), PReserved.implied(PSym.Colon), TypeHelper.Ref)(p))), PReserved.implied(PSym.Colon), TypeHelper.Bool, PDelimited.implied(Seq(PSpecification(PReserved.implied(PKw.Requires), requires)(p)), None), PDelimited.empty, None)(p)
-    val program = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(function), Seq(), Seq(), Seq(), Seq())(p)
+    val program = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(function), Seq(), Seq(), Seq())(p, Seq())
 
     case class Context()
 
diff --git a/src/test/scala/PluginTests.scala b/src/test/scala/PluginTests.scala
index 98428308f..955489a0a 100644
--- a/src/test/scala/PluginTests.scala
+++ b/src/test/scala/PluginTests.scala
@@ -131,8 +131,7 @@ class TestPluginAddPredicate extends SilverPlugin {
       input.predicates :+ PPredicate(Seq(), PReserved.implied(PKw.Predicate), PIdnDef("testPredicate")(p), PGrouped.impliedParen(PDelimited.empty), None)(p),
       input.methods,
       input.extensions,
-      input.errors
-    )(p)
+    )(p, input.errors)
   }
 
   /** Called after methods are filtered but before the verification by the backend happens.
diff --git a/src/test/scala/SemanticAnalysisTests.scala b/src/test/scala/SemanticAnalysisTests.scala
index 98ef7a4a3..1d4e16207 100644
--- a/src/test/scala/SemanticAnalysisTests.scala
+++ b/src/test/scala/SemanticAnalysisTests.scala
@@ -31,7 +31,7 @@ class SemanticAnalysisTests extends AnyFunSuite {
     val binExp2 = PBinExp(PIntLit(1)(p), PReserved.implied(PSymOp.EqEq), PIntLit(1)(p))(p)
     val body = PSeqn(PDelimited.impliedBlock(Seq(PAssert(PReserved.implied(PKw.Assert), binExp1)(p), PSeqn(PDelimited.impliedBlock(Seq(PAssert(PReserved.implied(PKw.Assert), binExp2)(p))))(p))))(p)
     val method = PMethod(Seq(), PReserved.implied(PKw.Method), PIdnDef("m")(p), PGrouped.impliedParen(PDelimited.empty), None, PDelimited.empty, PDelimited.empty, Some(body))(p)
-    val program = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(), Seq(), Seq(method), Seq(), Seq())(p)
+    val program = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(), Seq(), Seq(method), Seq())(p, Seq())
     assert(frontend.doSemanticAnalysis(program) === frontend.Succ(program))
   }
 
@@ -40,7 +40,7 @@ class SemanticAnalysisTests extends AnyFunSuite {
     val binExp = PBinExp(PIntLit(1)(p), PReserved.implied(PSymOp.EqEq), PIntLit(1)(p))(p)
     val body = PSeqn(PDelimited.impliedBlock(Seq(PAssert(PReserved.implied(PKw.Assert), binExp)(p), PSeqn(PDelimited.impliedBlock(Seq(PAssert(PReserved.implied(PKw.Assert), binExp)(p))))(p))))(p)
     val method = PMethod(Seq(), PReserved.implied(PKw.Method), PIdnDef("m")(p), PGrouped.impliedParen(PDelimited.empty), None, PDelimited.empty, PDelimited.empty, Some(body))(p)
-    val program = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(), Seq(), Seq(method), Seq(), Seq())(p)
+    val program = PProgram(Seq(), Seq(), Seq(), Seq(), Seq(), Seq(), Seq(method), Seq())(p, Seq())
     assert(frontend.doSemanticAnalysis(program) === frontend.Succ(program))
   }
 }