chore: remove dangerous instances

Lake/Build/Info.lean

@@ -7,7 +7,6 @@ import Lake.Config.LeanExe
 import Lake.Config.ExternLib
 import Lake.Build.Facets
 import Lake.Util.EquipT
-import Lake.Util.Fact
 
 /-!
 # Build Info
@@ -73,6 +72,12 @@ abbrev BuildInfo.key : (self : BuildInfo) → BuildKey
 | dynlibExternLib l => l.dynlibBuildKey
 | target p t => p.targetBuildKey t
 
+/-- Class recording that a package `p` has name `n`. -/
+class PackageName (p : Package) (n : outParam Name) : Prop where
+  proof : p.name = n
+
+instance : PackageName p p.name := ⟨rfl⟩
+
 /-! ### Instances for deducing data types of `BuildInfo` keys -/
 
 instance [FamilyDef ModuleData f α]
@@ -83,7 +88,7 @@ instance [FamilyDef PackageData f α]
 : FamilyDef BuildData (BuildInfo.key (.packageFacet p f)) α where
   family_key_eq_type := by unfold BuildData; simp
 
-instance [h : Fact (p.name = n)] [FamilyDef CustomData (n, t) α]
+instance [h : PackageName p n] [FamilyDef CustomData (n, t) α]
 : FamilyDef BuildData (BuildInfo.key (.target p t)) α where
   family_key_eq_type := by unfold BuildData; simp [h.proof]
 

Lake/Config/TargetConfig.lean

@@ -11,7 +11,7 @@ namespace Lake
 /-- A custom target's declarative configuration. -/
 structure TargetConfig (pkgName name : Name) : Type where
   /-- The target's build function. -/
-  build : (pkg : Package) → [Fact (pkg.name = pkgName)] →
+  build : (pkg : Package) → [PackageName pkg pkgName] →
     IndexBuildM (CustomData (pkgName, name))
   /-- The target's resulting build job. -/
   getJob : CustomData (pkgName, name) → BuildJob Unit
@@ -19,7 +19,7 @@ structure TargetConfig (pkgName name : Name) : Type where
 
 /-- A smart constructor for target configurations that generate CLI targets. -/
 @[inline] def mkTargetJobConfig
-(build : (pkg : Package) → [Fact (pkg.name = pkgName)] → IndexBuildM (BuildJob α))
+(build : (pkg : Package) → [PackageName pkg pkgName] → IndexBuildM (BuildJob α))
 [h : FamilyDef CustomData (pkgName, name) (BuildJob α)] : TargetConfig pkgName name where
   build := cast (by rw [← h.family_key_eq_type]) build
   getJob := fun data => discard <| ofFamily data

Lake/Util/Fact.lean

@@ -1,13 +0,0 @@
-/-
-Copyright (c) 2022 Mac Malone. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mac Malone
--/
-
-namespace Lake
-
-/-- Type class synthesis of propositions. -/
-class Fact (P : Prop) : Prop where
-  proof : P
-
-instance : Fact (a = a) := ⟨rfl⟩

Lake/Util/MainM.lean

@@ -74,8 +74,7 @@ protected def error (msg : String) (rc : ExitCode := 1) : MainM α := do
   exit rc
 
 instance : MonadError MainM := ⟨MainM.error⟩
-instance [ToString ε] : MonadLift (EIO ε) MainM := ⟨MonadError.runEIO⟩
-instance : MonadLift IO MainM := inferInstance -- necessary, but don't know why
+instance : MonadLift IO MainM := ⟨MonadError.runEIO⟩
 
 def runLogIO (x : LogIO α) (verbosity := Verbosity.normal) : MainM α :=
   liftM <| x.run <| MonadLog.eio verbosity