From de1f3069045e5b21804b9f58a3510999ef580c84 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 9 Nov 2013 13:28:38 +0100
Subject: Be defensive in univ/eq_instances, raise an anomaly on incompatible
 instances.

---
 kernel/univ.ml | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8047a36f48..d203c2b737 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1899,15 +1899,22 @@ let enforce_leq_level u v c =
   if Level.equal u v then c else Constraint.add (u,Le,v) c
 
 let enforce_eq_instances x y = 
-  CArray.fold_right2 enforce_eq_level (Instance.to_array x) (Instance.to_array y)
+  let ax = Instance.to_array x and ay = Instance.to_array y in
+    if Array.length ax != Array.length ay then
+      anomaly (Pp.str "Invalid argument: enforce_eq_instances called with instances of different lengths");
+    CArray.fold_right2 enforce_eq_level ax ay
 
 type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
 
-let enforce_eq_instances_univs strict t1 t2 c = 
+let enforce_eq_instances_univs strict x y c = 
   let d = if strict then ULub else UEq in
-    CArray.fold_right2 (fun x y -> UniverseConstraints.add (Universe.make x, d, Universe.make y))
-      (Instance.to_array t1) (Instance.to_array t2) c
-
+  let ax = Instance.to_array x and ay = Instance.to_array y in
+    if Array.length ax != Array.length ay then
+      anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with instances of different lengths");    
+    CArray.fold_right2
+      (fun x y -> UniverseConstraints.add (Universe.make x, d, Universe.make y))
+      ax ay c
+      
 let merge_constraints c g =
   Constraint.fold enforce_constraint c g
 
-- 
cgit v1.2.3