From 14c5b4bb8a9c5f62081594d2beaca274eaa0b8f3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 2 Nov 2018 12:55:21 +0100
Subject: Print full binders in subtyping incompatible polymorphism error.

Close #8891
---
 kernel/subtyping.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'kernel/subtyping.ml')

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index d64342dbb0..347c30dd64 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -93,10 +93,8 @@ let check_conv_error error why cst poly f env a1 a2 =
      | Univ.UniverseInconsistency e -> error (IncompatibleUniverses e)
 
 let check_polymorphic_instance error env auctx1 auctx2 =
-  if not (Univ.AUContext.size auctx1 == Univ.AUContext.size auctx2) then
-    error IncompatibleInstances
-  else if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then
-    error (IncompatibleConstraints auctx1)
+  if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then
+    error (IncompatibleConstraints { got = auctx1; expect = auctx2; } )
   else
     Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env
 
-- 
cgit v1.2.3