Justus Matthiesen

Here is what goes wrong: when `checkAppWith'` encounters a function type `ty` that doesn't have pi-shape, it constructs a type `Bind fc argn (Pi fc top Explicit argTy) (weaken retTy)`,...

Seeing that the current CSE is unsound with respect to `%delay`, I think this should be merged unless our backend maintainers (@stefan-hoeck, in particular) have concerns.

Thanks @stefan-hoeck! I am merging this now and am happy to take the blame if something goes wrong.

I am fairly certain this is due to #2954. Prior to PR #2953, the termination checker was accepting some functions for the wrong reason, masking issue #2954. I am currently...

I have now merged my changes to the termination checker. Unfortunately, they do not address this particular termination issue. The problem here is caused by the with-abstraction, see #403. The...

Good detective work! We had the same issue with as-patterns previously ([issue](https://github.com/idris-lang/Idris2/issues/3143), [PR](https://github.com/idris-lang/Idris2/pull/3146)). At some point, we should address the two larger issues as well: - [`impossibleErrOk`](https://github.com/idris-lang/Idris2/blob/5d04f89c7b42afba384d19108b5e0cdaee99a224/src/TTImp/ProcessDef.idr#L92-L149) is too liberal....

I reduced the example a bit: ```idris data D : Type -> Type where C : (a : Type) -> D a f : D (Type -> Type) -> ()...