diff --git a/library/collection/List.scala b/library/collection/List.scala
index 521a573a1f811e21d1a33ca583305b706eb4d8b0..26355f8e7ac19ab154e33d3830894dc9ad93d9de 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -287,6 +287,11 @@ sealed abstract class List[T] {
 
 }
 
+@ignore
+object List {
+  def apply[T](elems: T*): List[T] = ???
+}
+
 @library
 object ListOps {
   def flatten[T](ls: List[List[T]]): List[T] = ls match {
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 559dc93a0e4a2140b368ba893c506d746ffa5648..00f039d29373605df84d95e1d3bad3e154d9ffe4 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -164,6 +164,17 @@ trait ASTExtractors {
       }
     }
 
+    object ExListLiteral {
+      def unapply(tree: Apply): Option[(Type, List[Tree])] = tree  match {
+        case Apply(
+              TypeApply(ExSelected("leon", "collection", "List", "apply"), tpe :: Nil),
+              args) =>
+          Some((tpe.tpe, args))
+        case _ =>
+          None
+      }
+    }
+
     object ExAssertExpression {
       /** Extracts the 'assert' contract from an expression (only if it's the
        * first call in the block). */
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 40e3a61177d434915c01a0a36508d67f66d89152..b79616a39c45e2dc8b281a48d9d581195ae9069a 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1378,6 +1378,15 @@ trait CodeExtraction extends ASTExtractors {
 
           ArrayUpdated(rar, rk, rv)
 
+        case l @ ExListLiteral(tpe, elems) =>
+          val rtpe = extractType(l)
+          val cons = CaseClassType(libraryCaseClass(l.pos, "leon.collection.Cons"), Seq(rtpe));
+          val nil  = CaseClassType(libraryCaseClass(l.pos, "leon.collection.Nil"),  Seq(rtpe));
+
+          elems.foldRight(CaseClass(nil, Seq())) {
+            case (e, ls) => CaseClass(cons, Seq(extractTree(e), ls))
+          }
+
         case chr @ ExCharLiteral(c) =>
           CharLiteral(c)
 
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index a00e2d2450f34e45a6dbc63806eb991144764daa..fca74d2626bd56a5a08ff36d237ebd14e7f1638e 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -13,7 +13,8 @@ import utils._
 
 import java.lang.StringBuffer
 import PrinterHelpers._
-import TreeOps.isStringLiteral
+import TreeOps.{isStringLiteral, isListLiteral}
+import TypeTreeOps.leastUpperBound
 
 case class PrinterContext(
   current: Tree,
@@ -230,17 +231,27 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
           p"""|?($es)"""
         }
       case e @ CaseClass(cct, args) =>
-
-        isStringLiteral(e) match {
-          case Some(str) =>
-            val q = '"';
-            p"$q$str$q"
+        isListLiteral(e) match {
+          case Some((tpe, elems)) =>
+            val elemTps = leastUpperBound(elems.map(_.getType))
+            if (elemTps == Some(tpe)) {
+              p"List($elems)"  
+            } else {
+              p"List[$tpe]($elems)"  
+            }
 
           case None =>
-            if (cct.classDef.isCaseObject) {
-              p"$cct"
-            } else {
-              p"$cct($args)"
+            isStringLiteral(e) match {
+              case Some(str) =>
+                val q = '"';
+                p"$q$str$q"
+
+              case None =>
+                if (cct.classDef.isCaseObject) {
+                  p"$cct"
+                } else {
+                  p"$cct($args)"
+                }
             }
         }
 
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index a98519e19f742899d8c95bf85dd6091ba6278a85..8e8b831ec7277e5657086692bb0546d4e666802c 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1995,8 +1995,8 @@ object TreeOps {
       val lib = inProgram(cct.classDef).library
 
       if (Some(cct.classDef) == lib.String) {
-        listLiteralToList(args(0)) match {
-          case Some(chars) =>
+        isListLiteral(args(0)) match {
+          case Some((_, chars)) =>
             val str = chars.map {
               case CharLiteral(c) => Some(c)
               case _              => None
@@ -2018,15 +2018,15 @@ object TreeOps {
       None
   }
 
-  def listLiteralToList(e: Expr): Option[List[Expr]] = e match {
+  def isListLiteral(e: Expr): Option[(TypeTree, List[Expr])] = e match {
     case CaseClass(cct, args) =>
       val lib = inProgram(cct.classDef).library
 
       if (Some(cct.classDef) == lib.Nil) {
-        Some(Nil)
+        Some((cct.tps.head, Nil))
       } else if (Some(cct.classDef) == lib.Cons) {
-        listLiteralToList(args(1)).map { t =>
-          args(0) :: t
+        isListLiteral(args(1)).map { case (_, t) =>
+          (cct.tps.head, args(0) :: t)
         }
       } else {
         None