Opened 16 months ago

Closed 6 months ago

#14170 closed bug (fixed)

8.2.1 regression: GHC fails to simplify `natVal`

Reported by: vagarenko Owned by: Bodigrim
Priority: high Milestone: 8.6.1
Component: Compiler Version: 8.2.1
Keywords: Cc: Bodigrim, phadej
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D4212
Wiki Page:

Description

When GHC 8.2.1 compiles this code with -O:

{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeInType            #-}

module NatVal where

import Data.Proxy
import GHC.TypeLits

foo = natVal $ Proxy @0

it produces the following Core:

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
NatVal.foo1 :: Integer
NatVal.foo1 = 0

-- RHS size: {terms: 41, types: 18, coercions: 0, joins: 0/0}
foo :: Integer
foo
  = case NatVal.foo1 of wild_a1iV {
      integer-gmp-1.0.1.0:GHC.Integer.Type.S# i#_a2ke ->
        case GHC.Prim.tagToEnum# @ Bool (GHC.Prim.>=# i#_a2ke 0#) of {
          False -> case GHC.Natural.underflowError of wild2_00 { };
          True ->
            integer-gmp-1.0.1.0:GHC.Integer.Type.wordToInteger
              (GHC.Prim.int2Word# i#_a2ke)
        };
      integer-gmp-1.0.1.0:GHC.Integer.Type.Jp# dt_a2km ->
        case GHC.Prim.uncheckedIShiftRL#
               (GHC.Prim.sizeofByteArray# dt_a2km) 3#
        of {
          __DEFAULT ->
            case GHC.Prim.sizeofByteArray# dt_a2km of {
              __DEFAULT -> wild_a1iV;
              0# -> case GHC.Natural.underflowError of wild4_00 { }
            };
          1# ->
            case GHC.Prim.indexWordArray# dt_a2km 0# of wild2_a2kq
            { __DEFAULT ->
            integer-gmp-1.0.1.0:GHC.Integer.Type.wordToInteger wild2_a2kq
            }
        };
      integer-gmp-1.0.1.0:GHC.Integer.Type.Jn# ipv_a2kt ->
        case GHC.Natural.underflowError of wild1_00 { }
    }

while GHC-8.0.1 does the right thing:

-- RHS size: {terms: 1, types: 0, coercions: 0}
foo :: Integer
foo = 0

Change History (20)

comment:1 Changed 16 months ago by RyanGlScott

I was able to track this down to commit 1fcede43d2b30f33b7505e25eb6b1f321be0407f (Introduce GHC.TypeNats module, change KnownNat evidence to be Natural), which hints at the problem. In that commit, we switched the internal representation of Nats from Integers to Naturals (from Numeric.Natural). For whatever reason, however, Natural values don't seem to simplify as well as Integers, as evidenced by this simpler program:

module Bug where

import Numeric.Natural

foo :: Natural
foo = 0

which also produces essentially identical core:

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
Bug.foo1 :: Integer
[GblId,
 Caf=NoCafRefs,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 100 0}]
Bug.foo1 = 0

-- RHS size: {terms: 39, types: 12, coercions: 0, joins: 0/0}
foo :: Natural
[GblId,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
         WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 126 60}]
foo
  = case Bug.foo1 of {
      integer-gmp-1.0.1.0:GHC.Integer.Type.S# i#_a2bZ ->
        case GHC.Prim.tagToEnum# @ Bool (GHC.Prim.>=# i#_a2bZ 0#) of {
          False -> GHC.Natural.underflowError @ Natural;
          True -> GHC.Natural.NatS# (GHC.Prim.int2Word# i#_a2bZ)
        };
      integer-gmp-1.0.1.0:GHC.Integer.Type.Jp# dt_a2c9 ->
        case GHC.Prim.uncheckedIShiftRL#
               (GHC.Prim.sizeofByteArray# dt_a2c9) 3#
        of {
          __DEFAULT ->
            case GHC.Prim.sizeofByteArray# dt_a2c9 of {
              __DEFAULT -> GHC.Natural.NatJ# dt_a2c9;
              0# -> GHC.Natural.underflowError @ Natural
            };
          1# ->
            case GHC.Prim.indexWordArray# dt_a2c9 0# of wild2_a2cd
            { __DEFAULT ->
            GHC.Natural.NatS# wild2_a2cd
            }
        };
      integer-gmp-1.0.1.0:GHC.Integer.Type.Jn# ipv_a2cg ->
        GHC.Natural.underflowError @ Natural
    }

comment:2 Changed 16 months ago by simonpj

OK here's the deal.

  • In the olden days we represented in Integer literal, say 3, in Core by S# 3#; that is, we exposed its reprsentation. That made constant folding of plusInteger 3 5 hard, becuase it meant inlining plusInteger which is remarkably big. Result: tons of useless clutter.
  • Nowadays an Integer literal, say 3, is represented in GHC by Lit (LitInteger 3), and not by an application of the data constructor S#. This latter expansion is done right at the end, by CorePrep.
  • That makes constant-folding, like 3+4 rewriting to 7 much, much easier.
  • We refrain from inlining things like plusInteger, negateInteger etc until a later stage, and instead add constant-folding rwerite rules for each of these functions. By delaying inlining, the constant-folding rewrite rules (all in compiler/prelude/PrelRules) have a decent chance to fire first.
  • However, in introducing Natural we failed to do any of this. The code
    foo :: Natural
    foo = 0
    
    turns into foo = naturalFromInteger (0::Integer), and naturalFromInteger has an INLINE pragma.

The right thing is presumably to treat Natural just like we treat Integer:

  • Keep it as a LitInteger. Conveniently LitInteger already stores its type, so we can distinguish literal integers from naturals.
  • Expand the literal in CorePrep.
  • Delay the inlining of Natural operations.
  • Add constant-folding rewrite rules to PrelRules

I suppose we could also consider making exprIsConApp_maybe on an Integer literal return S# n or whatnot; just possibly that'd be useful anyway, but only for funcions that lack a constant-fold rewrite rule.

comment:3 Changed 15 months ago by bgamari

I'm not really sure representing Integer and Natural is a great idea. Afterall, we then need to painstakingly evaluate all of the constant folding rules to ensure we don't, for instance, rewrite (5 - 9) :: Natural to -4.

Moreover, distinguishing Integer LitIntegers from Natural LitIntegers on the basis of type alone would mean that CorePrep will need to do a type comparison in cpeRhsE instead of just deciding on the basis of which Literal constructor was used. This seems more costly than necessary.

In sum, I suspect Integer and Natural are just different enough to warrant separate constructors.

Last edited 15 months ago by bgamari (previous) (diff)

comment:4 Changed 15 months ago by bgamari

Milestone: 8.2.28.2.3

Regardless, it doesn't look like this is going to happen for 8.2.2.

comment:5 Changed 13 months ago by Bodigrim

Cc: Bodigrim added

comment:6 Changed 13 months ago by Bodigrim

I am interested in this issue due to #14465. I tried to prepare a patch Phab:D4212, but stumbled upon a build issue. Can someone please explain what went wrong? Sorry, I am new to GHC build system.

"inplace/bin/ghc-stage1" -hisuf hi -osuf  o -hcsuf hc -static  -O0 -H64m -Wall      -this-unit-id base-4.11.0.0 -hide-all-packages -i -ilibraries/base/. -ilibraries/base/dist-install/build -Ilibraries/base/dist-install/build -ilibraries/base/dist-install/build/./autogen -Ilibraries/base/dist-install/build/./autogen -Ilibraries/base/include   -optP-DOPTIMISE_INTEGER_GCD_LCM -optP-include -optPlibraries/base/dist-install/build/./autogen/cabal_macros.h -package-id rts -package-id ghc-prim-0.5.2.0 -package-id integer-gmp-1.0.1.0 -this-unit-id base -XHaskell2010 -O  -no-user-package-db -rtsopts  -Wno-trustworthy-safe -Wno-deprecated-flags     -Wnoncanonical-monad-instances  -odir libraries/base/dist-install/build -hidir libraries/base/dist-install/build -stubdir libraries/base/dist-install/build   -dynamic-too -c libraries/base/./GHC/Natural.hs -o libraries/base/dist-install/build/GHC/Natural.o -dyno libraries/base/dist-install/build/GHC/Natural.dyn_o

<interactive>:1:1: error:
    Bad interface file: libraries/base/dist-install/build/GHC/Natural.hi
        libraries/base/dist-install/build/GHC/Natural.hi: openBinaryFile: does not exist (No such file or directory)

comment:7 Changed 13 months ago by bgamari

Have you tried cleaning your tree? It looks like the build system neglected to build that interface file (which is a bit perplexing, but stranger things have happened with the make build system).

comment:8 Changed 10 months ago by Bodigrim

Owner: set to Bodigrim

I'll continue with my patch this weekend, sorry for long delay.

comment:9 Changed 10 months ago by mpickering

Could we not fix this by reverting 1fcede43d2b30f33b7505e25eb6b1f321be0407f ?

Is there enough motivation to replace the evidence type?

comment:10 Changed 10 months ago by RyanGlScott

Cc: phadej added

We certainly wouldn't want to revert that commit in its entirety (if that is the route we decide to embark on)—besides changing the evidence type, that commit also reworked base a bit to export a different API in the form of the GHC.TypeNats module. We could conceivably change the evidence type and keep the new API, but it would take some care.

To be honest, I'm inclined to just wait for Bodigrim's patch. After all, these changes are already in a released version of GHC—I'd rather wait slightly longer to get things right.

(cc'ing phadej, who authored 1fcede43d2b30f33b7505e25eb6b1f321be0407f)

comment:11 Changed 10 months ago by phadej

Yes, IMO there is enough motivation to have evidence as Natural. We are talking about type level Nats, not Ints.

The fact that term value Naturals are second-grade citizens in GHC atm is unfortunate. If we are able to constant fold other numeric types, we should be able to do that for Natural too.

See https://phabricator.haskell.org/D3024 discussion.

I'm in great favour of adding Natural literal into core. It was untrivial and I didn't pursue that back then, but again IMO it's the right thing to do.

Pushing even further, I'd propose to introduce {-# LANGUAGE NaturalLiterals #-}, so 2 is desugared to 2 :: FromNatural a => a where class fromNatural :: FromNatural a where Natural -> a (use Num or better FromInteger if NegativeLiterals is enabled and literal is in fact negative). Putting that behind the language extension doesn't break old code (which needs Num a => a).

Side-question: how constant folding works when cross-compiling, when Int is of different bit-widths on host and target?

comment:12 Changed 10 months ago by simonpj

I'm in great favour of adding Natural literal into core. It was untrivial and I didn't pursue that back then,

As comment:2 says, it's not trivial in the sense of "only 3 lines of code", but it is trivial (or at least easy) in the sense of "just follow the pattern of Integer". I often find myself liking things that are simple and explicable even if they do a bit more duplication than we'd ideally like.

comment:13 Changed 9 months ago by hsyl20

Differential Rev(s): Phab:D4212
Status: newpatch

comment:14 Changed 8 months ago by hsyl20

Milestone: 8.2.38.6.1

comment:15 Changed 6 months ago by darchon

I would really like this patch to land in 8.6.1 as our Clash Haskell-to-Hardware compiler has to work a lot harder with these unsimplified naturals. I just saw that a 8.6 branch was created on git, hence why I'm posting now. Patch D4212 seems to have gotten the OKs, what still needs to happen to it before it lands in HEAD and can end up in the 8.6 branch?

comment:16 Changed 6 months ago by Bodigrim

+1 to have it merged into 8.6.1.

comment:17 Changed 6 months ago by hsyl20

I've just rebased D4212 on master. It should be ready to land.

comment:18 Changed 6 months ago by bgamari

Alright, given how long this patch has been in limbo I'm willing to merge it. Thanks for the rebase, hsyl20.

comment:19 Changed 6 months ago by Ben Gamari <ben@…>

In fe770c21/ghc:

Built-in Natural literals in Core

Add support for built-in Natural literals in Core.

- Replace MachInt,MachWord, LitInteger, etc. with a single LitNumber
  constructor with a LitNumType field
- Support built-in Natural literals
- Add desugar warning for negative literals
- Move Maybe(..) from GHC.Base to GHC.Maybe for module dependency
  reasons

This patch introduces only a few rules for Natural literals (compared
to Integer's rules). Factorization of the built-in rules for numeric
literals will be done in another patch as this one is already big to
review.

Test Plan:
  validate
  test build with integer-simple

Reviewers: hvr, bgamari, goldfire, Bodigrim, simonmar

Reviewed By: bgamari

Subscribers: phadej, simonpj, RyanGlScott, carter, hsyl20, rwbarton,
thomie

GHC Trac Issues: #14170, #14465

Differential Revision: https://phabricator.haskell.org/D4212

comment:20 Changed 6 months ago by bgamari

Resolution: fixed
Status: patchclosed
Note: See TracTickets for help on using tickets.