Merge pull request #2045 from dotty-staging/fix-hlist-hmap

Fix type inference for HLists and HMaps

23 files changed, 430 insertions, 64 deletions

diff --git a/compiler/src/dotty/tools/dotc/config/Config.scala b/compiler/src/dotty/tools/dotc/config/Config.scala
index 119af9483..dc56ad8b8 100644
--- a/compiler/src/dotty/tools/dotc/config/Config.scala
+++ b/compiler/src/dotty/tools/dotc/config/Config.scala
@@ -75,6 +75,15 @@ 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 }` 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 = true
+
   /** 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/Constraint.scala b/compiler/src/dotty/tools/dotc/core/Constraint.scala
index c99b748b7..50136a26c 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 b3c50fb71..2a1f4ee6e 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/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 1be47c1da..4d4350f98 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -355,6 +355,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/OrderingConstraint.scala b/compiler/src/dotty/tools/dotc/core/OrderingConstraint.scala
index 72c7a8e51..61dd5a445 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/StdNames.scala b/compiler/src/dotty/tools/dotc/core/StdNames.scala
index 766e3733f..5b7dc3d1d 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/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index b97dfe684..b61fccf31 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -1300,23 +1300,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 }` 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
+          // 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 (homogenizeArgs &&
+              isNonvariantAlias(rinfo1) && isNonvariantAlias(rinfo2))
+            isSameType(rinfo1, rinfo2) // establish new constraint
+
+          tp1.derivedRefinedType(parent, tp1.refinedName, rinfo1 & rinfo2)
         case _ =>
           NoType
       }
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index cb462af45..546473b68 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -1681,7 +1681,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.
      */
diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
index 0d1068b8c..6af902d1b 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/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index 222717e7e..a65ef00cc 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -213,16 +213,15 @@ 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 resultApprox = resultTypeApprox(methType)
+        val savedConstraint = ctx.typerState.constraint
+        if (!constrainResult(resultApprox, 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 +1099,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 =>
+        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 d666b563e..17f13d7c1 100644
--- a/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
+++ b/compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala
@@ -57,19 +57,14 @@ object ProtoTypes {
       case pt: FunProto =>
         mt match {
           case mt: MethodType =>
-            mt.isDependent || constrainResult(mt.resultType, pt.resultType)
+            constrainResult(resultTypeApprox(mt), pt.resultType)
           case _ =>
             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
     }
@@ -394,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,
@@ -413,22 +428,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)
+        if (mt.isImplicit) resultTypeApprox(mt)
+        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
     }
diff --git a/tests/pending/pos/depmet_implicit_oopsla_session_simpler.scala b/tests/disabled/pos/depmet_implicit_oopsla_session_simpler.scala
index fad5eba40..8cc6fe754 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_oopsla_session_2.scala b/tests/pending/pos/depmet_implicit_oopsla_session_2.scala
index 29a76d5cf..26fa2a4cc 100644
--- a/tests/pending/pos/depmet_implicit_oopsla_session_2.scala
+++ b/tests/pending/pos/depmet_implicit_oopsla_session_2.scala
@@ -1,3 +1,8 @@
+// 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
 
diff --git a/tests/pending/pos/depmet_implicit_norm_ret.scala b/tests/pos/depmet_implicit_norm_ret.scala
index 42bfb9fe1..42bfb9fe1 100644
--- a/tests/pending/pos/depmet_implicit_norm_ret.scala
+++ b/tests/pos/depmet_implicit_norm_ret.scala
diff --git a/tests/pos/t5070.scala b/tests/pos/t5070.scala
index 410afba14..0e5c0ffc0 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 000000000..1ce34ba36
--- /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)]
+}
diff --git a/tests/run/HLists-nonvariant.check b/tests/run/HLists-nonvariant.check
new file mode 100644
index 000000000..53efe30d7
--- /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 000000000..a3a639bcd
--- /dev/null
+++ b/tests/run/HLists-nonvariant.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))))
+  }
+}
diff --git a/tests/run/HLists.check b/tests/run/HLists.check
new file mode 100644
index 000000000..53efe30d7
--- /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 000000000..eebbcb4cd
--- /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))))
+  }
+}
diff --git a/tests/run/hmap-covariant.scala b/tests/run/hmap-covariant.scala
new file mode 100644
index 000000000..475cc6ee6
--- /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")
+  }
+}
diff --git a/tests/run/i2004.check b/tests/run/i2004.check
new file mode 100644
index 000000000..d00491fd7
--- /dev/null
+++ b/tests/run/i2004.check
@@ -0,0 +1 @@
+1
diff --git a/tests/run/i2004.scala b/tests/run/i2004.scala
new file mode 100644
index 000000000..ff21a6cc9
--- /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))
+
+  }
+}