"Efficient Subtyping" (if you ignore all the inefficiencies).

Subtyping.swift

indirect enum Type : CustomStringConvertible {
  case TyVar(String)
  case Top
  case Bottom
  case Arrow(Type, Type)
  case Pair(Type, Type)
  case Rec(String, Type)

  func subst(_ s : String, _ t : Type) -> Type {
    switch self {
    case .Top:
      return .Top
    case .Bottom:
      return .Bottom
    case let .TyVar(n) where s == n:
      return t
    case .TyVar(_):
      return self
    case let .Rec(x, b) where s == x:
      return .Rec(x, b.subst(s, t))
    case .Rec(_, _):
      return self
    case let .Arrow(i, o):
      return .Arrow(i.subst(s, t), o.subst(s, t))
    case let .Pair(l, r):
      return .Pair(l.subst(s, t), r.subst(s, t))
    }
  }

  var description: String {
    switch self {
    case .Top:
      return "⊤"
    case .Bottom:
      return "⊥"
    case let .TyVar(n):
      return "$\(n)"
    case let .Arrow(arg, res):
      return "\(arg) → \(res)"
    case let .Pair(f, s):
      return "(\(f), \(s))"
    case let .Rec(x, t):
      return "μ\(x).\(t)"
    }
  }

  static func == (l : Type, r : Type) -> Bool {
    switch (l, r) {
    case (.Top, .Top), (.Bottom, .Bottom):
      return true
    case let (.TyVar(n1), .TyVar(n2)):
      return n1 == n2
    case let (.Pair(f1, s1), .Pair(f2, s2)):
      return f1 == f2 && s1 == s2
    case let (.Arrow(t1, r1), .Arrow(t2, r2)):
      return t1 == t2 && r1 == r2
    case let (.Rec(x1, t1), .Rec(x2, t2)):
      return x1 == x2 && t1 == t2
    default:
      return false
    }
  }
}

func <= (_ s : Type, _ t : Type) -> Bool {
  enum Bail : Error {
    case Out
  }

  // Kozen and Palsburg's O(n^2) subtyping algorithm - assuming you ignore the complexity of
  // deciding type equality, which is exponential, and lookup into the context, which is linear.
  // That can probably be remedied with a clever enough hashing scheme so the environment 
  // can be queried in constant time.
  func subtype(_ a : [(Type, Type)], _ s : Type, _ t : Type) throws -> [(Type, Type)] {
    if let _ = a.first(where: { (s2, t2) in s == s2 && t == t2 }) {
      return a
    }

    var newEnv = a
    newEnv.append(s, t)
    switch (s, t) {
    case (_, .Top):
      return newEnv
    case (.Bottom, _):
      return newEnv
    case let (.Arrow(s1, s2), .Arrow(t1, t2)):
      let a1 = try subtype(newEnv, t1, s1)
      return try subtype(a1, s2, t2)
    case let (.Pair(f1, s1), .Pair(f2, s2)):
      let a1 = try subtype(newEnv, f1, f2)
      return try subtype(a1, s1, s2)
    case let (.Rec(x, s1), t), let (t, .Rec(x, s1)):
      return try subtype(newEnv, s1.subst(x, .Rec(x, s1)), t)
    default:
      throw Bail.Out
    }
  }

  // Amadio and Cardelli's algorithm contains, what I hope is, a mistake.  The recursive
  // calls don't keep track of pairs that will be visited by each side of the conjunct, and 
  // in doing so result in a traversal of the entire type tree.  The algorithm is thus
  // exponential in its input.
  func subtypeAC(_ a : [(Type, Type)], _ s : Type, _ t : Type) -> Bool {
    if let _ = a.first(where: { (s2, t2) in s == s2 && t == t2 }) {
      return true
    }

    var newEnv = a
    newEnv.append(s, t)
    switch (s, t) {
    case (_, .Top):
      return true
    case (.Bottom, _):
      return true
    case let (.Arrow(s1, s2), .Arrow(t1, t2)):
      return subtypeAC(newEnv, t1, s1) && subtypeAC(newEnv, s2, t2)
    case let (.Pair(f1, s1), .Pair(f2, s2)):
      return subtypeAC(newEnv, f1, f2) && subtypeAC(newEnv, s1, s2)
    case let (.Rec(x, s1), t), let (t, .Rec(x, s1)):
      return subtypeAC(newEnv, s1.subst(x, .Rec(x, s1)), t)
    default:
      return false
    }
  }

  return (try? subtype([], s, t)) != nil
}

.Rec("X", .Pair(.Top, .TyVar("X"))) <= .Rec("X", .Pair(.Top, .Pair(.Top, .TyVar("X"))))