I ran into this issue when updating one of the Iris projects to Coq 8.18, see https://gitlab.mpi-sws.org/iris/actris/-/jobs/252795 It happens with a setoid_rewrite
where rewriting happens below a binder (i.e., in a case where normal rewrite fails).
Anyone experience with debugging these FLambda
error messages? I have not seen them before, and my attempts to minimize the problem have failed so far.
This topic was moved here from #Coq users > "Anomaly "conversion was given unreduced term (FLambda)." wi by Karl Palmskog.
since anomalies are (nearly by definition) problems in Coq itself, I move this topic here to get more dev eyes on it
This kind of problem is typically due to the legacy unification sending ill-typed terms to conversion. The FLambda thing happens when there is an eta-expansion needed somewhere but one side has a non-functional type.
Last updated: Oct 13 2024 at 01:02 UTC