diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala
index 922ef7b3b..3fb6d0008 100644
--- a/src/main/scala/viper/silver/parser/ParseAst.scala
+++ b/src/main/scala/viper/silver/parser/ParseAst.scala
@@ -7,7 +7,6 @@
 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.{Exp, MagicWandOp, Member, NoPosition, Position, Stmt, Type}
@@ -243,6 +242,8 @@ case class PDomainType(domain: PIdnUse, args: Seq[PType])(val pos: (Position, Po
     r
   }
 
+  override def withTypeArguments(s: Seq[PType]) = copy(args = s)(pos)
+
   override def toString = domain.name + (if (args.isEmpty) "" else s"[${args.mkString(", ")}]")
 }
 
@@ -292,6 +293,8 @@ trait PGenericType extends PType {
   def typeArguments : Seq[PType]
   override def isGround = typeArguments.forall(_.isGround)
   override def toString = s"$genericName[${typeArguments.mkString(", ")}]"
+
+  def withTypeArguments(s: Seq[PType]) : PGenericType
 }
 
 sealed trait PGenericCollectionType extends PGenericType {
@@ -304,14 +307,20 @@ sealed trait PGenericCollectionType extends PGenericType {
 case class PSeqType(elementType: PType)(val pos: (Position, Position) = (NoPosition, NoPosition)) extends PType with PGenericCollectionType {
   override val genericName = "Seq"
   override def substitute(map: PTypeSubstitution) = PSeqType(elementType.substitute(map))(pos)
+
+  override def withTypeArguments(s: Seq[PType]) = copy(elementType = s.head)(pos)
 }
 case class PSetType(elementType: PType)(val pos: (Position, Position) = (NoPosition, NoPosition)) extends PType with PGenericCollectionType {
   override val genericName = "Set"
   override def substitute(map: PTypeSubstitution) = PSetType(elementType.substitute(map))(pos)
+
+  override def withTypeArguments(s: Seq[PType]) = copy(elementType = s.head)(pos)
 }
 case class PMultisetType(elementType: PType)(val pos: (Position, Position) = (NoPosition, NoPosition)) extends PType with PGenericCollectionType {
   override val genericName = "Multiset"
   override def substitute(map: PTypeSubstitution) = PMultisetType(elementType.substitute(map))(pos)
+
+  override def withTypeArguments(s: Seq[PType]): PMultisetType = copy(elementType = s.head)(pos)
 }
 
 case class PMapType(keyType : PType, valueType : PType)(val pos: (Position, Position) = (NoPosition, NoPosition)) extends PType with PGenericType {
@@ -321,6 +330,8 @@ case class PMapType(keyType : PType, valueType : PType)(val pos: (Position, Posi
 
   override def isValidOrUndeclared = typeArguments.forall(_.isValidOrUndeclared)
   override def substitute(map: PTypeSubstitution) = PMapType(keyType.substitute(map), valueType.substitute(map))(pos)
+
+  override def withTypeArguments(s: Seq[PType]): PMapType = copy(keyType = s.head, valueType = s(1))(pos)
 }
 
 /** Type used for internal nodes (e.g. typing predicate accesses) - should not be
@@ -382,27 +393,42 @@ class PTypeSubstitution(val m:Map[String,PType])  //extends Map[String,PType]()
     val ts = PTypeSubstitution(Map(a -> b))
     PTypeSubstitution(m.map(kv => kv._1 -> kv._2.substitute(ts)))
   }
-  def *(other:PTypeSubstitution) : Option[PTypeSubstitution] =
-    other.m.foldLeft(Some(this):Option[PTypeSubstitution])({
-      case (Some(s),p)=>s.add(PTypeVar(p._1),p._2);
-      case (None,_) => None })
 
-  def add(a:String,b:PType): Option[PTypeSubstitution] = add(PTypeVar(a),b)
+  // The following methods all return a type substitution if successful,
+  // otherwise a pair containing the expected and the found type.
+  def *(other:PTypeSubstitution) : Either[(PType, PType), PTypeSubstitution] =
+    other.m.foldLeft(Right(this):Either[(PType, PType), PTypeSubstitution])({
+      case (Right(s),p)=>s.add(PTypeVar(p._1),p._2);
+      case (l@Left(_),_) => l })
+
+  def add(a:String,b:PType): Either[(PType, PType), PTypeSubstitution] = add(PTypeVar(a),b)
 
-  def add(a:PType,b:PType): Option[PTypeSubstitution] = {
+  def add(a:PType,b:PType): Either[(PType, PType), PTypeSubstitution] = {
     val as = a.substitute(this)
     val bs = b.substitute(this)
     (as, bs) match {
-      case (aa,bb) if aa == bb => Some(this)
-      case (PTypeVar(name), t) if PTypeVar.isFreePTVName(name) => assert(!contains(name)); Some(substitute(name,t)+(name->t))
+      case (aa,bb) if aa == bb => Right(this)
+      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)
       case (gt1: PGenericType, gt2: PGenericType) if gt1.genericName == gt2.genericName =>
-        ((gt1.typeArguments zip gt2.typeArguments).foldLeft[Option[PTypeSubstitution]](Some(this))
-          ((ss: Option[PTypeSubstitution], p: (PType, PType)) => ss match {
-            case Some(sss) => sss.add(p._1,p._2)
-            case None => None
+        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 {
+              case l@Left(pair) =>
+                val problemArg = zippedArgs.zipWithIndex.find(_._1 == pair)
+                problemArg match {
+                  case None => l
+                  case Some((_, index)) =>
+                    val newArgs = zippedArgs.updated(index, pair)
+                    val (argsA, argsB) = newArgs.unzip
+                    Left(gt1.withTypeArguments(argsA), gt1.withTypeArguments(argsB))
+                }
+              case r => r
+            }
+            case Left((aa, bb)) => Left((aa, bb))
           }))
-      case _ => None
+      case (aa, bb) => Left((aa, bb))
     }
 
   }
@@ -516,7 +542,7 @@ case class PCall(func: PIdnUse, args: Seq[PExp], typeAnnotated : Option[PType] =
         assert(s3.m.forall(_._2.isGround))
         domainSubstitution = Some(s3)
         dtr.mm.values.foldLeft(ots)(
-          (tss,s)=> if (tss.contains(s)) tss else tss.add(s, PTypeSubstitution.defaultType).get)
+          (tss,s)=> if (tss.contains(s)) tss else tss.add(s, PTypeSubstitution.defaultType).getOrElse(null))
       case _ => ots
     }
     super.forceSubstitution(ts)
diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala
index c8dc264d3..d5ff61570 100644
--- a/src/main/scala/viper/silver/parser/Resolver.scala
+++ b/src/main/scala/viper/silver/parser/Resolver.scala
@@ -459,11 +459,12 @@ case class TypeChecker(names: NameAnalyser) {
    * 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) : Option[PTypeSubstitution] = {
+  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 */
-      return None
+      val nonMatchingKey = sharedKeys.find(p => pts1.get(p).get != pts2.get(p).get).get
+      return Left((pts1.get(nonMatchingKey).get, pts2.get(nonMatchingKey).get))
     }
 
     //composed substitution before add
@@ -472,28 +473,45 @@ case class TypeChecker(names: NameAnalyser) {
         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
+   *          _3 is the set of substitutions of the argument expression
+   *          _4 is the argument expression itself (used to extract a precise position)
+   * Returns:
+   * Either a new type substitution (right case) or, in case of failure (left) a triple containing
+   *          _1 the expected type
+   *          _2 the found type
+   *          _3 the argument that caused the failure
+   */
   def unifySequenceWithSubstitutions(
-    rlts: Seq[PTypeSubstitution], //local substitutions, refreshed
-    argData: scala.collection.immutable.Seq[(PType, PType, Seq[PTypeSubstitution])]) : Seq[PTypeSubstitution]
-    // a sequence of triples, one per op arguments, where
-    //_1 is the fresh local argument type
-    //_2 is the type of the argument expression
-    //_3 is the set of substitutions of the argument expression
+    rlts: Seq[PTypeSubstitution],
+    argData: scala.collection.immutable.Seq[(PType, PType, Seq[PTypeSubstitution], PExp)]) : Either[(PType, PType, PExp), Seq[PTypeSubstitution]]
       = {
     var pss = rlts
     for (tri <- argData){
-      val current = (for (ps <- pss; aps <- tri._3) yield composeAndAdd(ps, aps, tri._1, tri._2))
-      pss = current.flatten
+      val current = (for (ps <- pss; aps <- tri._3)
+        yield composeAndAdd(ps, aps, 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)
     }
-    pss
-    //(a:Set[PTypeSubstitution], e:Option[PTypeSubstitution])=>{
+    Right(pss)
   }
 
   def ground(exp: PExp, pts: PTypeSubstitution) : PTypeSubstitution =
     pts.m.flatMap(kv=>kv._2.freeTypeVariables &~ pts.m.keySet).foldLeft(pts)((ts,fv)=>
       {
         messages ++= FastMessaging.message(exp, s"Unconstrained type parameter, substituting default type ${PTypeSubstitution.defaultType}.", error=false)
-        ts.add(PTypeVar(fv),PTypeSubstitution.defaultType).get
+        ts.add(PTypeVar(fv),PTypeSubstitution.defaultType).toOption.get
       }
     )
 
@@ -517,7 +535,7 @@ case class TypeChecker(names: NameAnalyser) {
     checkInternal(exp)
     if (exp.typ.isValidOrUndeclared && exp.typeSubstitutions.nonEmpty) {
       val etss = oexpected match {
-        case Some(expected) if expected.isValidOrUndeclared => exp.typeSubstitutions.flatMap(_.add(exp.typ, expected))
+        case Some(expected) if expected.isValidOrUndeclared => exp.typeSubstitutions.flatMap(_.add(exp.typ, expected).toOption)
         case _ => exp.typeSubstitutions
       }
       if (etss.nonEmpty) {
@@ -526,7 +544,12 @@ case class TypeChecker(names: NameAnalyser) {
       } else {
         oexpected match {
           case Some(expected) =>
-            messages ++= FastMessaging.message(exp, s"Expected type ${expected.toString}, but found ${exp.typ.toString} at the expression at ${exp.pos._1}")
+            val reportedActual = if (exp.typ.isGround) {
+              exp.typ
+            } else {
+              exp.typ.substitute(selectAndGroundTypeSubstitution(exp, exp.typeSubstitutions))
+            }
+            messages ++= FastMessaging.message(exp, s"Expected type ${expected.toString}, but found ${reportedActual} at the expression at ${exp.pos._1}")
           case None =>
             typeError(exp)
         }
@@ -713,19 +736,23 @@ case class TypeChecker(names: NameAnalyser) {
               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 triples below are: (fresh argument type, argument type as used in domain of substitutions, substitutions)
-              poa.typeSubstitutions ++= unifySequenceWithSubstitutions(rlts, flat.indices.map(i => (flat(i), poa.args(i).typ, poa.args(i).typeSubstitutions.distinct.toSeq)) ++
+              // 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)))
+                    case Some(t) => Seq((rrt, t, List(PTypeSubstitution.id), poa))
                   }
                 )
-              )
-              val ts = poa.typeSubstitutions.distinct
-              if (ts.isEmpty)
-                typeError(poa)
-              poa.typ = if (ts.size == 1) rrt.substitute(ts.head) else rrt
+              val unifiedSequence = unifySequenceWithSubstitutions(rlts, argData)
+              if (unifiedSequence.isLeft && poa.typeSubstitutions.isEmpty) {
+                val problem = unifiedSequence.swap.toOption.get
+                messages ++= FastMessaging.message(problem._3, s"Type error in the expression at ${problem._3.pos._1}. Expected type ${problem._1} but found ${problem._2}.")
+              } else {
+                poa.typeSubstitutions ++= unifiedSequence.toOption.get
+                val ts = poa.typeSubstitutions.distinct
+                poa.typ = if (ts.size == 1) rrt.substitute(ts.head) else rrt
+              }
             } else {
               poa.typeSubstitutions.clear()
               poa.typ = PUnknown()()
@@ -749,7 +776,7 @@ case class TypeChecker(names: NameAnalyser) {
         ns.variable.typ = e.typ
         checkInternal(pl.body)
         pl.typ = pl.body.typ
-        pl._typeSubstitutions = (for (ts1 <- pl.body.typeSubstitutions;ts2 <- e.typeSubstitutions) yield ts1*ts2).flatten.toList.distinct
+        pl._typeSubstitutions = (for (ts1 <- pl.body.typeSubstitutions;ts2 <- e.typeSubstitutions) yield (ts1*ts2).toOption).flatten.toList.distinct
         curMember = oldCurMember
 
       case pq: PForPerm =>
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 9a4626c07..8a4b8ba59 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala
@@ -240,6 +240,8 @@ case class PAdtType(adt: PIdnUse, args: Seq[PType])
     }
   }
 
+  override def withTypeArguments(s: Seq[PType]): PGenericType = copy(args = s)(pos)
+
   override def toString: String = adt.name + (if (args.isEmpty) "" else s"[${args.mkString(", ")}]")
 
 }
@@ -282,7 +284,7 @@ sealed trait PAdtOpApp extends PExtender with POpApp {
         assert(s3.m.forall(_._2.isGround))
         adtSubstitution = Some(s3)
         dtr.mm.values.foldLeft(ots)(
-          (tss, s) => if (tss.contains(s)) tss else tss.add(s, PTypeSubstitution.defaultType).get)
+          (tss, s) => if (tss.contains(s)) tss else tss.add(s, PTypeSubstitution.defaultType).toOption.get)
       case _ => ots
     }
     super.forceSubstitution(ts)
@@ -378,15 +380,15 @@ object PAdtOpApp {
           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 triples below are: (fresh argument type, argument type as used in domain of substitutions, substitutions)
-          poa.typeSubstitutions ++= t.unifySequenceWithSubstitutions(rlts, flat.indices.map(i => (flat(i), poa.args(i).typ, poa.args(i).typeSubstitutions.distinct.toSeq)) ++
+          // 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)))
+                case Some(t) => Seq((rrt, t, List(PTypeSubstitution.id), poa))
               }
               )
-          )
+          ).getOrElse(Seq())
           val ts = poa.typeSubstitutions.distinct
           if (ts.isEmpty)
             t.typeError(poa)