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