Skip to content

template haskell: use a precise condition when implicitly lifting

Matthew Pickering requested to merge wip/t26088 into master

Implicit lifting corrects a level error by replacing references to x with $(lift x), therefore you can use a level n binding at level n + 1, if it can be lifted.

Therefore, we now have a precise check that the use level is 1 more than the bind level.

Before this bug was not observable as you only had 0 and 1 contexts but it is easily evident when using explicit level imports.

Fixes #26088 (closed)

Edited by Matthew Pickering

Merge request reports