From d6ca9b2f71bced8711b184400fa7e80061497fd7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 12 Feb 2018 14:46:05 +0100
Subject: Adding a sanity check on inductive variance subtyping.

---
 checker/univ.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'checker/univ.ml')

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
-- 
cgit v1.2.3