feat: deriving BEq, Hashable for Lean.Import (#10018)

This PR derives `BEq` and `Hashable` for `Lean.Import`. Lake already did
this later, but it now done when defining `Import`.

Doing this in Lake became problematic when porting it to the module
system (#9749).

src/Lean/Setup.lean

@@ -29,7 +29,8 @@ structure Import where
   isExported : Bool := true
   /-- Whether all definitions (transitively) reachable through the -/
   isMeta     : Bool := false
-  deriving Repr, Inhabited, ToJson, FromJson
+  deriving Repr, Inhabited, ToJson, FromJson,
+    BEq, Hashable -- needed by Lake (in `Lake.Load.Elab.Lean`)
 
 instance : Coe Name Import := ⟨({module := ·})⟩
 

src/lake/Lake/Load/Lean/Elab.lean

@@ -21,8 +21,6 @@ open System Lean
 
 namespace Lake
 
-deriving instance BEq, Hashable for Import
-
 /- Cache for the imported header environment of Lake configuration files. -/
 builtin_initialize importEnvCache : IO.Ref (Std.HashMap (Array Import) Environment) ← IO.mkRef {}