Explanation and examples for "Subtyping currently intentionally answers certain queries incorrectly for kind types"?

nsajko · February 5, 2024, 4:44am

I noticed this in the Julia source:

JuliaLang/julia/blob/6defd59986503acc3891938be47563fd385fe2c6/base/compiler/typeutils.jl#L51-L55


      
          # Subtyping currently intentionally answers certain queries incorrectly for kind types. For
          # some of these queries, this check can be used to somewhat protect against making incorrect
          # decisions based on incorrect subtyping. Note that this check, itself, is broken for
          # certain combinations of `a` and `b` where one/both isa/are `Union`/`UnionAll` type(s)s.
          isnotbrokensubtype(@nospecialize(a), @nospecialize(b)) = (!iskindtype(b) || !isType(a) || hasuniquerep(a.parameters[1]) || b <: a)

It was added in this PR:

github.com/JuliaLang/julia

Avoid broken kind type handling when compiling `isa`

JuliaLang:master ← JuliaLang:jr/avoidbrokenkindtypes

opened 08:43PM - 22 Jun 18 UTC

jrevels

+68 -31

This fixes https://github.com/JuliaLang/julia/issues/27078, https://github.com/j…revels/Cassette.jl/issues/42, and some other bugs with tuples. I'm not at all a fan of my replacements for the tuple handling code here - I just need to get the aforementioned bugs fixed. It should be "more correct" than it was before (modulo any bugs I introduced...), but it feels like it's going to be slower w.r.t. to compilation, runtime, or both. I haven't done benchmarking yet, though. I would be **extremely grateful** for some tips on faster/cleaner alternatives (as long as they don't reintroduce the bugs I'm trying to fix). This might be another case in favor of making `ntuple` an intrinsic...EDIT: see comment below, moved the tuple changes out of this PR @nanosoldier `runbenchmarks(ALL, vs = ":master")`

AFAIU isnotbrokensubtype(a, b) basically means “a <: b is probably valid”? But when is it not valid? I think some examples would help my understanding and enable being more sure about writing correct code.

On a more basic level, what are kind types in Julia? I assume it refers to DataType, Type, Union and UnionAll? Is it just that? Wikipedia seems to have a page for this, but I’m not sure how relevant it is for Julia: Kind (type theory) - Wikipedia

I’m also curious about the “intentionally” part, what’s the rationale for intentionally breaking subtyping?

As a more specific question, can anyone give example inputs for which typesplit is broken:

github.com

JuliaLang/julia/blob/6defd59986503acc3891938be47563fd385fe2c6/base/promotion.jl#L137-L152


      
          # return an upper-bound on type `a` with type `b` removed
          # such that `return <: a` && `Union{return, b} == Union{a, b}`
          # WARNING: this is wrong for some objects for which subtyping is broken
          #          (Core.Compiler.isnotbrokensubtype), use only simple types for `b`
          function typesplit(@nospecialize(a), @nospecialize(b))
              @_foldable_meta
              @_nospecializeinfer_meta
              if a <: b
                  return Bottom
              end
              if isa(a, Union)
                  return Union{typesplit(a.a, b),
                               typesplit(a.b, b)}
              end
              return a
          end