Lower the boom on the mess in the saw-script typechecker

[sauclovian-g]

No description provided.

[sauclovian-g]

Provided the CI doesn't fail, this probably ought to get reviewed and merged before I go on.

You'll almost certainly want to review it commit by commit; the overall diff to MGU.hs is completely unreadable.

[RyanGlScott]

I've done a first pass, although I will admit that my review did not thoroughly examine some of the denser parts of the code. Please let me know if there are parts that you think warrant further scrutiny.

[sauclovian-g]

On the further/deeper scrutiny topic: the one to be suspicious of is 01c4ca8, particularly the statement checking; it's unlikely that any of the other ones that weren't supposed to cause functional changes actually did, and the other changes afterwards are all relatively straightforward.

[RyanGlScott]

On the further/deeper scrutiny topic: the one to be suspicious of is 01c4ca8, particularly the statement checking; it's unlikely that any of the other ones that weren't supposed to cause functional changes actually did, and the other changes afterwards are all relatively straightforward.

I take it that you're referring to test suite failures such as this one?

[23:54:57.507] /workdir/memory-safety/salsa20/solution.saw:3:32-3:40: Unbound type variable LLVMType

That is worrisome indeed. I decided to see how this worked to begin with, and it's quite miraculous that it ever did:

• Unlike, say, LLVMSpec (which is hard-coded as a type constant), LLVMType is not hard-coded anywhere. How, then, does SAW know how to treat LLVMType differently from other types?

• The only knowledge of LLVMType that SAW has is that it is listed in the types of various primitives in SAWScript.Interpreter. That turns out to be of vital importance...

• ...here, which builds the initial TopLevel RW environment. If you trace through the code here, you'll see that it is constructing an initial rwTypes map by mapping each primitive's name to its type (as specified in SAWScript.Interpreter).

  As one example, consider the primitive "llvm_float" "LLVMType". The type is specified as a string, so we need a way to turn the string into a full-blown AST Type. That is done using SAWScript's parser. Specifically, when it sees a type name that is not hard-coded (such as LLVMSpec), it assumes that it is a TyVar:

  saw-script/src/SAWScript/Parser.y

  Lines 219 to 220 in 69a2dd3

  	BaseType :: { Type }
  	: name { tVar (getPos $1) (tokStr $1) }

  TyVar is a somewhat interesting choice, as we will see later.

• Now let's suppose we want to define a SAWScript function of the following type:

  let f (x : LLVMType) = x;
  

  There are two conceivable types that SAW could give to f:

  1. {LLVMType} LLVMType -> LLVMType (i.e., LLVMType is a forall-quantified type variable)
  2. LLVMType -> LLVMType (i.e., LLVMType is a type constructor)

  SAW chooses which type to give f in the generalize function in SAWScript.MGU.

• generalize determines which variables are already in scope (and therefore do not need to be generalized) by consulting the type environment here:

  saw-script/src/SAWScript/MGU.hs

  Lines 844 to 847 in 69a2dd3

  	envUnify <- unifyVarsInEnv
  	envNamed <- namedVarsInEnv
  	let is = M.toList (unifyVars ts M.\\ envUnify)
  	let bs = M.toList (namedVars ts M.\\ envNamed)

  If you trace back through this code, the type environment ultimately comes from the initial TopLevel RW, which contains the types of all primitives. Moreover, there is at least one primitive whose type contains a TyVar with the name LLVMType, which means that as far as generalize is concerned, LLVMType is already in scope. As such, generalize will pick the type LLVMType -> LLVMType (without a forall) for f.

Phew, that was a lot! (Apologies if I am repeating things that you already know here, but I found it useful to write this up for my own understanding.)

---

A related question: what changed in this PR? My guess is that commit 91f9bbf subtly broke the delicate arrangement that allowed this to work previously. Specifically, the checkType case for TyVar pos x looks up the type variable x in the typedefEnv, and if it's not found, it throws the Unbound type variable error seen above. As far as I understand, this is a check that was simply not performed before this PR, and functions like f above will now fail this check since LLVMType is not in the typedefEnv.

One possible (albeit hacky) way to restore the old behavior prior to this PR would be to see if x is in the namedVars of the typeEnv (which contains primitives that use the name LLVMType in their types). Alternatively, we could make LLVMType et al. hard-coded constants, which avoid this problem in the first place. I am somewhat more fond of this alternative idea, as it feels a bit more principled, although it would likely be more work to implement. Let me know what you think.

[kiniry]

One possible (albeit hacky) way to restore the old behavior prior to this PR would be to see if x is in the namedVars of the typeEnv (which contains primitives that use the name LLVMType in their types).

"hacky" a thousand times is what got us into this mess, IMO.

[sauclovian-g]

I take it that you're referring to test suite failures such as this one?

Actually, unfortunately, I wasn't -- was speaking in general. I didn't mean for you to have to go investigate that problem yourself; I posted elsewhere about it but I guess you saw this first.

However, that explains what the intended purpose of the code at lines 844-847 is. (See #2105, wherein it fails to handle user typedefs.) Note that this relies on the fact that the primitives in the primitives table are not actually declared via the typechecker; if it were, the types like LLVMType would get generalized and forall-bound.

Anyway the right way to fix this is to declare the abstract types. I've been thinking about what the best way to represent them is, and I'll push a draft version shortly.

[RyanGlScott]

Nearly there!

[RyanGlScott]

Excellent work, @sauclovian-g. I'm eager to see this land!

[sauclovian-g]

Yay! 😸 I'll merge it once the CI finishes.