Oddities of top-level binds

[sauclovian-g]

Suppose I start out with the following definitions:

let f x = return x;
let g x = do { disable_crucible_profiling; return x; };
let h x = do { llvm_assert {{ True }}; return x; };

These give me the following types:

sawscript> :t f
{a.0, a.1} a.0 -> a.1 a.0
sawscript> :t g
{a.0} a.0 -> TopLevel a.0
sawscript> :t h
{a.0} a.0 -> LLVMSetup a.0

which is all as expected.

I can then run g 3 at the top level:

sawscript> g 3
[02:44:05.115] 3

I cannot run h 3 at the top level because it's in the wrong monad. It doesn't fail, though, just passes the value through:

sawscript> h 3
[02:45:16.771] <<monadic>>
sawscript> :t h 3
LLVMSetup Int

If I try to run f 3 it fails:

sawscript> f 3

Stack trace:
Not a monomorphic type: {a.3} a.3 Int

That is, it refuses to run a value that's polymorphic over its monad in the top level monad. This is consistent with it not failing on h 3, in the sense that it's evidently not trying to unify the type with TopLevel a. However, it doesn't seem like desirable behavior.

This behavior is also special-cased in the (syntactic) top level. In nested do-blocks the monad type is unified across the do-block:

sawscript> let foo () = do { a <- f 3; b <- g 3; return (a, b); };
sawscript> :t foo
() -> TopLevel (Int, Int)
sawscript> foo ()
[02:57:21.549] (3,3)

and

sawscript> let bar () = do { a <- f 3; b <- h 3; return (a, b); };
sawscript> :t bar
() -> LLVMSetup (Int, Int)
sawscript> bar ()
[02:58:35.553] <<monadic>>

and if you don't pin it down, it stays general:

sawscript> let baz () = do { a <- f 3; return a; };
sawscript> :t baz
{a.0} () -> a.0 Int

I think this is also undesirable and we'd be better off if the syntactic top level were equivalent to a do-block in the TopLevel monad.

(Since this weirdness is a result of the interpreter special-casing its top level, I expect it also applies to a ProofScript repl, but I haven't checked that.)

(Also, I'm not convinced this prohibition against evaluating a polymorphic term at the top level serves any purpose. But perhaps that's a separate issue.)

Note though that changing this might cause existing badly-written scripts to fail if they do <- at the top level in places where they ought to have done let.

[sauclovian-g]

It turns out that quite a few of our own scripts do in fact use <- at the top level in places where they should have used let. Also, a couple cases have turned up where an action in the wrong monad entirely was used at the top level, which previously was silently ignored.

Because of the likelihood of further fallout downstream among users, I've added workarounds so that the following forms generate warnings:

• x <- e; for non-monadic e
• x <- e; for monadic e in the wrong monad
• e; for monadic e in the wrong monad

These warnings will be kept as warnings for at least one release and possibly longer, but will eventually be changed to errors.

Note that the following form which was previously accepted (and ignored because it obviously does nothing) is now rejected:

• e; for non-monadic e

All of the above applies only at the top syntactic level. Within explicit do-blocks all of these forms were previously, and still are, rejected.

I've opened a separate ticket (#2167) for converting these warnings to errors in the future so it doesn't get forgotten.