Nested dot notation fails with type classes

Stream: general

[pandaman]

Hi. I came across a case where a nested dot notation results in a compiler error with type classes while it works with structures. Is this an intended behavior or should I open an Issue? Thanks!

Here is MWE. You can also run the code in Playground.

structure NFA where
  nodes : Array Unit

def NFA.pushRegex (nfa : NFA) : NFA := { nodes := nfa.nodes.push () }

namespace Class
class ProofData where
  nfa : NFA

def ProofData.nfa' [pd : ProofData] : NFA := pd.nfa.pushRegex

class Alternate extends ProofData where

variable [pd : Alternate]

-- Single dot works
example : NFA := pd.nfa'
/-
function expected at
  ProofData.nfa'
term has type
  NFA
-/
-- example : Array Unit := pd.nfa'.nodes
end Class

[Daniel Weber]

(pd.nfa').nodes also works :thinking:

[pandaman]

Reported as https://github.com/leanprover/lean4/issues/6400