From cada5caf9c739efc7a2d932af4498b61f7fc9608 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 21 Sep 2020 13:35:42 +0200
Subject: No bidirectionality when expected type for lambda is an evar.

This fixes #12623 (bidirectionality breaks impredicativity).
---
 kernel/environ.ml  | 5 +++++
 kernel/environ.mli | 1 +
 2 files changed, 6 insertions(+)

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index e497b7904a..dec9e1deb8 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -274,6 +274,11 @@ let is_impredicative_sort env = function
 
 let is_impredicative_univ env u = is_impredicative_sort env (Sorts.sort_of_univ u)
 
+let is_impredicative_family env = function
+  | Sorts.InSProp | Sorts.InProp -> true
+  | Sorts.InSet -> is_impredicative_set env
+  | Sorts.InType -> false
+
 let type_in_type env = not (typing_flags env).check_universes
 let deactivated_guard env = not (typing_flags env).check_guarded
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 47a118aa42..f443ba38e1 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -122,6 +122,7 @@ val indices_matter : env -> bool
 
 val is_impredicative_sort : env -> Sorts.t -> bool
 val is_impredicative_univ : env -> Univ.Universe.t -> bool
+val is_impredicative_family : env -> Sorts.family -> bool
 
 (** is the local context empty *)
 val empty_context : env -> bool
-- 
cgit v1.2.3