diff --git a/base/compiler/abstractinterpretation.jl b/base/compiler/abstractinterpretation.jl
index 1249e91f885da..2d72a171ff070 100644
--- a/base/compiler/abstractinterpretation.jl
+++ b/base/compiler/abstractinterpretation.jl
@@ -12,9 +12,11 @@ const _REF_NAME = Ref.body.name
 # logic #
 #########
 
-# see if the inference result might affect the final answer
-call_result_unused(frame::InferenceState, pc::LineNum=frame.currpc) =
-    isexpr(frame.src.code[frame.currpc], :call) && isempty(frame.ssavalue_uses[pc])
+# See if the inference result of the current statement's result value might affect
+# the final answer for the method (aside from optimization potential and exceptions).
+# To do that, we need to check both for slot assignment and SSA usage.
+call_result_unused(frame::InferenceState) =
+    isexpr(frame.src.code[frame.currpc], :call) && isempty(frame.ssavalue_uses[frame.currpc])
 
 # check if this return type is improvable (i.e. whether it's possible that with
 # more information, we might get a more precise type)
@@ -192,6 +194,16 @@ function abstract_call_gf_by_type(interp::AbstractInterpreter, @nospecialize(f),
         end
     end
     #print("=> ", rettype, "\n")
+    if rettype isa LimitedAccuracy
+        union!(sv.pclimitations, rettype.causes)
+        rettype = rettype.typ
+    end
+    if !isempty(sv.pclimitations) # remove self, if present
+        delete!(sv.pclimitations, sv)
+        for caller in sv.callers_in_cycle
+            delete!(sv.pclimitations, caller)
+        end
+    end
     return CallMeta(rettype, info)
 end
 
@@ -313,7 +325,6 @@ function abstract_call_method_with_const_args(interp::AbstractInterpreter, @nosp
         inf_result = InferenceResult(mi, argtypes)
         frame = InferenceState(inf_result, #=cache=#false, interp)
         frame === nothing && return Any # this is probably a bad generated function (unsound), but just ignore it
-        frame.limited = true
         frame.parent = sv
         push!(inf_cache, inf_result)
         typeinf(interp, frame) || return Any
@@ -394,7 +405,7 @@ function abstract_call_method(interp::AbstractInterpreter, method::Method, @nosp
                             parent = parent::InferenceState
                             parent_method2 = parent.src.method_for_inference_limit_heuristics # limit only if user token match
                             parent_method2 isa Method || (parent_method2 = nothing) # Union{Method, Nothing}
-                            if (parent.cached || parent.limited) && parent.linfo.def === sv.linfo.def && sv_method2 === parent_method2
+                            if (parent.cached || parent.parent !== nothing) && parent.linfo.def === sv.linfo.def && sv_method2 === parent_method2
                                 topmost = infstate
                                 edgecycle = true
                             end
@@ -443,7 +454,8 @@ function abstract_call_method(interp::AbstractInterpreter, method::Method, @nosp
                 # (non-typically, this means that we lose the ability to detect a guaranteed StackOverflow in some cases)
                 return Any, true, nothing
             end
-            poison_callstack(sv, topmost::InferenceState, true)
+            topmost = topmost::InferenceState
+            poison_callstack(sv, topmost.parent === nothing ? topmost : topmost.parent)
             sig = newsig
             sparams = svec()
         end
@@ -1129,7 +1141,12 @@ function abstract_eval_value(interp::AbstractInterpreter, @nospecialize(e), vtyp
     if isa(e, Expr)
         return abstract_eval_value_expr(interp, e, vtypes, sv)
     else
-        return abstract_eval_special_value(interp, e, vtypes, sv)
+        typ = abstract_eval_special_value(interp, e, vtypes, sv)
+        if typ isa LimitedAccuracy
+            union!(sv.pclimitations, typ.causes)
+            typ = typ.typ
+        end
+        return typ
     end
 end
 
@@ -1252,13 +1269,21 @@ function abstract_eval_statement(interp::AbstractInterpreter, @nospecialize(e),
             end
         end
     else
-        return abstract_eval_value_expr(interp, e, vtypes, sv)
+        t = abstract_eval_value_expr(interp, e, vtypes, sv)
     end
     @assert !isa(t, TypeVar)
     if isa(t, DataType) && isdefined(t, :instance)
         # replace singleton types with their equivalent Const object
         t = Const(t.instance)
     end
+    if !isempty(sv.pclimitations)
+        if t isa Const || t === Union{}
+            empty!(sv.pclimitations)
+        else
+            t = LimitedAccuracy(t, sv.pclimitations)
+            sv.pclimitations = IdSet{InferenceState}()
+        end
+    end
     return t
 end
 
@@ -1313,10 +1338,18 @@ function typeinf_local(interp::AbstractInterpreter, frame::InferenceState)
             elseif isa(stmt, GotoIfNot)
                 condt = abstract_eval_value(interp, stmt.cond, s[pc], frame)
                 if condt === Bottom
+                    empty!(frame.pclimitations)
                     break
                 end
                 condval = maybe_extract_const_bool(condt)
                 l = stmt.dest::Int
+                if !isempty(frame.pclimitations)
+                    # we can't model the possible effect of control
+                    # dependencies on the return value, so we propagate it
+                    # directly to all the return values (unless we error first)
+                    condval isa Bool || union!(frame.limitations, frame.pclimitations)
+                    empty!(frame.pclimitations)
+                end
                 # constant conditions
                 if condval === true
                 elseif condval === false
@@ -1351,6 +1384,14 @@ function typeinf_local(interp::AbstractInterpreter, frame::InferenceState)
                     # and is valid inter-procedurally
                     rt = widenconst(rt)
                 end
+                # copy limitations to return value
+                if !isempty(frame.pclimitations)
+                    union!(frame.limitations, frame.pclimitations)
+                    empty!(frame.pclimitations)
+                end
+                if !isempty(frame.limitations)
+                    rt = LimitedAccuracy(rt, copy(frame.limitations))
+                end
                 if tchanged(rt, frame.bestguess)
                     # new (wider) return type for frame
                     frame.bestguess = tmerge(frame.bestguess, rt)
@@ -1425,6 +1466,8 @@ function typeinf_local(interp::AbstractInterpreter, frame::InferenceState)
                 end
             end
 
+            @assert isempty(frame.pclimitations) "unhandled LimitedAccuracy"
+
             if t === nothing
                 # mark other reached expressions as `Any` to indicate they don't throw
                 frame.src.ssavaluetypes[pc] = Any
diff --git a/base/compiler/inferencestate.jl b/base/compiler/inferencestate.jl
index 2d5fce04c0454..3a25cf753ae82 100644
--- a/base/compiler/inferencestate.jl
+++ b/base/compiler/inferencestate.jl
@@ -10,6 +10,8 @@ mutable struct InferenceState
     slottypes::Vector{Any}
     mod::Module
     currpc::LineNum
+    pclimitations::IdSet{InferenceState} # causes of precision restrictions (LimitedAccuracy) on currpc ssavalue
+    limitations::IdSet{InferenceState} # causes of precision restrictions (LimitedAccuracy) on return
 
     # info on the state of inference and the linfo
     src::CodeInfo
@@ -39,7 +41,6 @@ mutable struct InferenceState
 
     # TODO: move these to InferenceResult / Params?
     cached::Bool
-    limited::Bool
     inferred::Bool
     dont_work_on_me::Bool
 
@@ -105,6 +106,7 @@ mutable struct InferenceState
         frame = new(
             InferenceParams(interp), result, linfo,
             sp, slottypes, inmodule, 0,
+            IdSet{InferenceState}(), IdSet{InferenceState}(),
             src, get_world_counter(interp), valid_worlds,
             nargs, s_types, s_edges, stmt_info,
             Union{}, W, 1, n,
@@ -113,7 +115,7 @@ mutable struct InferenceState
             Vector{Tuple{InferenceState,LineNum}}(), # cycle_backedges
             Vector{InferenceState}(), # callers_in_cycle
             #=parent=#nothing,
-            cached, false, false, false,
+            cached, false, false,
             CachedMethodTable(method_table(interp)),
             interp)
         result.result = frame
@@ -261,37 +263,13 @@ function add_mt_backedge!(mt::Core.MethodTable, @nospecialize(typ), caller::Infe
     nothing
 end
 
-function poison_callstack(infstate::InferenceState, topmost::InferenceState, poison_topmost::Bool)
-    poison_topmost && (topmost = topmost.parent)
-    while !(infstate === topmost)
-        if call_result_unused(infstate)
-            # If we won't propagate the result any further (since it's typically unused),
-            # it's OK that we keep and cache the "limited" result in the parents
-            # (non-typically, this means that we lose the ability to detect a guaranteed StackOverflow in some cases)
-            # TODO: we might be able to halt progress much more strongly here,
-            # since now we know we won't be able to keep anything much that we learned.
-            # We were mainly only here to compute the calling convention return type,
-            # but in most situations now, we are unlikely to be able to use that information.
-            break
-        end
-        infstate.limited = true
-        for infstate_cycle in infstate.callers_in_cycle
-            infstate_cycle.limited = true
-        end
-        infstate = infstate.parent
-        infstate === nothing && return
-    end
-end
-
 function print_callstack(sv::InferenceState)
     while sv !== nothing
         print(sv.linfo)
-        sv.limited && print("  [limited]")
         !sv.cached && print("  [uncached]")
         println()
         for cycle in sv.callers_in_cycle
             print(' ', cycle.linfo)
-            cycle.limited && print("  [limited]")
             println()
         end
         sv = sv.parent
diff --git a/base/compiler/tfuncs.jl b/base/compiler/tfuncs.jl
index dca508d605cde..faaee3d9ba0b1 100644
--- a/base/compiler/tfuncs.jl
+++ b/base/compiler/tfuncs.jl
@@ -1586,10 +1586,14 @@ function return_type_tfunc(interp::AbstractInterpreter, argtypes::Vector{Any}, s
                         # output was computed to be constant
                         return Const(typeof(rt.val))
                     else
+                        inaccurate = nothing
+                        rt isa LimitedAccuracy && (inaccurate = rt.causes; rt = rt.typ)
                         rt = widenconst(rt)
                         if hasuniquerep(rt) || rt === Bottom
                             # output type was known for certain
                             return Const(rt)
+                        elseif inaccurate !== nothing
+                            return LimitedAccuracy(Type{<:rt}, inaccurate)
                         elseif (isa(tt, Const) || isconstType(tt)) &&
                             (isa(aft, Const) || isconstType(aft))
                             # input arguments were known for certain
diff --git a/base/compiler/typeinfer.jl b/base/compiler/typeinfer.jl
index c2769bf18c81e..b71bd93fa3072 100644
--- a/base/compiler/typeinfer.jl
+++ b/base/compiler/typeinfer.jl
@@ -28,7 +28,6 @@ struct InferenceFrameInfo
     sptypes::Vector{Any}
     slottypes::Vector{Any}
     nargs::Int
-    limited::Bool
 end
 
 function _typeinf_identifier(frame::Core.Compiler.InferenceState)
@@ -38,7 +37,6 @@ function _typeinf_identifier(frame::Core.Compiler.InferenceState)
         copy(frame.sptypes),
         copy(frame.slottypes),
         frame.nargs,
-        frame.limited,
     )
     return mi_info
 end
@@ -85,7 +83,7 @@ function reset_timings()
     empty!(_timings)
     push!(_timings, Timing(
         # The MethodInstance for ROOT(), and default empty values for other fields.
-        InferenceFrameInfo(ROOTmi, 0x0, Any[], Any[Core.Const(ROOT)], 1, false),
+        InferenceFrameInfo(ROOTmi, 0x0, Any[], Any[Core.Const(ROOT)], 1),
         _time_ns()))
     return nothing
 end
@@ -234,51 +232,45 @@ function _typeinf(interp::AbstractInterpreter, frame::InferenceState)
     results = Tuple{InferenceResult, Vector{Any}, Bool}[
             ( frames[i].result,
               frames[i].stmt_edges[1],
-              frames[i].cached || frames[i].parent !== nothing )
+              frames[i].cached )
         for i in 1:length(frames) ]
     empty!(frames)
-    cached = frame.cached
-    if cached || frame.parent !== nothing
-        for (caller, _, doopt) in results
+    if may_optimize(interp)
+        for (caller, _, _) in results
             opt = caller.src
             if opt isa OptimizationState
-                run_optimizer = doopt && may_optimize(interp)
-                if run_optimizer
-                    optimize(interp, opt, OptimizationParams(interp), caller.result)
-                    finish(opt.src, interp)
-                    # finish updating the result struct
-                    validate_code_in_debug_mode(opt.linfo, opt.src, "optimized")
-                    if opt.const_api
-                        if caller.result isa Const
-                            caller.src = caller.result
-                        else
-                            @assert isconstType(caller.result)
-                            caller.src = Const(caller.result.parameters[1])
-                        end
-                    elseif opt.src.inferred
-                        caller.src = opt.src::CodeInfo # stash a copy of the code (for inlining)
+                result_type = caller.result
+                @assert !(result_type isa LimitedAccuracy)
+                optimize(interp, opt, OptimizationParams(interp), result_type)
+                finish(opt.src, interp)
+                # finish updating the result struct
+                validate_code_in_debug_mode(opt.linfo, opt.src, "optimized")
+                if opt.const_api
+                    if result_type isa Const
+                        caller.src = result_type
                     else
-                        caller.src = nothing
+                        @assert isconstType(result_type)
+                        caller.src = Const(result_type.parameters[1])
                     end
+                elseif opt.src.inferred
+                    caller.src = opt.src::CodeInfo # stash a copy of the code (for inlining)
+                else
+                    caller.src = nothing
                 end
                 caller.valid_worlds = opt.inlining.et.valid_worlds[]
             end
         end
     end
-    for (caller, edges, doopt) in results
+    for (caller, edges, cached) in results
         valid_worlds = caller.valid_worlds
-        if last(valid_worlds) == get_world_counter()
-            valid_worlds = WorldRange(first(valid_worlds), typemax(UInt))
-        end
-        caller.valid_worlds = valid_worlds
-        if cached
-            cache_result!(interp, caller)
-        end
-        if doopt && last(valid_worlds) == typemax(UInt)
+        if last(valid_worlds) >= get_world_counter()
             # if we aren't cached, we don't need this edge
             # but our caller might, so let's just make it anyways
             store_backedges(caller, edges)
         end
+        if cached
+            cache_result!(interp, caller)
+        end
     end
     return true
 end
@@ -286,20 +278,22 @@ end
 function CodeInstance(result::InferenceResult, @nospecialize(inferred_result::Any),
                       valid_worlds::WorldRange)
     local const_flags::Int32
+    result_type = result.result
+    @assert !(result_type isa LimitedAccuracy)
     if inferred_result isa Const
         # use constant calling convention
         rettype_const = (result.src::Const).val
         const_flags = 0x3
         inferred_result = nothing
     else
-        if isa(result.result, Const)
-            rettype_const = (result.result::Const).val
+        if isa(result_type, Const)
+            rettype_const = result_type.val
             const_flags = 0x2
-        elseif isconstType(result.result)
-            rettype_const = result.result.parameters[1]
+        elseif isconstType(result_type)
+            rettype_const = result_type.parameters[1]
             const_flags = 0x2
-        elseif isa(result.result, PartialStruct)
-            rettype_const = (result.result::PartialStruct).fields
+        elseif isa(result_type, PartialStruct)
+            rettype_const = result_type.fields
             const_flags = 0x2
         else
             rettype_const = nothing
@@ -307,7 +301,7 @@ function CodeInstance(result::InferenceResult, @nospecialize(inferred_result::An
         end
     end
     return CodeInstance(result.linfo,
-        widenconst(result.result), rettype_const, inferred_result,
+        widenconst(result_type), rettype_const, inferred_result,
         const_flags, first(valid_worlds), last(valid_worlds))
 end
 
@@ -365,6 +359,11 @@ end
 
 function cache_result!(interp::AbstractInterpreter, result::InferenceResult)
     valid_worlds = result.valid_worlds
+    if last(valid_worlds) == get_world_counter()
+        # if we've successfully recorded all of the backedges in the global reverse-cache,
+        # we can now widen our applicability in the global cache too
+        valid_worlds = WorldRange(first(valid_worlds), typemax(UInt))
+    end
     # check if the existing linfo metadata is also sufficient to describe the current inference result
     # to decide if it is worth caching this
     already_inferred = already_inferred_quick_test(interp, result.linfo)
@@ -381,6 +380,28 @@ function cache_result!(interp::AbstractInterpreter, result::InferenceResult)
     nothing
 end
 
+function cycle_fix_limited(@nospecialize(typ), sv::InferenceState)
+    if typ isa LimitedAccuracy
+        if sv.parent === nothing
+            # when part of a cycle, we might have unintentionally introduced a limit marker
+            @assert !isempty(sv.callers_in_cycle)
+            return typ.typ
+        end
+        causes = copy(typ.causes)
+        delete!(causes, sv)
+        for caller in sv.callers_in_cycle
+            delete!(causes, caller)
+        end
+        if isempty(causes)
+            return typ.typ
+        end
+        if length(causes) != length(typ.causes)
+            return LimitedAccuracy(typ.typ, causes)
+        end
+    end
+    return typ
+end
+
 # inference completed on `me`
 # update the MethodInstance
 function finish(me::InferenceState, interp::AbstractInterpreter)
@@ -400,16 +421,43 @@ function finish(me::InferenceState, interp::AbstractInterpreter)
         append!(s_edges, me.src.edges)
         me.src.edges = nothing
     end
-    if me.limited && me.cached && me.parent !== nothing
-        # a top parent will be cached still, but not this intermediate work
+    # inspect whether our inference had a limited result accuracy,
+    # else it may be suitable to cache
+    me.bestguess = cycle_fix_limited(me.bestguess, me)
+    limited_ret = me.bestguess isa LimitedAccuracy
+    limited_src = false
+    if !limited_ret
+        gt = me.src.ssavaluetypes
+        for j = 1:length(gt)
+            gt[j] = gtj = cycle_fix_limited(gt[j], me)
+            if gtj isa LimitedAccuracy && me.parent !== nothing
+                limited_src = true
+                break
+            end
+        end
+    end
+    if limited_ret
+        # a parent may be cached still, but not this intermediate work:
         # we can throw everything else away now
+        me.result.src = nothing
         me.cached = false
+        me.src.inlineable = false
         unlock_mi_inference(interp, me.linfo)
+    elseif limited_src
+        # a type result will be cached still, but not this intermediate work:
+        # we can throw everything else away now
+        me.result.src = nothing
         me.src.inlineable = false
     else
-        # annotate fulltree with type information
-        type_annotate!(me)
-        me.result.src = OptimizationState(me, OptimizationParams(interp), interp)
+        # annotate fulltree with type information,
+        # either because we are the outermost code, or we might use this later
+        doopt = (me.cached || me.parent !== nothing)
+        type_annotate!(me, doopt)
+        if doopt
+            me.result.src = OptimizationState(me, OptimizationParams(interp), interp)
+        else
+            me.result.src = me.src::CodeInfo # stash a convenience copy of the code (e.g. for reflection)
+        end
     end
     me.result.valid_worlds = me.valid_worlds
     me.result.result = me.bestguess
@@ -497,7 +545,7 @@ end
 function visit_slot_load!(sl::Slot, vtypes::VarTable, sv::InferenceState, undefs::Array{Bool,1})
     id = slot_id(sl)
     s = vtypes[id]
-    vt = widenconditional(s.typ)
+    vt = widenconditional(ignorelimited(s.typ))
     if s.undef
         # find used-undef variables
         undefs[id] = true
@@ -542,10 +590,9 @@ function record_slot_assign!(sv::InferenceState)
 end
 
 # annotate types of all symbols in AST
-function type_annotate!(sv::InferenceState)
-    # delete dead statements only if we're building this IR to cache it
-    # (otherwise, we'll run the optimization passes later, outside of inference)
-    run_optimizer = (sv.cached || sv.parent !== nothing)
+function type_annotate!(sv::InferenceState, run_optimizer::Bool)
+    # as an optimization, we delete dead statements immediately if we're going to run the optimizer
+    # (otherwise, we'll perhaps run the optimization passes later, outside of inference)
 
     # remove all unused ssa values
     gt = sv.src.ssavaluetypes
@@ -560,6 +607,7 @@ function type_annotate!(sv::InferenceState)
     # to hold all of the items assigned into it
     record_slot_assign!(sv)
     sv.src.slottypes = sv.slottypes
+    @assert !(sv.bestguess isa LimitedAccuracy)
     sv.src.rettype = sv.bestguess
 
     # annotate variables load types
@@ -655,7 +703,7 @@ function union_caller_cycle!(a::InferenceState, b::InferenceState)
     return
 end
 
-function merge_call_chain!(parent::InferenceState, ancestor::InferenceState, child::InferenceState, limited::Bool)
+function merge_call_chain!(parent::InferenceState, ancestor::InferenceState, child::InferenceState)
     # add backedge of parent <- child
     # then add all backedges of parent <- parent.parent
     # and merge all of the callers into ancestor.callers_in_cycle
@@ -667,17 +715,17 @@ function merge_call_chain!(parent::InferenceState, ancestor::InferenceState, chi
         parent = child.parent
         child === ancestor && break
     end
-    if limited
-        for caller in ancestor.callers_in_cycle
-            caller.limited = true
-        end
-    end
 end
 
 function is_same_frame(interp::AbstractInterpreter, linfo::MethodInstance, frame::InferenceState)
     return linfo === frame.linfo
 end
 
+function poison_callstack(infstate::InferenceState, topmost::InferenceState)
+    push!(infstate.pclimitations, topmost)
+    nothing
+end
+
 # Walk through `linfo`'s upstream call chain, starting at `parent`. If a parent
 # frame matching `linfo` is encountered, then there is a cycle in the call graph
 # (i.e. `linfo` is a descendant callee of itself). Upon encountering this cycle,
@@ -688,28 +736,26 @@ end
 function resolve_call_cycle!(interp::AbstractInterpreter, linfo::MethodInstance, parent::InferenceState)
     frame = parent
     uncached = false
-    limited = false
     while isa(frame, InferenceState)
         uncached |= !frame.cached # ensure we never add an uncached frame to a cycle
-        limited |= frame.limited
         if is_same_frame(interp, linfo, frame)
             if uncached
                 # our attempt to speculate into a constant call lead to an undesired self-cycle
                 # that cannot be converged: poison our call-stack (up to the discovered duplicate frame)
                 # with the limited flag and abort (set return type to Any) now
-                poison_callstack(parent, frame, false)
+                poison_callstack(parent, frame)
                 return true
             end
-            merge_call_chain!(parent, frame, frame, limited)
+            merge_call_chain!(parent, frame, frame)
             return frame
         end
         for caller in frame.callers_in_cycle
             if is_same_frame(interp, linfo, caller)
                 if uncached
-                    poison_callstack(parent, frame, false)
+                    poison_callstack(parent, frame)
                     return true
                 end
-                merge_call_chain!(parent, frame, caller, limited)
+                merge_call_chain!(parent, frame, caller)
                 return caller
             end
         end
@@ -754,7 +800,7 @@ function typeinf_edge(interp::AbstractInterpreter, method::Method, @nospecialize
             unlock_mi_inference(interp, mi)
             return Any, nothing
         end
-        if caller.cached || caller.limited # don't involve uncached functions in cycle resolution
+        if caller.cached || caller.parent !== nothing # don't involve uncached functions in cycle resolution
             frame.parent = caller
         end
         typeinf(interp, frame)
@@ -787,12 +833,12 @@ function typeinf_code(interp::AbstractInterpreter, method::Method, @nospecialize
     if typeinf(interp, frame) && run_optimizer
         opt_params = OptimizationParams(interp)
         opt = OptimizationState(frame, opt_params, interp)
-        optimize(interp, opt, opt_params, result.result)
+        optimize(interp, opt, opt_params, ignorelimited(result.result))
         opt.src.inferred = true
     end
     ccall(:jl_typeinf_end, Cvoid, ())
     frame.inferred || return (nothing, Any)
-    return (frame.src, widenconst(result.result))
+    return (frame.src, widenconst(ignorelimited(result.result)))
 end
 
 # compute (and cache) an inferred AST and return type
@@ -873,7 +919,7 @@ function typeinf_type(interp::AbstractInterpreter, method::Method, @nospecialize
     typeinf(interp, frame, true)
     ccall(:jl_typeinf_end, Cvoid, ())
     frame.result isa InferenceState && return nothing
-    return widenconst(frame.result)
+    return widenconst(ignorelimited(frame.result))
 end
 
 # This is a bridge for the C code calling `jl_typeinf_func()`
diff --git a/base/compiler/typelattice.jl b/base/compiler/typelattice.jl
index 48419ce5e9788..5df8dfd411ba3 100644
--- a/base/compiler/typelattice.jl
+++ b/base/compiler/typelattice.jl
@@ -56,6 +56,7 @@ end
 
 # Wraps a type and represents that the value may also be undef at this point.
 # (only used in optimize, not abstractinterpret)
+# N.B. in the lattice, this is epsilon bigger than `typ` (even Any)
 struct MaybeUndef
     typ
     MaybeUndef(@nospecialize(typ)) = new(typ)
@@ -77,6 +78,16 @@ struct StateUpdate
     state::VarTable
 end
 
+# Represent that the type estimate has been approximated, due to "causes"
+# (only used in abstractinterpret, doesn't appear in optimize)
+# N.B. in the lattice, this is epsilon smaller than `typ` (except Union{})
+struct LimitedAccuracy
+    typ
+    causes::IdSet{InferenceState}
+    LimitedAccuracy(@nospecialize(typ), causes::IdSet{InferenceState}) =
+        new(typ, causes)
+end
+
 struct NotFound end
 
 const NOT_FOUND = NotFound()
@@ -113,6 +124,16 @@ end
 maybe_extract_const_bool(@nospecialize c) = nothing
 
 function ⊑(@nospecialize(a), @nospecialize(b))
+    if isa(b, LimitedAccuracy)
+        if !isa(a, LimitedAccuracy)
+            return false
+        end
+        if b.causes ⊈ a.causes
+            return false
+        end
+        b = b.typ
+    end
+    isa(a, LimitedAccuracy) && (a = a.typ)
     if isa(a, MaybeUndef) && !isa(b, MaybeUndef)
         return false
     end
@@ -220,6 +241,7 @@ widenconst(c::PartialTypeVar) = TypeVar
 widenconst(t::PartialStruct) = t.typ
 widenconst(t::Type) = t
 widenconst(t::TypeVar) = t
+widenconst(t::LimitedAccuracy) = error("unhandled LimitedAccuracy")
 
 issubstate(a::VarState, b::VarState) = (a.typ ⊑ b.typ && a.undef <= b.undef)
 
@@ -245,6 +267,10 @@ function widenconditional(typ::Conditional)
         return Bool
     end
 end
+widenconditional(t::LimitedAccuracy) = error("unhandled LimitedAccuracy")
+
+ignorelimited(@nospecialize typ) = typ
+ignorelimited(typ::LimitedAccuracy) = typ.typ
 
 function stupdate!(state::Nothing, changes::StateUpdate)
     newst = copy(changes.state)
@@ -255,9 +281,13 @@ function stupdate!(state::Nothing, changes::StateUpdate)
         for i = 1:length(newst)
             newtype = newst[i]
             if isa(newtype, VarState)
-                newtypetyp = newtype.typ
+                newtypetyp = ignorelimited(newtype.typ)
                 if isa(newtypetyp, Conditional) && slot_id(newtypetyp.var) == changeid
-                    newst[i] = VarState(widenconditional(newtypetyp), newtype.undef)
+                    newtypetyp = widenconditional(newtypetyp)
+                    if newtype.typ isa LimitedAccuracy
+                        newtypetyp = LimitedAccuracy(newtypetyp, newtype.typ.causes)
+                    end
+                    newst[i] = VarState(newtypetyp, newtype.undef)
                 end
             end
         end
@@ -280,9 +310,13 @@ function stupdate!(state::VarTable, changes::StateUpdate)
         oldtype = state[i]
         # remove any Conditional for this Slot from the vtable
         if isa(newtype, VarState)
-            newtypetyp = newtype.typ
+            newtypetyp = ignorelimited(newtype.typ)
             if isa(newtypetyp, Conditional) && slot_id(newtypetyp.var) == changeid
-                newtype = VarState(widenconditional(newtypetyp), newtype.undef)
+                newtypetyp = widenconditional(newtypetyp)
+                if newtype.typ isa LimitedAccuracy
+                    newtypetyp = LimitedAccuracy(newtypetyp, newtype.typ.causes)
+                end
+                newtype = VarState(newtypetyp, newtype.undef)
             end
         end
         if schanged(newtype, oldtype)
@@ -319,9 +353,13 @@ function stupdate1!(state::VarTable, change::StateUpdate)
     for i = 1:length(state)
         oldtype = state[i]
         if isa(oldtype, VarState)
-            oldtypetyp = oldtype.typ
+            oldtypetyp = ignorelimited(oldtype.typ)
             if isa(oldtypetyp, Conditional) && slot_id(oldtypetyp.var) == changeid
-                state[i] = VarState(widenconditional(oldtypetyp), oldtype.undef)
+                oldtypetyp = widenconditional(oldtypetyp)
+                if oldtype.typ isa LimitedAccuracy
+                    oldtypetyp = LimitedAccuracy(oldtypetyp, oldtype.typ.causes)
+                end
+                state[i] = VarState(oldtypetyp, oldtype.undef)
             end
         end
     end
diff --git a/base/compiler/typelimits.jl b/base/compiler/typelimits.jl
index a64b5fba1f356..9497bfa874e2a 100644
--- a/base/compiler/typelimits.jl
+++ b/base/compiler/typelimits.jl
@@ -278,7 +278,9 @@ union_count_abstract(x::Union) = union_count_abstract(x.a) + union_count_abstrac
 union_count_abstract(@nospecialize(x)) = !isdispatchelem(x)
 
 function issimpleenoughtype(@nospecialize t)
-    return unionlen(t)+union_count_abstract(t) <= MAX_TYPEUNION_LENGTH && unioncomplexity(t) <= MAX_TYPEUNION_COMPLEXITY
+    t = ignorelimited(t)
+    return unionlen(t) + union_count_abstract(t) <= MAX_TYPEUNION_LENGTH &&
+           unioncomplexity(t) <= MAX_TYPEUNION_COMPLEXITY
 end
 
 # pick a wider type that contains both typea and typeb,
@@ -294,6 +296,24 @@ function tmerge(@nospecialize(typea), @nospecialize(typeb))
     suba && subb && return typea
     subb && issimpleenoughtype(typea) && return typea
 
+    # type-lattice for LimitedAccuracy wrapper
+    # the merge create a slightly narrower type than needed, but we can't
+    # represent the precise intersection of causes and don't attempt to
+    # enumerate some of these cases where we could
+    if isa(typea, LimitedAccuracy) && isa(typeb, LimitedAccuracy)
+        if typea.causes ⊆ typeb.causes
+            causes = typeb.causes
+        elseif typeb.causes ⊆ typea.causes
+            causes = typea.causes
+        else
+            causes = union!(copy(typea.causes), typeb.causes)
+        end
+        return LimitedAccuracy(tmerge(typea.typ, typeb.typ), causes)
+    elseif isa(typea, LimitedAccuracy)
+        return LimitedAccuracy(tmerge(typea.typ, typeb), typea.causes)
+    elseif isa(typeb, LimitedAccuracy)
+        return LimitedAccuracy(tmerge(typea, typeb.typ), typeb.causes)
+    end
     # type-lattice for MaybeUndef wrapper
     if isa(typea, MaybeUndef) || isa(typeb, MaybeUndef)
         return MaybeUndef(tmerge(