diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 9767d6a0a6..8dc78d2bc4 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -294,6 +294,7 @@ def reduceMatcher? (e : Expr) : MetaM ReduceMatcherResult := do
 /- Given an expression `e`, compute its WHNF and if the result is a constructor, return field #i. -/
 def project? (e : Expr) (i : Nat) : MetaM (Option Expr) := do
   let e ← whnf e
+  let e := toCtorIfLit e
   matchConstCtor e.getAppFn (fun _ => pure none) fun ctorVal _ =>
     let numArgs := e.getAppNumArgs
     let idx := ctorVal.numParams + i
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 1e53e8beea..8e86bc3768 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -366,6 +366,8 @@ optional<expr> type_checker::reduce_proj(expr const & e, bool cheap) {
         c = whnf_core(proj_expr(e), cheap);
     else
         c = whnf(proj_expr(e));
+    if (is_string_lit(c))
+        c = string_lit_to_constructor(c);
     buffer<expr> args;
     expr const & mk = get_app_args(c, args);
     if (!is_constant(mk))
diff --git a/tests/lean/run/strLitProj.lean b/tests/lean/run/strLitProj.lean
new file mode 100644
index 0000000000..5c9bcf0125
--- /dev/null
+++ b/tests/lean/run/strLitProj.lean
@@ -0,0 +1,5 @@
+#reduce "".data
+
+example : "".data = [] := rfl
+
+theorem ex : "".data = [] := rfl