[BUG] ")dis op groebner" error only in SBCL

[Qian Yun]

There are 6 unexposed functions called groebner :

>> System error:
The value
(|#| D4)
is not of type
INTEGER
when binding |n|


With the help of fricas0 and fricas0-repo, it is easily bisected
to commit 2e4faf4b (2022-01-15).

Strangely, this error only happens in SBCL.

- Qian

[Qian Yun]

So the added check in this commit exposed the bug, real problem
happen in "formArguments2String" when trying to format a type.

Can the recently added "constructor_to_OutputForm" be helpful
in here?

- Qian

[Waldek Hebisch]

On Thu, Nov 23, 2023 at 05:06:59PM +0800, Qian Yun wrote:
> So the added check in this commit exposed the bug, real problem
> happen in "formArguments2String" when trying to format a type.
>
> Can the recently added "constructor_to_OutputForm" be helpful
> in here?

We need more. AFAICS trouble is caused by condition which
contains an expression. This is actually _much_ bigger
problem, it is related to using types with nontrivial
parameters in signatures.

Ideally, one should be able to put arbitrary (or at least
resonably complex) expression in place of non-domain parameter
to a type. But currently even "interesting" constants
cause troubles. First step in solving this is to define consistent
representation of such types. Currently compiler/interprter code
basically takes representaion from Lisp. But in Lisp
we have unevaluated expressions which in some situations must
be evaluated to get runtime values. So in fact we get
two distinct Lisp representatins. When we dealing with
expressions, Spad compiler has its own represention which
is later transformed to Lisp. Actually, when typechecking
compiler and interpeter change between various representations.
And interpeter uses different representation than Spad compiler.
So, there is several different representation and only one
'form2String' which tries to handle all and consequently
get confused in more complicated cases.

So proper fix will require work in many places to make
various part consistent. ATM we could try to add some
local tests to avoid popular bad cases, but those are
workarounds that do not solve core problem.

--
Waldek Hebisch

[Qian Yun]

On 11/24/23 09:55, Waldek Hebisch wrote:
> On Thu, Nov 23, 2023 at 05:06:59PM +0800, Qian Yun wrote:
>> So the added check in this commit exposed the bug, real problem
>> happen in "formArguments2String" when trying to format a type.
>>
>> Can the recently added "constructor_to_OutputForm" be helpful
>> in here?
>
> We need more. AFAICS trouble is caused by condition which
> contains an expression. This is actually _much_ bigger
> problem, it is related to using types with nontrivial
> parameters in signatures.

Is this dependent type? If so, correctly implement it
requires lots of work I guess.

- Qian