A strongly-kinded nonce generator

[langston-barrett]

I just spent a bunch of time fixing up some confusion I had about type variables. The problem was that I was writing Expr sym when I should have been writing Expr t, for t a phantom type parameter related to nonces. I only uncovered this mistake late in the development process, when trying to string together the end-to-end functionality I had in mind.

This confusion was possible because we tend to use the kind Type for a wide variety of type-level variables throughout What4 and Crucible. This PR suggests an wrapper for NonceGenerator that would avoid this pitfall. The primary downside is that we can no longer offer runSTNonceGenerator, as the ST monad phantom parameter does have kind Type. FWIW, this function appears unused in our Github repos, so this seems like a minor drawback.

[RyanGlScott]

I'm of two minds on this. On the one hand, this is a clever trick that lets you catch certain kinds of mistakes more easily. On the other hand, you have to accept that type variables of kind NonceBranch can't be passed to ST. This matters for this PR as all of the functions that involve ST (e.g., withGlobalSTNonceGenerator) require that the variable that you pass to ST is different from the variable you pass to NonceGenerator. As such, I don't think that any of the ST-related functions in this PR could be used in practice, as you almost always want these variables to be the same.

Moreover, wouldn't you need to rewrite what4's Expr in order to make its t type variable be of kind NonceBrand instead of Type? As such, this isn't really a drop-in replacement for Data.Parameterized.Nonce (unless I'm missing something).

[langston-barrett]

As such, I don't think that any of the ST-related functions in this PR could be used in practice, as you almost always want these variables to be the same.

I think they wouldn't be as convenient to use in practice, because you'd have to track two type variables (one for the ST monad and one for the nonces), not that they'd be completely unusable, correct?

In any case, I've pushed a patch that fixes this. I think it's still sound, as it yields a NonceGenerator (ST t) (NonceBrand t) where type NonceBrand = 'NonceBrand but the constructor NonceBrand itself is still not exported, so I think you still shouldn't be able to match NonceBrand t ~ NonceBrand s for any s !~ t.

Moreover, wouldn't you need to rewrite what4's Expr in order to make its t type variable be of kind NonceBrand instead of Type? As such, this isn't really a drop-in replacement for Data.Parameterized.Nonce (unless I'm missing something).

Certainly, it's far too late for Expr. But this module might present a nice alternative for new developments using nonces.

[RyanGlScott]

Ah, you've pushed a new version which unifies the two kinds of type variables. Very well.

This patch still makes me a bit uneasy, however—likely because this adds quite a lot of additional scaffolding. All of this scaffolding is for the sake of producing better error messages, but it's not immediately obvious to me that the error messages you'd get with this interface actually would be more obvious than the old interface. Moreover, I wonder what is stopping users from writing, say, Expr (NonceBrand sym) instead of Expr (NonceBrand t) and making the same mistake as in the original motivation, but with NonceBrandKind instead of Type.

[langston-barrett]

it's not immediately obvious to me that the error messages you'd get with this interface actually would be more obvious than the old interface.

They changed in the way I expected when I made this PR:

data Foo (t :: NonceBrandKind) = Foo

test :: forall a. a
test = let f = Foo :: Foo a in ()

yields

src/Foo.hs:10:27: error: [GHC-83865]
    • Expected kind ‘NonceBrandKind’, but ‘a’ has kind ‘*’
    • In the first argument of ‘Foo’, namely ‘a’
      In an expression type signature: Foo a
      In the expression: Foo :: Foo a
    |
147 | test = let f = Foo :: Foo a in ()
    |                           ^

To me, this indicates that I should probably:

1. See if I have any type variables in scope that do have kind NonceBrandKind
2. Go look at the docs for NonceBrandKind to understand what's happening here

IMO, this is better than the Couldn't match SymExpr sym with Expr sym message that motivated this PR. Additionally, you'd get this message immediately when writing the type signature, rather than later when writing code in a downstream package.

Moreover, I wonder what is stopping users from writing, say, Expr (NonceBrand sym) instead of Expr (NonceBrand t) and making the same mistake as in the original motivation, but with NonceBrandKind instead of Type.

Great point. This is certainly possible, but IMO less likely than the mistake I made. I think it'd be odd for someone to write Expr (NonceBrand sym) without knowing what NonceBrand is, in a way that it's not that odd to write Expr sym without knowing the intent of the type parameter to Expr.

It would be interesting to see if we could also make a more strongly-kinded version of ST, which might help avoid this issue...

I don't feel strongly about this PR one way or another and would be fine with just closing it at this point.

[langston-barrett]

Moreover, I wonder what is stopping users from writing, say, Expr (NonceBrand sym) instead of Expr (NonceBrand t) and making the same mistake as in the original motivation, but with NonceBrandKind instead of Type.

I've pushed a commit that eliminates NonceBrand from the public API, replacing it with uses of UnwrapNonceBrand, leading to (admittedly, ugly) type signatures like this:

type family UnwrapNonceBrand (nk :: NonceBrandKind) :: Type where
  UnwrapNonceBrand ('NonceBrand s) = s

-- snip --

runSTNonceGenerator :: (forall s . NonceGenerator (ST (UnwrapNonceBrand s)) s -> ST (UnwrapNonceBrand s) a)
                    -> a

This would need more documentation before merging if we decide we like it now, but I at least wanted to see if it was technically feasible to forbid this kind of error as well.