fix: projection of string literals

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

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))

tests/lean/run/strLitProj.lean

@@ -0,0 +1,5 @@
+#reduce "".data
+
+example : "".data = [] := rfl
+
+theorem ex : "".data = [] := rfl