Warning?

[Ralf Hemmecke]

Hello Waldek,

during compilation of a package of mine, I get a warning. I think that
this should not appear since I believe that everything is fine.

Warnings:
[1] findIdentity: not known that (QEtaAlgebra C) is of mode
(CATEGORY domain (SIGNATURE * ($ C $)) (IF (has (Finite0Series C (QUOTE
q) (Zero)) (QEtaGradedAlgebra C)) (ATTRIBUTE (QEtaGradedAlgebra C))
noBranch) (IF (has (Finite0Series C (QUOTE q) (Zero)) (XEtaGradedAlgebra
C)) (ATTRIBUTE (XEtaGradedAlgebra C)) noBranch))

Clearly, it is hard for you to figure out where it comes from, but the
actual code is too big to post it here. Let me give more details. I
actually would like to know whether you think that it is worth it to
investigate further.

A1 C ==> Finite0Series(C, 'q, 0)
CA1 C ==> QEtaAlgebraCachedPower(C, A1 C)
CPol C ==> QEtaAlgebraCachedPower(C, Pol C)
X1 C ==> QEtaExtendedAlgebra(C, CA1 C, CPol C)
toX1(C, a, b) ==> embed(a::CA1(C), b::CPol(C))$X1(C)

The warning starts to appear when I use/compile toX1(f, pol) in another
package.

Since the QEtaAlgebraCachedPower it only a wrapper domain, I can also
compile without it.

X1 C ==> QEtaExtendedAlgebra(C, A1 C, Pol C)
toX1(C, a, b) ==> embed(a, b)$X1(C)

In that case no warnig appears.

So let's look at

QEtaAlgebraCachedPower(C, A): Exports == Implementation where
C: CommutativeRing
A: Join(Monoid, AbelianGroup) with
_*: (C, %) -> %
Exports ==> Join(Monoid, AbelianGroup, CoercibleFrom A, CoercibleTo A)
with
_*: (C, %) -> %
if A has QEtaGradedAlgebra C then QEtaGradedAlgebra C
if A has XEtaGradedAlgebra C then XEtaGradedAlgebra C
Implementation ==> CachedPower A add ...

Finit0Series is definitely of category QEtaGradedAlgebra (which is an
extension of QEtaAlgebra by a few functions connected to grading).

So compiler knows that QEtaExtendedAlgebra is to be compiled with
arguments that are of type QEtaGradedAlgebra.

It seems that the compiler is unable to figure out during compilation of
embed(a::CA1(C), b::CPol(C))$X1(C) that the arguments for
QEtaExtendedAlgebra are perfectly fine of type QEtaGradedAlgebra. All
information is there.

My guess is that the compiler is a bit weak to conclude from the fact
that A in QEtaAlgebraCachedPower(C, A) is of type QEtaGradedAlgebra,
also QEtaAlgebraCachedPower(C, A) is of type QEtaGradedAlgebra and
therefore throws the warning at me.

Well, it is only a warning, but if warings appear when they shouldn't
that is irritating.

BTW, so far I detected no problem at runtime.

Ralf

[Waldek Hebisch]

On Sat, Nov 14, 2020 at 10:45:39AM +0100, Ralf Hemmecke wrote:
> Hello Waldek,
>
> during compilation of a package of mine, I get a warning. I think that
> this should not appear since I believe that everything is fine.
>
> Warnings:
> [1] findIdentity: not known that (QEtaAlgebra C) is of mode
> (CATEGORY domain (SIGNATURE * ($ C $)) (IF (has (Finite0Series C (QUOTE
> q) (Zero)) (QEtaGradedAlgebra C)) (ATTRIBUTE (QEtaGradedAlgebra C))
> noBranch) (IF (has (Finite0Series C (QUOTE q) (Zero)) (XEtaGradedAlgebra
> C)) (ATTRIBUTE (XEtaGradedAlgebra C)) noBranch))
>
> Clearly, it is hard for you to figure out where it comes from,

Well, message is generated in 'src/interp/c-util.boot' in
function 'extendsCategoryForm'. This function is called only
in few places, so it is clear "where it comes from".

> but the
> actual code is too big to post it here. Let me give more details. I
> actually would like to know whether you think that it is worth it to
> investigate further.

There are several warnings like above during build. They
are really compiler bug: compiler issues this warning when it
accepts code "on faith". There are tens of domains which
would not compile when the hole is removed. In some cases
with reasonable effort one could rewrite code so that it
is accepted by current compiler. But in many cases it is not
clear if reasonable workaround is possible.

Your example is iteresting, because actual failure looks
different than other examples.

Of course, proper fix is to modify compiler so that it
can correctly perform type checks, but that is "global"
problem, namely we need to collect type information in
proper places, store and propagate it etc. Currently
compiler has problem because some information is only
available at runtime and playes tricks to compute
what will happen at runtime before code is compiled
(this is hard problem, full and correct solution is
uncomputable). Unfortunatly, there are mismatches
between compile time and runtime representation of data.
'extendsCategoryForm' is particularly strongly
affected...

--
Waldek Hebisch

[Ralf Hemmecke]

> Your example is iteresting, because actual failure looks
> different than other examples.

Does that mean you want to investigate further and want me to perpare a
minimal example?

I'm asking, because it would probably take me quite some time to remove
all code that is not relevant for that bug. And at the moment I am
rather interested in working code (which I currently have) than in doing
other stuff.

Ralf

[Waldek Hebisch]

On Sat, Nov 14, 2020 at 10:00:12PM +0100, Ralf Hemmecke wrote:
> > Your example is iteresting, because actual failure looks
> > different than other examples.
>
> Does that mean you want to investigate further and want me to perpare a
> minimal example?

No, from your data I can produce resonably small example giving:

[1] get_it: not known that (QEtaGradedAlgebra C) is of mode (CATEGORY domain (SIGNATURE * ($ C $)) (IF (has (Finite0Series C) (QEtaGradedAlgebra C)) (ATTRIBUTE (QEtaGradedAlgebra C)) noBranch) (IF (has (Finite0Series C) (XEtaGradedAlgebra C)) (ATTRIBUTE (XEtaGradedAlgebra C)) noBranch))

That should be enough.

--
Waldek Hebisch