try making Quoted a structure

Qq/Macro.lean

@@ -247,7 +247,7 @@ partial def unquoteExpr (e : Expr) : UnquoteM Expr := do
     }
     return fv
   let e ← whnf e
-  let .const c _ ← pure e.getAppFn | throwError "unquoteExpr: {e} : {eTy}"
+  let .const c _ ← pure e.getAppFn | throwError "unquoteExpr: {e} : {eTy}: {e.getAppFn} not a constant"
   let nargs := e.getAppNumArgs
   match c, nargs with
     | ``betaRev', 2 => return betaRev' (← unquoteExpr (e.getArg! 0)) (← unquoteExprList (e.getArg! 1))
@@ -536,9 +536,11 @@ elab_rules : term <= expectedType
         let u ← mkFreshExprMVar (some (.const ``Level []))
         let u' := .app (.const ``Expr.sort []) u
         let t ← mkFreshExprMVar (mkApp (.const ``Quoted []) u')
-        expectedType := .app (.const ``Quoted []) t
+        expectedType := .app (.const ``Quoted []) (.app (.const ``QuotedStruct.raw []) t)
       Impl.macro t expectedType
 
+#check q(Type)
+
 /-- `Q(α)` is the type of Lean expressions having type `α`.  -/
 scoped syntax "Q(" term Parser.Term.optType ")" : term
 
@@ -547,7 +549,7 @@ macro_rules | `(Q($t : $ty)) => `(Q(($t : $ty)))
 elab_rules : term <= expectedType
   | `(Q($t)) => do
     let expectedType ← instantiateMVars expectedType
-    unless ← isDefEq expectedType q(Type) do
+    unless ← isDefEq expectedType q(Type).raw do
       throwError "Q(.) has type Type, expected type is{indentExpr expectedType}"
     commitIfDidNotPostpone do Impl.macro t expectedType
 

Qq/Typ.lean

@@ -5,29 +5,29 @@ set_option linter.unusedVariables false
 
 namespace Qq
 
+structure QuotedStruct where
+    unsafeMk ::
+  raw : Expr
+deriving BEq, Hashable, Inhabited, Repr
+
 /--
 `Quoted α` is the type of Lean expressions having type `α`.
 
 You should usually write this using the notation `Q($α)`.
 -/
-def Quoted (α : Expr) := Expr
+def Quoted (α : Expr) := QuotedStruct
 
-/--
-Creates a quoted expression.  Requires that `e` has type `α`.
+protected def Quoted.unsafeMk (e : Expr) : Quoted α := ⟨e⟩
 
-You should usually write this using the notation `q($e)`.
--/
-protected def Quoted.unsafeMk (e : Expr) : Quoted α := e
+instance : BEq (Quoted α) := inferInstanceAs (BEq QuotedStruct)
+instance : Hashable (Quoted α) := inferInstanceAs (Hashable QuotedStruct)
+instance : Inhabited (Quoted α) := inferInstanceAs (Inhabited QuotedStruct)
+-- instance : ToString (Quoted α) := inferInstanceAs (ToString QuotedStruct)
+instance : Repr (Quoted α) := inferInstanceAs (Repr QuotedStruct)
 
-instance : BEq (Quoted α) := inferInstanceAs (BEq Expr)
-instance : Hashable (Quoted α) := inferInstanceAs (Hashable Expr)
-instance : Inhabited (Quoted α) := inferInstanceAs (Inhabited Expr)
-instance : ToString (Quoted α) := inferInstanceAs (ToString Expr)
-instance : Repr (Quoted α) := inferInstanceAs (Repr Expr)
-
-instance : CoeOut (Quoted α) Expr where coe e := e
-instance : CoeOut (Quoted α) MessageData where coe := .ofExpr
-instance : ToMessageData (Quoted α) where toMessageData := .ofExpr
+-- instance : CoeOut (Quoted α) Expr where coe e := e
+instance : CoeOut (Quoted α) MessageData where coe q := .ofExpr q.raw
+instance : ToMessageData (Quoted α) where toMessageData q := .ofExpr q.raw
 
 /-- Gets the type of a quoted expression.  -/
 protected abbrev Quoted.ty (t : Quoted α) : Expr := α
@@ -37,7 +37,7 @@ protected abbrev Quoted.ty (t : Quoted α) : Expr := α
 
 You should usually write this using the notation `$lhs =Q $rhs`.
 -/
-structure QuotedDefEq {α : Quoted (.sort u)} (lhs rhs : Quoted α) : Prop :=
+structure QuotedDefEq {α : Quoted (.sort u)} (lhs rhs : Quoted α.raw) : Prop :=
   unsafeIntro ::
 
 /--
@@ -50,19 +50,19 @@ structure QuotedLevelDefEq (u v : Level) : Prop :=
 
 open Meta in
 protected def Quoted.check (e : Quoted α) : MetaM Unit := do
-  let α' ← inferType e
+  let α' ← inferType e.raw
   unless ← isDefEq α α' do
-    throwError "type mismatch{indentExpr e}\n{← mkHasTypeButIsExpectedMsg α' α}"
+    throwError "type mismatch{indentExpr e.raw}\n{← mkHasTypeButIsExpectedMsg α' α}"
 
 open Meta in
 protected def QuotedDefEq.check (e : @QuotedDefEq u α lhs rhs) : MetaM Unit := do
   α.check
   lhs.check
   rhs.check
-  unless ← isDefEq lhs rhs do
+  unless ← isDefEq lhs.raw rhs.raw do
     throwError "{lhs} and {rhs} are not defeq"
 
 open Meta in
 protected def QuotedLevelDefEq.check (e : QuotedLevelDefEq lhs rhs) : MetaM Unit := do
   unless ← isLevelDefEq lhs rhs do
-    throwError "{lhs} and {rhs} are not defeq"
+    throwError "{lhs} and {rhs} are not defeq"