diff --git a/Lake/Build/Data.lean b/Lake/Build/Data.lean
index 4fb462e224..2b2838ad40 100644
--- a/Lake/Build/Data.lean
+++ b/Lake/Build/Data.lean
@@ -50,23 +50,11 @@ theorem isModuleKey_data {k : BuildKey}
 (h : k.isModuleKey = true) : BuildData k = ModuleData k.facet := by
   unfold BuildData; simp [h]
 
-instance (k : ModuleBuildKey f)
-[t : DynamicType ModuleData f α] : DynamicType BuildData k α where
-  eq_dynamic_type := by
-    have h := isModuleKey_data k.is_module_key
-    simp [h, k.facet_eq_fixed, t.eq_dynamic_type]
-
 theorem isPackageKey_data {k : BuildKey}
 (h : k.isPackageKey = true) : BuildData k = PackageData k.facet := by
   unfold BuildData, BuildKey.isModuleKey
   simp [of_decide_eq_true (of_decide_eq_true h |>.1), h]
 
-instance (k : PackageBuildKey f)
-[t : DynamicType PackageData f α] : DynamicType BuildData k α where
-  eq_dynamic_type := by
-    have h := isPackageKey_data k.is_package_key
-    simp [h, k.facet_eq_fixed, t.eq_dynamic_type]
-
 theorem isTargetKey_data {k : BuildKey}
 (h : k.isTargetKey = true) : BuildData k = TargetData k.facet := by
   unfold BuildData, BuildKey.isModuleKey, BuildKey.isPackageKey
diff --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean
index a40400071d..d8054e3c26 100644
--- a/Lake/Build/Info.lean
+++ b/Lake/Build/Info.lean
@@ -34,11 +34,11 @@ inductive BuildInfo
 
 /-! ### Build Key Helper Constructors -/
 
-abbrev Module.mkBuildKey (facet : WfName) (self : Module) : ModuleBuildKey facet :=
-  ⟨⟨none, self.keyName, facet⟩, rfl, rfl⟩
+abbrev Module.facetBuildKey (facet : WfName) (self : Module) : BuildKey :=
+  ⟨none, self.keyName, facet⟩
 
-abbrev Package.mkBuildKey (facet : WfName) (self : Package) : PackageBuildKey facet :=
-  ⟨⟨self.name, none, facet⟩, rfl, rfl⟩
+abbrev Package.facetBuildKey (facet : WfName) (self : Package) : BuildKey :=
+  ⟨self.name, none, facet⟩
 
 abbrev LeanLib.staticBuildKey (self : LeanLib) : BuildKey :=
   ⟨self.pkg.name, self.name, staticFacet⟩
@@ -59,8 +59,8 @@ abbrev ExternLib.sharedBuildKey (self : ExternLib) : BuildKey :=
 
 /-- The key that identifies the build in the Lake build store. -/
 abbrev BuildInfo.key : (self : BuildInfo) → BuildKey
-| module m f => m.mkBuildKey f
-| package p f => p.mkBuildKey f
+| module m f => m.facetBuildKey f
+| package p f => p.facetBuildKey f
 | staticLeanLib l => l.staticBuildKey
 | sharedLeanLib l => l.sharedBuildKey
 | leanExe x => x.buildKey
diff --git a/Lake/Build/Key.lean b/Lake/Build/Key.lean
index 19b768290f..b5bbe00b31 100644
--- a/Lake/Build/Key.lean
+++ b/Lake/Build/Key.lean
@@ -108,38 +108,3 @@ theorem eq_of_quickCmp :
 
 instance : EqOfCmp BuildKey quickCmp where
   eq_of_cmp := eq_of_quickCmp
-
-end BuildKey
-
--- ## Subtypes
-
-/-- The type of build keys for modules. -/
-structure ModuleBuildKey (fixedFacet : WfName) extends BuildKey where
-  is_module_key : toBuildKey.isModuleKey = true
-  facet_eq_fixed : toBuildKey.facet = fixedFacet
-
-instance : Coe (ModuleBuildKey f) BuildKey := ⟨(·.toBuildKey)⟩
-
-@[inline] def BuildKey.toModuleKey
-(self : BuildKey) (h : self.isModuleKey) : ModuleBuildKey self.facet :=
-  ⟨self, h, rfl⟩
-
-@[inline] def ModuleBuildKey.module (self : ModuleBuildKey f) : WfName :=
-  self.toBuildKey.module self.is_module_key
-
-/-- The type of build keys for packages. -/
-structure PackageBuildKey (fixedFacet : WfName) extends BuildKey where
-  is_package_key : toBuildKey.isPackageKey = true
-  facet_eq_fixed : toBuildKey.facet = fixedFacet
-
-instance : Coe (PackageBuildKey f) BuildKey := ⟨(·.toBuildKey)⟩
-
-@[inline] def BuildKey.toPackageKey
-(self : BuildKey) (h : self.isPackageKey) : PackageBuildKey self.facet :=
-  ⟨self, h, rfl⟩
-
-@[inline] def PackageBuildKey.package (self : PackageBuildKey f) : WfName :=
-  self.toBuildKey.package <| by
-    have h := self.is_package_key
-    unfold BuildKey.isPackageKey at h
-    exact (of_decide_eq_true h).1
diff --git a/Lake/Build/Store.lean b/Lake/Build/Store.lean
index b7bedc2045..91cea34733 100644
--- a/Lake/Build/Store.lean
+++ b/Lake/Build/Store.lean
@@ -16,23 +16,9 @@ topological-based build of an initial key's dependencies).
 
 namespace Lake
 
-/-! ## Abstract Monad -/
-
 /-- A monad equipped with a Lake build store. -/
 abbrev MonadBuildStore (m) := MonadDStore BuildKey BuildData m
 
-@[inline] instance [MonadBuildStore m]
-[DynamicType ModuleData f α] : MonadStore (ModuleBuildKey f) α m where
-  fetch? k := fetch? k.toBuildKey
-  store k a := store k.toBuildKey a
-
-@[inline] instance [MonadBuildStore m]
-[DynamicType PackageData f α] : MonadStore (PackageBuildKey f) α m where
-  fetch? k := fetch? k.toBuildKey
-  store k a := store k.toBuildKey a
-
-/-! ## Concrete Type -/
-
 /-- The type of the Lake build store. -/
 abbrev BuildStore :=
   DRBMap BuildKey BuildData BuildKey.quickCmp