diff --git a/examples/juliatypes.jl b/examples/juliatypes.jl
deleted file mode 100644
index 5b580f0392eb3..0000000000000
--- a/examples/juliatypes.jl
+++ /dev/null
@@ -1,1037 +0,0 @@
-# This file is a part of Julia. License is MIT: https://julialang.org/license
-
-import Base: convert, show
-
-abstract type Ty end
-
-mutable struct TypeName
-    name::Symbol
-    abs::Bool
-    super::Ty    # actually TagT
-    # arity
-    # representation
-    # mutable
-    TypeName(name, abs, super) = new(name, abs, super)
-    TypeName(name, abs) = new(name, abs)
-end
-
-show(io::IO, x::TypeName) = print(io, x.name)
-
-mutable struct TagT <: Ty
-    name::TypeName
-    params
-    vararg::Bool
-    TagT(n, p, v=false) = new(n, p, v)
-end
-
-function show(io::IO, t::TagT)
-    print(io, t.name.name)
-    isempty(t.params) && return
-    print(io, '{')
-    l = length(t.params)
-    for i=1:l
-        show(io, t.params[i])
-        if i == l && t.vararg
-            print(io, "...")
-        elseif i < l
-            print(io, ",")
-        end
-    end
-    print(io, '}')
-end
-
-mutable struct BottomTy <: Ty
-end
-
-show(io::IO, ::BottomTy) = print(io, "BottomT")
-
-mutable struct UnionT <: Ty
-    a
-    b
-    UnionT() = BottomT
-    UnionT(a) = a
-    UnionT(a, b) = new(a, b)
-    UnionT(a, ts...) = new(a, UnionT(ts...))
-end
-
-function show(io::IO, t::UnionT)
-    print(io, "UnionT(")
-    while true
-        show(io, t.a)
-        print(io, ",")
-        if isa(t.b, UnionT)
-            t = t.b
-        else
-            show(io, t.b)
-            break
-        end
-    end
-    print(io, ')')
-end
-
-mutable struct Var
-    name::Symbol
-    lb
-    ub
-    Var(n, lb=BottomT, ub=AnyT) = new(n, lb, ub)
-end
-
-function show_var_bounds(io::IO, v::Var)
-    if v.lb !== BottomT
-        if v.ub === AnyT
-            print(io, v.name)
-            print(io, ">:")
-            show(io, v.lb)
-            return
-        end
-        show(io, v.lb)
-        print(io, "<:")
-    end
-    print(io, v.name)
-    if v.ub !== AnyT
-        print(io, "<:")
-        show(io, v.ub)
-    end
-end
-
-show(io::IO, v::Var) = print(io, v.name)
-
-mutable struct UnionAllT <: Ty
-    var::Var
-    T
-    UnionAllT(v::Var, t) = new(v, t)
-    UnionAllT(v::Var, t::Union{Type,Tuple}) = new(v, convert(Ty, t))
-end
-
-function show(io::IO, x::UnionAllT)
-    print(io, "(@UnionAll ")
-    show_var_bounds(io, x.var)
-    print(io, " ")
-    show(io, x.T)
-    print(io, ")")
-end
-
-
-# Any, Bottom, and Tuple
-
-const AnyT = TagT(TypeName(:Any,true), ())
-AnyT.name.super = AnyT
-
-const BottomT = BottomTy()
-
-const TupleName = TypeName(:Tuple,false,AnyT)
-const TupleT = TagT(TupleName, (AnyT,), true)
-tupletype(xs...) = inst(TupleName, xs...)
-vatype(xs...) = (t = inst(TupleName, xs...); t.vararg = true; t)
-
-
-# type application
-
-inst(typename::TypeName, params...) = TagT(typename, params)
-
-inst(t::TagT) = t
-
-inst(t::UnionAllT, param) = subst(t.T, Dict{Any,Any}(t.var => param))
-inst(t::UnionAllT, param, rest...) = inst(inst(t,param), rest...)
-
-supertype(t::TagT) = t.name===TupleName ? AnyT : inst(t.name.super, t.params...)
-
-extend(d::Dict, k, v) = (x = copy(d); x[k]=v; x)
-
-subst(t::TagT,    env) = t===AnyT ? t : TagT(t.name, map(x->subst(x,env), t.params), t.vararg)
-subst(t::UnionT,  env) = UnionT(subst(t.a,env), subst(t.b,env))
-subst(t::Var,     env) = get(env, t, t)
-subst(t::UnionAllT, env) = (assert(!haskey(env, t.var));
-                            newVar = Var(t.var.name, subst(t.var.lb, env), subst(t.var.ub, env));
-                            UnionAllT(newVar, subst(t.T, extend(env, t.var, newVar))))
-subst(t, env) = t
-
-
-# subtype
-
-isequal_type(x, y) = issub(x, y) && issub(y, x)
-
-mutable struct Bounds
-    # record current lower and upper bounds of a Var
-    # right: whether this Var is on the right-hand side of A <: B
-    lb
-    ub
-    right::Bool
-end
-
-mutable struct UnionState
-    depth::Int           # number of union decision points we're inside
-    more::Bool           # new union found; need to grow stack
-    stack::Vector{Bool}  # stack of decisions
-    UnionState() = new(1,0,Bool[])
-end
-
-mutable struct Env
-    vars::Dict{Var,Bounds}
-    Lunions::UnionState
-    Runions::UnionState
-    outer::Bool
-    Env() = new(Dict{Var,Bounds}(), UnionState(), UnionState(), true)
-end
-
-function issub_env(x, y)
-    e = Env()
-    ans = forall_exists_issub(x, y, e)
-    ans, e.vars
-end
-issub(x, y) = issub_env(x, y)[1]
-issub(x, y, env) = (x === y)
-issub(x::Ty, y::Ty, env) = (x === y) || x === BottomT
-
-function forall_exists_issub(x, y, env)
-    # for all combinations of elements from Unions on the left, there must
-    # exist a combination of elements from Unions on the right that makes
-    # issub() true. Unions in invariant position are on both the left and
-    # the right in this formula.
-    sub = exists_issub(x, y, env)
-
-    if sub && env.Lunions.more
-        push!(env.Lunions.stack, false)
-        sub = forall_exists_issub(x, y, env)
-        if sub
-            env.Lunions.stack[end] = true
-            sub = forall_exists_issub(x, y, env)
-        end
-        pop!(env.Lunions.stack)
-    end
-    return sub
-end
-
-function exists_issub(x, y, env)
-    env.Lunions.depth = env.Runions.depth = 1
-    env.Lunions.more = env.Runions.more = false
-
-    found = issub(x, y, env)
-
-    if env.Lunions.more
-        # return up to forall_exists_issub. the recursion must have this shape:
-        # ∀₁         ∀₁
-        #   ∃₁  =>     ∀₂
-        #                ...
-        #                ∃₁
-        #                  ∃₂
-        return true
-    end
-    if env.Runions.more
-        push!(env.Runions.stack, false)
-        found = exists_issub(x, y, env)
-        if !found
-            env.Runions.stack[end] = true
-            found = exists_issub(x, y, env)
-        end
-        pop!(env.Runions.stack)
-    end
-    return found
-end
-
-function issub_union(t, u::UnionT, env, R, state::UnionState)
-    env.outer = false
-    if state.depth > length(state.stack)
-        # indicate that stack needs to grow
-        state.more = true
-        return true
-    end
-    ui = state.stack[state.depth]; state.depth += 1
-    choice = getfield(u, 1+ui)
-    return R ? issub(t, choice, env) : issub(choice, t, env)
-end
-
-issub(a::UnionT, b::UnionT, env) = a === b || issub_union(a, b, env, true, env.Runions)
-issub(a::UnionT, b::Ty, env) = b===AnyT || issub_union(b, a, env, false, env.Lunions)
-issub(a::Ty, b::UnionT, env) =
-    a===BottomT || a===b.a || a===b.b || issub_union(a, b, env, true, env.Runions)
-
-# handle vars before unions
-issub(a::UnionT, b::Var, env) = var_gt(b, a, env)
-issub(a::Var, b::UnionT, env) = var_lt(a, b, env)
-
-function issub(a::TagT, b::TagT, env)
-    env.outer = false
-    a === b && return true
-    b === AnyT && return true
-    a === AnyT && return false
-    if a.name !== b.name
-        return issub(supertype(a), b, env)
-    end
-    if a.name === TupleName
-        va, vb = a.vararg, b.vararg
-        la, lb = length(a.params), length(b.params)
-        ai = bi = 1
-        while ai <= la
-            bi > lb && return false
-            !issub(a.params[ai], b.params[bi], env) && return false
-            ai += 1
-            if bi < lb || !vb
-                bi += 1
-            end
-        end
-        return (la==lb && va==vb) || (vb && (la >= (va ? lb : lb-1)))
-    end
-    for i = 1:length(a.params)
-        ai, bi = a.params[i], b.params[i]
-        # use issub in both directions to test equality
-        if !(ai===bi || (issub(ai, bi, env) && issub(bi, ai, env)))
-            return false
-        end
-    end
-    return true
-end
-
-function join(a,b)
-    (a===BottomT || b===AnyT || a === b) && return b
-    (b===BottomT || a===AnyT) && return a
-    UnionT(a,b)
-end
-
-issub(a::Ty, b::Var, env) = var_gt(b, a, env)
-issub(a::Var, b::Ty, env) = var_lt(a, b, env)
-function issub(a::Var, b::Var, env)
-    env.outer = false
-    a === b && return true
-    aa = env.vars[a]; bb = env.vars[b]
-    if aa.right
-        # this is a bit odd, but seems necessary to make this case work:
-        # (@UnionAll x<:T<:x RefT{RefT{T}}) == RefT{@UnionAll x<:T<:x RefT{T}}
-        bb.right && return issub(bb.ub, bb.lb, env)
-        return var_lt(a, b, env)
-    else
-        if !bb.right   # check ∀a,b . a<:b
-            # the bounds of left-side variables never change, and can only lead
-            # to other left-side variables, so using || here is safe.
-            return issub(aa.ub, b, env) || issub(a, bb.lb, env)
-        end
-        return var_gt(b, a, env)
-    end
-end
-
-# issub, but taking apart unions before handling vars
-issub_ufirst(a::UnionT, b::Var, env) = issub_union(b, a, env, false, env.Lunions)
-issub_ufirst(a::Var, b::UnionT, env) = a===b.a || a===b.b || issub_union(a, b, env, true, env.Runions)
-issub_ufirst(a, b, env) = issub(a, b, env)
-
-function var_lt(b::Var, a::Union{Ty,Var}, env)
-    env.outer = false
-    bb = env.vars[b]
-    #println("$b($(bb.lb),$(bb.ub)) <: $a")
-    !bb.right && return issub_ufirst(bb.ub, a, env)  # check ∀b . b<:a
-    !issub_ufirst(bb.lb, a, env) && return false
-    # for contravariance we would need to compute a meet here, but
-    # because of invariance bb.ub ⊓ a == a here always. however for this
-    # to work we need to compute issub(left,right) before issub(right,left),
-    # since otherwise the issub(a, bb.ub) check in var_gt becomes vacuous.
-    bb.ub = a  # meet(bb.ub, a)
-    return true
-end
-
-function var_gt(b::Var, a::Union{Ty,Var}, env)
-    env.outer = false
-    bb = env.vars[b]
-    #println("$b($(bb.lb),$(bb.ub)) >: $a")
-    !bb.right && return issub_ufirst(a, bb.lb, env)  # check ∀b . b>:a
-    !issub_ufirst(a, bb.ub, env) && return false
-    bb.lb = join(bb.lb, a)
-    return true
-end
-
-function rename(t::UnionAllT)
-    v = Var(t.var.name, t.var.lb, t.var.ub)
-    UnionAllT(v, inst(t,v))
-end
-
-function issub_unionall(t::Ty, u::UnionAllT, env, R)
-    outer = env.outer
-    haskey(env.vars, u.var) && (u = rename(u))
-    env.vars[u.var] = Bounds(u.var.lb, u.var.ub, R)
-    ans = R ? issub(t, u.T, env) : issub(u.T, t, env)
-    !outer && delete!(env.vars, u.var)
-    return ans
-end
-
-issub(a::UnionAllT, b::UnionAllT, env) = a === b || issub_unionall(a, b, env, true)
-issub(a::UnionT, b::UnionAllT, env) = issub_unionall(a, b, env, true)
-issub(a::UnionAllT, b::UnionT, env) = issub_unionall(b, a, env, false)
-issub(a::Ty, b::UnionAllT, env) = a === BottomT || issub_unionall(a, b, env, true)
-issub(a::UnionAllT, b::Ty, env) = b === AnyT || issub_unionall(b, a, env, false)
-
-
-# convenient syntax
-
-macro UnionAll(var, expr)
-    lb = :BottomT
-    ub = :AnyT
-    if isa(var,Expr) && var.head === :comparison
-        if length(var.args) == 3
-            v = var.args[1]
-            if var.args[2] == :(<:)
-                ub = esc(var.args[3])
-            elseif var.args[2] == :(>:)
-                lb = esc(var.args[3])
-            else
-                error("invalid bounds in UnionAll")
-            end
-        elseif length(var.args) == 5
-            v = var.args[3]
-            if var.args[2] == var.args[4] == :(<:)
-                lb = esc(var.args[1])
-                ub = esc(var.args[5])
-            else
-                error("invalid bounds in UnionAll")
-            end
-        else
-            error("invalid bounds in UnionAll")
-        end
-    elseif isa(var,Expr) && var.head === :(<:)
-        v = var.args[1]
-        ub = esc(var.args[2])
-    elseif isa(var,Expr) && var.head === :(>:)
-        v = var.args[1]
-        lb = esc(var.args[2])
-    elseif !isa(var,Symbol)
-        error("invalid variable in UnionAll")
-    else
-        v = var
-    end
-    quote
-        let $(esc(v)) = Var($(Expr(:quote,v)), $lb, $ub)
-            UnionAllT($(esc(v)), $(esc(expr)))
-        end
-    end
-end
-
-
-# translating from existing julia types
-
-const tndict = ObjectIdDict()
-
-xlate(t) = xlate(t, ObjectIdDict())
-
-xlate(t, env) = t
-
-function xlate(t::Union, env)
-    if t === Union{}
-        return BottomT
-    end
-    UnionT(map(x->xlate(x,env), t.types)...)
-end
-
-function xlate(t::Tuple, env)
-    if length(t) == 0
-        return inst(TupleName)
-    end
-    va = Base.isvarargtype(t[end])
-    ts = map(x->(Base.isvarargtype(x) ? xlate(x.parameters[1],env) : xlate(x,env)), t)
-    tnew = inst(TupleName, ts...)
-    tnew.vararg = va
-    tnew
-end
-
-function xlate(t::TypeVar, env)
-    if haskey(env, t)
-        return env[t]
-    end
-    v = Var(t.name, xlate(t.lb,env), xlate(t.ub,env))
-    env[t] = v
-    v
-end
-
-function xlate(t::DataType, env)
-    if t === Any
-        return AnyT
-    elseif t <: Tuple
-        return xlate((t.parameters...,), env)
-    elseif !haskey(tndict,t.name)
-        para = map(x->xlate(x,env), t.name.primary.parameters)  # adds tvars to env
-        sup = xlate(t.name.primary.super, env)
-        for i = length(para):-1:1
-            sup = UnionAllT(para[i], sup)
-        end
-        tn = TypeName(t.name.name, t.abstract, sup)
-        tndict[t.name] = tn
-    else
-        tn = tndict[t.name]
-    end
-    inst(tn, map(x->xlate(x,env), t.parameters)...)
-end
-
-convert(::Type{Ty}, t::Union{Type,Tuple}) = xlate(t)
-convert(::Type{Ty}, t::TypeVar) = xlate(t)
-
-issub(a::Union{Type,Tuple}, b::Union{Type,Tuple}) = issub(xlate(a), xlate(b))
-issub(a::Ty  , b::Union{Type,Tuple})              = issub(a       , xlate(b))
-issub(a::Union{Type,Tuple}, b::Ty  )              = issub(xlate(a), b)
-issub_env(a::Union{Type,Tuple}, b::Union{Type,Tuple}) = issub_env(xlate(a), xlate(b))
-issub_env(a::Ty  , b::Union{Type,Tuple})              = issub_env(a       , xlate(b))
-issub_env(a::Union{Type,Tuple}, b::Ty  )              = issub_env(xlate(a), b)
-
-tt(ts...) = Tuple{ts...}
-vt(ts...) = Tuple{ts[1:end-1]..., Vararg{ts[end]}}
-
-# tests
-
-AbstractArrayT =
-    let AbstractArrayName = TypeName(:AbstractArray, true, @UnionAll T @UnionAll N AnyT)
-        @UnionAll T @UnionAll N inst(AbstractArrayName, T, N)
-    end
-
-ArrayT =
-    let ArrayName = TypeName(:Array, false, @UnionAll T @UnionAll N inst(AbstractArrayT, T, N))
-        @UnionAll T @UnionAll N inst(ArrayName, T, N)
-    end
-
-PairT = let PairName = TypeName(:Pair, false, @UnionAll A @UnionAll B AnyT)
-    @UnionAll A @UnionAll B inst(PairName, A, B)
-end
-
-RefT = let RefName = TypeName(:Ref, false, @UnionAll T AnyT)
-    @UnionAll T inst(RefName, T)
-end
-
-tndict[AbstractArray.name] = AbstractArrayT.T.T.name
-tndict[Array.name] = ArrayT.T.T.name
-tndict[Pair.name] = PairT.T.T.name
-
-using Test
-
-issub_strict(x,y) = issub(x,y) && !issub(y,x)
-
-# level 1: no varags, union, UnionAll
-function test_1()
-    @test issub_strict(Int, Integer)
-    @test issub_strict(Array{Int,1}, AbstractArray{Int,1})
-
-    @test isequal_type(Int, Int)
-    @test isequal_type(Integer, Integer)
-    @test isequal_type(Array{Int,1}, Array{Int,1})
-    @test isequal_type(AbstractArray{Int,1}, AbstractArray{Int,1})
-
-    @test issub_strict((Int,Int), (Integer,Integer))
-    @test issub_strict((Array{Int,1},), (AbstractArray{Int,1},))
-
-    @test isequal_type((Integer,Integer), (Integer,Integer))
-
-    @test !issub((Int,Int), (Int,))
-    @test !issub((Int,), (Integer,Integer))
-end
-
-# level 2: varargs
-function test_2()
-    @test issub_strict((Int,Int), vt(Int,))
-    @test issub_strict((Int,Int), vt(Int,Int,))
-    @test issub_strict((Int,Int), vt(Int,Integer,))
-    @test issub_strict((Int,Int), vt(Int,Int,Integer,))
-    @test issub_strict(vt(Int,Int), vt(Int,))
-    @test issub_strict(vt(Int,Int,Int), vt(Int,))
-    @test issub_strict(vt(Int,Int,Int), vt(Integer,Int,))
-    @test issub_strict(vt(Int,), vt(Any,))
-    @test issub_strict((), vt(Any,))
-
-    @test isequal_type(vt(Int,), vt(Int,))
-    @test isequal_type(vt(Integer,), vt(Integer,))
-
-    @test !issub((), vt(Int, Int))
-    @test !issub((Int,), vt(Int, Int, Int))
-
-    @test !issub((Int, (Real, Integer)), vt(Int))
-end
-
-function test_no_diagonal()
-    # from test_3
-    @test issub((@UnionAll T @UnionAll S tupletype(T,S)), (@UnionAll T tupletype(T,T)))
-
-    @test isequal_type((@UnionAll T tupletype(T,T)), (@UnionAll T @UnionAll S tupletype(T,S)))
-
-    @test issub(tupletype(inst(ArrayT,Ty(Integer),1), Ty(Int)),
-                (@UnionAll T<:Ty(Integer) tupletype(inst(ArrayT,T,1),T)))
-
-    @test issub(Ty((Int,AbstractString,Vector{Any})),
-                @UnionAll T tupletype(T, T, inst(ArrayT,T,1)))
-
-    @test isequal_type(Ty(Array{Tuple{Integer,Integer},1}),
-                       inst(ArrayT, (@UnionAll T<:Ty(Integer) tupletype(T,T)), 1))
-
-    @test issub(Ty((Float32,Array{Real,1})),
-                @UnionAll T<:Ty(Real) @UnionAll S<:inst(AbstractArrayT,T,1) tupletype(T,S))
-
-    @test isequal_type((@UnionAll T tupletype(inst(RefT,T), T)),
-                       (@UnionAll T @UnionAll S<:T tupletype(inst(RefT,T),S)))
-    @test isequal_type((@UnionAll T tupletype(inst(RefT,T), T)),
-                       (@UnionAll T @UnionAll S<:T @UnionAll R<:S tupletype(inst(RefT,T),R)))
-
-    @test  issub((@UnionAll S<:Ty(Int) (@UnionAll R<:Ty(AbstractString) tupletype(S,R,Ty(Vector{Any})))),
-                 (@UnionAll T tupletype(T, T, inst(ArrayT,T,1))))
-end
-
-# level 3: UnionAll
-function test_3()
-    @test issub_strict(Ty(Array{Int,1}), @UnionAll T inst(ArrayT, T, 1))
-    @test issub_strict((@UnionAll T inst(PairT,T,T)), (@UnionAll T @UnionAll S inst(PairT,T,S)))
-    @test issub(inst(PairT,Ty(Int),Ty(Int8)), (@UnionAll T @UnionAll S inst(PairT,T,S)))
-    @test issub(inst(PairT,Ty(Int),Ty(Int8)), (@UnionAll S inst(PairT,Ty(Int),S)))
-
-    @test !issub((@UnionAll T<:Ty(Real) T), (@UnionAll T<:Ty(Integer) T))
-
-    # diagonal
-    #@test issub_strict((@UnionAll T tupletype(T,T)), (@UnionAll T @UnionAll S tupletype(T,S)))
-    @test issub((@UnionAll T tupletype(T,T)), (@UnionAll T @UnionAll S tupletype(T,S)))
-    @test isequal_type((@UnionAll T tupletype(T,T)), (@UnionAll R tupletype(R,R)))
-    # diagonal
-    #@test !issub(tupletype(Ty(Real),Ty(Real)), @UnionAll T<:Ty(Real) tupletype(T,T))
-
-    @test !issub((@UnionAll T<:Ty(Integer) @UnionAll S<:Ty(Number) (T,S)),
-                 (@UnionAll T<:Ty(Integer) @UnionAll S<:Ty(Number) (S,T)))
-
-    AUA = inst(ArrayT, (@UnionAll T inst(ArrayT,T,1)), 1)
-    UAA = (@UnionAll T inst(ArrayT, inst(ArrayT,T,1), 1))
-
-    @test !issub(AUA, UAA)
-    @test !issub(UAA, AUA)
-    @test !isequal_type(AUA, UAA)
-
-    @test issub_strict((@UnionAll T Int), (@UnionAll T<:Ty(Integer) Integer))
-
-    @test isequal_type((@UnionAll T @UnionAll S tupletype(T, tupletype(S))),
-                       (@UnionAll T tupletype(T, @UnionAll S tupletype(S))))
-
-    @test !issub((@UnionAll T inst(PairT,T,T)), inst(PairT,Ty(Int),Ty(Int8)))
-    @test !issub((@UnionAll T inst(PairT,T,T)), inst(PairT,Ty(Int),Ty(Int)))
-
-    @test isequal_type((@UnionAll T tupletype(T)), tupletype(AnyT))
-    @test isequal_type((@UnionAll T<:Ty(Real) tupletype(T)), tupletype(Ty(Real)))
-
-    #@test !issub(tupletype(inst(ArrayT,Ty(Integer),1), Ty(Int)),
-    #             (@UnionAll T<:Ty(Integer) tupletype(inst(ArrayT,T,1),T)))
-    @test  issub(tupletype(inst(ArrayT,Ty(Integer),1), Ty(Int)),
-                 (@UnionAll T<:Ty(Integer) @UnionAll S<:T tupletype(inst(ArrayT,T,1),S)))
-
-    @test !issub(tupletype(inst(ArrayT,Ty(Integer),1), Ty(Real)),
-                 (@UnionAll T<:Ty(Integer) tupletype(inst(ArrayT,T,1),T)))
-
-    @test !issub(Ty((Int,AbstractString,Vector{Integer})),
-                 @UnionAll T tupletype(T, T, inst(ArrayT,T,1)))
-    @test !issub(Ty((AbstractString,Int,Vector{Integer})),
-                 @UnionAll T tupletype(T, T, inst(ArrayT,T,1)))
-    @test !issub(Ty((Int,AbstractString,Vector{Tuple{Integer}})),
-                 @UnionAll T tupletype(T,T,inst(ArrayT,tupletype(T),1)))
-
-    #@test !issub(Ty((Int,AbstractString,Vector{Any})),
-    #             @UnionAll T tupletype(T, T, inst(ArrayT,T,1)))
-
-    @test isequal_type(Ty(Array{Int,1}), inst(ArrayT, (@UnionAll T<:Ty(Int) T), 1))
-    @test isequal_type(Ty(Array{Tuple{Any},1}), inst(ArrayT, (@UnionAll T tupletype(T)), 1))
-
-    @test isequal_type(Ty(Array{Tuple{Int,Int},1}),
-                       inst(ArrayT, (@UnionAll T<:Ty(Int) tupletype(T,T)), 1))
-    @test !issub(Ty(Array{Tuple{Int,Integer},1}),
-                 inst(ArrayT, (@UnionAll T<:Ty(Integer) tupletype(T,T)), 1))
-
-
-    @test !issub(inst(PairT,Ty(Int),Ty(Int8)), (@UnionAll T inst(PairT,T,T)))
-
-    @test !issub(tupletype(inst(ArrayT,Ty(Int),1), Ty(Integer)),
-                 (@UnionAll T<:Ty(Integer) tupletype(inst(ArrayT,T,1),T)))
-
-    @test !issub(tupletype(Ty(Integer), inst(ArrayT,Ty(Int),1)),
-                 (@UnionAll T<:Ty(Integer) tupletype(T, inst(ArrayT,T,1))))
-
-    @test !issub(Ty(Array{Array{Int,1},Integer}),
-                 (@UnionAll T inst(ArrayT,inst(ArrayT,T,1),T)))
-
-    @test issub(Ty(Array{Array{Int,1},Int}),
-                (@UnionAll T inst(ArrayT,inst(ArrayT,T,1),T)))
-
-    @test  issub(Ty((Integer,Int)), @UnionAll T<:Ty(Integer) @UnionAll S<:T tupletype(T,S))
-    @test !issub(Ty((Integer,Int)), @UnionAll T<:Ty(Int) @UnionAll S<:T tupletype(T,S))
-    @test !issub(Ty((Integer,Int)), @UnionAll T<:Ty(AbstractString) @UnionAll S<:T tupletype(T,S))
-
-    @test issub(Ty((Float32,Array{Float32,1})),
-                @UnionAll T<:Ty(Real) @UnionAll S<:inst(AbstractArrayT,T,1) tupletype(T,S))
-
-    @test !issub(Ty((Float32,Array{Float64,1})),
-                 @UnionAll T<:Ty(Real) @UnionAll S<:inst(AbstractArrayT,T,1) tupletype(T,S))
-
-    #@test !issub(Ty((Float32,Array{Real,1})),
-    #             @UnionAll T<:Ty(Real) @UnionAll S<:inst(AbstractArrayT,T,1) tupletype(T,S))
-
-    @test !issub(Ty((Number,Array{Real,1})),
-                 @UnionAll T<:Ty(Real) @UnionAll S<:inst(AbstractArrayT,T,1) tupletype(T,S))
-
-    @test issub((@UnionAll Ty(Int)<:T<:Ty(Integer) T), @UnionAll T<:Ty(Real) T)
-    @test issub((@UnionAll Ty(Int)<:T<:Ty(Integer) inst(ArrayT,T,1)),
-                (@UnionAll T<:Ty(Real) inst(ArrayT,T,1)))
-
-    @test issub((@UnionAll Ty(Int)<:T<:Ty(Integer) T),
-                (@UnionAll Ty(Integer)<:T<:Ty(Real) T))
-    @test !issub((@UnionAll Ty(Int)<:T<:Ty(Integer) inst(ArrayT,T,1)),
-                 (@UnionAll Ty(Integer)<:T<:Ty(Real) inst(ArrayT,T,1)))
-
-    X = (@UnionAll T<:Ty(Real) @UnionAll S<:inst(AbstractArrayT,T,1) tupletype(T,S))
-    Y = (@UnionAll A<:Ty(Real) @UnionAll B<:inst(AbstractArrayT,A,1) tupletype(A,B))
-    @test isequal_type(X,Y)
-    Z = (@UnionAll A<:Ty(Real) @UnionAll B<:inst(AbstractArrayT,A,1) tupletype(Ty(Real),B))
-    @test issub_strict(X,Z)
-
-    @test issub_strict((@UnionAll T @UnionAll S<:T inst(PairT,T,S)),
-                       (@UnionAll T @UnionAll S    inst(PairT,T,S)))
-    @test issub_strict((@UnionAll T @UnionAll S>:T inst(PairT,T,S)),
-                       (@UnionAll T @UnionAll S    inst(PairT,T,S)))
-
-    #@test issub_strict((@UnionAll T tupletype(inst(RefT,T), T)),
-    #                   (@UnionAll T @UnionAll S<:T tupletype(inst(RefT,T),S)))
-    #@test issub_strict((@UnionAll T tupletype(inst(RefT,T), T)),
-    #                   (@UnionAll T @UnionAll S<:T @UnionAll R<:S tupletype(inst(RefT,T),R)))
-    @test isequal_type((@UnionAll T tupletype(inst(RefT,T), T)),
-                       (@UnionAll T @UnionAll T<:S<:T tupletype(inst(RefT,T),S)))
-    @test issub_strict((@UnionAll T tupletype(inst(RefT,T), T)),
-                       (@UnionAll T @UnionAll S>:T tupletype(inst(RefT,T),S)))
-end
-
-# level 4: Union
-function test_4()
-    @test isequal_type(UnionT(BottomT,BottomT), BottomT)
-
-    @test issub_strict(Int, Union{Int,AbstractString})
-    @test issub_strict(Union{Int,Int8}, Integer)
-
-    @test isequal_type(Union{Int,Int8}, Union{Int,Int8})
-
-    @test isequal_type(UnionT(Ty(Int),Ty(Integer)), Ty(Integer))
-
-    @test isequal_type(tt(Union{Int,Int8},Int16), Union{tt(Int,Int16),tt(Int8,Int16)})
-
-    @test issub_strict((Int,Int8,Int), vt(Union{Int,Int8},))
-    @test issub_strict((Int,Int8,Int), vt(Union{Int,Int8,Int16},))
-
-    # nested unions
-    @test !issub(UnionT(Ty(Int),inst(RefT,UnionT(Ty(Int),Ty(Int8)))),
-                 UnionT(Ty(Int),inst(RefT,UnionT(Ty(Int8),Ty(Int16)))))
-
-    A = Ty(Int);   B = Ty(Int8)
-    C = Ty(Int16); D = Ty(Int32)
-    @test  issub(UnionT(UnionT(A,UnionT(A,UnionT(B,C))), UnionT(D,BottomT)),
-                 UnionT(UnionT(A,B),UnionT(C,UnionT(B,D))))
-    @test !issub(UnionT(UnionT(A,UnionT(A,UnionT(B,C))), UnionT(D,BottomT)),
-                 UnionT(UnionT(A,B),UnionT(C,UnionT(B,A))))
-
-    @test isequal_type(UnionT(UnionT(A,B,C), UnionT(D)),  UnionT(A,B,C,D))
-    @test isequal_type(UnionT(UnionT(A,B,C), UnionT(D)),  UnionT(A,UnionT(B,C),D))
-    @test isequal_type(UnionT(UnionT(UnionT(UnionT(A)),B,C), UnionT(D)),
-                       UnionT(A,UnionT(B,C),D))
-
-    @test issub_strict(UnionT(UnionT(A,C), UnionT(D)),  UnionT(A,B,C,D))
-
-    @test !issub(UnionT(UnionT(A,B,C), UnionT(D)),  UnionT(A,C,D))
-
-    # obviously these unions can be simplified, but when they aren't there's trouble
-    X = UnionT(UnionT(A,B,C),UnionT(A,B,C),UnionT(A,B,C),UnionT(A,B,C),
-               UnionT(A,B,C),UnionT(A,B,C),UnionT(A,B,C),UnionT(A,B,C))
-    Y = UnionT(UnionT(D,B,C),UnionT(D,B,C),UnionT(D,B,C),UnionT(D,B,C),
-               UnionT(D,B,C),UnionT(D,B,C),UnionT(D,B,C),UnionT(A,B,C))
-    @test issub_strict(X,Y)
-end
-
-# level 5: union and UnionAll
-function test_5()
-    u = Ty(Union{Int8,Int})
-
-    @test issub(Ty((AbstractString,Array{Int,1})),
-                (@UnionAll T UnionT(tupletype(T,inst(ArrayT,T,1)),
-                                    tupletype(T,inst(ArrayT,Ty(Int),1)))))
-
-    @test issub(Ty((Union{Vector{Int},Vector{Int8}},)),
-                @UnionAll T tupletype(inst(ArrayT,T,1),))
-
-    @test !issub(Ty((Union{Vector{Int},Vector{Int8}},Vector{Int})),
-                 @UnionAll T tupletype(inst(ArrayT,T,1), inst(ArrayT,T,1)))
-
-    @test !issub(Ty((Union{Vector{Int},Vector{Int8}},Vector{Int8})),
-                 @UnionAll T tupletype(inst(ArrayT,T,1), inst(ArrayT,T,1)))
-
-    @test !issub(Ty(Vector{Int}), @UnionAll T>:u inst(ArrayT,T,1))
-    @test  issub(Ty(Vector{Integer}), @UnionAll T>:u inst(ArrayT,T,1))
-    @test  issub(Ty(Vector{Union{Int,Int8}}), @UnionAll T>:u inst(ArrayT,T,1))
-
-    @test issub((@UnionAll Ty(Int)<:T<:u inst(ArrayT,T,1)),
-                (@UnionAll Ty(Int)<:T<:u inst(ArrayT,T,1)))
-
-    # with varargs
-    @test !issub(inst(ArrayT,tupletype(inst(ArrayT,Ty(Int)),inst(ArrayT,Ty(Vector{Int16})),inst(ArrayT,Ty(Vector{Int})),inst(ArrayT,Ty(Int)))),
-                 @UnionAll T<:(@UnionAll S vatype(UnionT(inst(ArrayT,S),inst(ArrayT,inst(ArrayT,S,1))))) inst(ArrayT,T))
-
-    @test issub(inst(ArrayT,tupletype(inst(ArrayT,Ty(Int)),inst(ArrayT,Ty(Vector{Int})),inst(ArrayT,Ty(Vector{Int})),inst(ArrayT,Ty(Int)))),
-                @UnionAll T<:(@UnionAll S vatype(UnionT(inst(ArrayT,S),inst(ArrayT,inst(ArrayT,S,1))))) inst(ArrayT,T))
-
-    @test !issub(tupletype(inst(ArrayT,Ty(Int)),inst(ArrayT,Ty(Vector{Int16})),inst(ArrayT,Ty(Vector{Int})),inst(ArrayT,Ty(Int))),
-                 @UnionAll S vatype(UnionT(inst(ArrayT,S),inst(ArrayT,inst(ArrayT,S,1)))))
-
-    @test issub(tupletype(inst(ArrayT,Ty(Int)),inst(ArrayT,Ty(Vector{Int})),inst(ArrayT,Ty(Vector{Int})),inst(ArrayT,Ty(Int))),
-                @UnionAll S vatype(UnionT(inst(ArrayT,S),inst(ArrayT,inst(ArrayT,S,1)))))
-
-    B = @UnionAll S<:u tupletype(S, tupletype(AnyT,AnyT,AnyT), inst(RefT,S))
-    # these tests require renaming in issub_unionall
-    @test  issub((@UnionAll T<:B tupletype(Ty(Int8), T, inst(RefT,Ty(Int8)))), B)
-    @test !issub((@UnionAll T<:B tupletype(Ty(Int8), T, inst(RefT,T))),        B)
-
-    # the `convert(Type{T},T)` pattern, where T is a Union
-    # required changing priority of unions and vars
-    @test issub(tupletype(inst(ArrayT,u,1),Ty(Int)),
-                @UnionAll T tupletype(inst(ArrayT,T,1), T))
-    @test issub(tupletype(inst(ArrayT,u,1),Ty(Int)),
-                @UnionAll T @UnionAll S<:T tupletype(inst(ArrayT,T,1), S))
-end
-
-# tricky type variable lower bounds
-function test_6()
-    # diagonal
-    #@test !issub((@UnionAll S<:Ty(Int) (@UnionAll R<:Ty(AbstractString) tupletype(S,R,Ty(Vector{Any})))),
-    #             (@UnionAll T tupletype(T, T, inst(ArrayT,T,1))))
-    @test issub((@UnionAll S<:Ty(Int) (@UnionAll R<:Ty(AbstractString) tupletype(S,R,Ty(Vector{Any})))),
-                (@UnionAll T tupletype(T, T, inst(ArrayT,T,1))))
-
-    @test !issub((@UnionAll S<:Ty(Int) (@UnionAll R<:Ty(AbstractString) tupletype(S,R,Ty(Vector{Integer})))),
-                 (@UnionAll T tupletype(T, T, inst(ArrayT,T,1))))
-
-    t = @UnionAll T tupletype(T,T,inst(RefT,T))
-    @test isequal_type(t, rename(t))
-
-    @test !issub((@UnionAll T tupletype(T,Ty(AbstractString),inst(RefT,T))),
-                 (@UnionAll T tupletype(T,T,inst(RefT,T))))
-
-    @test !issub((@UnionAll T tupletype(T,inst(RefT,T),Ty(AbstractString))),
-                 (@UnionAll T tupletype(T,inst(RefT,T),T)))
-
-    i = Ty(Int); ai = Ty(Integer)
-    @test isequal_type((@UnionAll i<:T<:i   inst(RefT,T)), inst(RefT,i))
-    @test isequal_type((@UnionAll ai<:T<:ai inst(RefT,T)), inst(RefT,ai))
-
-    # Pair{T,S} <: Pair{T,T} can be true with certain bounds
-    @test issub_strict((@UnionAll i<:T<:i @UnionAll i<:S<:i inst(PairT,T,S)),
-                       @UnionAll T inst(PairT,T,T))
-
-    @test issub_strict(tupletype(i, inst(RefT,i)),
-                       (@UnionAll T @UnionAll S<:T tupletype(S,inst(RefT,T))))
-
-    @test !issub(tupletype(Ty(Real), inst(RefT,i)),
-                 (@UnionAll T @UnionAll S<:T tupletype(S,inst(RefT,T))))
-
-    # S >: T
-    @test issub_strict(tupletype(Ty(Real), inst(RefT,i)),
-                       (@UnionAll T @UnionAll S>:T tupletype(S,inst(RefT,T))))
-
-    @test !issub(tupletype(inst(RefT,i), inst(RefT,ai)),
-                 (@UnionAll T @UnionAll S>:T tupletype(inst(RefT,S),inst(RefT,T))))
-
-    @test issub_strict(tupletype(inst(RefT,Ty(Real)), inst(RefT,ai)),
-                       (@UnionAll T @UnionAll S>:T tupletype(inst(RefT,S),inst(RefT,T))))
-
-
-    @test issub_strict(tupletype(Ty(Real), inst(RefT,tupletype(i))),
-                       (@UnionAll T @UnionAll S>:T tupletype(S,inst(RefT,tupletype(T)))))
-
-    @test !issub(tupletype(inst(RefT,tupletype(i)), inst(RefT,tupletype(ai))),
-                 (@UnionAll T @UnionAll S>:T tupletype(inst(RefT,tupletype(S)),inst(RefT,tupletype(T)))))
-
-    @test issub_strict(tupletype(inst(RefT,tupletype(Ty(Real))), inst(RefT,tupletype(ai))),
-                       (@UnionAll T @UnionAll S>:T tupletype(inst(RefT,tupletype(S)),inst(RefT,tupletype(T)))))
-
-    # (@UnionAll x<:T<:x Q{T}) == Q{x}
-    @test isequal_type(inst(RefT,inst(RefT,i)),
-                       inst(RefT,@UnionAll i<:T<:i inst(RefT,T)))
-    @test isequal_type((@UnionAll i<:T<:i inst(RefT,inst(RefT,T))),
-                       inst(RefT,@UnionAll i<:T<:i inst(RefT,T)))
-    @test !issub((@UnionAll i<:T<:i inst(RefT,inst(RefT,T))),
-                 inst(RefT,@UnionAll T<:i inst(RefT,T)))
-
-    u = Ty(Union{Int8,Int64})
-    A = inst(RefT,BottomT)
-    B = @UnionAll S<:u inst(RefT,S)
-    @test issub(inst(RefT,B), @UnionAll A<:T<:B inst(RefT,T))
-
-    C = @UnionAll S<:u S
-    @test issub(inst(RefT,C), @UnionAll u<:T<:u inst(RefT,T))
-
-    BB = @UnionAll S<:BottomT S
-    @test issub(inst(RefT,B), @UnionAll BB<:U<:B inst(RefT,U))
-end
-
-# tests that don't pass yet
-function test_failing()
-    # TODO: S <: Array{T} cases
-end
-
-function test_all()
-    test_1()
-    test_2()
-    test_no_diagonal()
-    test_3()
-    test_4()
-    test_5()
-    test_6()
-    test_failing()
-end
-
-const menagerie =
-    Any[BottomT, AnyT, Ty(Int), Ty(Int8), Ty(Integer), Ty(Real),
-        Ty(Array{Int,1}), Ty(AbstractArray{Int,1}),
-        Ty(vt(Int,Integer,)), Ty(vt(Integer,Int,)), Ty(()),
-        Ty(Union{Int,Int8}),
-        (@UnionAll T inst(ArrayT, T, 1)),
-        (@UnionAll T inst(PairT,T,T)),
-        (@UnionAll T @UnionAll S inst(PairT,T,S)),
-        inst(PairT,Ty(Int),Ty(Int8)),
-        (@UnionAll S inst(PairT,Ty(Int),S)),
-        (@UnionAll T tupletype(T,T)),
-        (@UnionAll T<:Ty(Integer) tupletype(T,T)),
-        (@UnionAll T @UnionAll S tupletype(T,S)),
-        (@UnionAll T<:Ty(Integer) @UnionAll S<:Ty(Number) (T,S)),
-        (@UnionAll T<:Ty(Integer) @UnionAll S<:Ty(Number) (S,T)),
-        inst(ArrayT, (@UnionAll T inst(ArrayT,T,1)), 1),
-        (@UnionAll T inst(ArrayT, inst(ArrayT,T,1), 1)),
-        inst(ArrayT, (@UnionAll T<:Ty(Int) T), 1),
-        (@UnionAll T<:Ty(Real) @UnionAll S<:inst(AbstractArrayT,T,1) tupletype(T,S)),
-        UnionT(Ty(Int),inst(RefT,UnionT(Ty(Int),Ty(Int8)))),
-        (@UnionAll T UnionT(tupletype(T,inst(ArrayT,T,1)),
-                            tupletype(T,inst(ArrayT,Ty(Int),1)))),
-        ]
-
-let new = Any[]
-    # add variants of each type
-    for T in menagerie
-        push!(new, inst(RefT, T))
-        push!(new, tupletype(T))
-        push!(new, tupletype(T,T))
-        push!(new, vatype(T))
-        push!(new, @UnionAll S<:T S)
-        push!(new, @UnionAll S<:T inst(RefT,S))
-    end
-    append!(menagerie, new)
-end
-
-function test_properties()
-    x→y = !x || y
-    ¬T = @UnionAll X>:T inst(RefT,X)
-
-    for T in menagerie
-        # top and bottom identities
-        @test issub(BottomT, T)
-        @test issub(T, AnyT)
-        @test issub(T, BottomT) → isequal_type(T, BottomT)
-        @test issub(AnyT, T) → isequal_type(T, AnyT)
-
-        # unionall identity
-        @test isequal_type(T, @UnionAll S<:T S)
-        @test isequal_type(inst(RefT,T), @UnionAll T<:U<:T inst(RefT,U))
-
-        # equality under renaming
-        if isa(T, UnionAllT)
-            @test isequal_type(T, rename(T))
-        end
-
-        # inequality under wrapping
-        @test !isequal_type(T, inst(RefT,T))
-
-        for S in menagerie
-            issubTS = issub(T, S)
-            # transitivity
-            if issubTS
-                for R in menagerie
-                    if issub(S, R)
-                        if !issub(T, R)
-                            @show T
-                            @show S
-                            @show R
-                        end
-                        @test issub(T, R)  # issub(S, R) → issub(T, R)
-                        @test issub(inst(RefT,S), @UnionAll T<:U<:R inst(RefT,U))
-                    end
-                end
-            end
-
-            # union subsumption
-            @test isequal_type(T, UnionT(T,S)) → issub(S, T)
-
-            # invariance
-            @test isequal_type(T, S) == isequal_type(inst(RefT,T), inst(RefT,S))
-
-            # covariance
-            @test issubTS == issub(tupletype(T), tupletype(S))
-            @test issubTS == issub(vatype(T), vatype(S))
-            @test issubTS == issub(tupletype(T), vatype(S))
-
-            # contravariance
-            @test issubTS == issub(¬S, ¬T)
-        end
-    end
-end
-
-# function non_terminating_F()
-#     # undecidable F_<: instance
-#     ¬T = @ForAll α<:T α
-#     θ = @ForAll α ¬(@ForAll β<:α ¬β)
-#     a₀ = Var(:a₀, BottomT, θ)
-#     issub(a₀, (@ForAll a₁<:a₀ ¬a₁))
-# end
-
-# attempt to implement non-terminating example from
-# "On the Decidability of Subtyping with Bounded Existential Types"
-function non_terminating_2()
-    C = let CName = TypeName(:C, false, @UnionAll T AnyT)
-        @UnionAll T inst(CName, T)
-    end
-    D = let DName = TypeName(:D, false, @UnionAll T AnyT)
-        @UnionAll T inst(DName, T)
-    end
-    ¬T = @UnionAll X>:T inst(D,X)
-    U = AnyT
-    X = Var(:X, BottomT, ¬U)
-    e = Env()
-    e.vars[X] = Bounds(BottomT, ¬U, false)
-    issub(X, ¬inst(C,X), e)
-end
-
-#=
-Replacing type S with a union over var T(ᶜ)<:S can affect the subtype
-relation in all possible ways:
-
-    (C{Real},C{Real}) < @U T<:Real (C{T},C{T})
-    (Real,Real)       = @U T<:Real (T,T)
-
-    (C{Real},C{Real}) ! @U Tᶜ<:Real (C{T},C{T})  (*)  # neither <= nor >=
-    (Real,Real)       > @U Tᶜ<:Real (T,T)
-
-    (C{Real},) < @U T<:Real (C{T},)
-    (Real,)    = @U T<:Real (T,)
-    (C{Real},) ! @U Tᶜ<:Real (C{T},)  (*)
-    (Real,)    = @U Tᶜ<:Real (T,)
-
-cases (*) are probably not needed in practice.
-
-
-transform all covariant occurrences of non-concrete types to
-vars: (Real,Real) => @U T<:Real @U S<:Real (T,S)
-and then treat all vars as invariant.
-this can maybe even be done on the fly without actually making the
-UnionAll types up-front.
-in fact this may only need to be done on the left.
-which implies right away that the algorithm works as-is if the left
-side is a concrete type.
-
-possible explanation:
-
-1. match all tvars with invariant rule
-2. imagine left side is concrete
-3. therefore all (right-) vars will have to equal concrete types
-   (this completes the base case)
-4. inductive hypothesis: tvars match concrete types
-5. "build up" an abstract type on the left over the initial concrete type
-6. handle all abstract types T in covariant position on the left by treating
-   them as variables V<:T instead
-7. by the inductive hypothesis tvars continue to match concrete types
-
-it seems you need to plug in the isconcrete predicate in step 6.
-
-=#