fix(init/meta/expr,library): reflect should accept Props

Fixes #1590

library/init/meta/expr.lean

@@ -56,9 +56,9 @@ universes u v
 
     The quotation expression `(a) (outside of patterns) is equivalent to `reflect a`
     and thus can be used as an explicit way of inferring an instance of `reflected a`. -/
-meta constant reflected {α : Type u} : α → Type u
-meta constant reflected.to_expr {α : Type u} {a : α} : reflected a → expr
-meta constant reflected.subst {α : Type u} {β : α → Type v} {f : Π a : α, β a} {a : α} :
+meta constant reflected {α : Sort u} : α → Sort (max 1 u)
+meta constant reflected.to_expr {α : Sort u} {a : α} : reflected a → expr
+meta constant reflected.subst {α : Sort u} {β : α → Sort v} {f : Π a : α, β a} {a : α} :
   reflected f → reflected a → reflected (f a)
 meta constant expr.reflect (e : expr elab) : reflected e
 meta constant string.reflect (s : string) : reflected s

library/init/meta/has_reflect.lean

@@ -6,7 +6,7 @@ Authors: Sebastian Ullrich
 prelude
 import init.meta.expr init.util
 
-@[reducible] meta def {u} has_reflect (α : Type u) := Π a : α, reflected a
+@[reducible] meta def {u} has_reflect (α : Sort u) := Π a : α, reflected a
 
 meta instance bool.reflect : has_reflect bool
 | tt := `(tt)

src/library/quote.cpp

@@ -33,11 +33,7 @@ public:
     virtual expr check_type(expr const & m, abstract_type_context & ctx, bool infer_only) const {
         expr const & e = get_expr_quote_value(m);
         expr ty = ctx.check(e, infer_only);
-        if (auto l = dec_level(get_level(ctx, ty))) {
-            return mk_app(mk_constant(get_reflected_name(), {*l}), ty, e);
-        } else {
-            return *g_expr;
-        }
+        return mk_app(mk_constant(get_reflected_name(), {get_level(ctx, ty)}), ty, e);
     }
     virtual optional<expr> expand(expr const &, abstract_type_context &) const {
         return optional<expr>();

src/library/type_context.cpp

@@ -32,7 +32,6 @@ Author: Leonardo de Moura
 #include "library/fun_info.h"
 #include "library/num.h"
 #include "library/quote.h"
-#include "library/app_builder.h"
 
 #ifndef LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH
 #define LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH 32
@@ -3529,12 +3528,13 @@ struct instance_synthesizer {
             expr q = mk_expr_quote(r);
             buffer<expr> new_inst_mvars;
             for (expr const & local : r_locals.get_collected()) {
-                expr cls = mk_app(m_ctx, get_reflected_name(), local);
+                expr ty = m_ctx.infer(local);
+                expr cls = mk_app(mk_constant(get_reflected_name(), {get_level(m_ctx, ty)}), ty, local);
                 expr new_mvar = m_ctx.mk_tmp_mvar(cls);
                 new_inst_mvars.push_back(new_mvar);
                 expr local_ty = m_ctx.infer(local);
-                level u = *dec_level(get_level(m_ctx, local_ty));
-                level v = *dec_level(get_level(m_ctx, instantiate(binding_body(r_ty), local)));
+                level u = get_level(m_ctx, local_ty);
+                level v = get_level(m_ctx, instantiate(binding_body(r_ty), local));
                 q = mk_app(mk_constant(get_reflected_subst_name(), {v, u}),
                            {local_ty, mk_lambda("_x", binding_domain(r_ty), binding_body(r_ty)), r, local, q, new_mvar});
                 r = instantiate(binding_body(r), local);

tests/lean/run/1590.lean

@@ -0,0 +1,2 @@
+#check `(true.intro)
+#check λ (h : true) [reflected h], `(id h)