[m-dev.] accepting "any" as "ground" for non-solver types

[Julien Fischer]

On Tue, 2 Jul 2024 at 15:16, Zoltan Somogyi <zoltan.somogyi at runbox.com> wrote:
>
> Since a commit in 2003 (whose log message is attached), we have
> been accepting "any" insts on non-solver types as being "ground".
> I am just finishing a change that passes the actual type of the variable
> being tested for groundness to inst_is_ground, and this ancient rule
> causes a minor problem. The symptom is a missing error message
> for tests/invalid/bad_fact_table_decls. The message in question
> is the one that complains about mode "ia", i.e. input-any, as not
> being acceptable in a fact table.
>
> The underlying reason lies the call chain from code of inst_is_ground_mt_2
> to maybe_any_to_bound, to type_may_contain_solver_type.
> In the absence of valid type info, the type being passed here
> was a type var, for which the conservative answer to "may this contain
> a solver type" was yes. This caused "ia" to NOT be treated as a non-solver
> type, so it was not considered ground. But when you pass the *actual* type
> of the argument, an integer, type_may_contain_a_solver_type fails,
> and the any *is* considered to be ground, and thus you get no error message.
>
> This is quite unintuitive behavior. The log messages says that this behavior
> is required to support HAL, but of course HAL is long dead. Is there any
> *current* reason to retain this behavior? If not, I would very much like to
> get rid of it.

I am not aware of any reason for continuing to support that behaviour.

Julien.