type inferencing failure on (* float t) SBCL 2.0.9

[Andrew Berkley]

(declaim (ftype (function (fixnum) (values fixnum)) blarg))

(defun blarg (n)
  (declare (type fixnum n))
  n)

(defun does-not-warn-on-compilation (x)
  (blarg (* 3f0 x)))

(defun does-warn-on-compilation (x)
  (declare (type fixnum x))
  (blarg (* 3f0 x)))

The result of the multiply should be (or float (complex float)) which does not intersect fixnum. Instead we get type number (I think) because we end up with generic numeric-contagion?

[Andrew Berkley (ajberkley)]

While fixing this I found what looks like a bug in https://github.com/sbcl/sbcl/commit/eb3307177a80c124f233d21ca9087fea63c39019#diff-716727851812af3d6d0a0b227549af70c133e6080bd085d52fa939a25f5b4515

at line 373 of early-type.lisp, (specifier-type 'real) should be (specifier-type 'float)

[Andrew Berkley (ajberkley)]

Here is a proposed solution https://github.com/ajberkley/sbcl/commit/5464c1729b49c06708e91b21abc2452fe60cdddf

It includes the fix to the problem I listed above.

I don't understand the reason I need the type-union in numeric-contagion as :complexp nil should be an OK specification for a numeric-type, but it messes up some type derivation while compiling the examples above.

I will look further into it.

[Andrew Berkley (ajberkley)]

Updated against changes to master

 https://github.com/ajberkley/sbcl/commit/6f682759ee598f460d973d70f3efd30d016cf022

[Andrew Berkley (ajberkley)]

Sorry for the spam. I removed some of the code indentation changes

https://github.com/ajberkley/sbcl/commit/59b88de767e07b5bb870a6d3ee42b198edc4b996

[Stas Boukarev (stassats)]

(let ((x 813.0d0))
    (values
     (decf x)
     x))

fails to compile after this.

[Stas Boukarev (stassats)]

And (lambda (x y) (atan x y))

[Andrew Berkley (ajberkley)]

I'll look into it!

[Andrew Berkley (ajberkley)]

The atan case looks fixable, though ugly. There are several other cases where numeric-contagion is assumed to return a numeric-type, not a union type, though it explicitly says it can return a union type. I need to understand how and why the code chooses to represent types in certain ways to make progress which will take some time.

I added a patch to handle the decf case here https://github.com/ajberkley/sbcl/commit/2bec2009920685254aad0af1bc36551ac6399839

It is triggered also with the simpler:

(let ((x 813.0d0))
   (decf x))

The problem was maybe-infer-iteration-var-type which assumes that numeric-contagion always returns a numeric-type and not a union of numeric types. Similar to the atan case. If the comment on numeric-contagion is correct, then fixing this is good. I will need to think through whether we would want to do better than just failing in this case (assuming that in a later pass of the constraint phase the types will be tighter and we will succeed?).

[Andrew Berkley (ajberkley)]

And similarly a patch to handle atan (and others): https://github.com/ajberkley/sbcl/commit/67e675483898636773cd2c512cf28d5064361a07

I'm not particularly happy with my knowledge of the whole type / type derivation system here and what promises may or may not be broken. But, since stassats patch to return a union-type on :complexp nil is in the main branch probably best to get these in.

[Andrew Berkley (ajberkley)]

and finally a test

https://github.com/ajberkley/sbcl/commit/760c33b44bf92635c13f77a725e214acfb18f653

[Stas Boukarev (stassats)]

Can you format it into a single patch?

[Andrew Berkley (ajberkley)]

Done, and made a pull request to github.com/sbcl/sbcl

[Stas Boukarev (stassats)]

SBCL isn't developed through github, so pull requests don't do much.

[Andrew Berkley (ajberkley)]

OK: https://github.com/ajberkley/sbcl/commit/8b120a5c4fb9478addcd7fa14aa195d72810f394

I'm attaching a diff here.

[Andrew Berkley (ajberkley)]

Attaching a minor one line tightening fix to this change.

[Stas Boukarev (stassats)]

Do you have a test case for it?

[Andrew Berkley (ajberkley)]

I can't find one--- it may be that it never occurs. It's just a consistency change to make sure the code does the same thing for union types as it would for non-union types.

[Stas Boukarev (stassats)]

Ok.