Tightening up typer state + printing refinements

1) Made consistency checking water tight, so that inconsistencies are always catched wehn they arise
2) Fixed problem in implicit search that led to inconsistencies
3) Refined printing of type parameters and type arguments

11 files changed, 94 insertions, 32 deletions

diff --git a/src/dotty/tools/dotc/Compiler.scala b/src/dotty/tools/dotc/Compiler.scala
index 8a37dba61..e6675237a 100644
--- a/src/dotty/tools/dotc/Compiler.scala
+++ b/src/dotty/tools/dotc/Compiler.scala
@@ -23,7 +23,7 @@ class Compiler {
       .withOwner(defn.RootClass)
       .withTyper(new Typer)
       .withNewMode(Mode.ImplicitsEnabled)
-      .withTyperState(new MutableTyperState(ctx.typerState, new ConsoleReporter()(ctx)))
+      .withTyperState(new MutableTyperState(ctx.typerState, new ConsoleReporter()(ctx), committable = true))
     def addImport(ctx: Context, sym: Symbol) =
       ctx.fresh.withImportInfo(ImportInfo.rootImport(sym)(ctx))
     (start.withRunInfo(new RunInfo(start)) /: rootImports)(addImport)
diff --git a/src/dotty/tools/dotc/core/Contexts.scala b/src/dotty/tools/dotc/core/Contexts.scala
index 3110d8fd9..3de6337b1 100644
--- a/src/dotty/tools/dotc/core/Contexts.scala
+++ b/src/dotty/tools/dotc/core/Contexts.scala
@@ -288,7 +288,8 @@ object Contexts {
     def withPeriod(period: Period): this.type = { this.period = period; this }
     def withNewMode(mode: Mode): this.type = { this.mode = mode; this }
     def withTyperState(typerState: TyperState): this.type = { this.typerState = typerState; this }
-    def withNewTyperState: this.type = withTyperState(typerState.fresh)
+    def withNewTyperState: this.type = withTyperState(typerState.fresh(committable = true))
+    def withExploreTyperState: this.type = withTyperState(typerState.fresh(committable = false))
     def withPrinterFn(printer: Context => Printer): this.type = { this.printerFn = printer; this }
     def withOwner(owner: Symbol): this.type = { this.owner = owner; this }
     def withSettings(sstate: SettingsState): this.type = { this.sstate = sstate; this }
diff --git a/src/dotty/tools/dotc/core/TypeComparer.scala b/src/dotty/tools/dotc/core/TypeComparer.scala
index 5701fcc95..cf24743bf 100644
--- a/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -796,7 +796,7 @@ class ExplainingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
   }
 
   override def isSubType(tp1: Type, tp2: Type) =
-    traceIndented(s"${show(tp1)} <:< ${show(tp2)} ${tp1.getClass} ${tp2.getClass}") {
+    traceIndented(s"${show(tp1)} <:< ${show(tp2)}") {
       super.isSubType(tp1, tp2)
     }
 
diff --git a/src/dotty/tools/dotc/core/TyperState.scala b/src/dotty/tools/dotc/core/TyperState.scala
index 4fcfa323e..8ee219cec 100644
--- a/src/dotty/tools/dotc/core/TyperState.scala
+++ b/src/dotty/tools/dotc/core/TyperState.scala
@@ -29,32 +29,45 @@ class TyperState(val reporter: Reporter) extends DotClass with Showable {
   def undetVars_=(vs: Set[TypeVar]): Unit = unsupported("undetVars_=")
   def instType_=(m: SimpleMap[TypeVar, Type]): Unit = unsupported("instType_=")
 
-  def fresh: TyperState = this
+  def fresh(committable: Boolean): TyperState = this
 
   def commit()(implicit ctx: Context): Unit = unsupported("commit")
 
   @elidable(elidable.FINER)
   def checkConsistent(implicit ctx: Context) = ()
 
+  @elidable(elidable.FINER)
+  def enableChecking(b: Boolean): Boolean = true
+
+  def withCheckingDisabled[T](op: => T)(implicit ctx: Context): T = op
+
   override def toText(printer: Printer): Text = "ImmutableTyperState"
 }
 
-class MutableTyperState(previous: TyperState, reporter: Reporter)
+class MutableTyperState(previous: TyperState, reporter: Reporter, committable: Boolean)
 extends TyperState(reporter) {
 
   private var myConstraint: Constraint = previous.constraint
   private var myUndetVars: Set[TypeVar] = previous.undetVars
   private var myInstType: SimpleMap[TypeVar, Type] = previous.instType
+  private var checkingEnabled: Boolean = committable
 
   override def constraint = myConstraint
   override def undetVars = myUndetVars
   override def instType = myInstType
 
-  override def constraint_=(c: Constraint) = myConstraint = c
-  override def undetVars_=(vs: Set[TypeVar]) = myUndetVars = vs
+  override def constraint_=(c: Constraint) = {
+    myConstraint = c
+    checkConsistent()
+  }
+  override def undetVars_=(vs: Set[TypeVar]) = {
+    myUndetVars = vs
+    checkConsistent()
+  }
   override def instType_=(m: SimpleMap[TypeVar, Type]): Unit = myInstType = m
 
-  override def fresh: TyperState = new MutableTyperState(this, new StoreReporter)
+  override def fresh(committable: Boolean): TyperState =
+    new MutableTyperState(this, new StoreReporter, committable)
 
   /** Commit typer state so that its information is copied into current typer state
    *  In addition (1) the owning state of undetermined or temporarily instantiated
@@ -63,10 +76,13 @@ extends TyperState(reporter) {
    *  instantiated instead.
    */
   override def commit()(implicit ctx: Context) = {
+    checkConsistent
     val targetState = ctx.typerState
+    val prev = targetState.enableChecking(false)
     targetState.constraint = constraint
     targetState.undetVars = undetVars
     targetState.instType = instType
+    targetState.enableChecking(prev)
 
     def adjustOwningState(tvar: TypeVar) =
       if (tvar.owningState eq this) tvar.owningState = targetState
@@ -84,8 +100,8 @@ extends TyperState(reporter) {
   }
 
   @elidable(elidable.FINER)
-  override def checkConsistent(implicit ctx: Context) = {
-    def err(msg: String, what: Showable) = s"$msg: ${what.show}\n${this.show}"
+  def checkConsistent(show: Showable => String = MutableTyperState.toStr): Unit = if (checkingEnabled) {
+    def err(msg: String, what: Showable) = s"$msg: ${show(what)}\n${show(this)}"
     for (tvar <- undetVars)
       assert(constraint(tvar.origin).exists, err("unconstrained type var", tvar))
     val undetParams = undetVars map (_.origin)
@@ -96,6 +112,25 @@ extends TyperState(reporter) {
     }
   }
 
+  @elidable(elidable.FINER)
+  override def checkConsistent(implicit ctx: Context): Unit = checkConsistent(_.show)
+
+  @elidable(elidable.FINER)
+  override def enableChecking(b: Boolean) = {
+    val prev = checkingEnabled
+    checkingEnabled = checkingEnabled && b
+    prev
+  }
+
+  override def withCheckingDisabled[T](op: => T)(implicit ctx: Context): T = {
+    val prev = enableChecking(false)
+    try op
+    finally {
+      enableChecking(prev)
+      checkConsistent
+    }
+  }
+
   override def toText(printer: Printer): Text = {
     val header: Text = "Typer state:"
     val undetVarsText =
@@ -111,3 +146,7 @@ extends TyperState(reporter) {
     Text.lines(List(header, undetVarsText, constrainedText, constraintText, instTypeText))
   }
 }
+
+object MutableTyperState {
+  private def toStr(x: Any) = x.toString
+}
diff --git a/src/dotty/tools/dotc/core/Types.scala b/src/dotty/tools/dotc/core/Types.scala
index 257128821..a7dadbd0e 100644
--- a/src/dotty/tools/dotc/core/Types.scala
+++ b/src/dotty/tools/dotc/core/Types.scala
@@ -1862,7 +1862,6 @@ object Types {
       owningState.undetVars -= this
       if (ctx.typerState eq creatorState) inst = tp
       else ctx.typerState.instType = ctx.typerState.instType.updated(this, tp)
-      ctx.typerState.checkConsistent // !!! DEBUG
       tp
     }
 
@@ -1881,10 +1880,12 @@ object Types {
         case OrType(tp1, tp2) => isSingleton(tp1) & isSingleton(tp2)
         case _ => false
       }
-      var inst = ctx.typeComparer.approximate(origin, fromBelow)
-      if (fromBelow && isSingleton(inst) && !isSingleton(upperBound))
-        inst = inst.widen
-      instantiateWith(inst)
+      ctx.typerState.withCheckingDisabled {
+        var inst = ctx.typeComparer.approximate(origin, fromBelow)
+        if (fromBelow && isSingleton(inst) && !isSingleton(upperBound))
+          inst = inst.widen
+        instantiateWith(inst)
+      }
     }
 
     /** If the variable is instantiated, its instance, otherwise its origin */
diff --git a/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/src/dotty/tools/dotc/printing/RefinedPrinter.scala
index bad2c071e..46a272c70 100644
--- a/src/dotty/tools/dotc/printing/RefinedPrinter.scala
+++ b/src/dotty/tools/dotc/printing/RefinedPrinter.scala
@@ -98,7 +98,12 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
           return (toTextLocal(tycon) ~ "[" ~ toTextGlobal(args, ", ") ~ "]").close
         }
       case tp @ TypeRef(pre, name) =>
-        if (tp.symbol is TypeParam) return nameString(tp.symbol)
+        if (tp.symbol is TypeParam | TypeArgument) {
+          return tp.info match {
+            case TypeAlias(hi) => toText(hi)
+            case _ => nameString(tp.symbol)
+          }
+        }
       case _ =>
     }
     super.toText(tp)
diff --git a/src/dotty/tools/dotc/reporting/Reporter.scala b/src/dotty/tools/dotc/reporting/Reporter.scala
index 9ef16d67a..6f5f3b5cb 100644
--- a/src/dotty/tools/dotc/reporting/Reporter.scala
+++ b/src/dotty/tools/dotc/reporting/Reporter.scala
@@ -97,8 +97,10 @@ trait Reporting { this: Context =>
   def warning(msg: => String, pos: SourcePosition = NoSourcePosition): Unit =
     reporter.report(Diagnostic(msg, pos, WARNING))
 
-  def error(msg: => String, pos: SourcePosition = NoSourcePosition): Unit =
+  def error(msg: => String, pos: SourcePosition = NoSourcePosition): Unit = {
+    // println("*** ERROR: " + msg) // !!! DEBUG
     reporter.report(Diagnostic(msg, pos, ERROR))
+  }
 
   def incompleteInputError(msg: String, pos: SourcePosition = NoSourcePosition)(implicit ctx: Context): Unit =
     reporter.incomplete(Diagnostic(msg, pos, ERROR))(ctx)
diff --git a/src/dotty/tools/dotc/typer/Applications.scala b/src/dotty/tools/dotc/typer/Applications.scala
index 05008ac1a..ef0fcf709 100644
--- a/src/dotty/tools/dotc/typer/Applications.scala
+++ b/src/dotty/tools/dotc/typer/Applications.scala
@@ -633,7 +633,7 @@ trait Applications extends Compatibility { self: Typer =>
    *  @param  resultType   The expected result type of the application
    */
   def isApplicableToTrees(methRef: TermRef, args: List[Tree], resultType: Type)(implicit ctx: Context): Boolean =
-    new ApplicableToTrees(methRef, args, resultType)(ctx.fresh.withNewTyperState).success
+    new ApplicableToTrees(methRef, args, resultType)(ctx.fresh.withExploreTyperState).success
 
   def isApplicableToTrees(tp: Type, args: List[Tree], resultType: Type)(implicit ctx: Context): Boolean = tp match {
     case methRef: TermRef => isApplicableToTrees(methRef, args, resultType)
@@ -647,7 +647,7 @@ trait Applications extends Compatibility { self: Typer =>
    *  @param  resultType   The expected result type of the application
    */
   def isApplicableToTypes(methRef: TermRef, args: List[Type], resultType: Type = WildcardType)(implicit ctx: Context) =
-    new ApplicableToTypes(methRef, args, resultType)(ctx.fresh.withNewTyperState).success
+    new ApplicableToTypes(methRef, args, resultType)(ctx.fresh.withExploreTyperState).success
 
   def isApplicableToTypes(tp: Type, args: List[Type], resultType: Type)(implicit ctx: Context): Boolean = tp match {
     case methRef: TermRef => isApplicableToTypes(methRef, args, resultType)
@@ -659,7 +659,7 @@ trait Applications extends Compatibility { self: Typer =>
 
   /** Is `tp` a subtype of `pt`? */
   def testCompatible(tp: Type, pt: Type)(implicit ctx: Context) =
-    isCompatible(tp, pt)(ctx.fresh.withNewTyperState)
+    isCompatible(tp, pt)(ctx.fresh.withExploreTyperState)
 
   /** In a set of overloaded applicable alternatives, is `alt1` at least as good as
    *  `alt2`? `alt1` and `alt2` are nonoverloaded references.
diff --git a/src/dotty/tools/dotc/typer/Implicits.scala b/src/dotty/tools/dotc/typer/Implicits.scala
index af36962a5..c84e3cbd6 100644
--- a/src/dotty/tools/dotc/typer/Implicits.scala
+++ b/src/dotty/tools/dotc/typer/Implicits.scala
@@ -37,9 +37,17 @@ object Implicits {
 
     /** Return those references in `refs` that are compatible with type `pt`. */
     protected def filterMatching(pt: Type)(implicit ctx: Context): List[TermRef] = track("filterMatching") {
-      def result(implicit ctx: Context) =
-        refs filter (ref => isCompatible(normalize(ref), pt))
-      result(ctx.fresh.withNewTyperState) // create a defensive copy of ctx to avoid constraint pollution
+      def result(implicit ctx: Context) = {
+        def refMatches(ref: TermRef) = {
+          if (ref.name.toString == "cb") {
+            println(i"refMatches ${ref.symbol}, ref = $ref, normalze = ${normalize(ref)}, pt = $pt = ${isCompatible(normalize(ref), pt)}")
+            println(err.typeMismatchStr(normalize(ref), pt))
+          }
+          isCompatible(normalize(ref), pt)
+        }
+        refs filter refMatches
+      }
+      result(ctx.fresh.withExploreTyperState) // create a defensive copy of ctx to avoid constraint pollution
     }
 
     /** No further implicit conversions can be applied when searching for implicits. */
@@ -267,6 +275,9 @@ trait Implicits { self: Typer =>
   /** An implicit search; parameters as in `inferImplicit` */
   class ImplicitSearch(protected val pt: Type, protected val argument: Tree, pos: Position)(implicit ctx: Context) {
 
+    val initctx: Context = ctx.fresh.withNewTyperState.retractMode(ImplicitsEnabled)
+    def nestedContext = initctx.fresh.withNewTyperState
+
     protected def nonMatchingImplicit(ref: TermRef): SearchFailure = NoImplicitMatches
     protected def shadowedImplicit(ref: TermRef, shadowing: Type): SearchFailure = NoImplicitMatches
     protected def failedSearch: SearchFailure = NoImplicitMatches
@@ -277,12 +288,14 @@ trait Implicits { self: Typer =>
 
       /** Try to typecheck an implicit reference */
       def typedImplicit(ref: TermRef)(implicit ctx: Context): SearchResult = track("typedImplicit") {
-        ctx.typerState.checkConsistent // !!! DEBUG
         val id = Ident(ref).withPos(pos)
         val tree =
-          if (argument.isEmpty) adapt(id, pt)
-          else typedApply(id, ref, argument :: Nil, pt)
-        lazy val shadowing = typed(untpd.Ident(ref.name), ref).tpe
+          if (argument.isEmpty)
+            adapt(id, pt)
+          else
+            typed(untpd.Apply(untpd.TypedSplice(id), untpd.TypedSplice(argument) :: Nil), pt)
+        lazy val shadowing =
+            typed(untpd.Ident(ref.name), ref)(nestedContext).tpe
         if (ctx.typerState.reporter.hasErrors) nonMatchingImplicit(ref)
         else if (contextual && !(shadowing =:= ref)) shadowedImplicit(ref, shadowing)
         else SearchSuccess(tree)(ref, ctx.typerState)
@@ -295,7 +308,7 @@ trait Implicits { self: Typer =>
        */
       def rankImplicits(pending: List[TermRef], acc: List[SearchSuccess]): List[SearchSuccess] = pending match {
         case ref :: pending1 =>
-          typedImplicit(ref)(ctx.fresh.withNewTyperState.retractMode(ImplicitsEnabled)) match {
+          typedImplicit(ref)(nestedContext) match {
             case fail: SearchFailure =>
               rankImplicits(pending1, acc)
             case best: SearchSuccess =>
diff --git a/src/dotty/tools/dotc/typer/Inferencing.scala b/src/dotty/tools/dotc/typer/Inferencing.scala
index 6f78409d0..8d85c1911 100644
--- a/src/dotty/tools/dotc/typer/Inferencing.scala
+++ b/src/dotty/tools/dotc/typer/Inferencing.scala
@@ -41,7 +41,7 @@ object Inferencing {
         isCompatible(normalize(mbrType), /*(new WildApprox) apply (needed?)*/ proto)
       name == nme.WILDCARD || {
         val mbr = tp1.member(name)
-        mbr.exists && mbr.hasAltWith(m => testCompatible(m.info)(ctx.fresh.withNewTyperState))
+        mbr.exists && mbr.hasAltWith(m => testCompatible(m.info)(ctx.fresh.withExploreTyperState))
       }
     }
     override def toString = "Proto" + super.toString
@@ -207,7 +207,6 @@ object Inferencing {
         println(s"interpolate non-occurring ${tvar.show} in ${tp.show}")
         tvar.instantiate(fromBelow = true)
       }
-      ctx.typerState.checkConsistent
     }
 
     /** Instantiate undetermined type variables to that type `tp` is
diff --git a/src/dotty/tools/dotc/typer/Typer.scala b/src/dotty/tools/dotc/typer/Typer.scala
index 8a4ee2d83..0e246480c 100644
--- a/src/dotty/tools/dotc/typer/Typer.scala
+++ b/src/dotty/tools/dotc/typer/Typer.scala
@@ -1084,8 +1084,10 @@ class Typer extends Namer with Applications with Implicits {
         case poly: PolyType =>
           if (pt.isInstanceOf[PolyProto]) tree
           else {
-            val tracked = ctx.track(poly)
-            val tvars = ctx.newTypeVars(tracked, tree.pos)
+            val tvars = ctx.typerState.withCheckingDisabled {
+              val tracked = ctx.track(poly)
+              ctx.newTypeVars(tracked, tree.pos)
+            }
             adapt(tpd.TypeApply(tree, tvars map (tpd.TypeTree(_))), pt)
           }
         case wtp =>