Inconsistency in totality checker with different constants values and representations

[AntonPing]

Steps to Reproduce

Consider the following code:

%default total

%tcinline
f : Nat -> a -> a
f Z x = x
f (S k) x = f k x

-- this will typecheck
g1 : Nat -> Nat
g1 Z = Z
g1 (S k) = g1 (f 99 k)

-- but this will not
g2 : Nat -> Nat
g2 Z = Z
g2 (S k) = g2 (f 100 k)

-- and ... this typechecks again?!!
g3 : Nat -> Nat
g3 Z = Z
g3 (S k) = g3 (f
    ( -- here are totally 100 Ss
        S $ S $ S $ S $ S $ S $ S $ S $ S $ S $
        S $ S $ S $ S $ S $ S $ S $ S $ S $ S $
        S $ S $ S $ S $ S $ S $ S $ S $ S $ S $
        S $ S $ S $ S $ S $ S $ S $ S $ S $ S $
        S $ S $ S $ S $ S $ S $ S $ S $ S $ S $
        S $ S $ S $ S $ S $ S $ S $ S $ S $ S $
        S $ S $ S $ S $ S $ S $ S $ S $ S $ S $
        S $ S $ S $ S $ S $ S $ S $ S $ S $ S $
        S $ S $ S $ S $ S $ S $ S $ S $ S $ S $
        S $ S $ S $ S $ S $ S $ S $ S $ S $ S $
        Z
    )
    k )

Expected Behavior

Function g2 and g3 should give the same results, both typecheck or both fail. And perferrably g1 should also give the same result of g2, since there is no essential difference between 99 and 100 .

Observed Behavior

Function g1 typechecks, but g2 does not, g3 typechecks again.

Clues

Here is a copy of code in src/TTImp/Elab/App.idr

    -- If the term is an application of a primitive conversion (fromInteger etc)
    -- and it's applied to a constant, fully normalise the term.
    normalisePrims : {vs : _} ->
                     List Name -> Env Term vs ->
                     (Term vs, Glued vs) ->
                     Core (Term vs, Glued vs)
    normalisePrims prims env res
        = do tm <- Normalise.normalisePrims (`boundSafe` elabMode elabinfo)
                                            isIPrimVal
                                            (onLHS (elabMode elabinfo))
                                            prims n expargs (fst res) env
             pure (fromMaybe (fst res) tm, snd res)

      where

        boundSafe : Constant -> ElabMode -> Bool
        boundSafe _ (InLHS _) = True -- always need to expand on LHS
        -- only do this for relatively small bounds.
        -- Once it gets too big, we might be making the term
        -- bigger than it would have been without evaluating!
        boundSafe (BI x) _ = abs x < 100
        boundSafe (Str str) _ = length str < 10
        boundSafe _ _ = True

As far as I understand, it seems that compiler will normalize primitive conversion if the constant is not very large. Hence (fromInteger 99) is normalized to (S $ S $ ... $ S $ Z), while (fromInteger 100) did not. This caused that (fromInteger 100) can not pattern match against S k and Z and evaluation get stuck.