Automatically import BOOL when strictness is applied

[radumereuta]

Fixes: #2564
This is done for the compiled definition so we don't taint program parsing.

[dwightguth]

We should generally be very careful about automatically importing things.

Before we merge this, please check whether importing BOOL into the main module fixes this issue; if it does, we should probably just fix the error message.

[ehildenb]

@dwightguth you can't even write a requires clause without BOOL being imported. Do we implicitly import bool in other contexts? What about Map module for configurations?

I think we should likely follow whatever we're doing elsewhere. As long as it's documented well, we should be OK with it. But I guess it should be disabled if the user wants too (eg. --no-implicit-imports or extend --no-prelude).

[ehildenb]

The 95% case is that users want to have BOOL implicitly imported, but we should have an escape hatch (credit to Bruce). I think I agree with this.

[dwightguth]

Sounds like the consensus is that this should just work, so I'll rescind my review.

Disagreeing opinions

[radumereuta]

A summary:

1. crashing with key not found: _andBool_ when we add strict inside the syntax module is clearly not acceptable.
2. manually adding imports private BOOL won't work because it's going to taint the program syntax.

$ kast -e 'true andBool false'
`_andBool_`(#token("true","Bool"),#token("false","Bool"))

3. ResolveStrict generates the rules in place. So importing BOOL only in the main module won't fix the problem.
4. we have precedence with implicit imports when parsing the configuration. We import MAP.
5. right now it's failing in the 95% of cases. Let's have a 5% case and see how that workaround should behave. I'm importing the module by name, so if you define your own domains.md with your own BOOL, then you can override the contents.

One thing I agree with is that documentation should be updated, so I pushed another commit. Please re-review.