singletons-th: Make pr_scoped_vars a list of LocalVars, not Names
#614
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Instead of making `LocalVar` a type synonym around a tuple type, `LocalVar` is now a proper data type definition. This is purely a refactoring. In a subsequent commit, we will make use of `LocalVar` being a distinct data type in order to give it `Eq` and `Ord` instances.
Doing so makes it possible to track the kinds of scoped type variables with greater precision during lambda lifting. See the golden output for the new `T613` test case to see an example of this in action. Fixes #613.
|
This PR has revealed a latent bug. Consider this variation on the {-# LANGUAGE GHC2024 #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -ddump-splices #-}
module Bug where
import Data.Proxy
import Data.Proxy.Singletons
import Data.Singletons.TH
$(promote [d|
f :: forall k (a :: k). Proxy a -> Proxy a
f = g
where
g :: forall (b :: k). Proxy b -> Proxy b
g x = y
where
y = Proxy
|])After the changes in this PR, this program now fails to promote: Note the generated code for type family Let6989586621679026486Y (b6989586621679026436 :: k6989586621679026433) k6989586621679026433 (a6989586621679026434 :: k6989586621679026433) (x6989586621679026485 :: Proxy b6989586621679026436) (a_69895866216790264766989586621679026481 :: Proxy a6989586621679026434) where
Let6989586621679026486Y b_a4ks k_a4kp a_a4kq x_a4lf a_6989586621679026476_a4lb = ProxySym0This quantifies singletons/singletons-th/src/Data/Singletons/TH/Promote/Monad.hs Lines 82 to 88 in 9d5a811 Note that the newly bound scoped type variables are placed before type variables that were bound earlier, resulting in oddities like the ones seen above. This wasn't as much of a problem back when we didn't track the kinds of scoped type variables, but now that we do, it's a much more glaring issue. We should swap the order of |
...at least, I thought that would fix the issue above. Sadly, doing that just reveals another issue, this time with It's not obvious to me how we'd make this work without giving |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Doing so makes it possible to track the kinds of scoped type variables with greater precision during lambda lifting. See the golden output for the new
T613test case to see an example of this in action.Fixes #613.