aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/univ.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/univ.ml')
-rw-r--r--checker/univ.ml7
1 files changed, 7 insertions, 0 deletions
diff --git a/checker/univ.ml b/checker/univ.ml
index 46b3ce680..ebc37bc10 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1011,6 +1011,13 @@ struct
A'] as opposed to [A' <= A]. *)
type t = Irrelevant | Covariant | Invariant
+ let check_subtype x y = match x, y with
+ | (Irrelevant | Covariant | Invariant), Irrelevant -> true
+ | Irrelevant, Covariant -> false
+ | (Covariant | Invariant), Covariant -> true
+ | (Irrelevant | Covariant), Invariant -> false
+ | Invariant, Invariant -> true
+
let leq_constraint csts variance u u' =
match variance with
| Irrelevant -> csts