From 3ce16207eeb709a95437aff89baecfe68f1c9a35 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 3 May 2023 19:51:06 +0200 Subject: [PATCH 1/4] Better type error reporting --- .../scala/viper/silver/parser/ParseAst.scala | 53 +++++++++++++------ .../scala/viper/silver/parser/Resolver.scala | 42 +++++++++------ .../standard/adt/AdtPASTExtension.scala | 6 ++- 3 files changed, 68 insertions(+), 33 deletions(-) diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala index 922ef7b3b..5e9352d61 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,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) diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala index c8dc264d3..aba51f260 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 @@ -474,7 +475,7 @@ 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 @@ -482,10 +483,15 @@ case class TypeChecker(names: NameAnalyser) { = { 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 badMatch = current.find(e => e.isLeft) + if (badMatch.isDefined) { + return Left(badMatch.get.swap.toOption.get) + } + pss = current.flatMap(_.toOption) } - pss + Right(pss) //(a:Set[PTypeSubstitution], e:Option[PTypeSubstitution])=>{ } @@ -493,7 +499,7 @@ case class TypeChecker(names: NameAnalyser) { 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 +523,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) { @@ -714,18 +720,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}. Could not unify ${problem._1} with ${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 +759,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..16dfbeb04 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) @@ -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) From 0c1d62ba2db01464d19614e4e54cc5a82546eef8 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 3 May 2023 21:06:39 +0200 Subject: [PATCH 2/4] Fixed bug, better message for case with expected type and type var --- src/main/scala/viper/silver/parser/Resolver.scala | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala index aba51f260..d7267baaa 100644 --- a/src/main/scala/viper/silver/parser/Resolver.scala +++ b/src/main/scala/viper/silver/parser/Resolver.scala @@ -485,8 +485,9 @@ case class TypeChecker(names: NameAnalyser) { for (tri <- argData){ val current = (for (ps <- pss; aps <- tri._3) yield composeAndAdd(ps, aps, tri._1, tri._2)) - val badMatch = current.find(e => e.isLeft) - if (badMatch.isDefined) { + 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) @@ -532,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) } @@ -730,7 +736,7 @@ case class TypeChecker(names: NameAnalyser) { 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}. Could not unify ${problem._1} with ${problem._2}.") + 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 From 8eed8195ff2f1a74db93829e062b110d34917179 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 4 May 2023 14:03:39 +0200 Subject: [PATCH 3/4] Fixed error positions, added comments --- .../scala/viper/silver/parser/Resolver.scala | 39 ++++++++++++------- .../standard/adt/AdtPASTExtension.scala | 6 +-- 2 files changed, 28 insertions(+), 17 deletions(-) diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala index d7267baaa..d5ff61570 100644 --- a/src/main/scala/viper/silver/parser/Resolver.scala +++ b/src/main/scala/viper/silver/parser/Resolver.scala @@ -473,13 +473,24 @@ 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])]) : 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 + 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){ @@ -488,12 +499,12 @@ case class TypeChecker(names: NameAnalyser) { val allBad = current.forall(e => e.isLeft) if (allBad) { val badMatch = current.find(e => e.isLeft) - return Left(badMatch.get.swap.toOption.get) + val badTypes = badMatch.get.swap.toOption.get + return Left(badTypes._1, badTypes._2, tri._4) } pss = current.flatMap(_.toOption) } Right(pss) - //(a:Set[PTypeSubstitution], e:Option[PTypeSubstitution])=>{ } def ground(exp: PExp, pts: PTypeSubstitution) : PTypeSubstitution = @@ -725,18 +736,18 @@ 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) - val arg = 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 unifiedSequence = unifySequenceWithSubstitutions(rlts, arg) + ) + val unifiedSequence = unifySequenceWithSubstitutions(rlts, argData) 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}.") + 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 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 16dfbeb04..8a4b8ba59 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -380,12 +380,12 @@ 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()) From 519e9425f6da1997e97648c89e526f3e4ec7f6b7 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Thu, 4 May 2023 14:07:36 +0200 Subject: [PATCH 4/4] Added another comment --- src/main/scala/viper/silver/parser/ParseAst.scala | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala index 5e9352d61..3fb6d0008 100644 --- a/src/main/scala/viper/silver/parser/ParseAst.scala +++ b/src/main/scala/viper/silver/parser/ParseAst.scala @@ -393,6 +393,9 @@ 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))) } + + // 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);