Elektrine lite

← Feed

@pepper0@aus.social

Post #2945914

2026-02-14 17:28 UTC

@BoydStephenSmithJr@hachyderm.io Idris 1 or 2? paste code to reproduce here

Replies (2)

  • @pepper0@aus.social 2, but I don't have a small repro that will fit here. If you are interested, I can probably cook one up, or just share a link to a commit that breaks my build but "shouldn't".

    Open ##2945915

  • @pepper0@aus.social This is the function that "goes missing": https://gitlab.com/bss03/type-aligned/-/blob/main/src/TypeAligned.idr?ref_type=heads#L418 If you push TypeAligned.mapOnce and TypeAligned.map into a parameters block, then https://gitlab.com/bss03/type-aligned/-/blob/main/src/TypeAligned.idr?ref_type=heads#L393 can find it to perform the (indirectly, non-uniform) recursive call. I'll start working on a simpler repro once my currently builds complete and I can task-switch without losing track of what I'm doing.

    Open ##2945921