Better type error reporting

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,39 @@ 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 *(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): Option[PTypeSubstitution] = add(PTypeVar(a),b)
+  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 +539,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)

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
@@ -474,26 +475,32 @@ case class TypeChecker(names: NameAnalyser) {
   }
   def unifySequenceWithSubstitutions(
     rlts: Seq[PTypeSubstitution], //local substitutions, refreshed
-    argData: scala.collection.immutable.Seq[(PType, PType, Seq[PTypeSubstitution])]) : Seq[PTypeSubstitution]
+    argData: scala.collection.immutable.Seq[(PType, PType, Seq[PTypeSubstitution])]) : Either[(PType, PType), 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
       = {
     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)
+        return Left(badMatch.get.swap.toOption.get)
+      }
+      pss = current.flatMap(_.toOption)
     }
-    pss
+    Right(pss)
     //(a:Set[PTypeSubstitution], e:Option[PTypeSubstitution])=>{
   }
 
   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 +524,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 +533,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)
         }
@@ -714,18 +726,22 @@ case class TypeChecker(names: NameAnalyser) {
               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)) ++
+              val arg = flat.indices.map(i => (flat(i), poa.args(i).typ, poa.args(i).typeSubstitutions.distinct.toSeq)) ++
                 (
                   extraReturnTypeConstraint match {
                     case None => Nil
                     case Some(t) => Seq((rrt, t, List(PTypeSubstitution.id)))
                   }
-                )
-              )
-              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, arg)
+              if (unifiedSequence.isLeft && poa.typeSubstitutions.isEmpty) {
+                val problem = unifiedSequence.swap.toOption.get
+                messages ++= FastMessaging.message(exp, s"Type error in the expression at ${exp.pos._1}. Expected ${problem._1} but got ${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 +765,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 =>

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)
@@ -386,7 +388,7 @@ object PAdtOpApp {
                 case Some(t) => Seq((rrt, t, List(PTypeSubstitution.id)))
               }
               )
-          )
+          ).getOrElse(Seq())
           val ts = poa.typeSubstitutions.distinct
           if (ts.isEmpty)
             t.typeError(poa)