fix: unfold class projections when using TransparencyMode.instances

src/Lean/Meta/Basic.lean

@@ -262,14 +262,14 @@ def mkFreshExprMVarWithId (mvarId : MVarId) (type? : Option Expr := none) (kind
     let type ← mkFreshExprMVar (mkSort u)
     mkFreshExprMVarWithIdCore mvarId type kind userName
 
+def getTransparency : MetaM TransparencyMode :=
+  return (← getConfig).transparency
+
 def shouldReduceAll : MetaM Bool :=
-  return (← read).config.transparency == TransparencyMode.all
+  return (← getTransparency) == TransparencyMode.all
 
 def shouldReduceReducibleOnly : MetaM Bool :=
-  return (← read).config.transparency == TransparencyMode.reducible
-
-def getTransparency : MetaM TransparencyMode :=
-  return (← read).config.transparency
+  return (← getTransparency) == TransparencyMode.reducible
 
 def getMVarDecl (mvarId : MVarId) : MetaM MetavarDecl := do
   let mctx ← getMCtx
@@ -432,7 +432,7 @@ def getTheoremInfo (info : ConstantInfo) : MetaM (Option ConstantInfo) := do
     return none
 
 private def getDefInfoTemp (info : ConstantInfo) : MetaM (Option ConstantInfo) := do
-  match (← read).config.transparency with
+  match (← getTransparency) with
   | TransparencyMode.all => return some info
   | TransparencyMode.default => return some info
   | _ =>

src/Lean/Meta/WHNF.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.ToExpr
 import Lean.AuxRecursor
+import Lean.ProjFns
 import Lean.Meta.Basic
 import Lean.Meta.LevelDefEq
 import Lean.Meta.GetConst
@@ -364,11 +365,33 @@ mutual
         | some e => whnfUntilIdRhs e
         | none   => pure e -- failed because of symbolic argument
 
+  /--
+    Auxiliary method for unfolding a class projection when transparency is set to `TransparencyMode.instances`.
+    Recall that that class instance projections are not marked with `[reducible]` because we want them to be
+    in "reducible canonical form".
+  -/
+  private partial def unfoldProjInst (e : Expr) : MetaM (Option Expr) := do
+    if (← getTransparency) != TransparencyMode.instances then
+      return none
+    else
+      match e.getAppFn with
+      | Expr.const declName .. =>
+        match (← getProjectionFnInfo? declName) with
+        | some { fromClass := true, .. } =>
+          match (← withDefault <| unfoldDefinition? e) with
+          | none   => return none
+          | some e =>
+            match (← reduceProj? e.getAppFn) with
+            | none   => return none
+            | some r => return mkAppN r e.getAppArgs
+        | _ => return none
+      | _ => return none
+
   /-- Unfold definition using "smart unfolding" if possible. -/
   partial def unfoldDefinition? (e : Expr) : MetaM (Option Expr) :=
     match e with
     | Expr.app f _ _ =>
-      matchConstAux f.getAppFn (fun _ => pure none) fun fInfo fLvls => do
+      matchConstAux f.getAppFn (fun _ => unfoldProjInst e) fun fInfo fLvls => do
         if fInfo.lparams.length != fLvls.length then
           return none
         else

src/Lean/ReducibilityAttrs.lean

@@ -9,7 +9,7 @@ namespace Lean
 
 inductive ReducibilityStatus where
   | reducible | semireducible | irreducible
-  deriving Inhabited
+  deriving Inhabited, Repr
 
 builtin_initialize reducibilityAttrs : EnumAttributes ReducibilityStatus ←
   registerEnumAttributes `reducibility

src/library/constructions/projection.cpp

@@ -98,7 +98,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
         expr proj_val  = mk_proj(n, i, c);
         proj_val = lctx.mk_lambda(proj_args, proj_val);
         declaration new_d = mk_definition_inferring_unsafe(env, proj_name, lvl_params, proj_type, proj_val,
-                                                         reducibility_hints::mk_abbreviation());
+                                                           reducibility_hints::mk_abbreviation());
         new_env = new_env.add(new_d);
         if (!inst_implicit)
             new_env = set_reducible(new_env, proj_name, reducible_status::Reducible, true);

tests/lean/whnfProj.lean

@@ -0,0 +1,22 @@
+import Lean
+
+def h (x : Nat) := x
+def f (x : Nat) := x + 1
+def g (x : Nat) := (x, x+1).fst
+
+
+open Lean
+open Lean.Meta
+
+def tst (declName : Name) : MetaM Unit := do
+  let c ← getConstInfo declName
+  lambdaTelescope c.value! fun _ b => do
+    trace[Meta.debug]! "1. {b}"
+    trace[Meta.debug]! "2. {← withReducible <| whnf b}"
+    trace[Meta.debug]! "3. {← withReducibleAndInstances <| whnf b}"
+    trace[Meta.debug]! "4. {← withDefault <| whnf b}"
+    pure ()
+
+set_option trace.Meta.debug true
+#eval tst `f
+#eval tst `g

tests/lean/whnfProj.lean.expected.out

@@ -0,0 +1,8 @@
+[Meta.debug] 1. x + 1
+[Meta.debug] 2. x + 1
+[Meta.debug] 3. Nat.add x 1
+[Meta.debug] 4. Nat.succ (Nat.add x 0)
+[Meta.debug] 1. (x, x + 1).fst
+[Meta.debug] 2. x
+[Meta.debug] 3. x
+[Meta.debug] 4. x