Better kind-checking of SAWScript types

[samcowger]

#2748 modified SAWScript parsing in a way that allowed users to write previously-syntactically-invalid types, like Int Int. SAWScript currently fails to reject such a type as ill-kinded. SAW even allows values of such types to be constructed without resorting to undefined:

sawscript> let x : Int Int = return 0
sawscript> :t x
Int Int
sawscript> print x
[17:05:52.428] return 0
sawscript>

More comprehensive kind-checking ought to put a stop to this.

In terms of code, note that a fix for this may go hand in hand with substantially reworking or removing the BlockCon AST node, into which all type constructor applications are currently parsed and through which kind-checking flows. Several notes (authored by @sauclovian-g in #2157) suggest that BlockCon ought to be removed outright:

saw-script/saw-script/src/SAWScript/Typechecker.hs

Lines 1786 to 1789 in e9844d6

	-- XXX: while BlockCon exists, ContextCon has kind * and you
	-- have to use BlockCon to paste a result type to a ContextCon.
	-- (BlockCon should be removed. Then ContextCon has kind * -> *
	-- like you'd expect.)

saw-script/saw-script/src/SAWScript/Typechecker.hs

Line 1810 in e9844d6

-- XXX special case for BlockCon (remove along with BlockCon)

saw-script/saw-script/src/SAWScript/Typechecker.hs

Lines 1951 to 1953 in e9844d6

	-- position associated with the monad context. (This part is a
	-- result of BlockCon existing and can go away when BlockCon is
	-- removed.)

Note also that (I believe) this issue encompasses much of the "other cleanup" referred to in #2163.

[sauclovian-g]

I started on a patch to kill off BlockCon and it ended up getting complicated. Basically the problem is that BlockCon is an extra layer of indirection for type application, and without it you can apply type arguments to type constructors but not type variables, and then of course that doesn't work. It isn't entirely obvious how best to rearrange the internal representation to fix that. There's also an issue where for some uses the source position of the application should be tracked separately and others where that doesn't make sense, and unifying the treatment in the representation naively messes that up.

However, that shouldn't be why the kind-checking doesn't work. There's still an application happening in Int Int and it shouldn't be allowed.

[samcowger]

I think part of the fault lies in SAWScript.Typechecker.lookupTycon:

saw-script/saw-script/src/SAWScript/Typechecker.hs

Lines 1768 to 1791 in 1c52684

	-- Look up a type constructor (in our fixed environment of hardcoded
	-- types) and return its params as a list of kinds.
	lookupTyCon :: TyCon -> [Kind]
	lookupTyCon tycon = case tycon of
	TupleCon n -> genericTake n (repeat kindStar)
	ArrayCon -> [kindStar]
	FunCon -> [kindStar, kindStar]
	StringCon -> []
	TermCon -> []
	TypeCon -> []
	BoolCon -> []
	IntCon -> []
	BlockCon -> [kindStar, kindStar]
	AIGCon -> []
	CFGCon -> []
	JVMSpecCon -> []
	LLVMSpecCon -> []
	MIRSpecCon -> []
	ContextCon _ctx ->
	-- XXX: while BlockCon exists, ContextCon has kind * and you
	-- have to use BlockCon to paste a result type to a ContextCon.
	-- (BlockCon should be removed. Then ContextCon has kind * -> *
	-- like you'd expect.)
	[]

IIUC, BlockCon [C, T] signifies the application of C to T. So, if the application has any hope of being well-kinded, then the expected kind for C is (at the very least) not *. However, lookupTycon is declaring that the first argument to a BlockCon must be *. This allows construction of good types like TopLevel () because lookupTycon (incorrectly, in principle) declares that TopLevel, as well as all other ContextCons, are of kind *. Because Int is also *, though, it allows construction of bad types like Int Int by the same token.

FWIW, these changes get us a lot of the error-checking and reporting that we want, and keep the test suite happy:

diff --git a/saw-script/src/SAWScript/Typechecker.hs b/saw-script/src/SAWScript/Typechecker.hs
index c7e9f6c85..e2c7316f7 100644
--- a/saw-script/src/SAWScript/Typechecker.hs
+++ b/saw-script/src/SAWScript/Typechecker.hs
@@ -275,8 +275,8 @@ kindStar :: Kind
 kindStar = Kind 0
 
 -- these aren't currently used
---kindStarToStar :: Kind
---kindStarToStar = Kind 1
+kindStarToStar :: Kind
+kindStarToStar = Kind 1
 --
 --kindStarToStarToStar :: Kind
 --kindStarToStarToStar = Kind 2
@@ -1776,7 +1776,7 @@ lookupTyCon tycon = case tycon of
     TypeCon -> []
     BoolCon -> []
     IntCon -> []
-    BlockCon -> [kindStar, kindStar]
+    BlockCon -> [kindStarToStar, kindStar]
     AIGCon -> []
     CFGCon -> []
     JVMSpecCon -> []
@@ -1787,7 +1787,7 @@ lookupTyCon tycon = case tycon of
       -- have to use BlockCon to paste a result type to a ContextCon.
       -- (BlockCon should be removed. Then ContextCon has kind * -> *
       -- like you'd expect.)
-      []
+      [kindStar]
 
 -- Check a type for validity and also for having the
 -- correct kinding.
@@ -1860,22 +1860,7 @@ checkType kind ty = case ty of
               -- initial environment we were given that depends on the
               -- interpreter not doing unfortunate things. This isn't
               -- currently seeming like a very good bet.)
-              --
-              -- For now at least we require typedefs to be kind *
-              -- (they can't have parameters and the expansions are thus
-              -- restricted) so just fail if we use one in a context
-              -- expecting something else.
-              --
-              -- The same holds for abstract types, so we don't need
-              -- separate cases.
-              if kind /= kindStar then do
-                  recordError pos ("Kind mismatch: expected " ++ pShow kind ++
-                                   " but found " ++ pShow kindStar)
-                  getErrorTyVar pos
-              else
-                  -- We do _not_ want to expand typedefs when checking,
-                  -- so return the original TyVar.
-                  return ty
+              return ty
            | otherwise -> do
                   recordError pos $ "Inaccessible type: " ++ show x
                   let how = if lc == HideDeprecated then "deprecated" else "experimental"

...though I don't understand the purpose of the kind /= kindStar check to speak about the wisdom of its removal, and I don't think it's appropriate in general to declare that the first argument for a BlockCon is * -> * (even though that's the only kind we ever supply to it now).

Basically the problem is that BlockCon is an extra layer of indirection for type application, and without it you can apply type arguments to type constructors but not type variables, and then of course that doesn't work. It isn't entirely obvious how best to rearrange the internal representation to fix that.

When I've done this in the past, I've represented type application at the type level, rather that the type constructor level - so, in SAWCentral.AST terms, something like this:

 data Type
-  = TyCon Pos TyCon [Type]
+  = TyCon Pos TyCon
+  | TyApp Pos Type Type  -- or `Type [Type]`
   | TyRecord Pos (Map Name Type)
   | TyVar Pos Name
   | TyUnifyVar Pos TypeIndex

Might a representation like this let us remove BlockCon and still maintain enough flexibility to support treating type variables as type constructors?

[sauclovian-g]

Yeah, I just derived basically the same patch.

It opens a can of worms, though:

sawscript> :t jvm_assert

You have encountered a bug in saw-script's implementation.
*** Please create an issue at https://github.com/GaloisInc/saw-script/issues

%< --------------------------------------------------- 
  Revision:  25a447189
  Branch:    fix-kind-checking
  Location:  <type of jvm_assert>
  Message:   Unexpected errors:
             <type of jvm_assert>:1:9-1:17: Kind mismatch: expected "* -> *" but found "*"
CallStack (from HasCallStack):
  panic, called at saw-support/src/SAWSupport/PanicSupport.hs:133:3 in saw-1.4.0.99-inplace-saw-support:SAWSupport.PanicSupport
  doPanic, called at saw-script/src/SAWScript/Panic.hs:19:19 in saw-1.4.0.99-inplace-saw-script:SAWScript.Panic
  panic, called at saw-script/src/SAWScript/Loader.hs:103:8 in saw-1.4.0.99-inplace-saw-script:SAWScript.Loader
%< --------------------------------------------------- 

It seems we have two different types in here: JavaSetup and JVMSetup, of which JavaSetup is the builtin monad type that appears in the AST Context type and all that, and JVMSetup is a separate abstract type. But JVMSetup is the type that all the JVM verification builtins actually use. There is no mention of JavaSetup at all in the builtins table. The problem then is that all the abstract types are assumed to be kind *, and it's only been working by accident all this time.

This obviously needs to be cleaned out. I am not inclined to think it's good that any of these types are special-cased in the AST, so I think I'm going to add a way to (internally) declare abstract types with kind * -> *, fix JVMSetup, and remove JavaSetup.

[sauclovian-g]

I made two more issues (#2768 and #2769) for the sub-points because without threading this discussion is going to overflow 🙀 So, please post your thoughts on those there...

On the subject of typedefs all being kind *, there's no particular reason I can think of to prohibit doing things like typedef IO = TopLevel. Until you fixed it that wouldn't have been allowed by the parser; but now it is. You still can't do typedef IO a = TopLevel a, because typedefs can't have parameters; we could lift that restriction, but I see no immediate reason to worry about it.

[sauclovian-g]

However, after having now examined the situation, it's not as simple as just removing that check. That's the part where it assumes typedefs have kind * and rejects usage in other contexts. There's also a check when it sees a typedef that the expansion has kind *, and that's a bigger deal to rearrange, because it requires changing the current kind-checking code to kind-inference code. That in turn is a big enough change (because among other things we don't track the kinds of unification vars, but would need to) that I don't think being able to do typedef IO = TopLevel or similar warrants it; there's no real reason to prohibit that but there's also no real reason to want to be able to do it that I can think of.

There is a problem of sorts with my current patch, which is that this will fail:

let f (action : m a) = do { x <- action; return x; };

because there code that forall-binds free type variables naively assumes all those variables should have kind *. This is a regression of sorts, since it allowed it before; however, since it typechecks without the type signature, this isn't absolutely critical. Fixing this also requires kind inference, but of a much simpler form that's probably doable. Do we think it's worthwhile?

[sauclovian-g]

The above turns out to matter -- the failure showing in #2781 is precisely the above case with m. I think that means I should probably implement the simple kind inference needed for generalize...