Auxiliary function for projecting "type class dictionary access".
That is, we are trying to extract one of the type class instance elements.
Remark: We do not consider parent instances to be elements.
For example, suppose e is _x_4.1, and we have
_x_2 : Monad (ReaderT Bool (ExceptT String Id)) := @ReaderT.Monad Bool (ExceptT String Id) _x_1
_x_3 : Applicative (ReaderT Bool (ExceptT String Id)) := _x_2.1
_x_4 : Functor (ReaderT Bool (ExceptT String Id)) := _x_3.1
Then, we will expand _x_4.1 since it corresponds to the Functor map element,
and its type is not a type class, but is of the form
{α β : Type u} → (α → β) → ...
In the example above, the compiler should not expand _x_3.1 or _x_2.1 because they are
type class applications: Functor and Applicative respectively.
By eagerly expanding them, we may produce inefficient and bloated code.
For example, we may be using _x_3.1 to invoke a function that expects a Functor instance.
By expanding _x_3.1 we will be just expanding the code that creates this instance.
The result is representing a sequence of code containing let-declarations and local function declarations (Array CodeDecl)
and the free variable containing the result (FVarId). The resulting FVarId often depends only on a small
subset of Array CodeDecl. However, this method does try to filter the relevant ones.
We rely on the used var set available in SimpM to filter them. See attachCodeDecls.
Equations
- One or more equations did not get rendered due to their size.
- Lean.Compiler.LCNF.Simp.inlineProjInst? e = pure none