It occurred to me recently that the sorts of nondeterminism issues that plagued GHC for years also plague singletons. While GHC has fixed these issues, singletons has not. The following example illustrates the problem well:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

import Data.Singletons
import Data.Singletons.TH (singletonsOnly)

$(singletonsOnly [d|
  const :: a -> b -> a
  const x _ = x
  |])

When a user writes sConst @Bool, which type gets instantiated to Bool: a or b? You might think "well obviously the answer is a", and a quick smoke-test in GHCi would appear to confirm that hunch:

$ /opt/ghc/8.6.1/bin/ghci Bug.hs -XTypeApplications
GHCi, version 8.6.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
Ok, one module loaded.
λ> :type +v sConst @Bool
sConst @Bool
  :: forall b (t1 :: Bool) (t2 :: b). Sing t1 -> Sing t2 -> Sing t1

However, that's only because of a lucky fluke. As it turns out, if you pass -dunique-increment=-1 to GHC, then you'll get a different answer:

$ /opt/ghc/8.6.1/bin/ghci Bug.hs -XTypeApplications -dunique-increment=-1
GHCi, version 8.6.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
Ok, one module loaded.
λ> :type +v sConst @Bool
sConst @Bool
  :: forall a (t1 :: a) (t2 :: Bool). Sing t1 -> Sing t2 -> Sing t1

Ack. It turns out that the order of the kind variables a and b in sConst's type signature completely depend on which unique values happen to be gensymmed for them (by newName) in singletons' Template Haskell machinery. This is because several functions in th-desugar and singletons collect type variables using Set Name, and the Ord Name instance compares by Name's unique values first and foremost. If a happens to have a smaller unique than b, then when you call Set.toList on a set containing {a, b}, then you'll get [a,b]. If b has a smaller unique than a, on the other hand, then you'll get [b,a].

Essentially, any place in singletons where call S.toList on a Set Name (that can affect the user-facing API) should be treated as nondeterministic code. I count at least three places in th-desugar and singletons (each!) where we do this at the time of writing.

Luckily, GHC has figured out how to solve this problem, so we should be able to learn from its mistakes. One of the main tricks that GHC uses to avoid this sort of nondeterminism is by switching out uses of Set for a deterministic, insert-ordered set, such as UniqDSet. It seems likely that we'll need to find such a data structure on Hackage (or conjure up one ourselves) and use it throughout th-desugar and singletons where appropriate.