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.

  • One or more equations did not get rendered due to their size.