... | ... | @@ -140,6 +140,13 @@ sorts: `TY` (for kinds that classify normal types) or `CO` (for kinds that |
|
|
classify coercion evidence). The coercion kind, `T1 :=: T2`, is
|
|
|
represented by `PredTy (EqPred T1 T2)`.
|
|
|
|
|
|
### Kind subtyping
|
|
|
|
|
|
[](https://docs.google.com/drawings/pub?id=1M5yBP8iAWTgqdI3oG1UNnYihVlipnvvk2vLInAFxtNM&w=359&h=229)
|
|
|
|
|
|
|
|
|
(You can edit this picture [ here](https://docs.google.com/drawings/d/1M5yBP8iAWTgqdI3oG1UNnYihVlipnvvk2vLInAFxtNM/edit?hl=en_GB).)
|
|
|
|
|
|
## Type variables
|
|
|
|
|
|
|
... | ... | |