From f449d9d3f83c7e28526cb827aa19b8eaebbb784b Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sun, 26 Feb 2017 14:41:18 +0100
Subject: [PATCH 01/16] Fix printing of refined applied types

If an applied type has a refinement, it was
printed before as one large refinement type
including the type parameter bindings.
---
 compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala     | 4 +++-
 .../src/dotty/tools/dotc/reporting/diagnostic/messages.scala  | 2 +-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 0d1068b8c32b..6af902d1b4dc 100644
--- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
+++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
@@ -4,6 +4,7 @@ package printing
 import core._
 import Texts._, Types._, Flags._, Names._, Symbols._, NameOps._, Constants._, Denotations._
 import Contexts.Context, Scopes.Scope, Denotations.Denotation, Annotations.Annotation
+import TypeApplications.AppliedType
 import StdNames.{nme, tpnme}
 import ast.Trees._, ast._
 import typer.Implicits._
@@ -119,10 +120,11 @@ class PlainPrinter(_ctx: Context) extends Printer {
   }
 
   /** The longest sequence of refinement types, starting at given type
-   *  and following parents.
+   *  and following parents, but stopping at applied types.
    */
   private def refinementChain(tp: Type): List[Type] =
     tp :: (tp match {
+      case AppliedType(_, _) => Nil
       case tp: RefinedType => refinementChain(tp.parent.stripTypeVar)
       case _ => Nil
     })
diff --git a/compiler/src/dotty/tools/dotc/reporting/diagnostic/messages.scala b/compiler/src/dotty/tools/dotc/reporting/diagnostic/messages.scala
index 34190c1141bf..4599665c8cca 100644
--- a/compiler/src/dotty/tools/dotc/reporting/diagnostic/messages.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/diagnostic/messages.scala
@@ -1138,7 +1138,7 @@ object messages {
            |
            |You may want to create an anonymous class extending ${cls.name} with
            |  ${s"class ${cls.name} { }"}
-           |  
+           |
            |or add a companion object with
            |  ${s"object ${cls.name} extends ${cls.name}"}
            |

From e4775b87c2b5e8f55bb32da9160cd37322a18f2c Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sun, 26 Feb 2017 16:12:19 +0100
Subject: [PATCH 02/16] Constrain results of dependent implicits

No reason why we should not - normalize handles implicit
methods just fine. This fixes type errors in test HLists.scala.
---
 .../dotty/tools/dotc/typer/ProtoTypes.scala   | 23 ++++++++-----------
 1 file changed, 9 insertions(+), 14 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
index d666b563e3f4..48f79d147b3c 100644
--- a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
+++ b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
@@ -62,14 +62,9 @@ object ProtoTypes {
             true
         }
       case _: ValueTypeOrProto if !disregardProto(pt) =>
-        mt match {
-          case mt: MethodType =>
-            mt.isDependent || isCompatible(normalize(mt, pt), pt)
-          case _ =>
-            isCompatible(mt, pt)
-        }
-      case _: WildcardType =>
-        isCompatible(mt, pt)
+        isCompatible(normalize(mt, pt), pt)
+      case pt: WildcardType if pt.optBounds.exists =>
+        isCompatible(normalize(mt, pt), pt)
       case _ =>
         true
     }
@@ -421,12 +416,12 @@ object ProtoTypes {
           if (mt.isDependent) tp
           else {
             val rt = normalize(mt.resultType, pt)
-          pt match {
-            case pt: IgnoredProto  => mt
-            case pt: ApplyingProto => mt.derivedMethodType(mt.paramNames, mt.paramTypes, rt)
-            case _ =>
-              val ft = defn.FunctionOf(mt.paramTypes, rt)
-              if (mt.paramTypes.nonEmpty || ft <:< pt) ft else rt
+            pt match {
+              case pt: IgnoredProto  => mt
+              case pt: ApplyingProto => mt.derivedMethodType(mt.paramNames, mt.paramTypes, rt)
+              case _ =>
+                val ft = defn.FunctionOf(mt.paramTypes, rt)
+                if (mt.paramTypes.nonEmpty || ft <:< pt) ft else rt
             }
           }
       case et: ExprType => et.resultType

From c3a90a4a9a9827d199ec436fcfda7c5447731542 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Mon, 27 Feb 2017 09:34:57 +0100
Subject: [PATCH 03/16] Systematic treatment of result types of dependent
 methods

We approximate dependencies to parameters by Wildcards. This was already
done in one place, is now done in other places as well, instead of doing nothing for
dependent methods.
---
 .../src/dotty/tools/dotc/core/Types.scala     | 11 +++++++-
 .../dotty/tools/dotc/typer/Applications.scala | 24 +++++++---------
 .../dotty/tools/dotc/typer/ProtoTypes.scala   | 28 ++++++++-----------
 3 files changed, 32 insertions(+), 31 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 200e94a1e120..8bd729472376 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -1686,7 +1686,10 @@ object Types {
           }
         else newLikeThis(prefix)
       }
-      else newLikeThis(prefix)
+      else prefix match {
+        case _: WildcardType => WildcardType
+        case _ => newLikeThis(prefix)
+      }
 
     /** Create a NamedType of the same kind as this type, but with a new prefix.
      */
@@ -2391,6 +2394,12 @@ object Types {
      */
     def isDependent(implicit ctx: Context): Boolean = dependencyStatus == TrueDeps
 
+    /** The result type where every reference to a parameter is replaced by a Wildcard
+     */
+    def resultTypeApprox(implicit ctx: Context): Type =
+      if (isDependent) resultType.substParams(this, paramTypes.map(Function.const(WildcardType)))
+      else resultType
+
     protected def computeSignature(implicit ctx: Context): Signature =
       resultSignature.prepend(paramTypes, isJava)
 
diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index e9df12b42a96..bca44997df85 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -213,16 +213,14 @@ trait Applications extends Compatibility { self: Typer with Dynamic =>
     protected def init() = methType match {
       case methType: MethodType =>
         // apply the result type constraint, unless method type is dependent
-        if (!methType.isDependent) {
-          val savedConstraint = ctx.typerState.constraint
-          if (!constrainResult(methType.resultType, resultType))
-            if (ctx.typerState.isCommittable)
-              // defer the problem until after the application;
-              // it might be healed by an implicit conversion
-              assert(ctx.typerState.constraint eq savedConstraint)
-            else
-              fail(err.typeMismatchMsg(methType.resultType, resultType))
-        }
+        val savedConstraint = ctx.typerState.constraint
+        if (!constrainResult(methType.resultTypeApprox, resultType))
+          if (ctx.typerState.isCommittable)
+            // defer the problem until after the application;
+            // it might be healed by an implicit conversion
+            assert(ctx.typerState.constraint eq savedConstraint)
+          else
+            fail(err.typeMismatchMsg(methType.resultType, resultType))
         // match all arguments with corresponding formal parameters
         matchArgs(orderedArgs, methType.paramTypes, 0)
       case _ =>
@@ -1100,10 +1098,8 @@ trait Applications extends Compatibility { self: Typer with Dynamic =>
 
     /** Drop any implicit parameter section */
     def stripImplicit(tp: Type): Type = tp match {
-      case mt: ImplicitMethodType if !mt.isDependent =>
-        mt.resultType
-          // todo: make sure implicit method types are not dependent?
-          // but check test case in /tests/pos/depmet_implicit_chaining_zw.scala
+      case mt: ImplicitMethodType =>
+        mt.resultTypeApprox
       case pt: PolyType =>
         pt.derivedPolyType(pt.paramNames, pt.paramBounds, stripImplicit(pt.resultType))
       case _ =>
diff --git a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
index 48f79d147b3c..4d88fc4f5c10 100644
--- a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
+++ b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
@@ -57,7 +57,7 @@ object ProtoTypes {
       case pt: FunProto =>
         mt match {
           case mt: MethodType =>
-            mt.isDependent || constrainResult(mt.resultType, pt.resultType)
+            constrainResult(mt.resultTypeApprox, pt.resultType)
           case _ =>
             true
         }
@@ -408,22 +408,18 @@ object ProtoTypes {
     tp.widenSingleton match {
       case poly: PolyType => normalize(constrained(poly).resultType, pt)
       case mt: MethodType =>
-        if (mt.isImplicit)
-          if (mt.isDependent)
-            mt.resultType.substParams(mt, mt.paramTypes.map(Function.const(WildcardType)))
-          else mt.resultType
-        else
-          if (mt.isDependent) tp
-          else {
-            val rt = normalize(mt.resultType, pt)
-            pt match {
-              case pt: IgnoredProto  => mt
-              case pt: ApplyingProto => mt.derivedMethodType(mt.paramNames, mt.paramTypes, rt)
-              case _ =>
-                val ft = defn.FunctionOf(mt.paramTypes, rt)
-                if (mt.paramTypes.nonEmpty || ft <:< pt) ft else rt
-            }
+        if (mt.isImplicit) mt.resultTypeApprox
+        else if (mt.isDependent) tp
+        else {
+          val rt = normalize(mt.resultType, pt)
+          pt match {
+            case pt: IgnoredProto  => mt
+            case pt: ApplyingProto => mt.derivedMethodType(mt.paramNames, mt.paramTypes, rt)
+            case _ =>
+              val ft = defn.FunctionOf(mt.paramTypes, rt)
+              if (mt.paramTypes.nonEmpty || ft <:< pt) ft else rt
           }
+        }
       case et: ExprType => et.resultType
       case _ => tp
     }

From 0baeb8e22c085a73a129859f7c07d578e1122c0b Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Mon, 27 Feb 2017 11:25:33 +0100
Subject: [PATCH 04/16] Don't align aliases in refined types by default

We previously tried to force S1 and S2 be the same type
when encountering a lub like `T1 { A = S1 } & T2 { A = S2 }`.
The comments in this commit explain why this is unsound, so
this rewrite is now made subject to a new config option, which
is off by default.

I verified that the new behavior does not affect the performance of
the junit tests.
---
 .../src/dotty/tools/dotc/config/Config.scala  | 15 +++++++++
 .../dotty/tools/dotc/core/TypeComparer.scala  | 33 +++++++++++--------
 2 files changed, 34 insertions(+), 14 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/config/Config.scala b/compiler/src/dotty/tools/dotc/config/Config.scala
index 119af9483c3e..900e5669f9e6 100644
--- a/compiler/src/dotty/tools/dotc/config/Config.scala
+++ b/compiler/src/dotty/tools/dotc/config/Config.scala
@@ -75,6 +75,21 @@ object Config {
   /** If this flag is set, take the fast path when comparing same-named type-aliases and types */
   final val fastPathForRefinedSubtype = true
 
+  /** If this flag is set, and we compute `T1 { X = S1 }` & `T2 { X = S2 }`,
+   *  try to align the refinements by computing `S1 =:= S2` (which might instantiate type parameters).
+   *  This rule is contentious because it cuts the constraint set. Also, it is
+   *  currently unsound because `&` gets called in computations on a constraint
+   *  itself. If the `=:=` test generates a new constraint, that constraint is then
+   *  out of sync with with the constraint on which the computation is performed.
+   *  The constraint resulting from `=:=` ends up to be thrown away whereas
+   *  its result is used, which is unsound. So if we want to turn this flag on
+   *  permanently instead of just for debugging, we have to refactor occurrences
+   *  of `&` in `OrderedConstraint` so that they take the `=:=` result into account.
+   *
+   *  For more info, see the comment in `TypeComparer#distributeAnd`.
+   */
+  final val alignArgsInAnd = false
+
   /** If this flag is set, higher-kinded applications are checked for validity
    */
   final val checkHKApplications = false
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index fca11170243f..744112280766 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -1312,23 +1312,28 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
     case tp1: RefinedType =>
       tp2 match {
         case tp2: RefinedType if tp1.refinedName == tp2.refinedName =>
-          // Given two refinements `T1 { X = S1 }` and `T2 { X = S2 }`, if `S1 =:= S2`
-          // (possibly by instantiating type parameters), rewrite to `T1 & T2 { X = S1 }`.
-          // Otherwise rewrite to `T1 & T2 { X B }` where `B` is the conjunction of
-          // the bounds of `X` in `T1` and `T2`.
-          // The first rule above is contentious because it cuts the constraint set.
-          // But without it we would replace the two aliases by
-          // `T { X >: S1 | S2 <: S1 & S2 }`, which looks weird and is probably
-          // not what's intended.
+          // Given two refinements `T1 { X = S1 }` and `T2 { X = S2 }` rwrite to
+          // `T1 & T2 { X B }` where `B` is the conjunction of the bounds of `X` in `T1` and `T2`.
+          //
+          // However, if `Config.alignArgsInAnd` is set, and both aliases `X = Si` are
+          // nonvariant, and `S1 =:= S2` (possibly by instantiating type parameters),
+          // rewrite instead to `T1 & T2 { X = S1 }`. This rule is contentious because
+          // it cuts the constraint set. On the other hand, without it we would replace
+          // the two aliases by `T { X >: S1 | S2 <: S1 & S2 }`, which looks weird
+          // and is probably not what's intended.
           val rinfo1 = tp1.refinedInfo
           val rinfo2 = tp2.refinedInfo
           val parent = tp1.parent & tp2.parent
-          val rinfo =
-            if (rinfo1.isAlias && rinfo2.isAlias && isSameType(rinfo1, rinfo2))
-              rinfo1
-            else
-              rinfo1 & rinfo2
-          tp1.derivedRefinedType(parent, tp1.refinedName, rinfo)
+
+          def isNonvariantAlias(tp: Type) = tp match {
+            case tp: TypeAlias => tp.variance == 0
+            case _ => false
+          }
+          if (Config.alignArgsInAnd &&
+              isNonvariantAlias(rinfo1) && isNonvariantAlias(rinfo2))
+            isSameType(rinfo1, rinfo2)
+
+          tp1.derivedRefinedType(parent, tp1.refinedName, rinfo1 & rinfo2)
         case _ =>
           NoType
       }

From 1d124e9455ecb56d8fcfa42c4523f70c5cb0a952 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Mon, 27 Feb 2017 11:26:17 +0100
Subject: [PATCH 05/16] New test

The HLists test brought out the unsoundness of alias
rewriting in glbs which is tackled in the last commit.
---
 tests/run/HLists.check |  8 +++++
 tests/run/HLists.scala | 78 ++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 86 insertions(+)
 create mode 100644 tests/run/HLists.check
 create mode 100644 tests/run/HLists.scala

diff --git a/tests/run/HLists.check b/tests/run/HLists.check
new file mode 100644
index 000000000000..53efe30d74e0
--- /dev/null
+++ b/tests/run/HLists.check
@@ -0,0 +1,8 @@
+1
+A
+true
+true
+HCons(1,HCons(A,HCons(true,HNil)))
+1
+A
+true
diff --git a/tests/run/HLists.scala b/tests/run/HLists.scala
new file mode 100644
index 000000000000..eebbcb4cdd14
--- /dev/null
+++ b/tests/run/HLists.scala
@@ -0,0 +1,78 @@
+sealed trait HList
+case class HCons[+HD, +TL](hd: HD, tl: TL) extends HList
+case object HNil extends HList
+
+sealed trait Num
+case object Zero extends Num
+case class Succ[N <: Num](pred: N) extends Num
+
+object Test {
+
+  type HNil = HNil.type
+  type Zero = Zero.type
+
+  trait Concat[Xs <: HList, Ys <: HList, Zs <: HList] {
+    def concat(xs: Xs, ys: Ys): Zs
+  }
+
+  implicit def concatNil[Xs <: HList]: Concat[HNil, Xs, Xs] =
+    new Concat[HNil, Xs, Xs] {
+      def concat(fst: HNil, snd: Xs) = snd
+    }
+
+  implicit def concatCons[X, Xs <: HList, Ys <: HList, Zs <: HList](
+    implicit ev: Concat[Xs, Ys, Zs]
+  ): Concat[HCons[X, Xs], Ys, HCons[X, Zs]] =
+    new Concat[HCons[X, Xs], Ys, HCons[X, Zs]] {
+      def concat(xs: HCons[X, Xs], ys: Ys): HCons[X, Zs] =
+        HCons(xs.hd, ev.concat(xs.tl, ys))
+    }
+
+  def concat[Xs <: HList, Ys <: HList, Zs <: HList](xs: Xs, ys: Ys)(implicit ev: Concat[Xs, Ys, Zs]): Zs =
+    ev.concat(xs, ys)
+
+  val xs = HCons(1, HCons("A", HNil))
+  val ys = HCons(true, HNil)
+  val zs = concat(xs, ys)
+  val zs1: HCons[Int, HCons[String, HCons[Boolean, HNil]]] = zs
+
+  trait At[Xs <: HList, N <: Num] {
+    type Out
+    def at(xs: Xs, n: N): Out
+  }
+
+  implicit def atZero[XZ, Xs <: HList]: At[HCons[XZ, Xs], Zero] { type Out = XZ } =
+    new At[HCons[XZ, Xs], Zero] {
+      type Out = XZ
+      def at(xs: HCons[XZ, Xs], n: Zero) = xs.hd
+    }
+
+  implicit def atSucc[XX, Xs <: HList, N <: Num](
+    implicit ev: At[Xs, N]
+  ): At[HCons[XX, Xs], Succ[N]] { type Out = ev.Out } = new At[HCons[XX, Xs], Succ[N]] {
+    type Out = ev.Out
+    def at(xs: HCons[XX, Xs], n: Succ[N]): Out = ev.at(xs.tl, n.pred)
+  }
+
+  def at[Xs <: HList, N <: Num](xs: Xs, n: N)(
+    implicit ev: At[Xs, N]
+  ): ev.Out = ev.at(xs, n)
+
+  def main(args: Array[String]) = {
+    val ys1 = HCons(1, HNil)
+    println(at(ys1, Zero))
+
+    val ys2 = HCons(1, HCons("A", HNil))
+    val y2 = at(ys2, Succ(Zero))
+    println(at(ys2, Succ(Zero)))
+    val ys3 = HCons(1, HCons("A", HCons(true, HNil)))
+    println(at(ys3, Succ(Succ(Zero))))
+    val ys4 = HCons(1, HCons("A", HCons(true, HCons(1.0, HNil))))
+    println(at(ys4, Succ(Succ(Zero))))
+
+    println(zs1)
+    println(at(zs1, Zero))
+    println(at(zs1, Succ(Zero)))
+    println(at(zs1, Succ(Succ(Zero))))
+  }
+}

From 860fd56990d0e6e24a404c5054e5821b18f7870f Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Mon, 27 Feb 2017 11:26:46 +0100
Subject: [PATCH 06/16] Independent test case, mentioned in #2004.

---
 tests/run/i2004.scala | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 tests/run/i2004.scala

diff --git a/tests/run/i2004.scala b/tests/run/i2004.scala
new file mode 100644
index 000000000000..ff21a6cc98ed
--- /dev/null
+++ b/tests/run/i2004.scala
@@ -0,0 +1,11 @@
+object Test {
+  def main(args: Array[String]) = {
+    val f: (Int, Int, Int, Int, Int, Int, Int, Int, Int, Int, Int, Int, Int, Int, Int, Int,Int, Int, Int, Int, Int, Int, Int, Int, Int, Int) => Int =
+      {
+        (x1: Int, x2: Int, x3: Int, x4: Int, x5: Int, x6: Int, x7: Int, x8: Int, x9: Int, x10: Int, x11: Int, x12: Int, x13: Int, x14: Int, x15: Int, x16: Int, x17: Int, x18: Int, x19: Int, x20: Int, x21: Int, x22: Int, x23: Int, x24: Int, x25: Int, x26: Int) =>
+        x1
+      }
+    println(f.apply(1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1))
+
+  }
+}

From 42fd456acf5535a0ec980d207db8cc9e6abc6110 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Mon, 27 Feb 2017 11:46:19 +0100
Subject: [PATCH 07/16] Re-instantiate depmeth tests

These now compile with the changes to dependent methods, except
for one which is invalid under dotty.
---
 .../pos/depmet_implicit_oopsla_session_simpler.scala           | 3 ++-
 tests/{pending => }/pos/depmet_implicit_norm_ret.scala         | 0
 tests/{pending => }/pos/depmet_implicit_oopsla_session.scala   | 0
 tests/{pending => }/pos/depmet_implicit_oopsla_session_2.scala | 3 +--
 4 files changed, 3 insertions(+), 3 deletions(-)
 rename tests/{pending => disabled}/pos/depmet_implicit_oopsla_session_simpler.scala (90%)
 rename tests/{pending => }/pos/depmet_implicit_norm_ret.scala (100%)
 rename tests/{pending => }/pos/depmet_implicit_oopsla_session.scala (100%)
 rename tests/{pending => }/pos/depmet_implicit_oopsla_session_2.scala (96%)

diff --git a/tests/pending/pos/depmet_implicit_oopsla_session_simpler.scala b/tests/disabled/pos/depmet_implicit_oopsla_session_simpler.scala
similarity index 90%
rename from tests/pending/pos/depmet_implicit_oopsla_session_simpler.scala
rename to tests/disabled/pos/depmet_implicit_oopsla_session_simpler.scala
index fad5eba4009e..8cc6fe754090 100644
--- a/tests/pending/pos/depmet_implicit_oopsla_session_simpler.scala
+++ b/tests/disabled/pos/depmet_implicit_oopsla_session_simpler.scala
@@ -1,3 +1,4 @@
+// Disabled because we now get an unsafe instantiation error
 object Sessions {
   trait Session {
     type Dual <: Session
@@ -40,5 +41,5 @@ object Sessions {
     In{z: Int => System.out.println(z)
     Stop()}}))
 
-  def myRun = addServer run addClient
+  def myRun = addServer run addClient // error: unsafe instantiation
 }
diff --git a/tests/pending/pos/depmet_implicit_norm_ret.scala b/tests/pos/depmet_implicit_norm_ret.scala
similarity index 100%
rename from tests/pending/pos/depmet_implicit_norm_ret.scala
rename to tests/pos/depmet_implicit_norm_ret.scala
diff --git a/tests/pending/pos/depmet_implicit_oopsla_session.scala b/tests/pos/depmet_implicit_oopsla_session.scala
similarity index 100%
rename from tests/pending/pos/depmet_implicit_oopsla_session.scala
rename to tests/pos/depmet_implicit_oopsla_session.scala
diff --git a/tests/pending/pos/depmet_implicit_oopsla_session_2.scala b/tests/pos/depmet_implicit_oopsla_session_2.scala
similarity index 96%
rename from tests/pending/pos/depmet_implicit_oopsla_session_2.scala
rename to tests/pos/depmet_implicit_oopsla_session_2.scala
index 29a76d5cf678..fcf18691abf5 100644
--- a/tests/pending/pos/depmet_implicit_oopsla_session_2.scala
+++ b/tests/pos/depmet_implicit_oopsla_session_2.scala
@@ -1,5 +1,4 @@
 object Sessions {
-  def ?[T <: AnyRef](implicit w: T): w.type = w
 
   // session states
   sealed case class Stop()
@@ -18,7 +17,7 @@ object Sessions {
 
   // friendly interface to the theory
   def runSession[S, D: Session[S]#HasDual](session: S, dual: D) =
-    ?[Session[S]#HasDual[D]].run(session, dual)
+    implicitly[Session[S]#HasDual[D]].run(session, dual)
 
   // facts in the theory:
 

From 76d9748d52360462a7bf7d1a04811f26a310be38 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Mon, 27 Feb 2017 12:41:45 +0100
Subject: [PATCH 08/16] Add check file

---
 tests/run/i2004.check | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 tests/run/i2004.check

diff --git a/tests/run/i2004.check b/tests/run/i2004.check
new file mode 100644
index 000000000000..d00491fd7e5b
--- /dev/null
+++ b/tests/run/i2004.check
@@ -0,0 +1 @@
+1

From f7a50713a3d9fb7a1a4d70e53b037dd7b8bc2d2b Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Tue, 28 Feb 2017 17:22:54 +0100
Subject: [PATCH 09/16] Add non-variant version of HLists for completeness

Variance changes quite a few things for type inference, so
it's good to check a non-variant version as well.
---
 tests/run/HLists-nonvariant.check |   8 ++
 tests/run/HLists-nonvariant.scala | 149 ++++++++++++++++++++++++++++++
 2 files changed, 157 insertions(+)
 create mode 100644 tests/run/HLists-nonvariant.check
 create mode 100644 tests/run/HLists-nonvariant.scala

diff --git a/tests/run/HLists-nonvariant.check b/tests/run/HLists-nonvariant.check
new file mode 100644
index 000000000000..53efe30d74e0
--- /dev/null
+++ b/tests/run/HLists-nonvariant.check
@@ -0,0 +1,8 @@
+1
+A
+true
+true
+HCons(1,HCons(A,HCons(true,HNil)))
+1
+A
+true
diff --git a/tests/run/HLists-nonvariant.scala b/tests/run/HLists-nonvariant.scala
new file mode 100644
index 000000000000..b912f50acae0
--- /dev/null
+++ b/tests/run/HLists-nonvariant.scala
@@ -0,0 +1,149 @@
+sealed trait HList
+case class HCons[HD, TL](hd: HD, tl: TL) extends HList
+case object HNil extends HList
+
+sealed trait Num
+case object Zero extends Num
+case class Succ[N <: Num](pred: N) extends Num
+
+object Test {
+
+  type HNil = HNil.type
+  type Zero = Zero.type
+
+  trait Concat[Xs <: HList, Ys <: HList, Zs <: HList] {
+    def concat(xs: Xs, ys: Ys): Zs
+  }
+
+  implicit def concatNil[Xs <: HList]: Concat[HNil, Xs, Xs] =
+    new Concat[HNil, Xs, Xs] {
+      def concat(fst: HNil, snd: Xs) = snd
+    }
+
+  implicit def concatCons[X, Xs <: HList, Ys <: HList, Zs <: HList](
+    implicit ev: Concat[Xs, Ys, Zs]
+  ): Concat[HCons[X, Xs], Ys, HCons[X, Zs]] =
+    new Concat[HCons[X, Xs], Ys, HCons[X, Zs]] {
+      def concat(xs: HCons[X, Xs], ys: Ys): HCons[X, Zs] =
+        HCons(xs.hd, ev.concat(xs.tl, ys))
+    }
+
+  def concat[Xs <: HList, Ys <: HList, Zs <: HList](xs: Xs, ys: Ys)(implicit ev: Concat[Xs, Ys, Zs]): Zs =
+    ev.concat(xs, ys)
+
+  val xs = HCons(1, HCons("A", HNil))
+  val ys = HCons(true, HNil)
+  val zs = concat(xs, ys)
+  val zs1: HCons[Int, HCons[String, HCons[Boolean, HNil]]] = zs
+
+  trait At[Xs <: HList, N <: Num] {
+    type Out
+    def at(xs: Xs, n: N): Out
+  }
+
+  implicit def atZero[XZ, Xs <: HList]: At[HCons[XZ, Xs], Zero] { type Out = XZ } =
+    new At[HCons[XZ, Xs], Zero] {
+      type Out = XZ
+      def at(xs: HCons[XZ, Xs], n: Zero) = xs.hd
+    }
+
+  implicit def atSucc[XX, Xs <: HList, N <: Num](
+    implicit ev: At[Xs, N]
+  ): At[HCons[XX, Xs], Succ[N]] { type Out = ev.Out } = new At[HCons[XX, Xs], Succ[N]] {
+    type Out = ev.Out
+    def at(xs: HCons[XX, Xs], n: Succ[N]): Out = ev.at(xs.tl, n.pred)
+  }
+
+  def at[Xs <: HList, N <: Num](xs: Xs, n: N)(
+    implicit ev: At[Xs, N]
+  ): ev.Out = ev.at(xs, n)
+
+  def main(args: Array[String]) = {
+    val ys1 = HCons(1, HNil)
+    println(at(ys1, Zero))
+
+    val ys2 = HCons(1, HCons("A", HNil))
+    val y2 = at(ys2, Succ(Zero))
+    println(at(ys2, Succ(Zero)))
+    val ys3 = HCons(1, HCons("A", HCons(true, HNil)))
+    println(at(ys3, Succ(Succ(Zero))))
+    val ys4 = HCons(1, HCons("A", HCons(true, HCons(1.0, HNil))))
+    println(at(ys4, Succ(Succ(Zero))))
+
+    println(zs1)
+    println(at(zs1, Zero))
+    println(at(zs1, Succ(Zero)))
+    println(at(zs1, Succ(Succ(Zero))))
+  }
+}
+
+object TestNonVariant {
+
+  type HNil = HNil.type
+  type Zero = Zero.type
+
+  trait Concat[Xs <: HList, Ys <: HList, Zs <: HList] {
+    def concat(xs: Xs, ys: Ys): Zs
+  }
+
+  implicit def concatNil[Xs <: HList]: Concat[HNil, Xs, Xs] =
+    new Concat[HNil, Xs, Xs] {
+      def concat(fst: HNil, snd: Xs) = snd
+    }
+
+  implicit def concatCons[X, Xs <: HList, Ys <: HList, Zs <: HList](
+    implicit ev: Concat[Xs, Ys, Zs]
+  ): Concat[HCons[X, Xs], Ys, HCons[X, Zs]] =
+    new Concat[HCons[X, Xs], Ys, HCons[X, Zs]] {
+      def concat(xs: HCons[X, Xs], ys: Ys): HCons[X, Zs] =
+        HCons(xs.hd, ev.concat(xs.tl, ys))
+    }
+
+  def concat[Xs <: HList, Ys <: HList, Zs <: HList](xs: Xs, ys: Ys)(implicit ev: Concat[Xs, Ys, Zs]): Zs =
+    ev.concat(xs, ys)
+
+  val xs = HCons(1, HCons("A", HNil))
+  val ys = HCons(true, HNil)
+  val zs = concat(xs, ys)
+  val zs1: HCons[Int, HCons[String, HCons[Boolean, HNil]]] = zs
+
+  trait At[Xs <: HList, N <: Num] {
+    type Out
+    def at(xs: Xs, n: N): Out
+  }
+
+  implicit def atZero[XZ, Xs <: HList]: At[HCons[XZ, Xs], Zero] { type Out = XZ } =
+    new At[HCons[XZ, Xs], Zero] {
+      type Out = XZ
+      def at(xs: HCons[XZ, Xs], n: Zero) = xs.hd
+    }
+
+  implicit def atSucc[XX, Xs <: HList, N <: Num](
+    implicit ev: At[Xs, N]
+  ): At[HCons[XX, Xs], Succ[N]] { type Out = ev.Out } = new At[HCons[XX, Xs], Succ[N]] {
+    type Out = ev.Out
+    def at(xs: HCons[XX, Xs], n: Succ[N]): Out = ev.at(xs.tl, n.pred)
+  }
+
+  def at[Xs <: HList, N <: Num](xs: Xs, n: N)(
+    implicit ev: At[Xs, N]
+  ): ev.Out = ev.at(xs, n)
+
+  def main(args: Array[String]) = {
+    val ys1 = HCons(1, HNil)
+    println(at(ys1, Zero))
+
+    val ys2 = HCons(1, HCons("A", HNil))
+    val y2 = at(ys2, Succ(Zero))
+    println(at(ys2, Succ(Zero)))
+    val ys3 = HCons(1, HCons("A", HCons(true, HNil)))
+    println(at(ys3, Succ(Succ(Zero))))
+    val ys4 = HCons(1, HCons("A", HCons(true, HCons(1.0, HNil))))
+    println(at(ys4, Succ(Succ(Zero))))
+
+    println(zs1)
+    println(at(zs1, Zero))
+    println(at(zs1, Succ(Zero)))
+    println(at(zs1, Succ(Succ(Zero))))
+  }
+}

From e01ca04c28e242a5f602dffc28a1b1eae358ecaf Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Wed, 1 Mar 2017 08:48:45 +0100
Subject: [PATCH 10/16] Drop duplication in test

---
 tests/run/HLists-nonvariant.scala | 71 -------------------------------
 1 file changed, 71 deletions(-)

diff --git a/tests/run/HLists-nonvariant.scala b/tests/run/HLists-nonvariant.scala
index b912f50acae0..a3a639bcd20e 100644
--- a/tests/run/HLists-nonvariant.scala
+++ b/tests/run/HLists-nonvariant.scala
@@ -76,74 +76,3 @@ object Test {
     println(at(zs1, Succ(Succ(Zero))))
   }
 }
-
-object TestNonVariant {
-
-  type HNil = HNil.type
-  type Zero = Zero.type
-
-  trait Concat[Xs <: HList, Ys <: HList, Zs <: HList] {
-    def concat(xs: Xs, ys: Ys): Zs
-  }
-
-  implicit def concatNil[Xs <: HList]: Concat[HNil, Xs, Xs] =
-    new Concat[HNil, Xs, Xs] {
-      def concat(fst: HNil, snd: Xs) = snd
-    }
-
-  implicit def concatCons[X, Xs <: HList, Ys <: HList, Zs <: HList](
-    implicit ev: Concat[Xs, Ys, Zs]
-  ): Concat[HCons[X, Xs], Ys, HCons[X, Zs]] =
-    new Concat[HCons[X, Xs], Ys, HCons[X, Zs]] {
-      def concat(xs: HCons[X, Xs], ys: Ys): HCons[X, Zs] =
-        HCons(xs.hd, ev.concat(xs.tl, ys))
-    }
-
-  def concat[Xs <: HList, Ys <: HList, Zs <: HList](xs: Xs, ys: Ys)(implicit ev: Concat[Xs, Ys, Zs]): Zs =
-    ev.concat(xs, ys)
-
-  val xs = HCons(1, HCons("A", HNil))
-  val ys = HCons(true, HNil)
-  val zs = concat(xs, ys)
-  val zs1: HCons[Int, HCons[String, HCons[Boolean, HNil]]] = zs
-
-  trait At[Xs <: HList, N <: Num] {
-    type Out
-    def at(xs: Xs, n: N): Out
-  }
-
-  implicit def atZero[XZ, Xs <: HList]: At[HCons[XZ, Xs], Zero] { type Out = XZ } =
-    new At[HCons[XZ, Xs], Zero] {
-      type Out = XZ
-      def at(xs: HCons[XZ, Xs], n: Zero) = xs.hd
-    }
-
-  implicit def atSucc[XX, Xs <: HList, N <: Num](
-    implicit ev: At[Xs, N]
-  ): At[HCons[XX, Xs], Succ[N]] { type Out = ev.Out } = new At[HCons[XX, Xs], Succ[N]] {
-    type Out = ev.Out
-    def at(xs: HCons[XX, Xs], n: Succ[N]): Out = ev.at(xs.tl, n.pred)
-  }
-
-  def at[Xs <: HList, N <: Num](xs: Xs, n: N)(
-    implicit ev: At[Xs, N]
-  ): ev.Out = ev.at(xs, n)
-
-  def main(args: Array[String]) = {
-    val ys1 = HCons(1, HNil)
-    println(at(ys1, Zero))
-
-    val ys2 = HCons(1, HCons("A", HNil))
-    val y2 = at(ys2, Succ(Zero))
-    println(at(ys2, Succ(Zero)))
-    val ys3 = HCons(1, HCons("A", HCons(true, HNil)))
-    println(at(ys3, Succ(Succ(Zero))))
-    val ys4 = HCons(1, HCons("A", HCons(true, HCons(1.0, HNil))))
-    println(at(ys4, Succ(Succ(Zero))))
-
-    println(zs1)
-    println(at(zs1, Zero))
-    println(at(zs1, Succ(Zero)))
-    println(at(zs1, Succ(Succ(Zero))))
-  }
-}

From 58b71ca50ded400efa92ac8d92f4378844baaf7d Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Wed, 1 Mar 2017 22:00:41 +0100
Subject: [PATCH 11/16] Fix handling of dependent method types

Need to use fresh PolyParams instead of WildcardTypes
if constraint is committable.
---
 .../dotty/tools/dotc/core/Definitions.scala   |  1 +
 .../src/dotty/tools/dotc/core/StdNames.scala  |  1 +
 .../src/dotty/tools/dotc/core/Types.scala     |  6 -----
 .../dotty/tools/dotc/typer/Applications.scala |  5 ++--
 .../dotty/tools/dotc/typer/ProtoTypes.scala   | 24 +++++++++++++++++--
 5 files changed, 27 insertions(+), 10 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 79e97becb6dd..5a2e260990a9 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -352,6 +352,7 @@ class Definitions {
     enterCompleteClassSymbol(
       ScalaPackageClass, tpnme.Singleton, PureInterfaceCreationFlags | Final,
       List(AnyClass.typeRef), EmptyScope)
+  def SingletonType = SingletonClass.typeRef
 
   lazy val SeqType: TypeRef = ctx.requiredClassRef("scala.collection.Seq")
   def SeqClass(implicit ctx: Context) = SeqType.symbol.asClass
diff --git a/compiler/src/dotty/tools/dotc/core/StdNames.scala b/compiler/src/dotty/tools/dotc/core/StdNames.scala
index 1e36361f8781..0f1b296b1206 100644
--- a/compiler/src/dotty/tools/dotc/core/StdNames.scala
+++ b/compiler/src/dotty/tools/dotc/core/StdNames.scala
@@ -97,6 +97,7 @@ object StdNames {
     val EMPTY: N                      = ""
     val EMPTY_PACKAGE: N              = Names.EMPTY_PACKAGE.toString
     val EVIDENCE_PARAM_PREFIX: N      = "evidence$"
+    val DEP_PARAM_PREFIX              = "<param>"
     val EXCEPTION_RESULT_PREFIX: N    = "exceptionResult"
     val EXPAND_SEPARATOR: N           = "$$"
     val IMPL_CLASS_SUFFIX: N          = "$class"
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 8bd729472376..36e0dfb0ea3c 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -2394,12 +2394,6 @@ object Types {
      */
     def isDependent(implicit ctx: Context): Boolean = dependencyStatus == TrueDeps
 
-    /** The result type where every reference to a parameter is replaced by a Wildcard
-     */
-    def resultTypeApprox(implicit ctx: Context): Type =
-      if (isDependent) resultType.substParams(this, paramTypes.map(Function.const(WildcardType)))
-      else resultType
-
     protected def computeSignature(implicit ctx: Context): Signature =
       resultSignature.prepend(paramTypes, isJava)
 
diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index bca44997df85..e45924f8316a 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -213,8 +213,9 @@ trait Applications extends Compatibility { self: Typer with Dynamic =>
     protected def init() = methType match {
       case methType: MethodType =>
         // apply the result type constraint, unless method type is dependent
+        val resultApprox = resultTypeApprox(methType)
         val savedConstraint = ctx.typerState.constraint
-        if (!constrainResult(methType.resultTypeApprox, resultType))
+        if (!constrainResult(resultApprox, resultType))
           if (ctx.typerState.isCommittable)
             // defer the problem until after the application;
             // it might be healed by an implicit conversion
@@ -1099,7 +1100,7 @@ trait Applications extends Compatibility { self: Typer with Dynamic =>
     /** Drop any implicit parameter section */
     def stripImplicit(tp: Type): Type = tp match {
       case mt: ImplicitMethodType =>
-        mt.resultTypeApprox
+        resultTypeApprox(mt)
       case pt: PolyType =>
         pt.derivedPolyType(pt.paramNames, pt.paramBounds, stripImplicit(pt.resultType))
       case _ =>
diff --git a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
index 4d88fc4f5c10..17f13d7c16a6 100644
--- a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
+++ b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
@@ -57,7 +57,7 @@ object ProtoTypes {
       case pt: FunProto =>
         mt match {
           case mt: MethodType =>
-            constrainResult(mt.resultTypeApprox, pt.resultType)
+            constrainResult(resultTypeApprox(mt), pt.resultType)
           case _ =>
             true
         }
@@ -389,6 +389,26 @@ object ProtoTypes {
   /**  Same as `constrained(pt, EmptyTree)`, but returns just the created polytype */
   def constrained(pt: PolyType)(implicit ctx: Context): PolyType = constrained(pt, EmptyTree)._1
 
+  /** Create a new polyparam that represents a dependent method parameter singleton */
+  def newDepPolyParam(tp: Type)(implicit ctx: Context): PolyParam = {
+    val poly = PolyType(ctx.freshName(nme.DEP_PARAM_PREFIX).toTypeName :: Nil, 0 :: Nil)(
+        pt => TypeBounds.upper(AndType(tp, defn.SingletonType)) :: Nil,
+        pt => defn.AnyType)
+    ctx.typeComparer.addToConstraint(poly, Nil)
+    PolyParam(poly, 0)
+  }
+
+  /** The result type of `mt`, where all references to parameters of `mt` are
+   *  replaced by either wildcards (if typevarsMissContext) or polyparams.
+   */
+  def resultTypeApprox(mt: MethodType)(implicit ctx: Context): Type =
+    if (mt.isDependent) {
+      def replacement(tp: Type) =
+        if (ctx.mode.is(Mode.TypevarsMissContext)) WildcardType else newDepPolyParam(tp)
+      mt.resultType.substParams(mt, mt.paramTypes.map(replacement))
+    }
+    else mt.resultType
+
   /** The normalized form of a type
    *   - unwraps polymorphic types, tracking their parameters in the current constraint
    *   - skips implicit parameters; if result type depends on implicit parameter,
@@ -408,7 +428,7 @@ object ProtoTypes {
     tp.widenSingleton match {
       case poly: PolyType => normalize(constrained(poly).resultType, pt)
       case mt: MethodType =>
-        if (mt.isImplicit) mt.resultTypeApprox
+        if (mt.isImplicit) resultTypeApprox(mt)
         else if (mt.isDependent) tp
         else {
           val rt = normalize(mt.resultType, pt)

From 1d237bb1f0c7aac949b52601e26e96fff0fe4ffd Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Wed, 1 Mar 2017 22:10:17 +0100
Subject: [PATCH 12/16] Make alignArgsInAnd safe and turn it on by default

Turned out hmaps.scala requires the arg alignment to compile.
So we have our first counterexample that we cannot drop this
hack. Now it is made safe in the sense that no constraints get
lost anymore.
---
 .../src/dotty/tools/dotc/config/Config.scala  | 16 ++++---------
 .../dotty/tools/dotc/core/Constraint.scala    |  6 -----
 .../tools/dotc/core/ConstraintHandling.scala  | 24 ++++++++++++++++++-
 .../tools/dotc/core/OrderingConstraint.scala  |  8 -------
 .../dotty/tools/dotc/core/TypeComparer.scala  |  4 ++--
 5 files changed, 30 insertions(+), 28 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/config/Config.scala b/compiler/src/dotty/tools/dotc/config/Config.scala
index 900e5669f9e6..dc56ad8b804f 100644
--- a/compiler/src/dotty/tools/dotc/config/Config.scala
+++ b/compiler/src/dotty/tools/dotc/config/Config.scala
@@ -75,20 +75,14 @@ object Config {
   /** If this flag is set, take the fast path when comparing same-named type-aliases and types */
   final val fastPathForRefinedSubtype = true
 
-  /** If this flag is set, and we compute `T1 { X = S1 }` & `T2 { X = S2 }`,
-   *  try to align the refinements by computing `S1 =:= S2` (which might instantiate type parameters).
-   *  This rule is contentious because it cuts the constraint set. Also, it is
-   *  currently unsound because `&` gets called in computations on a constraint
-   *  itself. If the `=:=` test generates a new constraint, that constraint is then
-   *  out of sync with with the constraint on which the computation is performed.
-   *  The constraint resulting from `=:=` ends up to be thrown away whereas
-   *  its result is used, which is unsound. So if we want to turn this flag on
-   *  permanently instead of just for debugging, we have to refactor occurrences
-   *  of `&` in `OrderedConstraint` so that they take the `=:=` result into account.
+  /** If this flag is set, and we compute `T1 { X = S1 }` & `T2 { X = S2 }` as a new
+   *  upper bound of a constrained parameter, try to align the refinements by computing
+   *  `S1 =:= S2` (which might instantiate type parameters).
+   *  This rule is contentious because it cuts the constraint set.
    *
    *  For more info, see the comment in `TypeComparer#distributeAnd`.
    */
-  final val alignArgsInAnd = false
+  final val alignArgsInAnd = true
 
   /** If this flag is set, higher-kinded applications are checked for validity
    */
diff --git a/compiler/src/dotty/tools/dotc/core/Constraint.scala b/compiler/src/dotty/tools/dotc/core/Constraint.scala
index c99b748b7782..50136a26c2df 100644
--- a/compiler/src/dotty/tools/dotc/core/Constraint.scala
+++ b/compiler/src/dotty/tools/dotc/core/Constraint.scala
@@ -111,12 +111,6 @@ abstract class Constraint extends Showable {
    */
   def replace(param: PolyParam, tp: Type)(implicit ctx: Context): This
 
-  /** Narrow one of the bounds of type parameter `param`
-   *  If `isUpper` is true, ensure that `param <: `bound`, otherwise ensure
-   *  that `param >: bound`.
-   */
-  def narrowBound(param: PolyParam, bound: Type, isUpper: Boolean)(implicit ctx: Context): This
-
   /** Is entry associated with `pt` removable? This is the case if
    *  all type parameters of the entry are associated with type variables
    *  which have their `inst` fields set.
diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
index 3aa20f15b29e..89861f6db128 100644
--- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
+++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
@@ -44,6 +44,13 @@ trait ConstraintHandling {
     try op finally alwaysFluid = saved
   }
 
+  /** If set, align arguments `S1`, `S2`when taking the glb
+   *  `T1 { X = S1 } & T2 { X = S2 }` of a constraint upper bound for some type parameter.
+   *  Aligning means computing `S1 =:= S2` which may change the current constraint.
+   *  See note in TypeComparer#distributeAnd.
+   */
+  protected var homogenizeArgs = false
+
   /** We are currently comparing polytypes. Used as a flag for
    *  optimization: when `false`, no need to do an expensive `pruneLambdaParams`
    */
@@ -64,7 +71,8 @@ trait ConstraintHandling {
       }
       if (Config.checkConstraintsSeparated)
         assert(!occursIn(bound), s"$param occurs in $bound")
-      val c1 = constraint.narrowBound(param, bound, isUpper)
+      val newBound = narrowedBound(param, bound, isUpper)
+      val c1 = constraint.updateEntry(param, newBound)
       (c1 eq constraint) || {
         constraint = c1
         val TypeBounds(lo, hi) = constraint.entry(param)
@@ -72,6 +80,20 @@ trait ConstraintHandling {
       }
     }
 
+  /** Narrow one of the bounds of type parameter `param`
+   *  If `isUpper` is true, ensure that `param <: `bound`, otherwise ensure
+   *  that `param >: bound`.
+   */
+  def narrowedBound(param: PolyParam, bound: Type, isUpper: Boolean)(implicit ctx: Context): TypeBounds = {
+    val oldBounds @ TypeBounds(lo, hi) = constraint.nonParamBounds(param)
+    val saved = homogenizeArgs
+    homogenizeArgs = Config.alignArgsInAnd
+    try
+      if (isUpper) oldBounds.derivedTypeBounds(lo, hi & bound)
+      else oldBounds.derivedTypeBounds(lo | bound, hi)
+    finally homogenizeArgs = saved
+  }
+
   protected def addUpperBound(param: PolyParam, bound: Type): Boolean = {
     def description = i"constraint $param <: $bound to\n$constraint"
     if (bound.isRef(defn.NothingClass) && ctx.typerState.isGlobalCommittable) {
diff --git a/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala b/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
index 72c7a8e51c49..61dd5a445744 100644
--- a/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
+++ b/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
@@ -354,14 +354,6 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
     updateEntry(p1, p1Bounds).replace(p2, p1)
   }
 
-  def narrowBound(param: PolyParam, bound: Type, isUpper: Boolean)(implicit ctx: Context): This = {
-    val oldBounds @ TypeBounds(lo, hi) = nonParamBounds(param)
-    val newBounds =
-      if (isUpper) oldBounds.derivedTypeBounds(lo, hi & bound)
-      else oldBounds.derivedTypeBounds(lo | bound, hi)
-    updateEntry(param, newBounds)
-  }
-
 // ---------- Removals ------------------------------------------------------------
 
   /** A new constraint which is derived from this constraint by removing
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 744112280766..6042cc12ca9b 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -1315,7 +1315,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
           // Given two refinements `T1 { X = S1 }` and `T2 { X = S2 }` rwrite to
           // `T1 & T2 { X B }` where `B` is the conjunction of the bounds of `X` in `T1` and `T2`.
           //
-          // However, if `Config.alignArgsInAnd` is set, and both aliases `X = Si` are
+          // However, if `homogenizeArgs` is set, and both aliases `X = Si` are
           // nonvariant, and `S1 =:= S2` (possibly by instantiating type parameters),
           // rewrite instead to `T1 & T2 { X = S1 }`. This rule is contentious because
           // it cuts the constraint set. On the other hand, without it we would replace
@@ -1329,7 +1329,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
             case tp: TypeAlias => tp.variance == 0
             case _ => false
           }
-          if (Config.alignArgsInAnd &&
+          if (homogenizeArgs &&
               isNonvariantAlias(rinfo1) && isNonvariantAlias(rinfo2))
             isSameType(rinfo1, rinfo2)
 

From 0a839b80aaed89dfd0d84fa3308b72de590171cb Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Wed, 1 Mar 2017 22:13:50 +0100
Subject: [PATCH 13/16] Move depmeth tests back to pending

I believe this worked only accidentally because we matched
more things with wildcards which turned out to be flawed. The test
errors show some funky _#_ types, so not sure whether the tests
are still valid or not. Moved back to pending awaiting further
resolution.
---
 tests/{ => pending}/pos/depmet_implicit_oopsla_session.scala   | 0
 tests/{ => pending}/pos/depmet_implicit_oopsla_session_2.scala | 0
 2 files changed, 0 insertions(+), 0 deletions(-)
 rename tests/{ => pending}/pos/depmet_implicit_oopsla_session.scala (100%)
 rename tests/{ => pending}/pos/depmet_implicit_oopsla_session_2.scala (100%)

diff --git a/tests/pos/depmet_implicit_oopsla_session.scala b/tests/pending/pos/depmet_implicit_oopsla_session.scala
similarity index 100%
rename from tests/pos/depmet_implicit_oopsla_session.scala
rename to tests/pending/pos/depmet_implicit_oopsla_session.scala
diff --git a/tests/pos/depmet_implicit_oopsla_session_2.scala b/tests/pending/pos/depmet_implicit_oopsla_session_2.scala
similarity index 100%
rename from tests/pos/depmet_implicit_oopsla_session_2.scala
rename to tests/pending/pos/depmet_implicit_oopsla_session_2.scala

From 4c6a69ec075de6948f2c82778f6ccf7a30b6bc70 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Thu, 2 Mar 2017 10:16:32 +0100
Subject: [PATCH 14/16] New test: covariant hmaps

Type inference tends to take quite different paths for non-variant
and variant data structures. Since, non-variant hmap has already exposed quite
a few problems, it's good to test it also in the covariant case.
---
 tests/run/hmap-covariant.scala | 97 ++++++++++++++++++++++++++++++++++
 1 file changed, 97 insertions(+)
 create mode 100644 tests/run/hmap-covariant.scala

diff --git a/tests/run/hmap-covariant.scala b/tests/run/hmap-covariant.scala
new file mode 100644
index 000000000000..475cc6ee66fe
--- /dev/null
+++ b/tests/run/hmap-covariant.scala
@@ -0,0 +1,97 @@
+trait Tuple
+case class TCons[+H, +T <: Tuple](h: H, t: T) extends Tuple
+final case object TNil extends Tuple
+
+// Type level natural numbers -------------------------------------------------
+
+sealed trait Nat
+sealed trait Succ[P <: Nat] extends Nat
+sealed trait Zero extends Nat
+
+// Accessor type class to compute the N'th element of an Tuple L --------------
+
+trait At[L <: Tuple, N <: Nat, Out] {
+  def apply(l: L): Out
+}
+
+object At {
+  implicit def caseZero[H, T <: Tuple]: At[H TCons T, Zero, H] =
+    new At[H TCons T, Zero, H] {
+      def apply(l: H TCons T): H = {
+        val (h TCons _) = l
+        h
+      }
+    }
+
+  implicit def caseN[H, T <: Tuple, N <: Nat, O]
+    (implicit a: At[T, N, O]): At[H TCons T, Succ[N], O] =
+      new At[H TCons T, Succ[N], O] {
+        def apply(l: H TCons T): O = {
+          val (_ TCons t) = l
+          a(t)
+        }
+      }
+}
+
+// An HMap is an Tuple with HEntry elements. We are reusing Tuple for it's nice syntax
+
+final case class HEntry[K, V](value: V)
+
+// Accessor type class to compute the element of type K in a HMap L -----------
+
+trait PhantomGet[K, M <: Tuple, I <: Nat] // extends PhantomAny
+
+object PhantomGet {
+  implicit def getHead[K, V, T <: Tuple]
+    : PhantomGet[K, HEntry[K, V] TCons T, Zero] = null
+
+  implicit def getTail[K, H, T <: Tuple, I <: Nat]
+    (implicit t: PhantomGet[K, T, I])
+    : PhantomGet[K, H TCons T, Succ[I]] = null
+}
+
+// Syntax ---------------------------------------------------------------------
+
+object syntax {
+  object hmap {
+    implicit class HmapGet[M <: Tuple](m: M) {
+      def get[K, V, I <: Nat](k: K)
+        (implicit
+          g: PhantomGet[k.type, M, I],
+          a: At[M, I, HEntry[k.type, V]]
+        ): V = a(m).value
+    }
+
+    def --[K, V](key: K, value: V) = HEntry[key.type, V](value)
+  }
+}
+
+object Test {
+  def main(args: Array[String]): Unit = {
+    import syntax.hmap._
+
+    val map1 =
+      TCons(HEntry[K = "name"]("foo"),
+      TCons(HEntry[K = "genre"](true),
+      TCons(HEntry[K = "moneyz"](123),
+      TCons(HEntry[K = "cat"]("bar"),
+      (TNil: TNil.type)))))
+
+    assert(map1.get("name") == "foo")
+    assert(map1.get("genre") == true)
+    assert(map1.get("moneyz") == 123)
+    assert(map1.get("cat") == "bar")
+
+    val map2 =
+      TCons(--("name"  , "foo"),
+      TCons(--("genre" , true),
+      TCons(--("moneyz", 123),
+      TCons(--("cat"   , "bar"),
+      TNil))))
+
+    assert(map2.get("name") == "foo")
+    assert(map2.get("genre") == true)
+    assert(map2.get("moneyz") == 123)
+    assert(map2.get("cat") == "bar")
+  }
+}

From 10d868ce335d1ecbb0a6acb8d4bd804d76edcac9 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Thu, 2 Mar 2017 18:14:24 +0100
Subject: [PATCH 15/16] More tests

and a typo fixed
---
 .../dotty/tools/dotc/core/TypeComparer.scala  |  2 +-
 tests/pos/t5070.scala                         | 23 +++++++++++++++++++
 tests/pos/t5643.scala                         | 19 +++++++++++++++
 3 files changed, 43 insertions(+), 1 deletion(-)
 create mode 100644 tests/pos/t5643.scala

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 6042cc12ca9b..1687422578b5 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -1312,7 +1312,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
     case tp1: RefinedType =>
       tp2 match {
         case tp2: RefinedType if tp1.refinedName == tp2.refinedName =>
-          // Given two refinements `T1 { X = S1 }` and `T2 { X = S2 }` rwrite to
+          // Given two refinements `T1 { X = S1 }` and `T2 { X = S2 }` rewrite to
           // `T1 & T2 { X B }` where `B` is the conjunction of the bounds of `X` in `T1` and `T2`.
           //
           // However, if `homogenizeArgs` is set, and both aliases `X = Si` are
diff --git a/tests/pos/t5070.scala b/tests/pos/t5070.scala
index 410afba148a1..0e5c0ffc06ff 100644
--- a/tests/pos/t5070.scala
+++ b/tests/pos/t5070.scala
@@ -13,3 +13,26 @@ class Test {
 
   implicitly[a.T](b(a)) // works
 }
+
+
+class ImplicitVsTypeAliasTezt {
+
+    class Monad[m[_]] {
+        type For[a] = _For[m, a]
+        implicit def toFor[a](m: m[a]): For[a] = throw new Error("todo") // lookup fails
+//        implicit def toFor[a](m: m[a]): _For[m, a] = throw new Error("todo") // fine.
+    }
+
+    trait _For[m[_], a] {
+        def map[b](p: a => b): m[b]
+    }
+
+    def useMonad[m[_], a](m: m[a])(implicit i: Monad[m]) = {
+        import i._
+
+        // value map is not a member of type parameter m[a]
+        for {
+            x <- m
+        } yield x.toString
+    }
+}
diff --git a/tests/pos/t5643.scala b/tests/pos/t5643.scala
new file mode 100644
index 000000000000..1ce34ba36226
--- /dev/null
+++ b/tests/pos/t5643.scala
@@ -0,0 +1,19 @@
+object TupledEvidenceTest {
+
+  abstract class TupledEvidence[M[_], T0] { type T = T0 }
+
+  implicit def witnessTuple2[M[_], T1, T2](implicit ev1: M[T1], ev2: M[T2]):
+    TupledEvidence[M, (T1, T2)] { type T = (T1, T2) } = sys.error("")
+
+  class GetResult[T]
+
+  implicit val getString: GetResult[String] = new GetResult[String]
+
+  implicit def getTuple[T](implicit w: TupledEvidence[GetResult, T]): GetResult[w.T] = sys.error("")
+
+  def f[T : GetResult] = ""
+
+  f[(String,String)](getTuple[(String, String)])
+
+  f[(String,String)]
+}

From c7f1f35c36593ac9454c8572a59c649610829b6a Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 3 Mar 2017 14:04:26 +0100
Subject: [PATCH 16/16] Adress reviewers comments

---
 compiler/src/dotty/tools/dotc/core/TypeComparer.scala    | 2 +-
 tests/pending/pos/depmet_implicit_oopsla_session_2.scala | 8 +++++++-
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 1687422578b5..e423dd68618b 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -1331,7 +1331,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
           }
           if (homogenizeArgs &&
               isNonvariantAlias(rinfo1) && isNonvariantAlias(rinfo2))
-            isSameType(rinfo1, rinfo2)
+            isSameType(rinfo1, rinfo2) // establish new constraint
 
           tp1.derivedRefinedType(parent, tp1.refinedName, rinfo1 & rinfo2)
         case _ =>
diff --git a/tests/pending/pos/depmet_implicit_oopsla_session_2.scala b/tests/pending/pos/depmet_implicit_oopsla_session_2.scala
index fcf18691abf5..26fa2a4cc736 100644
--- a/tests/pending/pos/depmet_implicit_oopsla_session_2.scala
+++ b/tests/pending/pos/depmet_implicit_oopsla_session_2.scala
@@ -1,4 +1,10 @@
+// Fails on line 70 with: no implicit argument of type Sessions.Session[
+//   |  Sessions.In[Int, Sessions.In[Int, Sessions.Out[Int, Sessions.Stop]]]^
+//   |]#HasDual[Sessions.Out[Int, Sessions.Out[Int, Sessions.In[Int, Sessions.Stop]]]^
+//   |  ] found for parameter evidence$1 of method runSession in object Sessions
+// This could be related to existential types (the # essentially boils down to one).
 object Sessions {
+  def ?[T <: AnyRef](implicit w: T): w.type = w
 
   // session states
   sealed case class Stop()
@@ -17,7 +23,7 @@ object Sessions {
 
   // friendly interface to the theory
   def runSession[S, D: Session[S]#HasDual](session: S, dual: D) =
-    implicitly[Session[S]#HasDual[D]].run(session, dual)
+    ?[Session[S]#HasDual[D]].run(session, dual)
 
   // facts in the theory: