Create deterministic names for all identifiers and variables

[mpickering]

@RyanGlScott If you had the time I would appreciate your feedback on the approach in this patch before I invest time finishing things off.

There are currently two sources of non-determinism when using
singletons-th.

1. Let bindings are promoted to a top-level type family named
   Let<UNIQUE>.

2. The `noExactTyVars` function shifts the unique into the OccName of a
   name in order to make distinct occnames.

Now there are two mechanisms to provide deterministic names in these two
cases.

1. The PrM monad carries an incrementing counter in order to uniquely
   name each top-level Let. Any name created by `newUniqueName` now uses
   this global counter.

2. For the names which require local uniqueness, `noExactTyVars` carries
   its own counter and renaming in order to substitute fresh names into
   a local scope.

Fixes https://github.com/goldfirere/singletons/issues/628

[RyanGlScott]

What about names with symbolic (infix) characters? Surely these would need to be sanitized as well? (See the only convert code from uniquePrefixes.)

[mpickering]

I think if you look at the callsites for newUniqueId, it's always called with a string which is is alphanumeric (prefix). Therefore the sanitising is just important for replacing characters in module names.

[RyanGlScott]

Ah, fair enough. And now that I look more closely, the Haddocks for th-desugar's newUniqueName (on which this function is based) do mention that the string has to be alphanumeric. Perhaps it would suffice to just document that here as well.

[RyanGlScott]

If I understand correctly, then if you call noExactTyVars in two different locations (e.g., (noExactTyVars x, noExactTyVars y)), then there is no guarantee that the Names used in one location will be distinct from the names used the other location. Is that correct? If so, it would be worth documenting this potential pitfall.

As an alternative, we could remove noExactTyVars and instead use freshenTyVarsM everywhere. I don't think this should be too hard to do—there's only one noExactTyVars call site remaining, and I suspect that we could replace it with freshenTyVarsM by making the function which calls it monadic.

[mpickering]

Yes. that's right, fresh names are created within each scope and substituted into the remaining parts of the expression.

[mpickering]

The place where noExactTyVars is called takes care to more precisely substitute into the right places
rather than the code in Data.Singletons.TH.Promote.Defun which also uses the traversal to perform the substitution. I feel like all this code is a bit hairy and I don't fully understand what it's doing so I would prefer to not modify it too intensively unless there are some additional tests which demonstrate what's missing. Is that ok with you Ryan?

[RyanGlScott]

That's fine! I am happy to take a closer look at this myself in a follow-up PR.

[mpickering]

Thanks for your review @RyanGlScott I will return to this tomorrow. I've finished chasing down the other determinism issues for now!

[mpickering]

I've made some of the changes you suggest @RyanGlScott. I'm not so familar with this code so I'm quite wary to embark on any major refactorings, perhaps this would be a good interim step and provide a baseline for improving the name freshening story at a later point.

[RyanGlScott]

Thanks! (Did you mean to push your changes? I see that various discussion threads have been closed, but the code in the PR itself hasn't yet changed.)

On the topic of removing th-desugar's newUniqueName function, I have realized that things aren't quite as simple as I originally envisioned. In particular, the th-desugar library itself uses newUniqueName when desugaring code. What's more, singletons-th is built on top of this desugaring functionality, which means that even after all of the changes in this PR, I suspect that the output of singletons-th is still not deterministic.

As a result, I am wondering if a better approach would be to port the unique identifier machinery from this PR over to th-desugar, and then we could update singletons-th to build on top of that machinery. I've opened goldfirere/th-desugar#239 to track this.

What do you think about this idea? It would unfortunately take some more work to implement, but if our goal is having a high degree of confidence that the output is deterministic, then I think we'll need to do something like this. (If you don't want to do this, that's fine too—I can understand if you feel like this has been more work than you originally anticipated.)

[mpickering]

@RyanGlScott I pushed now, I accidentally pushed to the wrong remote before.

I'm able to fix the level at whichever level is best for the ecosystem. For the project which I tested this on, these changes were sufficient. I am currently trying to modify the test harness to see if it can test for these kinds of failures so that we don't regress in the future if something changes.

[mpickering]

I've modified the testsuite now to check for deterministic interface files for all the tests. This has highlighted there are still some issues, perhaps that is your observation about the th-desugar issue being the root cause of the non-determinism.

[RyanGlScott]

Thanks for being extra thorough here! The determinism-related tests failing matches my expectations, as I suspect that every use of newUniqueName in th-desugar is a potential source of non-determinism. In particular, I think that the uses in Language.Haskell.TH.Desugar are the most dangerous, as these are involved any time you desugar the template-haskell AST to the th-desugar AST that singletons-th is built on top of.

As a particularly simple example, the use of newUniqueName here is particularly bad, as that line of code gets invoked every time you desugar any function clause with a where clause. As an example, consider:

{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Singletons.TH

$(singletons [d|
  f :: a -> a
  f x = y
    where
      y = x
  |])

You'll see different -ddump-splices output depending on how GHC's unique numbers are incremented:

$ ghc-9.14 Bug.hs -ddump-splices -fforce-recomp -dunique-increment=-1
Loaded package environment from /Users/rscott/Documents/Hacking/Haskell/singletons/.ghc.environment.aarch64-darwin-9.14.1
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
Bug.hs:(10,2)-(15,5): Splicing declarations
    singletons
      [d| f_a5k1wlNFEup :: a_a5k1wlNFEuo -> a_a5k1wlNFEuo
          f_a5k1wlNFEup x_a5k1wlNFEun
            = y_a5k1wlNFEum
            where
                y_a5k1wlNFEum = x_a5k1wlNFEun |]
  ======>
    f_a5k1wlNFEiL :: a_a5k1wlNFEiM -> a_a5k1wlNFEiM
    f_a5k1wlNFEiL x_a5k1wlNFEiK
      = y_a5k1wlNFEiJ
      where
          y_a5k1wlNFEiJ = x_a5k1wlNFEiK
    type family Let7061644215716926668YSym0 (x7061644215716926669 :: a7061644215716926676) where
      Let7061644215716926668YSym0 x7061644215716926669 = Let7061644215716926668Y x7061644215716926669
    type family Let7061644215716926668Y (x7061644215716926669 :: a7061644215716926676) where
      Let7061644215716926668Y x_a5k1wlNFEiF = x_a5k1wlNFEiF
    type FSym0 :: (~>) a_a5k1wlNFEiM a_a5k1wlNFEiM
    data FSym0 :: (~>) a_a5k1wlNFEiM a_a5k1wlNFEiM
      where
        FSym0KindInference :: SameKind (Apply FSym0 arg_a5k1wlNFEiH) (FSym1 arg_a5k1wlNFEiH) =>
                              FSym0 a7061644215716926670
    type instance Apply @a_a5k1wlNFEiM @a_a5k1wlNFEiM FSym0 a7061644215716926670 = F a7061644215716926670
    instance SuppressUnusedWarnings FSym0 where
      suppressUnusedWarnings = snd ((,) FSym0KindInference ())
    type FSym1 :: a_a5k1wlNFEiM -> a_a5k1wlNFEiM
    type family FSym1 @a_a5k1wlNFEiM (a7061644215716926670 :: a_a5k1wlNFEiM) :: a_a5k1wlNFEiM where
      FSym1 a7061644215716926670 = F a7061644215716926670
    type F :: a_a5k1wlNFEiM -> a_a5k1wlNFEiM
    type family F @a_a5k1wlNFEiM (a_a5k1wlNFEiI :: a_a5k1wlNFEiM) :: a_a5k1wlNFEiM where
      F x_a5k1wlNFEiF = Let7061644215716926668YSym0 x_a5k1wlNFEiF
    sF ::
      (forall (t_a5k1wlNFEiC :: a_a5k1wlNFEiM).
       Sing t_a5k1wlNFEiC
       -> Sing (F t_a5k1wlNFEiC :: a_a5k1wlNFEiM) :: Type)
    sF (sX :: Sing x_a5k1wlNFEiF)
      = let
          sY :: Sing @_ (Let7061644215716926668Y x_a5k1wlNFEiF)
          sY = sX
        in sY
    instance SingI (FSym0 :: (~>) a_a5k1wlNFEiM a_a5k1wlNFEiM) where
      sing = singFun1 @FSym0 sF

$ ghc-9.14 Bug.hs -ddump-splices -fforce-recomp -dunique-increment=1
Loaded package environment from /Users/rscott/Documents/Hacking/Haskell/singletons/.ghc.environment.aarch64-darwin-9.14.1
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
Bug.hs:(10,2)-(15,5): Splicing declarations
    singletons
      [d| f_a2GD :: a_a2GE -> a_a2GE
          f_a2GD x_a2GF
            = y_a2GG
            where
                y_a2GG = x_a2GF |]
  ======>
    f_a2Sh :: a_a2Sg -> a_a2Sg
    f_a2Sh x_a2Si
      = y_a2Sj
      where
          y_a2Sj = x_a2Si
    type family Let6989586621679020852YSym0 (x6989586621679020851 :: a6989586621679020844) where
      Let6989586621679020852YSym0 x6989586621679020851 = Let6989586621679020852Y x6989586621679020851
    type family Let6989586621679020852Y (x6989586621679020851 :: a6989586621679020844) where
      Let6989586621679020852Y x_a2Sn = x_a2Sn
    type FSym0 :: (~>) a_a2Sg a_a2Sg
    data FSym0 :: (~>) a_a2Sg a_a2Sg
      where
        FSym0KindInference :: SameKind (Apply FSym0 arg_a2Sl) (FSym1 arg_a2Sl) =>
                              FSym0 a6989586621679020850
    type instance Apply @a_a2Sg @a_a2Sg FSym0 a6989586621679020850 = F a6989586621679020850
    instance SuppressUnusedWarnings FSym0 where
      suppressUnusedWarnings = snd ((,) FSym0KindInference ())
    type FSym1 :: a_a2Sg -> a_a2Sg
    type family FSym1 @a_a2Sg (a6989586621679020850 :: a_a2Sg) :: a_a2Sg where
      FSym1 a6989586621679020850 = F a6989586621679020850
    type F :: a_a2Sg -> a_a2Sg
    type family F @a_a2Sg (a_a2Sk :: a_a2Sg) :: a_a2Sg where
      F x_a2Sn = Let6989586621679020852YSym0 x_a2Sn
    sF ::
      (forall (t_a2Sq :: a_a2Sg).
       Sing t_a2Sq -> Sing (F t_a2Sq :: a_a2Sg) :: Type)
    sF (sX :: Sing x_a2Sn)
      = let
          sY :: Sing @_ (Let6989586621679020852Y x_a2Sn)
          sY = sX
        in sY
    instance SingI (FSym0 :: (~>) a_a2Sg a_a2Sg) where
      sing = singFun1 @FSym0 sF

[mpickering]

Thanks Ryan, I added this test and it passes the determinism check on the branch.

Here is a minimised version of one of the failures:

$(singletons [d|
  foo7 (x :: a) (_ :: b) = x
  |])

which results in

      -    forall a (x :: a) b (wild_6989586621679030148 :: b).
      -      Foo7 x wild_6989586621679030148 = x
      +    forall a (x :: a) b (wild_6989586621680989414 :: b).
      +      Foo7 x wild_6989586621680989414 = x

[mpickering]

Updating th-desugar seems to fix all the issues with determinism 🙏

I will open a PR over there.

[mpickering]

@RyanGlScott I pushed another update which should be passing CI now (with the updated th-desugar commit).

[RyanGlScott]

Fantastic work! At this point, I think my only question concerns which parts of the code should live in th-desugar versus singletons-th.

[mpickering]

@RyanGlScott I have pushed the changes to th-desugar and updated/tested this PR against those changes. Let me know if there is anything else you would like me to do.

[RyanGlScott]

Thanks again, @mpickering! Let me know if you need new releases of singletons-{th,base} soon with these changes.