How about allowing an abstract type to be *frozen* (or, perhaps, *closed*) at some point? After the abstract type is frozen, any attempt at adding a new subtype to it would throw. Example:

```
abstract type A end
struct S <: A end
freeze_abstract_type(A)
struct T <: A end # throws!
```

The motivation is that subtyping could then use the fact that the set of subtypes is closed. For example, the subtyping query here should be able to return `true`

if we were to freeze `A`

before doing `A <: Union{S,T}`

:

```
julia> abstract type A end
julia> struct S <: A end
julia> struct T <: A end
julia> A <: Union{S,T}
false
```

FTR this proposal is basically an alternative to the following feature request:

## Motivating example 1: Peano natural numbers in the type domain

Suppose weâ€™re implementing natural numbers in the type domain recursively, like in Peanoâ€™s construction. Ref Haskell Wiki, Wikipedia.

### First try

An initial attempt might look like so:

```
"""
Nat(predecessor)
The `predecessor` must be either:
* `nothing`, we have `iszero(Nat(nothing))`
* a `Nat`
"""
struct Nat{Predecessor} <: Integer
predecessor::Predecessor
end
```

The obvious problem with the above is the absence of type safety, also resulting in bad abstract type inference. E.g., `Nat{Float32}`

or `Nat{:some_symbol}`

donâ€™t throw.

### Second try

We could make the design stricter by adding some abstract types:

```
recursive_step(t) = Union{Nothing,t}
abstract type UpperBound0{P <: recursive_step(Integer)} <: Integer end
abstract type UpperBound1{P <: recursive_step(UpperBound0)} <: UpperBound0{P} end
"""
Nat(predecessor)
The `predecessor` must be either:
* `nothing`, we have `iszero(Nat(nothing))`
* a `Nat`
"""
struct Nat{
Predecessor <: recursive_step(UpperBound1),
} <: UpperBound1{Predecessor}
predecessor::Predecessor
end
```

Now we have a design thatâ€™s type safe as long as no new subtypes are added to the abstract types:

```
julia> Nat{Float32}
ERROR: TypeError: in Nat, in Predecessor, expected Predecessor<:Union{Nothing, UpperBound1}, got Type{Float32}
Stacktrace:
[1] top-level scope
@ REPL[5]:1
```

However, the type inference is still not perfect, not without adding some type assertions:

```
julia> Base.infer_return_type((n -> n.predecessor), Tuple{Nat})
Union{Nothing, UpperBound1}
julia> Base.infer_return_type((n -> n.predecessor.predecessor), Tuple{Nat})
Any
```

Ideally, both results would be `Union{Nothing,Nat}`

, but this isnâ€™t possible because Juliaâ€™s subtyping assumes further subtypes may be added to the abstract types. Thus my feature request.

## Motivating example 2: recursive data structure

Suppose weâ€™re implementing a recursive homogeneous nonempty ordered collection of compile-time constant length. Basically a recursive equivalent to `Tuple{X, Vararg{X}} where {X}`

. Homogeneous trees, etc., might instead be constructed using a similar approach.

### First try

A design lacking type safety:

```
"""
List(elem, tail)
Construct a single-element list like so: `List(elem, nothing)`.
Prepend an element to an existing list like so: `List(elem, existing_list)`.
"""
struct List{Element, Tail}
first_element::Element
tail::Tail
end
```

The type system doesnâ€™t help enforce the homogeneity of `List`

:

```
julia> L1 = List{Int, Nothing}
List{Int64, Nothing}
julia> List{Float32, L1} # want this to throw
List{Float32, List{Int64, Nothing}}
```

### Second try

```
recursive_step(t) = Union{Nothing,t}
abstract type UpperBound0{E, T <: recursive_step(AbstractVector{E})} <: AbstractVector{E} end
abstract type UpperBound1{E, T <: recursive_step(UpperBound0{E})} <: UpperBound0{E,T} end
struct List{
Element,
Tail <: recursive_step(UpperBound1{Element}),
} <: UpperBound1{Element, Tail}
first_element::Element
tail::Tail
end
```

Again, we achieved type safety, as long as the abstract types donâ€™t get any new subtypes:

```
julia> L1 = List{Int, Nothing}
List{Int64, Nothing}
julia> List{Int, L1}
List{Int64, List{Int64, Nothing}}
julia> List{Float32, L1}
ERROR: TypeError: in List, in Tail, expected Tail<:Union{Nothing, UpperBound1{Float32, T} where T<:Union{Nothing, UpperBound0{Float32, T} where T<:Union{Nothing, AbstractVector{Float32}}}}, got Type{List{Int64, Nothing}}
Stacktrace:
[1] top-level scope
@ REPL[7]:1
julia> List{Int, Int}
ERROR: TypeError: in List, in Tail, expected Tail<:Union{Nothing, UpperBound1{Int64, T} where T<:Union{Nothing, UpperBound0{Int64, T} where T<:Union{Nothing, AbstractVector{Int64}}}}, got Type{Int64}
Stacktrace:
[1] top-level scope
@ REPL[8]:1
```

Again, the type inference fails:

```
julia> Base.infer_return_type((n -> n.tail), Tuple{List{Bool}})
Union{Nothing, UpperBound1{Bool, T} where T<:Union{Nothing, UpperBound0{Bool, T} where T<:Union{Nothing, AbstractVector{Bool}}}}
julia> Base.infer_return_type((n -> n.tail.tail), Tuple{List{Bool}})
Any
```