From 0ca9eb16c10afc365e23dee8b19a68dca0545f9d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 29 Nov 2017 17:40:06 +0100 Subject: [PATCH] fix(library/type_context): preprocess_class: always solve universe mvars in `inout` --- src/library/type_context.cpp | 2 +- tests/lean/run/inout_level.lean | 8 ++++++++ 2 files changed, 9 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/inout_level.lean diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 7e207284d9..fffe7f9b4a 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -3877,7 +3877,7 @@ For all these reasons, we have discarded this alternative design. expr type_context::preprocess_class(expr const & type, buffer & u_replacements, buffer & e_replacements) { - if (!has_expr_metavar(type)) + if (!has_metavar(type)) return type; type_context::tmp_locals locals(*this); expr it = type; diff --git a/tests/lean/run/inout_level.lean b/tests/lean/run/inout_level.lean new file mode 100644 index 0000000000..2a88929b68 --- /dev/null +++ b/tests/lean/run/inout_level.lean @@ -0,0 +1,8 @@ +section bug +variables (x y z : Type) +variables (f : x → y) (g : y → z) +variables (xy : set (x → y)) (yz : set (y → z)) (xz : set (x → z)) +--#check f ∈ xy +--#check g ∈ yz +#check (g ∘ f) ∈ xz --error +end bug