part 2 of the dependent method refactoring: imp...

part 2 of the dependent method refactoring: improved interaction with
implicit search (needed for oopsla paper)

more to come in this area, see e.g. #3346 (stanford edsl stuff)

reopens #13, which wasn't fixed properly before imo, anyway (have a look at -Xprint:typer output before this commit: a type that's not expressible in surface syntax is inferred -- also removed duplicate test file)

closes #3731: co-evolve type alias type symbols when their rhs is
updated and they are referenced by type selections (see typemap)

review by odersky

21 files changed, 533 insertions, 109 deletions

diff --git a/src/compiler/scala/tools/nsc/symtab/Types.scala b/src/compiler/scala/tools/nsc/symtab/Types.scala
index f17b33aa5a..19665715b5 100644
--- a/src/compiler/scala/tools/nsc/symtab/Types.scala
+++ b/src/compiler/scala/tools/nsc/symtab/Types.scala
@@ -807,12 +807,18 @@ trait Types extends reflect.generic.Types { self: SymbolTable =>
      */
     //TODO: use narrow only for modules? (correct? efficiency gain?)
     def findMember(name: Name, excludedFlags: Long, requiredFlags: Long, stableOnly: Boolean): Symbol = {
-      // if this type contains type variables, get rid of them;
+      val suspension = TypeVar.Suspension
+      // if this type contains type variables, put them to sleep for a while -- don't just wipe them out by
+      // replacing them by the corresponding type parameter, as that messes up (e.g.) type variables in type refinements
       // without this, the matchesType call would lead to type variables on both sides
       // of a subtyping/equality judgement, which can lead to recursive types being constructed.
       // See (t0851) for a situation where this happens.
-      if (!this.isGround)
-        return typeVarToOriginMap(this).findMember(name, excludedFlags, requiredFlags, stableOnly)
+      if (!this.isGround) {
+        // make each type var in this type use its original type for comparisons instead of collecting constraints
+        for(tv@TypeVar(_, _) <- this) {
+          suspension suspend tv
+        }
+      }
 
       incCounter(findMemberCount)
       val start = startTimer(findMemberNanos)
@@ -843,6 +849,7 @@ trait Types extends reflect.generic.Types { self: SymbolTable =>
                    (bcs0.head.hasTransOwner(bcs.head)))) {
                 if (name.isTypeName || stableOnly && sym.isStable) {
                   stopTimer(findMemberNanos, start)
+                  suspension.resumeAll
                   return sym
                 } else if (member == NoSymbol) {
                   member = sym
@@ -884,6 +891,7 @@ trait Types extends reflect.generic.Types { self: SymbolTable =>
         excluded = excludedFlags
       } // while (continue)
       stopTimer(findMemberNanos, start)
+      suspension.resumeAll
       if (members eq null) {
         if (member == NoSymbol) incCounter(noMemberCount)
         member
@@ -1729,32 +1737,41 @@ A type's typeSymbol should never be inspected directly.
 
     private var normalized: Type = null
 
+    @inline private def betaReduce: Type = {
+      assert(sym.info.typeParams.length == typeArgs.length, this)
+      // isHKSubType0 introduces synthetic type params so that betaReduce can first apply sym.info to typeArgs before calling asSeenFrom
+      // asSeenFrom then skips synthetic type params, which are used to reduce HO subtyping to first-order subtyping, but which can't be instantiated from the given prefix and class
+      // appliedType(sym.info, typeArgs).asSeenFrom(pre, sym.owner) // this crashes pos/depmet_implicit_tpbetareduce.scala
+      transform(sym.info.resultType)
+    }
+
+    // @M TODO: should not use PolyType, as that's the type of a polymorphic value -- we really want a type *function*
+    // @M: initialize (by sym.info call) needed (see test/files/pos/ticket0137.scala)
+    @inline private def etaExpand: Type = {
+      val tpars = sym.info.typeParams // must go through sym.info for typeParams to initialise symbol
+      PolyType(tpars, typeRef(pre, sym, tpars map (_.tpeHK))) // todo: also beta-reduce?
+    }
+
     override def dealias: Type =
       if (sym.isAliasType && sym.info.typeParams.length == args.length) {
-        val xform = transform(sym.info.resultType)
-        assert(xform ne this, this)
-        xform.dealias
+        betaReduce.dealias
       } else this
 
-    override def remove(clazz: Symbol): Type =
-      if (sym == clazz && !args.isEmpty) args.head else this
-
     def normalize0: Type =
-      if (isHigherKinded) {
-        // @M TODO: should not use PolyType, as that's the type of a polymorphic value -- we really want a type *function*
-        // @M: initialize (by sym.info call) needed (see test/files/pos/ticket0137.scala)
-        PolyType(sym.info.typeParams, typeRef(pre, sym, dummyArgs)) // must go through sym.info for typeParams
-      } else if (sym.isAliasType) { // beta-reduce
-        if(sym.info.typeParams.length == args.length) // don't do partial application
-          transform(sym.info.resultType).normalize // cycles have been checked in typeRef
-        else
-          ErrorType
-      } else if (sym.isRefinementClass) {
-        sym.info.normalize // @MO to AM: OK?
-        //@M I think this is okay, but changeset 12414 (which fixed #1241) re-introduced another bug (#2208)
-        // see typedTypeConstructor in Typers
-      } else {
-        super.normalize
+      if (pre eq WildcardType) WildcardType // arises when argument-dependent types are approximated (see def depoly in implicits)
+      else if (isHigherKinded) etaExpand   // eta-expand, subtyping relies on eta-expansion of higher-kinded types
+      else if (sym.isAliasType && sym.info.typeParams.length == args.length)
+                               betaReduce.normalize // beta-reduce, but don't do partial application -- cycles have been checked in typeRef
+      else if (sym.isRefinementClass)
+                               sym.info.normalize // I think this is okay, but see #1241 (r12414), #2208, and typedTypeConstructor in Typers
+      // else if (args nonEmpty) {
+      //   val argsNorm = args mapConserve (_.dealias)
+      //   if(argsNorm ne args) TypeRef(pre, sym, argsNorm)
+      //   else this
+      // }
+      else {
+        if(sym.isAliasType) ErrorType //println("!!error: "+(pre, sym, sym.info, sym.info.typeParams, args))
+        else super.normalize
       }
 
    // track number of type parameters that we saw when caching normalization,
@@ -2165,6 +2182,22 @@ A type's typeSymbol should never be inspected directly.
   // then, constr became mutable (to support UndoLog, I guess), but pattern-matching returned the original constr0 (a bug)
   // now, pattern-matching returns the most recent constr
   object TypeVar {
+    // encapsulate suspension so we can automatically link the suspension of cloned typevars to their original if this turns out to be necessary
+    def Suspension = new Suspension
+    class Suspension {
+      private val suspended = collection.mutable.HashSet[TypeVar]()
+      def suspend(tv: TypeVar): Unit = {
+        tv.suspended = true
+        suspended += tv
+      }
+      def resumeAll: Unit = {
+        for(tv <- suspended) {
+          tv.suspended = false
+        }
+        suspended.clear
+      }
+    }
+
     def unapply(tv: TypeVar): Some[(Type, TypeConstraint)] = Some((tv.origin, tv.constr))
     def apply(origin: Type, constr: TypeConstraint) = new TypeVar(origin, constr, List(), List())
     def apply(tparam: Symbol) = new TypeVar(tparam.tpeHK, new TypeConstraint, List(), tparam.typeParams) // TODO why not initialise TypeConstraint with bounds of tparam?
@@ -2226,6 +2259,9 @@ A type's typeSymbol should never be inspected directly.
       constr.addHiBound(tp, numBound)
     }
 
+    // ignore subtyping&equality checks while true -- see findMember
+    private[TypeVar] var suspended = false
+
     /** Called from isSubtype0 when a TypeVar is involved in a subtyping check.
      * if isLowerBound is true,
      *   registerBound returns whether this TypeVar could plausibly be a supertype of tp and,
@@ -2258,7 +2294,8 @@ A type's typeSymbol should never be inspected directly.
         if(isLowerBound) isSubArgs(args1, args2, params)
         else             isSubArgs(args2, args1, params)
 
-      if (constr.instValid) // type var is already set
+      if (suspended) checkSubtype(tp, origin)
+      else if (constr.instValid) // type var is already set
         checkSubtype(tp, constr.inst)
       else isRelatable(tp) && {
         if(params.isEmpty) { // type var has kind *
@@ -2283,7 +2320,8 @@ A type's typeSymbol should never be inspected directly.
         if(typeVarLHS) constr.inst =:= tp
         else           tp          =:= constr.inst
 
-      if (constr.instValid) checkIsSameType(tp)
+      if (suspended) tp =:= origin
+      else if (constr.instValid) checkIsSameType(tp)
       else isRelatable(tp) && {
         undoLog record this
 
@@ -2295,6 +2333,20 @@ A type's typeSymbol should never be inspected directly.
       }
     }
 
+    /**
+     * ?A.T =:= tp is rewritten as the constraint ?A <: {type T = tp}
+     *
+     * TODO: make these constraints count (incorporate them into implicit search in applyImplicitArgs)
+     * (T corresponds to @param sym)
+     */
+    def registerTypeSelection(sym: Symbol, tp: Type): Boolean = {
+      val bound = refinedType(List(WildcardType), NoSymbol)
+      val bsym = bound.typeSymbol.newAliasType(NoPosition, sym.name)
+      bsym setInfo tp
+      bound.decls enter bsym
+      registerBound(bound, false)
+    }
+
     /** Can this variable be related in a constraint to type `tp'?
      *  This is not the case if `tp' contains type skolems whose
      *  skolemization level is higher than the level of this variable.
@@ -2332,7 +2384,10 @@ A type's typeSymbol should never be inspected directly.
     override def isVolatile = origin.isVolatile
     override def kind = "TypeVar"
 
-    def cloneInternal = TypeVar(origin, constr cloneInternal, typeArgs, params) // @M TODO: clone args/params?
+    def cloneInternal = {
+      assert(!suspended) // cloning a suspended type variable when it's suspended will cause the clone to never be resumed with the current implementation
+      TypeVar(origin, constr cloneInternal, typeArgs, params) // @M TODO: clone args/params?
+    }
   }
 
   /** A type carrying some annotations. Created by the typechecker
@@ -2505,9 +2560,17 @@ A type's typeSymbol should never be inspected directly.
    *  todo: see how we can clean this up a bit
    */
   def typeRef(pre: Type, sym: Symbol, args: List[Type]): Type = {
-    var sym1 = if (sym.isAbstractType) rebind(pre, sym) else sym
+    def rebindTR(pre: Type, sym: Symbol): Symbol = {
+      if(sym.isAbstractType) rebind(pre, sym) else sym
+         // type alias selections are rebound in TypeMap ("coevolved", actually -- see #3731)
+         // e.g., when type parameters that are referenced by the alias are instantiated in the prefix
+         // see pos/depmet_rebind_typealias
+    }
+    val sym1 = rebindTR(pre, sym)
+
     def transform(tp: Type): Type =
       tp.resultType.asSeenFrom(pre, sym1.owner).instantiateTypeParams(sym1.typeParams, args)
+
     if (sym1.isAliasType && sym1.info.typeParams.length == args.length) {
       if (!sym1.lockOK)
         throw new TypeError("illegal cyclic reference involving " + sym1)
@@ -2524,8 +2587,7 @@ A type's typeSymbol should never be inspected directly.
     } else {
       val pre1 = removeSuper(pre, sym1)
       if (pre1 ne pre) {
-        if (sym1.isAbstractType) sym1 = rebind(pre1, sym1)
-        typeRef(pre1, sym1, args)
+        typeRef(pre1, rebindTR(pre1, sym1), args)
       }
       else if (sym1.isClass && pre.isInstanceOf[CompoundType]) {
         // sharpen prefix so that it is maximal and still contains the class.
@@ -2833,6 +2895,28 @@ A type's typeSymbol should never be inspected directly.
         case _ => false
       }
 
+    // #3731: return sym1 for which holds: pre bound sym.name to sym and pre1 now binds sym.name to sym1, conceptually exactly the same symbol as sym
+    // the selection of sym on pre must be updated to the selection of sym1 on pre1,
+    // since sym's info was probably updated by the TypeMap to yield a new symbol sym1 with transformed info
+    // @returns sym1
+    protected def coevolveSym(pre: Type, pre1: Type, sym: Symbol): Symbol =
+      if((pre ne pre1) && sym.isAliasType) // only need to rebind type aliases here, as typeRef already handles abstract types (they are allowed to be rebound more liberally)
+        (pre, pre1) match {
+          case (RefinedType(_, decls), RefinedType(_, decls1)) => // don't look at parents -- it would be an error to override alias types anyway
+            //val sym1 =
+            decls1.lookup(sym.name)
+//            assert(decls.lookupAll(sym.name).toList.length == 1)
+//            assert(decls1.lookupAll(sym.name).toList.length == 1)
+//            assert(sym1.isAliasType)
+//            println("coevolved "+ sym +" : "+ sym.info +" to "+ sym1 +" : "+ sym1.info +" with "+ pre +" -> "+ pre1)
+//            sym1
+          case _ => // TODO: is there another way a typeref's symbol can refer to a symbol defined in its pre?
+//            val sym1 = pre1.nonPrivateMember(sym.name).suchThat(sym => sym.isAliasType)
+//            println("??coevolve "+ sym +" : "+ sym.info +" to "+ sym1 +" : "+ sym1.info +" with "+ pre +" -> "+ pre1)
+            sym
+        }
+      else sym
+
     /** Map this function over given type */
     def mapOver(tp: Type): Type = tp match {
       case TypeRef(pre, sym, args) =>
@@ -2845,7 +2929,7 @@ A type's typeSymbol should never be inspected directly.
                       else mapOverArgs(args, tparams)
                     }
         if ((pre1 eq pre) && (args1 eq args)) tp
-        else typeRef(pre1, sym, args1)
+        else typeRef(pre1, coevolveSym(pre, pre1, sym), args1)
       case ThisType(_) => tp
       case SingleType(pre, sym) =>
         if (sym.isPackageClass) tp // short path
@@ -3232,6 +3316,7 @@ A type's typeSymbol should never be inspected directly.
 
   /** A base class to compute all substitutions */
   abstract class SubstMap[T](from: List[Symbol], to: List[T]) extends TypeMap {
+    assert(from.length == to.length, "Unsound substitution from "+ from +" to "+ to)
 
     /** Are `sym' and `sym1' the same.
      *  Can be tuned by subclasses.
@@ -4086,9 +4171,14 @@ A type's typeSymbol should never be inspected directly.
       case tr1: TypeRef =>
         tp2 match {
           case tr2: TypeRef =>
-            return equalSymsAndPrefixes(tr1.sym, tr1.pre, tr2.sym, tr2.pre) &&
+            return (equalSymsAndPrefixes(tr1.sym, tr1.pre, tr2.sym, tr2.pre) &&
               ((tp1.isHigherKinded && tp2.isHigherKinded && tp1.normalize =:= tp2.normalize) ||
-               isSameTypes(tr1.args, tr2.args))
+               isSameTypes(tr1.args, tr2.args))) ||
+               ((tr1.pre, tr2.pre) match {
+                 case (tv @ TypeVar(_,_), _) => tv.registerTypeSelection(tr1.sym, tr2)
+                 case (_, tv @ TypeVar(_,_)) => tv.registerTypeSelection(tr2.sym, tr1)
+                 case _ => false
+               })
           case _ =>
         }
       case tt1: ThisType =>
@@ -4312,7 +4402,7 @@ A type's typeSymbol should never be inspected directly.
             res1 <:< res2.substSym(tparams2, tparams1)
           } else { // normalized higher-kinded type
             //@M for an example of why we need to generate fresh symbols, see neg/tcpoly_ticket2101.scala
-            val tpsFresh = cloneSymbols(tparams1) // @M cloneSymbols(tparams2) should be equivalent -- TODO: check
+            val tpsFresh = cloneSymbols(tparams1)
 
             (tparams1 corresponds tparams2)((p1, p2) =>
               p2.info.substSym(tparams2, tpsFresh) <:< p1.info.substSym(tparams1, tpsFresh)) &&   // @PP: corresponds
diff --git a/src/compiler/scala/tools/nsc/typechecker/Implicits.scala b/src/compiler/scala/tools/nsc/typechecker/Implicits.scala
index adcae7d9b1..392223e1e2 100644
--- a/src/compiler/scala/tools/nsc/typechecker/Implicits.scala
+++ b/src/compiler/scala/tools/nsc/typechecker/Implicits.scala
@@ -234,11 +234,14 @@ self: Analyzer =>
     private def tparamsToWildcards(tp: Type, tparams: List[Symbol]) =
       tp.instantiateTypeParams(tparams, tparams map (t => WildcardType))
 
-    /* Map a polytype to one in which all type parameters are replaced by wildcards.
+    /* Map a polytype to one in which all type parameters and argument-dependent types are replaced by wildcards.
+     * Consider `implicit def b(implicit x: A): x.T = error("")`. We need to approximate DebruijnIndex types
+     * when checking whether `b` is a valid implicit, as we haven't even searched a value for the implicit arg `x`,
+     * so we have to approximate (otherwise it is excluded a priori).
      */
     private def depoly(tp: Type): Type = tp match {
-      case PolyType(tparams, restpe) => tparamsToWildcards(restpe, tparams)
-      case _ => tp
+      case PolyType(tparams, restpe) => tparamsToWildcards(ApproximateDependentMap(restpe), tparams)
+      case _ => ApproximateDependentMap(tp)
     }
 
     /** Does type `dtor` dominate type `dted`?
diff --git a/src/compiler/scala/tools/nsc/typechecker/Infer.scala b/src/compiler/scala/tools/nsc/typechecker/Infer.scala
index 687f7cae4b..dff9c3d0c3 100644
--- a/src/compiler/scala/tools/nsc/typechecker/Infer.scala
+++ b/src/compiler/scala/tools/nsc/typechecker/Infer.scala
@@ -171,9 +171,10 @@ trait Infer {
    *  This method seems to be performance critical.
    */
   def normalize(tp: Type): Type = tp match {
-    case mt @ MethodType(params, restpe) if (!restpe.isDependent) =>
-      if (mt.isImplicit) normalize(restpe)
-      else functionType(params map (_.tpe), normalize(restpe))
+    case mt @ MethodType(params, restpe) if mt.isImplicit =>
+      normalize(restpe)
+    case mt @ MethodType(params, restpe) if !restpe.isDependent =>
+      functionType(params map (_.tpe), normalize(restpe))
     case PolyType(List(), restpe) => // nullary method type
       normalize(restpe)
     case ExistentialType(tparams, qtpe) =>
@@ -1073,20 +1074,31 @@ trait Infer {
       substExpr(tree, undetparams, targs, lenientPt)
     }
 
-    /** Substitute free type variables `undetparams; of polymorphic expression
-     *  <code>tree</code>, given prototype <code>pt</code>.
-     *
-     *  @param tree ...
-     *  @param undetparams ...
-     *  @param pt ...
+    /** Infer type arguments for `tparams` of polymorphic expression in `tree`, given prototype `pt`.
      */
     def inferExprInstance(tree: Tree, tparams: List[Symbol], pt: Type, keepNothings: Boolean): List[Symbol] = {
       if (inferInfo)
         println("infer expr instance "+tree+":"+tree.tpe+"\n"+
                 "  tparams = "+tparams+"\n"+
                 "  pt = "+pt)
-      val targs = exprTypeArgs(tparams, tree.tpe, pt)
+      substAdjustedArgs(tree, tparams, pt, exprTypeArgs(tparams, tree.tpe, pt), keepNothings)
+    }
+
+    /** Infer type arguments for `tparams` of polymorphic expression in `tree`, given prototype `pt`.
+     * Use specified type `treeTp` instead of `tree.tp`
+     */
+    def inferExprInstance(tree: Tree, tparams: List[Symbol], pt: Type, treeTp: Type, keepNothings: Boolean): List[Symbol] = {
+      if (inferInfo)
+        println("infer expr instance "+tree+":"+tree.tpe+"\n"+
+                "  tparams = "+tparams+"\n"+
+                "  pt = "+pt)
+      substAdjustedArgs(tree, tparams, pt, exprTypeArgs(tparams, treeTp, pt), keepNothings)
+    }
 
+    /** Substitute tparams to targs, after adjustment by adjustTypeArgs,
+     * return tparams that were not determined
+     */
+    def substAdjustedArgs(tree: Tree, tparams: List[Symbol], pt: Type, targs: List[Type], keepNothings: Boolean): List[Symbol] = {
       if (keepNothings || (targs eq null)) { //@M: adjustTypeArgs fails if targs==null, neg/t0226
         substExpr(tree, tparams, targs, pt)
         List()
diff --git a/src/compiler/scala/tools/nsc/typechecker/Typers.scala b/src/compiler/scala/tools/nsc/typechecker/Typers.scala
index e71ad5475c..f793da0c54 100644
--- a/src/compiler/scala/tools/nsc/typechecker/Typers.scala
+++ b/src/compiler/scala/tools/nsc/typechecker/Typers.scala
@@ -178,18 +178,12 @@ trait Typers { self: Analyzer =>
      */
     def applyImplicitArgs(fun: Tree): Tree = fun.tpe match {
       case MethodType(params, _) =>
-        var positional = true
         val argResultsBuff = new ListBuffer[SearchResult]()
+        val argBuff = new ListBuffer[Tree]()
 
-        // apply the substitutions (undet type param -> type) that were determined
-        // by implicit resolution of implicit arguments on the left of this argument
-        for(param <- params) {
-          var paramTp = param.tpe
-          for(ar <- argResultsBuff)
-            paramTp = paramTp.subst(ar.subst.from, ar.subst.to)
-
-          argResultsBuff += inferImplicit(fun, paramTp, true, false, context)
-        }
+        def mkPositionalArg(argTree: Tree, paramName: Name) = argTree
+        def mkNamedArg(argTree: Tree, paramName: Name) = atPos(argTree.pos)(new AssignOrNamedArg(Ident(paramName), (argTree)))
+        var mkArg: (Tree, Name) => Tree = mkPositionalArg
 
         def errorMessage(paramName: Name, paramTp: Type) =
           paramTp.typeSymbol match {
@@ -200,23 +194,40 @@ trait Typers { self: Analyzer =>
                   else "parameter "+paramName+": ")+paramTp
           }
 
-        val argResults = argResultsBuff.toList
-        val args = argResults.zip(params) flatMap {
-          case (arg, param) =>
-            if (arg != SearchFailure) {
-              if (positional) List(arg.tree)
-              else List(atPos(arg.tree.pos)(new AssignOrNamedArg(Ident(param.name), (arg.tree))))
-            } else {
-              if (!param.hasFlag(DEFAULTPARAM))
-                context.error(fun.pos, errorMessage(param.name, param.tpe))
-              positional = false
-              Nil
-            }
+        // DEPMETTODO: instantiate type vars that depend on earlier implicit args (see adapt (4.1))
+        //
+        // apply the substitutions (undet type param -> type) that were determined
+        // by implicit resolution of implicit arguments on the left of this argument
+        for(param <- params) {
+          var paramTp = param.tpe
+          for(ar <- argResultsBuff)
+            paramTp = paramTp.subst(ar.subst.from, ar.subst.to)
+
+          val res = inferImplicit(fun, paramTp, true, false, context)
+          argResultsBuff += res
+
+          if (res != SearchFailure) {
+            argBuff += mkArg(res.tree, param.name)
+          } else {
+            mkArg = mkNamedArg // don't pass the default argument (if any) here, but start emitting named arguments for the following args
+            if (!param.hasFlag(DEFAULTPARAM))
+              context.error(fun.pos, errorMessage(param.name, param.tpe))
+            /* else {
+             TODO: alternative (to expose implicit search failure more) -->
+             resolve argument, do type inference, keep emitting positional args, infer type params based on default value for arg
+             for (ar <- argResultsBuff) ar.subst traverse defaultVal
+             val targs = exprTypeArgs(context.undetparams, defaultVal.tpe, paramTp)
+             substExpr(tree, tparams, targs, pt)
+            }*/
+          }
         }
-        for (s <- argResults map (_.subst)) {
-          s traverse fun
-          for (arg <- args) s traverse arg
+
+        val args = argBuff.toList
+        for (ar <- argResultsBuff) {
+          ar.subst traverse fun
+          for (arg <- args) ar.subst traverse arg
         }
+
         new ApplyToImplicitArgs(fun, args) setPos fun.pos
       case ErrorType =>
         fun
@@ -819,10 +830,20 @@ trait Typers { self: Analyzer =>
         context.undetparams = context.undetparams ::: tparams1
         adapt(tree1 setType restpe.substSym(tparams, tparams1), mode, pt, original)
       case mt: MethodType if mt.isImplicit && ((mode & (EXPRmode | FUNmode | LHSmode)) == EXPRmode) => // (4.1)
-        if (context.undetparams nonEmpty) // (9) -- should revisit dropped condition `(mode & POLYmode) == 0`
-                                          // dropped so that type args of implicit method are inferred even if polymorphic expressions are allowed
-                                          // needed for implicits in 2.8 collection library -- maybe once #3346 is fixed, we can reinstate the condition?
-          context.undetparams = inferExprInstance(tree, context.extractUndetparams(), pt, false) // false: retract Nothing's that indicate failure, ambiguities in manifests are dealt with in manifestOfType
+        if (context.undetparams nonEmpty) {  // (9) -- should revisit dropped condition `(mode & POLYmode) == 0`
+                                             // dropped so that type args of implicit method are inferred even if polymorphic expressions are allowed
+                                             // needed for implicits in 2.8 collection library -- maybe once #3346 is fixed, we can reinstate the condition?
+          context.undetparams =
+            inferExprInstance(tree, context.extractUndetparams(), pt,
+                    // approximate types that depend on arguments since dependency on implicit argument is like dependency on type parameter
+                    if(settings.YdepMethTpes.value) mt.approximate else mt,
+                    // if we are looking for a manifest, instantiate type to Nothing anyway,
+                    // as we would get ambiguity errors otherwise. Example
+                    // Looking for a manifest of Nil: This mas many potential types,
+                    // so we need to instantiate to minimal type List[Nothing].
+                    false) // false: retract Nothing's that indicate failure, ambiguities in manifests are dealt with in manifestOfType
+        }
+
         val typer1 = constrTyperIf(treeInfo.isSelfOrSuperConstrCall(tree))
         if (original != EmptyTree && pt != WildcardType)
           typer1.silent(tpr => tpr.typed(tpr.applyImplicitArgs(tree), mode, pt)) match {
diff --git a/test/files/pos/bug0013.scala b/test/files/pos/bug0013.scala
deleted file mode 100644
index 999a2ab61c..0000000000
--- a/test/files/pos/bug0013.scala
+++ /dev/null
@@ -1,31 +0,0 @@
-// covariant linked list
-abstract class M { self =>
-
-    type T
-    final type selfType = M {type T <: self.T}
-    type actualSelfType >: self.type <: selfType
-
-    def next: selfType
-
-    // I don't understand why this doesn't compile, but that's a separate matter
-    // error: method all2 cannot be accessed in M.this.selfType
-    // because its instance type => Stream[M{type T <: M.this.selfType#T}]
-    // contains a malformed type: M.this.selfType#T
-    // def all2: Stream[M {type T <: self.T}] = Stream.cons(self: actualSelfType, next.all2)
-
-
-    // compiles successfully
-    // def all3: Stream[M {type T <: self.T}] = all3Impl(self: actualSelfType)
-    // private def all3Impl(first: M {type T <: self.T}): Stream[M {type T <: self.T}] = Stream.cons(first, all3Impl(first.next))
-
-
-
-    def all4: Stream[M {type T <: self.T}] = Unrelated.all4Impl[T](self: actualSelfType)
-}
-
-object Unrelated {
-    def all4Impl[U](first: M {type T <: U}): Stream[M {type T <: U}] = Stream.cons(first, all4Impl(first.next))
-
-    // compiles successfully
-    // def all4Impl[U](first: M {type T <: U}): Stream[M {type T <: U}] = Stream.cons(first, all4Impl[U](first.next))
-}
\ No newline at end of file
diff --git a/test/files/pos/bug1279a.scala b/test/files/pos/bug1279a.scala
index 7568d3afcd..9212b583d4 100644
--- a/test/files/pos/bug1279a.scala
+++ b/test/files/pos/bug1279a.scala
@@ -1,3 +1,4 @@
+// see #13
 // providing the type parameter in the recursive call to all4Impl
 // avoids the problem
 
@@ -31,8 +32,9 @@ abstract class M
 
 object Unrelated
 {
-   def all4Impl[U](first: M {type T <: U}): Stream[M {type T <: U}] = Stream.cons(first, all4Impl(first.next))
+  // TODO!!! fix this bug for real, it compiles successfully, but weird types are inferred
+   // def all4Impl[U](first: M {type T <: U}): Stream[M {type T <: U}] = Stream.cons(first, all4Impl(first.next))
 
 // compiles successfully
-//      def all4Impl[U](first: M {type T <: U}): Stream[M {type T <: U}] = Stream.cons(first, all4Impl[U](first.next))
+     def all4Impl[U](first: M {type T <: U}): Stream[M {type T <: U}] = Stream.cons(first, all4Impl[U](first.next))
 }
diff --git a/test/files/pos/depmet_implicit_chaining_zw.flags b/test/files/pos/depmet_implicit_chaining_zw.flags
new file mode 100644
index 0000000000..1c26b24745
--- /dev/null
+++ b/test/files/pos/depmet_implicit_chaining_zw.flags
@@ -0,0 +1 @@
+-Ydependent-method-types
\ No newline at end of file
diff --git a/test/files/pos/depmet_implicit_chaining_zw.scala b/test/files/pos/depmet_implicit_chaining_zw.scala
new file mode 100644
index 0000000000..e3a145ab38
--- /dev/null
+++ b/test/files/pos/depmet_implicit_chaining_zw.scala
@@ -0,0 +1,28 @@
+trait Zero
+trait Succ[N]
+
+trait ZipWith[N, S] {
+  type T
+  val x: T = error("")
+}
+
+object ZipWith {
+  implicit def ZeroZipWith[S] = new ZipWith[Zero, S] {
+    type T = Stream[S]
+  }
+
+  implicit def SuccZipWith[N, S, R](implicit zWith : ZipWith[N, R]) = new ZipWith[Succ[N], S => R] {
+    type T = Stream[S] => zWith.T // dependent types replace the associated types functionality
+  }
+
+  // can't use implicitly[ZipWith[Succ[Succ[Zero]], Int => String => Boolean]],
+  // since that will chop of the {type T = ... } refinement in adapt (pt = ZipWith[Succ[Succ[Zero]], Int => String => Boolean])
+  // this works
+  // def zipWith(implicit zw: ZipWith[Succ[Succ[Zero]], Int => String => Boolean]): zw.T = zw.x
+  // thus, I present ?: implicitly on steroids!
+  def ?[T <: AnyRef](implicit w: T): w.type = w
+
+  type _2 = Succ[Succ[Zero]]
+  val zw = ?[ZipWith[_2, Int => String => Boolean]].x // : Stream[Int] => Stream[String] => Stream[Boolean]
+  // val zw = implicitly[ZipWith[Succ[Succ[Zero]], Int => String => Boolean]{type T = Stream[Int] => Stream[String] => Stream[Boolean]}].x
+}
\ No newline at end of file
diff --git a/test/files/pos/depmet_implicit_norm_ret.flags b/test/files/pos/depmet_implicit_norm_ret.flags
new file mode 100644
index 0000000000..1c26b24745
--- /dev/null
+++ b/test/files/pos/depmet_implicit_norm_ret.flags
@@ -0,0 +1 @@
+-Ydependent-method-types
\ No newline at end of file
diff --git a/test/files/pos/depmet_implicit_norm_ret.scala b/test/files/pos/depmet_implicit_norm_ret.scala
new file mode 100644
index 0000000000..4cdb2931c6
--- /dev/null
+++ b/test/files/pos/depmet_implicit_norm_ret.scala
@@ -0,0 +1,29 @@
+object Test{
+  def ?[S <: AnyRef](implicit w : S) : w.type = w
+
+  // fallback, lower priority (overloading rules apply: pick alternative in subclass lowest in subtyping lattice)
+  class ZipWithDefault {
+    implicit def ZeroZipWith[S] = new ZipWith[S] {
+      type T = Stream[S]
+    }
+  }
+
+  object ZipWith extends ZipWithDefault {
+    // def apply[S: ZipWith](s : S) = ?[ZipWith[S]].zipWith(s) // TODO: bug return type should be inferred
+    def apply[S](s : S)(implicit zw: ZipWith[S]): zw.T = zw.zipWith(s)
+
+    implicit def SuccZipWith[S,R](implicit zWith : ZipWith[R]) = new ZipWith[S => R] {
+      type T = Stream[S] => zWith.T // dependent types replace the associated types functionality
+    }
+  }
+
+  trait ZipWith[S] {
+    type T
+    def zipWith : S => T = error("")
+  }
+
+  // bug: inferred return type = (Stream[A]) => java.lang.Object with Test.ZipWith[B]{type T = Stream[B]}#T
+  // this seems incompatible with vvvvvvvvvvvvvvvvvvvvvv   -- #3731
+  def map[A,B](f : A => B)   /* : Stream[A] => Stream[B]*/ = ZipWith(f)
+  val tst: Stream[Int] = map{x: String => x.length}(Stream("a"))
+}
\ No newline at end of file
diff --git a/test/files/pos/depmet_implicit_oopsla_session.flags b/test/files/pos/depmet_implicit_oopsla_session.flags
new file mode 100644
index 0000000000..1c26b24745
--- /dev/null
+++ b/test/files/pos/depmet_implicit_oopsla_session.flags
@@ -0,0 +1 @@
+-Ydependent-method-types
\ No newline at end of file
diff --git a/test/files/pos/depmet_implicit_oopsla_session.scala b/test/files/pos/depmet_implicit_oopsla_session.scala
new file mode 100644
index 0000000000..21588a56ad
--- /dev/null
+++ b/test/files/pos/depmet_implicit_oopsla_session.scala
@@ -0,0 +1,63 @@
+object Sessions {
+  trait Session[This] {
+    type Dual
+    type HasDual[D] = Session[This]{type Dual=D}
+    def run(p: This, dp: Dual): Unit
+  }
+
+  implicit object StopSession extends Session[Stop] {
+    type Dual = Stop
+
+    def run(p: Stop, dp: Stop): Unit = {}
+  }
+
+  implicit def InDual[A, B](implicit sessionDIn: Session[B]) =
+    new Session[In[A, B]] {
+      type Dual = Out[A, sessionDIn.Dual]
+
+      def run(p: In[A, B], dp: Dual): Unit =
+        sessionDIn.run(p.func(dp.x), dp.y)
+  }
+
+  implicit def OutDual[A, B](implicit sessionDOut: Session[B]) =
+    new Session[Out[A, B]] {
+     type Dual = In[A, sessionDOut.Dual]
+
+     def run(p: Out[A, B], dp: Dual): Unit =
+       sessionDOut.run(p.y, dp.func(p.x))
+  }
+
+  sealed case class Stop()
+  sealed case class In[-A, +B](func: A => B)
+  sealed case class Out[+A, +B](x: A, y: B)
+
+  def addServer =
+    In{x: Int =>
+    In{y: Int => System.out.println("Thinking")
+    Out(x+y,
+    Stop())}}
+
+  def addClient =
+    Out(3,
+    Out(4, { System.out.println("Waiting")
+    In{z: Int => System.out.println(z)
+    Stop()}}))
+
+  def runSession[S, D: Session[S]#HasDual](p: S, dp: D) =
+    implicitly[Session[S]#HasDual[D]].run(p, dp)
+
+  // def runSession[S, D](p: S, dp: D)(implicit s: Session[S]#HasDual[D]) =
+  //   s.run(p, dp)
+  //
+  // def runSession[S, D](p: S, dp: D)(implicit s: Session[S]{type Dual=D}) =
+  //   s.run(p, dp)
+
+  // TODO: can we relax the ordering restrictions on dependencies so that we can use
+  // def runSession[S](p: S, dp: s.Dual)(implicit s: Session[S]) =
+  //   s.run(p, dp)
+  // to emphasise similarity of type parameters and implicit arguments:
+  // def runSession[S][val s: Session[S]](p: S, dp: s.Dual) =
+  //   s.run(p, dp)
+
+  def myRun = runSession(addServer, addClient)
+}
\ No newline at end of file
diff --git a/test/files/pos/depmet_implicit_oopsla_session_2.flags b/test/files/pos/depmet_implicit_oopsla_session_2.flags
new file mode 100644
index 0000000000..1c26b24745
--- /dev/null
+++ b/test/files/pos/depmet_implicit_oopsla_session_2.flags
@@ -0,0 +1 @@
+-Ydependent-method-types
\ No newline at end of file
diff --git a/test/files/pos/depmet_implicit_oopsla_session_2.scala b/test/files/pos/depmet_implicit_oopsla_session_2.scala
new file mode 100644
index 0000000000..5c3b78e3f5
--- /dev/null
+++ b/test/files/pos/depmet_implicit_oopsla_session_2.scala
@@ -0,0 +1,87 @@
+object Sessions {
+  def ?[T <: AnyRef](implicit w: T): w.type = w
+
+  // session states
+  sealed case class Stop()
+  sealed case class In[-Data, +Cont](recv: Data => Cont)
+  sealed case class Out[+Data, +Cont](data: Data, cont: Cont)
+
+  // the type theory of communicating sessions:
+
+  // an instance of type Session[S]{type Dual=D} is evidence that S and D are duals
+  // such a value witnesses this fact by describing how to compose an instance of S with an instance of D (through the run method)
+  trait Session[S] { type Self = S
+    type Dual
+    type HasDual[D] = Session[Self]{type Dual=D}
+    def run(self: Self, dual: Dual): Unit
+  }
+
+  // friendly interface to the theory
+  def runSession[S, D: Session[S]#HasDual](session: S, dual: D) =
+    ?[Session[S]#HasDual[D]].run(session, dual)
+
+  // facts in the theory:
+
+  // ------------------------[StopDual]
+  // Stop is the dual of Stop
+  implicit object StopDual extends Session[Stop] {
+    type Dual = Stop
+
+    def run(self: Self, dual: Dual): Unit = {}
+  }
+
+  //            CD is the dual of Cont
+  // -------------------------------------------[InDual]
+  // Out[Data, CD] is the dual of In[Data, Cont]
+  implicit def InDual[Data, Cont](implicit cont: Session[Cont]) = new Session[In[Data, Cont]] {
+    type Dual = Out[Data, cont.Dual]
+
+    def run(self: Self, dual: Dual): Unit =
+      cont.run(self.recv(dual.data), dual.cont)
+  }
+
+  //            CD is the dual of Cont
+  // -------------------------------------------[OutDual]
+  // In[Data, CD] is the dual of Out[Data, Cont]
+  implicit def OutDual[Data, Cont](implicit cont: Session[Cont]) = new Session[Out[Data, Cont]] {
+    type Dual = In[Data, cont.Dual]
+
+    def run(self: Self, dual: Dual): Unit =
+      cont.run(self.cont, dual.recv(self.data))
+  }
+
+  // a concrete session
+  def addServer =
+    In{x: Int =>
+    In{y: Int => System.out.println("Thinking")
+    Out(x+y,
+    Stop())}}
+
+  def addClient =
+    Out(3,
+    Out(4, { System.out.println("Waiting")
+    In{z: Int => System.out.println(z)
+    Stop()}}))
+
+  def myRun = runSession(addServer, addClient)
+}
+
+/* future improvements:
+
+
+  // def runSession[S, D](p: S, dp: D)(implicit s: Session[S]#HasDual[D]) =
+  //   s.run(p, dp)
+  //
+  // def runSession[S, D](p: S, dp: D)(implicit s: Session[S]{type Dual=D}) =
+  //   s.run(p, dp)
+
+  // TODO: can we relax the ordering restrictions on dependencies so that we can write
+  //  one possibility: graph of dependencies between arguments must be acyclic
+  // def runSession[S](p: S, dp: s.Dual)(implicit s: Session[S]) =
+  //   s.run(p, dp)
+  // to emphasise similarity of type parameters and implicit arguments:
+  // def runSession[S][val s: Session[S]](p: S, dp: s.Dual) =
+  //   s.run(p, dp)
+
+
+*/
\ No newline at end of file
diff --git a/test/files/pos/depmet_implicit_oopsla_session_simpler.flags b/test/files/pos/depmet_implicit_oopsla_session_simpler.flags
new file mode 100644
index 0000000000..1c26b24745
--- /dev/null
+++ b/test/files/pos/depmet_implicit_oopsla_session_simpler.flags
@@ -0,0 +1 @@
+-Ydependent-method-types
\ No newline at end of file
diff --git a/test/files/pos/depmet_implicit_oopsla_session_simpler.scala b/test/files/pos/depmet_implicit_oopsla_session_simpler.scala
new file mode 100644
index 0000000000..37bc0958d3
--- /dev/null
+++ b/test/files/pos/depmet_implicit_oopsla_session_simpler.scala
@@ -0,0 +1,44 @@
+object Sessions {
+  trait Session {
+    type Dual <: Session
+
+    def run(dp: Dual): Unit
+  }
+
+  sealed case class Stop extends Session {
+    type Dual = Stop
+
+    def run(dp: Dual): Unit = {}
+  }
+
+  // can't write B <: Session{type Dual = BDual} due to limitations in type inference algorithm
+  // (type variables cannot occur on both sides of <:)
+  // using B#Dual instead of BDual is too imprecise, since it is disconnected from the actual argument that is passed for B
+  // would be nice if we could introduce a universal quantification over BDual that is not part of the
+  // type parameter list
+  sealed case class In[A, B <: Session, BDual <: Session](recv: A => B)(implicit dual: B <:< Session{type Dual=BDual}) extends Session {
+    type Dual = Out[A, BDual]
+
+    def run(dp: Dual): Unit = recv(dp.data) run dp.cont
+  }
+
+  sealed case class Out[A, B <: Session](data: A, cont: B) extends Session {
+     type Dual = In[A, cont.Dual, cont.Dual#Dual]
+
+     def run(dp: Dual): Unit = cont run dp.recv(data)
+  }
+
+  def addServer =
+    In{x: Int =>
+    In{y: Int => System.out.println("Thinking")
+    Out(x+y,
+    Stop())}}
+
+  def addClient =
+    Out(3,
+    Out(4, { System.out.println("Waiting")
+    In{z: Int => System.out.println(z)
+    Stop()}}))
+
+  def myRun = addServer run addClient
+}
diff --git a/test/files/pos/depmet_implicit_oopsla_zipwith.flags b/test/files/pos/depmet_implicit_oopsla_zipwith.flags
new file mode 100644
index 0000000000..1c26b24745
--- /dev/null
+++ b/test/files/pos/depmet_implicit_oopsla_zipwith.flags
@@ -0,0 +1 @@
+-Ydependent-method-types
\ No newline at end of file
diff --git a/test/files/pos/depmet_implicit_oopsla_zipwith.scala b/test/files/pos/depmet_implicit_oopsla_zipwith.scala
new file mode 100644
index 0000000000..c76d02c1ae
--- /dev/null
+++ b/test/files/pos/depmet_implicit_oopsla_zipwith.scala
@@ -0,0 +1,44 @@
+case class Zero()
+case class Succ[N](x: N)
+import Stream.{cons, continually}
+
+trait ZipWith[N, S] {
+  type T
+
+  def manyApp: N => Stream[S] => T
+  def zipWith: N => S => T = n => f => manyApp(n)(continually(f))
+}
+object ZipWith {
+  implicit def ZeroZipWith[S] = new ZipWith[Zero, S] {
+    type T = Stream[S]
+
+    def manyApp = n => xs => xs
+  }
+
+  implicit def SuccZipWith[N, S, R](implicit zw: ZipWith[N, R]) =
+    new ZipWith[Succ[N],S => R] {
+      type T = Stream[S] => zw.T
+
+      def zapp[A, B](xs: Stream[A => B], ys: Stream[A]): Stream[B] = (xs, ys) match {
+        case (cons(f, fs), cons(s, ss)) => cons(f(s),zapp(fs, ss))
+        case (_, _) => Stream.empty
+      }
+
+      def manyApp = n => xs => ss => n match {
+        case Succ(i) => zw.manyApp(i)(zapp(xs, ss))
+      }
+    }
+}
+
+object Test {
+  def zWith[N, S](n: N, s: S)(implicit zw: ZipWith[N, S]): zw.T = zw.zipWith(n)(s)
+
+  def zipWith0: Stream[Int] = zWith(Zero(),0)
+
+// (Stream[A]) => java.lang.Object with ZipWith[Zero,B]{type T = Stream[B]}#T
+// should normalise to: Stream[A] => Stream[B]
+  def map[A, B](f: A => B) = zWith(Succ(Zero()),f)
+
+  def zipWith3[A, B, C, D](f: A => B => C => D) = //: Stream[A] => Stream[B] => Stream[C] => Stream[D] = // BUG why do we need a return type?
+    zWith(Succ(Succ(Succ(Zero()))),f)
+}
\ No newline at end of file
diff --git a/test/files/pos/depmet_implicit_tpbetareduce.flags b/test/files/pos/depmet_implicit_tpbetareduce.flags
new file mode 100644
index 0000000000..1c26b24745
--- /dev/null
+++ b/test/files/pos/depmet_implicit_tpbetareduce.flags
@@ -0,0 +1 @@
+-Ydependent-method-types
\ No newline at end of file
diff --git a/test/files/pos/depmet_implicit_tpbetareduce.scala b/test/files/pos/depmet_implicit_tpbetareduce.scala
new file mode 100644
index 0000000000..35d260683b
--- /dev/null
+++ b/test/files/pos/depmet_implicit_tpbetareduce.scala
@@ -0,0 +1,12 @@
+trait HOSeq {
+  trait Accumulator[+coll[x], elT]
+  trait Iterable[+t] {
+    type m[+x]
+    def accumulator[t]: Accumulator[m, t]
+  }
+  implicit def listAccumulator[elT]: Accumulator[List, elT] = new Accumulator[List, elT] {}
+  trait List[+t] extends Iterable[t] {
+    type m[+x] = List[x]
+    def accumulator[t]: Accumulator[List, t] = listAccumulator[t]
+  }
+}
\ No newline at end of file
diff --git a/test/files/pos/t3731.scala b/test/files/pos/t3731.scala
new file mode 100644
index 0000000000..9a617012b3
--- /dev/null
+++ b/test/files/pos/t3731.scala
@@ -0,0 +1,13 @@
+object Test{
+  trait ZW[S]{type T}
+  def ZipWith[S, M <: ZW[S]]: M#T = error("ZW")
+
+  // meh must be parameterised to force an asSeenFrom that
+  // duplicates the refinement in the TR's pre without updating its sym
+  def meh[A] = ZipWith[A, ZW[A]{type T=Stream[A]}]
+
+  meh[Int]: Stream[Int]
+}
+// debugging output in coevolveSym should say:
+// coevolved type T#11029 : Stream#3234[A#9228] to type T#11277 : Stream#3234[A#9227]
+// with Test.ZW#9219[A#9228]{type T#11029 = Stream#3234[A#9228]} -> Test.ZW#9219[A#9227]{type T#11277 = Stream#3234[A#9227]}