Viktor Yudov

The reason is that the name of the generated constructor is `MN`: https://github.com/idris-lang/Idris2/blob/6c6ee58eb26dc6c9ca9897f6f079c3a4c0e9e8b7/src/Idris/Desugar.idr#L1302-L1306 so its definition is not stored in `ttc`: https://github.com/idris-lang/Idris2/blob/6c6ee58eb26dc6c9ca9897f6f079c3a4c0e9e8b7/src/Core/TTC.idr#L1106-L1109 https://github.com/idris-lang/Idris2/blob/6c6ee58eb26dc6c9ca9897f6f079c3a4c0e9e8b7/src/Core/TTC.idr#L1120 Perhaps we should process `MN` in `TTC`....

> Another option is to generate `UN` as is done for interfaces: This solves the problem with `record` but we can still get `Void` using elaborator script: ```idris module Broken...

> t's interesting that the `TTC.idr` code suppresses those fields when `isUserName (fullname gdef) || cwName (fullname gdef)` but only reads them back in when `isUserName name`. I would expect...

I don't understand why we look at the name type. Judging from the message of [this commit](https://github.com/idris-lang/Idris2/commit/6ffe4c52578c680ea61c3d63c01316992c79ce3b), this is done to avoid storing metavariable information. Wouldn't it be better to...

I think we should handle any valid definition in TTImp, since we have an elaborator script. So we shouldn't focus on the name

From my experiments, we can save all `Def`s except `PMDef`: https://github.com/spcfox/Idris2/commit/3ae04b5e2519e37dfc2aa9994cd14241ff7501de Saving all `PMDef` breaks the `frex` tests. Maybe we should add a flag for `PMDef` that should not be...

Also this bug can be reproduced without `%search` and data constructors: ```idris module Broken import Language.Reflection %default total %language ElabReflection decls : List Decl decls = let name = MN...

The reason is that case builder matches on `IndexIn` after `xs`. The following two functions compile successfully: ```idris fun6 : {mainLst : _} -> ListOfIndices mainLst -> {t : _}...

> FYI Not-so-trivial rebase may occur [here](https://github.com/idris-lang/Idris2/pull/3626) I can help with that

The totality of the data declaration doesn't seem to count for anything right now: ```idris %default total partial data D : Type failing "D is not total, not strictly positive"...