# Subtype Check with Type DAG

Trying to understand how compiler/static-type-checker checks for subtyping, I run into 2 problems.

## 1. Reachability in DAG

Since both Python/C++ support multiple inheriatnce, the types can be represented as a DAG.


A  C
| / \
B    D
|\   |
E F /
|  x
| / \
G    H


Now is_subtype(A,B) -> bool becomes the problem of reachability query in the DAG.

For a single query, this will take O(n). For multiple queries, I found a 2-hop transitive closure paper, where reachability(a,b) operation can be done with first_edge(a,b) which takes |L_{out}(a)| + |L_{in}(b)|. Since the size of graph with added transitive closures is up to O(n^1.5), This is in average O(n^0.5), however O(n) in the worst case.

## 2. Generic Parameter

To check is_subtype(Sequence[String], Iterable[Any]), there can be 2 paths:

1. Sequence[String] to Sequence[Any] (covariant) to Iterable[Any]
2. Sequence[String] to Iterable[String] to Iterable[Any]

I don't know where to start if I have to augment the DAG in 1 with Parameters. Instantiating types and considering Sequence[String] as one node seems wasteful and uses too much cpu/memory.

## Questions

Q1. How do current compiler/checks solve this problem? Is brute-force enough for sparse graphs in practical usages?

Parent* ptr = new Child();  // gcc

b: List
a: Iterable = b  # mypy, pyright


Q4. Given let a = b; (Rust), auto a = b; (C++) or a = b (Python), Should I assume type(a)==type(b) for Rust/C++ and type(a)>=type(b) for Python? (Python allows a: Iterable = Sequence) How does type-bound check mix with type-interence? I guess I use equalities+unification for type-inference and a list of inequality constraints for type-bound checks.