-- This solution resolves all issues. It was proposed by Mario Carneiro at
-- https://proofassistants.stackexchange.com/a/2102/169

-- The idea is to load the data from a JSON file and circumvent elaboration
-- and the linter by creating the required objects more directly.
-- Note that the solution depends on mathlib4, and more precisely the
-- Qq library.

import Lean
import Qq

structure Edge (n : Nat) : Type :=
  edge ::
  fst : Fin n
  snd : Fin fst
open Edge

inductive Tree (α : Type) : Type
  | empty : Tree α
  | leaf : α → Tree α
  | node : α → Tree α → Tree α → Tree α

def Edge.mk' (n a b : Nat) (H : Nat.blt a n = true) (H2 : Nat.blt b a = true) : Edge n :=
  ⟨⟨a, by simp_all⟩, ⟨b, (by simp_all : b < a)⟩⟩

open Qq Lean Meta Elab

def mkEdge (n : Q(Nat)) (j : Json) : Except String Q(Edge $n) := do
  let arr ← j.getArr?
  have a : Q(Nat) := mkRawNatLit (← arr[0]!.getNat?)
  have b : Q(Nat) := mkRawNatLit (← arr[1]!.getNat?)
  have H : Q(Nat.blt $a $n = true) := (q(Eq.refl true) : Expr)
  have H2 : Q(Nat.blt $b $a = true) := (q(Eq.refl true) : Expr)
  pure q(Edge.mk' $n $a $b $H $H2)

partial def mkTree (n : Q(Nat)) (j : Json) : Except String Q(Tree (Edge $n)) := do
  let arr ← j.getArr?
  match arr with
  | #[e, l, r] => pure q(Tree.node $(← mkEdge n e) $(← mkTree n l) $(← mkTree n r))
  | #[] => pure q(Tree.empty)
  | _ => pure q(Tree.leaf $(← mkEdge n j))

elab "tree_from_file" name:ident " from " file:str : command => do
  let file ← IO.FS.readFile file.getString
  let result : Except String (Q(Nat) × Expr) := do
    let .arr #[n, tree] ← Json.parse file | throw "bad format"
    let n : Q(Nat) := mkRawNatLit (← n.getNat?)
    pure (n, ← mkTree n tree)
  let .ok (n, value) := result | throwError "failed to parse"
  Elab.Command.liftCoreM <| addDecl <| .defnDecl {
    name := name.getId
    levelParams := []
    type := q(Tree (Edge $n))
    value
    hints := .regular 0
    safety := .safe
  }

tree_from_file test from "test.json"
#check test -- test : Tree (Edge 666)