refactor(library/init/meta/expr): pure Lean implementation of reflected

library/init/meta/expr.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.meta.level init.category.monad
+universes u v
 
 structure pos :=
 (line   : nat)
@@ -47,39 +48,6 @@ meta inductive expr (elaborated : bool := tt)
 | macro       : macro_def → list expr → expr
 
 variable {elab : bool}
-/-- Internal representation for reflected_core -/
-meta constant {u} reflected_core : Sort u
-meta constant reflected_core.to_expr : reflected_core → expr
-meta constant reflected_core.subst : reflected_core → reflected_core → reflected_core
-/-- (reflected a) is a special opaque container for a closed `expr` representing `a`.
-    It can only be obtained via type class inference, which will use the representation
-    of `a` in the calling context. Local constants in the representation are replaced
-    by nested inference of `reflected` instances.
-
-    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 def {u} reflected {α : Sort u} : α → Sort (max 1 u) :=
-λ _, reflected_core
-
-@[inline] meta def {u} reflected.to_expr {α : Sort u} {a : α} : reflected a → expr :=
-reflected_core.to_expr
-
-@[inline] meta def {v u} reflected.subst {α : Sort u} {β : α → Sort v} {f : Π a : α, β a} {a : α} :
-  reflected f → reflected a → reflected (f a) :=
-reflected_core.subst
-
-meta constant expr.reflect (e : expr elab) : reflected e
-meta constant string.reflect (s : string) : reflected s
-
-attribute [class] reflected
-attribute [instance] expr.reflect string.reflect
-
-universes u
-
-@[inline] meta instance {α : Sort u} (a : α) : has_coe (reflected a) expr :=
-⟨reflected.to_expr⟩
-
-meta def reflect {α : Sort u} (a : α) [h : reflected a] : reflected a := h
 
 meta instance : inhabited expr :=
 ⟨expr.sort level.zero⟩
@@ -160,6 +128,35 @@ meta constant expr.collect_univ_params : expr → list name
 /-- `occurs e t` returns `tt` iff `e` occurs in `t` -/
 meta constant expr.occurs        : expr → expr → bool
 
+/-- (reflected a) is a special opaque container for a closed `expr` representing `a`.
+    It can only be obtained via type class inference, which will use the representation
+    of `a` in the calling context. Local constants in the representation are replaced
+    by nested inference of `reflected` instances.
+
+    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 def reflected {α : Sort u} : α → Type :=
+λ _, expr
+
+@[inline] meta def reflected.to_expr {α : Sort u} {a : α} : reflected a → expr :=
+id
+
+@[inline] meta def reflected.subst {α : Sort v} {β : α → Sort u} {f : Π a : α, β a} {a : α} :
+  reflected f → reflected a → reflected (f a) :=
+expr.subst
+
+meta constant expr.reflect (e : expr elab) : reflected e
+meta constant string.reflect (s : string) : reflected s
+
+attribute [class] reflected
+attribute [instance] expr.reflect string.reflect
+attribute [irreducible] reflected reflected.subst reflected.to_expr
+
+@[inline] meta instance {α : Sort u} (a : α) : has_coe (reflected a) expr :=
+⟨reflected.to_expr⟩
+
+meta def reflect {α : Sort u} (a : α) [h : reflected a] : reflected a := h
+
 namespace expr
 open decidable
 

src/library/vm/vm_expr.cpp

@@ -448,14 +448,6 @@ vm_obj expr_is_annotation(vm_obj const &, vm_obj const & _e) {
     }
 }
 
-vm_obj reflected_to_expr(vm_obj const & r) {
-    return r;
-}
-
-vm_obj reflected_subst(vm_obj const & e1, vm_obj const & e2) {
-    return expr_subst(mk_vm_unit(), e1, e2);
-}
-
 vm_obj reflect_expr(vm_obj const & elab, vm_obj const & e) {
     if (to_bool(elab))
         return to_obj(mk_expr_quote(to_expr(e)));
@@ -511,8 +503,6 @@ void initialize_vm_expr() {
     DECLARE_VM_BUILTIN(name({"expr", "collect_univ_params"}), expr_collect_univ_params);
     DECLARE_VM_CASES_BUILTIN(name({"expr", "cases_on"}),   expr_cases_on);
 
-    DECLARE_VM_BUILTIN(name({"reflected_core", "to_expr"}), reflected_to_expr);
-    DECLARE_VM_BUILTIN(name({"reflected_core", "subst"}),   reflected_subst);
     DECLARE_VM_BUILTIN(name("string", "reflect"),           reflect_string);
     DECLARE_VM_BUILTIN(name("expr", "reflect"),             reflect_expr);
 

tests/lean/reflect_type_defeq.lean

@@ -0,0 +1,2 @@
+meta def foo (x : reflected (3 : ℕ)) : reflected ([10] : list ℕ) :=
+x -- ERROR

tests/lean/reflect_type_defeq.lean.expected.out

@@ -0,0 +1,6 @@
+reflect_type_defeq.lean:2:0: error: equation type mismatch, expression
+  x
+has type
+  reflected 3
+but is expected to have type
+  reflected [10]