diff --git a/Lake/Build/Data.lean b/Lake/Build/Data.lean
index c5d59ca0a7..7d95a6570c 100644
--- a/Lake/Build/Data.lean
+++ b/Lake/Build/Data.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Build.Key
-import Lake.Util.DynamicType
+import Lake.Util.Family
 
 open Lean
 namespace Lake
@@ -14,22 +14,42 @@ namespace Lake
 --------------------------------------------------------------------------------
 
 /--
-Type of build data associated with a module facet in the Lake build store.
-For example a transitive × direct import pair for `imports` or an active build
-target for `lean.c`.
+The open type family which maps a module facet's name to it build data
+in the Lake build store. For example, a transitive × direct import pair
+for the `lean.imports` facet or an active build target for `lean.c`.
 
-It is a dynamic type, meaning additional alternatives can be add lazily
-as needed.
+It is an open type, meaning additional mappings can be add lazily
+as needed (via `module_data`).
 -/
 opaque ModuleData (facet : WfName) : Type
 
-/-- Type of build data associated with package facets (e.g., `extraDep`). -/
+/--
+The open type family which maps a package facet's name to it build data
+in the Lake build store. For example, a transitive dependencies of the package
+for the facet `deps`.
+
+It is an open type, meaning additional mappings can be add lazily
+as needed (via `package_data`).
+-/
 opaque PackageData (facet : WfName) : Type
 
-/-- Type of build data associated with Lake targets (e.g., `extern_lib`). -/
+/--
+The open type family which maps a (builtin) Lake target's (e.g., `extern_lib`)
+facet to its associated build data. For example, an active build target for
+the `externLib.static` facet.
+
+It is an open type, meaning additional mappings can be add lazily
+as needed (via `target_data`).
+-/
 opaque TargetData (facet : WfName) : Type
 
-/-- Type of build data associated with custom targets. -/
+/--
+The open type family which maps a custom target's name to its build data
+in the Lake build store.
+
+It is an open type, meaning additional mappings can be add lazily
+as needed (via `custom_data`).
+-/
 opaque CustomData (target : WfName) : Type
 
 --------------------------------------------------------------------------------
@@ -37,9 +57,9 @@ opaque CustomData (target : WfName) : Type
 --------------------------------------------------------------------------------
 
 /--
-Type of the build data associated with a key in the Lake build store.
-It is dynamic type composed of the three separate dynamic types for modules,
-packages, and targets.
+A mapping between a build key and its associated build data in the store.
+It is a simple type function composed of the separate open type families for
+modules facets, package facets, Lake target facets, and custom targets.
 -/
 abbrev BuildData : BuildKey → Type
 | .moduleFacet _ f => ModuleData f
@@ -56,25 +76,25 @@ scoped macro (name := packageDataDecl) doc?:optional(Parser.Command.docComment)
 "package_data " id:ident " : " ty:term : command => do
   let dty := mkCIdentFrom (← getRef) ``PackageData
   let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
-  `($[$doc?]? dynamic_data $id : $dty $key := $ty)
+  `($[$doc?]? family_def $id : $dty $key := $ty)
 
 /-- Macro for declaring new `ModuleData`. -/
 scoped macro (name := moduleDataDecl) doc?:optional(Parser.Command.docComment)
 "module_data " id:ident " : " ty:term : command => do
   let dty := mkCIdentFrom (← getRef) ``ModuleData
   let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
-  `($[$doc?]? dynamic_data $id : $dty $key := $ty)
+  `($[$doc?]? family_def $id : $dty $key := $ty)
 
 /-- Macro for declaring new `TargetData`. -/
 scoped macro (name := targetDataDecl) doc?:optional(Parser.Command.docComment)
 "target_data " id:ident " : " ty:term : command => do
   let dty := mkCIdentFrom (← getRef) ``TargetData
   let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
-  `($[$doc?]? dynamic_data $id : $dty $key := $ty)
+  `($[$doc?]? family_def $id : $dty $key := $ty)
 
 /-- Macro for declaring new `CustomData`. -/
 scoped macro (name := customDataDecl) doc?:optional(Parser.Command.docComment)
 "custom_data " id:ident " : " ty:term : command => do
   let dty := mkCIdentFrom (← getRef) ``CustomData
   let key := WfName.quoteFrom id <| WfName.ofName <| id.getId
-  `($[$doc?]? dynamic_data $id : $dty $key := $ty)
+  `($[$doc?]? family_def $id : $dty $key := $ty)
diff --git a/Lake/Build/Facets.lean b/Lake/Build/Facets.lean
index 681cab0eb3..57bb08c71f 100644
--- a/Lake/Build/Facets.lean
+++ b/Lake/Build/Facets.lean
@@ -27,11 +27,11 @@ structure ModuleFacet (α) where
   data_eq : ModuleData name = α
   deriving Repr
 
-instance (facet : ModuleFacet α) : DynamicType ModuleData facet.name α :=
+instance (facet : ModuleFacet α) : FamilyDef ModuleData facet.name α :=
   ⟨facet.data_eq⟩
 
-instance [DynamicType ModuleData facet α] : CoeDep WfName facet (ModuleFacet α) :=
-  ⟨facet, eq_dynamic_type⟩
+instance [FamilyDef ModuleData facet α] : CoeDep WfName facet (ModuleFacet α) :=
+  ⟨facet, family_key_eq_type⟩
 
 namespace Module
 abbrev leanBinFacet  := &`lean.bin
diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean
index f7344031d5..a47438f08d 100644
--- a/Lake/Build/Index.lean
+++ b/Lake/Build/Index.lean
@@ -55,24 +55,24 @@ Converts a conveniently typed module facet build function into its
 dynamically typed equivalent.
 -/
 @[inline] def mkModuleFacetBuild {facet : WfName} (build : Module → IndexT m α)
-[h : DynamicType ModuleData facet α] : Module → IndexT m (ModuleData facet) :=
-  cast (by rw [← h.eq_dynamic_type]) build
+[h : FamilyDef ModuleData facet α] : Module → IndexT m (ModuleData facet) :=
+  cast (by rw [← h.family_key_eq_type]) build
 
 /--
 Converts a conveniently typed package facet build function into its
 dynamically typed equivalent.
 -/
 @[inline] def mkPackageFacetBuild {facet : WfName} (build : Package → IndexT m α)
-[h : DynamicType PackageData facet α] : Package → IndexT m (PackageData facet) :=
-  cast (by rw [← h.eq_dynamic_type]) build
+[h : FamilyDef PackageData facet α] : Package → IndexT m (PackageData facet) :=
+  cast (by rw [← h.family_key_eq_type]) build
 
 /--
 Converts a conveniently typed target facet build function into its
 dynamically typed equivalent.
 -/
 @[inline] def mkTargetFacetBuild (facet : WfName) (build : IndexT m α)
-[h : DynamicType TargetData facet α] : IndexT m (TargetData facet) :=
-  cast (by rw [← h.eq_dynamic_type]) build
+[h : FamilyDef TargetData facet α] : IndexT m (TargetData facet) :=
+  cast (by rw [← h.family_key_eq_type]) build
 
 section
 variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
@@ -146,7 +146,7 @@ the initial set of Lake package facets (e.g., `extraDep`).
       build mod
     else if let some config := (← getWorkspace).findModuleFacetConfig? facet then
       if h : facet = config.name then
-        have : DynamicType ModuleData facet (ActiveBuildTarget config.resultType) :=
+        have : FamilyDef ModuleData facet (ActiveBuildTarget config.resultType) :=
           ⟨by simp [h]⟩
         mkModuleFacetBuild config.build mod
       else
@@ -158,7 +158,7 @@ the initial set of Lake package facets (e.g., `extraDep`).
       build pkg
     else if let some config := pkg.findPackageFacetConfig? facet then
       if h : facet = config.name then
-        have : DynamicType PackageData facet (ActiveBuildTarget config.resultType) :=
+        have : FamilyDef PackageData facet (ActiveBuildTarget config.resultType) :=
           ⟨by simp [h]⟩
         mkPackageFacetBuild config.build pkg
       else
@@ -168,9 +168,9 @@ the initial set of Lake package facets (e.g., `extraDep`).
   | .customTarget pkg target =>
     if let some config := pkg.findTargetConfig? target then
       if h : target = config.name then
-        have h' : DynamicType CustomData target (ActiveBuildTarget config.resultType) :=
+        have h' : FamilyDef CustomData target (ActiveBuildTarget config.resultType) :=
           ⟨by simp [h]⟩
-        liftM <| cast (by rw [← h'.eq_dynamic_type]) <| config.target.activate
+        liftM <| cast (by rw [← h'.family_key_eq_type]) <| config.target.activate
       else
         error "target's name in the configuration does not match the name it was registered with"
     else
@@ -200,23 +200,23 @@ Recursively build the given info using the Lake build index
 and a topological / suspending scheduler and return the dynamic result.
 -/
 @[inline] def buildIndexTop (info : BuildInfo)
-[DynamicType BuildData info.key α] : CycleT BuildKey m α := do
+[FamilyDef BuildData info.key α] : CycleT BuildKey m α := do
   cast (by simp) <| buildIndexTop' (m := m) info
 
 end
 
 /- Build the given Lake target using the given Lake build store. -/
 @[inline] def BuildInfo.buildIn (store : BuildStore) (self : BuildInfo)
-[DynamicType BuildData self.key α] : BuildM α := do
+[FamilyDef BuildData self.key α] : BuildM α := do
   failOnBuildCycle <| ← EStateT.run' (m := BuildM) store <| buildIndexTop self
 
 /- Build the given Lake target in a fresh build store. -/
-@[inline] def BuildInfo.build (self : BuildInfo) [DynamicType BuildData self.key α] : BuildM α :=
+@[inline] def BuildInfo.build (self : BuildInfo) [FamilyDef BuildData self.key α] : BuildM α :=
   buildIn BuildStore.empty self
 
 export BuildInfo (build buildIn)
 
 /-- An opaque target that builds the Lake target in a fresh build store. -/
 @[inline] def BuildInfo.target (self : BuildInfo)
-[DynamicType BuildData self.key (ActiveBuildTarget α)] : OpaqueTarget :=
+[FamilyDef BuildData self.key (ActiveBuildTarget α)] : OpaqueTarget :=
   BuildTarget.mk' () <| self.build <&> (·.task)
diff --git a/Lake/Build/IndexTargets.lean b/Lake/Build/IndexTargets.lean
index 7096ad04b1..02d30b6af5 100644
--- a/Lake/Build/IndexTargets.lean
+++ b/Lake/Build/IndexTargets.lean
@@ -13,7 +13,7 @@ namespace Lake
 -- # Module Facet Targets
 
 @[inline] def Module.facetTarget (facet : WfName) (self : Module)
-[DynamicType ModuleData facet (ActiveBuildTarget α)] : OpaqueTarget :=
+[FamilyDef ModuleData facet (ActiveBuildTarget α)] : OpaqueTarget :=
   self.facet facet |>.target
 
 @[inline] def Module.oleanTarget (self : Module) : FileTarget :=
@@ -36,7 +36,7 @@ and then build the target `facet` of library's modules recursively, constructing
 a single opaque target for the whole build.
 -/
 def LeanLib.buildModules (self : LeanLib) (facet : WfName)
-[DynamicType ModuleData facet (ActiveBuildTarget α)] : SchedulerM Job := do
+[FamilyDef ModuleData facet (ActiveBuildTarget α)] : SchedulerM Job := do
   let buildMods : BuildM _ := do
     let mods ← self.getModuleArray
     let modTargets ← failOnBuildCycle <| ← EStateT.run' BuildStore.empty
diff --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean
index 2976825bac..7ede07e23d 100644
--- a/Lake/Build/Info.lean
+++ b/Lake/Build/Info.lean
@@ -74,37 +74,37 @@ abbrev BuildInfo.key : (self : BuildInfo) → BuildKey
 
 /-! ### Instances for deducing data types of `BuildInfo` keys -/
 
-instance [DynamicType ModuleData f α]
-: DynamicType BuildData (BuildInfo.key (.moduleFacet m f)) α where
-  eq_dynamic_type := by unfold BuildData; simp
+instance [FamilyDef ModuleData f α]
+: FamilyDef BuildData (BuildInfo.key (.moduleFacet m f)) α where
+  family_key_eq_type := by unfold BuildData; simp
 
-instance [DynamicType PackageData f α]
-: DynamicType BuildData (BuildInfo.key (.packageFacet p f)) α where
-  eq_dynamic_type := by unfold BuildData; simp
+instance [FamilyDef PackageData f α]
+: FamilyDef BuildData (BuildInfo.key (.packageFacet p f)) α where
+  family_key_eq_type := by unfold BuildData; simp
 
-instance [DynamicType CustomData t α]
-: DynamicType BuildData (BuildInfo.key (.customTarget p t)) α where
-  eq_dynamic_type := by unfold BuildData; simp
+instance [FamilyDef CustomData t α]
+: FamilyDef BuildData (BuildInfo.key (.customTarget p t)) α where
+  family_key_eq_type := by unfold BuildData; simp
 
-instance [DynamicType TargetData LeanLib.staticFacet α]
-: DynamicType BuildData (BuildInfo.key (.staticLeanLib l)) α where
-  eq_dynamic_type := by unfold BuildData; simp
+instance [FamilyDef TargetData LeanLib.staticFacet α]
+: FamilyDef BuildData (BuildInfo.key (.staticLeanLib l)) α where
+  family_key_eq_type := by unfold BuildData; simp
 
-instance [DynamicType TargetData LeanLib.sharedFacet α]
-: DynamicType BuildData (BuildInfo.key (.sharedLeanLib l)) α where
-  eq_dynamic_type := by unfold BuildData; simp
+instance [FamilyDef TargetData LeanLib.sharedFacet α]
+: FamilyDef BuildData (BuildInfo.key (.sharedLeanLib l)) α where
+  family_key_eq_type := by unfold BuildData; simp
 
-instance [DynamicType TargetData LeanExe.facet α]
-: DynamicType BuildData (BuildInfo.key (.leanExe x)) α where
-  eq_dynamic_type := by unfold BuildData; simp
+instance [FamilyDef TargetData LeanExe.facet α]
+: FamilyDef BuildData (BuildInfo.key (.leanExe x)) α where
+  family_key_eq_type := by unfold BuildData; simp
 
-instance [DynamicType TargetData ExternLib.staticFacet α]
-: DynamicType BuildData (BuildInfo.key (.staticExternLib l)) α where
-  eq_dynamic_type := by unfold BuildData; simp
+instance [FamilyDef TargetData ExternLib.staticFacet α]
+: FamilyDef BuildData (BuildInfo.key (.staticExternLib l)) α where
+  family_key_eq_type := by unfold BuildData; simp
 
-instance [DynamicType TargetData ExternLib.sharedFacet α]
-: DynamicType BuildData (BuildInfo.key (.sharedExternLib l)) α where
-  eq_dynamic_type := by unfold BuildData; simp
+instance [FamilyDef TargetData ExternLib.sharedFacet α]
+: FamilyDef BuildData (BuildInfo.key (.sharedExternLib l)) α where
+  family_key_eq_type := by unfold BuildData; simp
 
 --------------------------------------------------------------------------------
 /-! ## Recursive Building                                                     -/
@@ -119,7 +119,7 @@ abbrev IndexBuildFn (m : Type → Type v) :=
 abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m
 
 /-- Build the given info using the Lake build index. -/
-@[inline] def BuildInfo.recBuild (self : BuildInfo) [DynamicType BuildData self.key α] : IndexT m α :=
+@[inline] def BuildInfo.recBuild (self : BuildInfo) [FamilyDef BuildData self.key α] : IndexT m α :=
   fun build => cast (by simp) <| build self
 
 export BuildInfo (recBuild)
diff --git a/Lake/Build/Store.lean b/Lake/Build/Store.lean
index ec3eba0492..a16f255dba 100644
--- a/Lake/Build/Store.lean
+++ b/Lake/Build/Store.lean
@@ -32,57 +32,57 @@ set_option linter.unusedVariables false
 
 /-- Derive an array of built module facets from the store. -/
 def collectModuleFacetArray (self : BuildStore)
-(facet : WfName) [DynamicType ModuleData facet α] : Array α := Id.run do
+(facet : WfName) [FamilyDef ModuleData facet α] : Array α := Id.run do
   let mut res : Array α := #[]
   for ⟨k, v⟩ in self do
     match k with
     | .moduleFacet m f =>
       if h : f = facet then
-        have of_data := by unfold BuildData; simp [h, eq_dynamic_type]
+        have of_data := by unfold BuildData; simp [h, family_key_eq_type]
         res := res.push <| cast of_data v
     | _ => pure ()
   return res
 
 /-- Derive a map of module names to built facets from the store. -/
 def collectModuleFacetMap (self : BuildStore)
-(facet : WfName) [DynamicType ModuleData facet α] : NameMap α := Id.run do
+(facet : WfName) [FamilyDef ModuleData facet α] : NameMap α := Id.run do
   let mut res := Lean.mkNameMap α
   for ⟨k, v⟩ in self do
     match k with
     | .moduleFacet m f =>
       if h : f = facet then
-        have of_data := by unfold BuildData; simp [h, eq_dynamic_type]
+        have of_data := by unfold BuildData; simp [h, family_key_eq_type]
         res := res.insert m <| cast of_data v
     | _ => pure ()
   return res
 
 /-- Derive an array of built package facets from the store. -/
 def collectPackageFacetArray (self : BuildStore)
-(facet : WfName) [DynamicType PackageData facet α] : Array α := Id.run do
+(facet : WfName) [FamilyDef PackageData facet α] : Array α := Id.run do
   let mut res : Array α := #[]
   for ⟨k, v⟩ in self do
     match k with
     | .packageFacet _ f =>
       if h : f = facet then
-        have of_data := by unfold BuildData; simp [h, eq_dynamic_type]
+        have of_data := by unfold BuildData; simp [h, family_key_eq_type]
         res := res.push <| cast of_data v
     | _ => pure ()
   return res
 
 /-- Derive an array of built target facets from the store. -/
 def collectTargetFacetArray (self : BuildStore)
-(facet : WfName) [DynamicType TargetData facet α] : Array α := Id.run do
+(facet : WfName) [FamilyDef TargetData facet α] : Array α := Id.run do
   let mut res : Array α := #[]
   for ⟨k, v⟩ in self do
     match k with
     | .targetFacet _ _ f =>
       if h : f = facet then
-        have of_data := by unfold BuildData; simp [h, eq_dynamic_type]
+        have of_data := by unfold BuildData; simp [h, family_key_eq_type]
         res := res.push <| cast of_data v
     | _ => pure ()
   return res
 
 /-- Derive an array of built external shared libraries from the store. -/
 def collectSharedExternLibs (self : BuildStore)
-[DynamicType TargetData &`externLib.shared α] : Array α :=
+[FamilyDef TargetData &`externLib.shared α] : Array α :=
   self.collectTargetFacetArray &`externLib.shared
diff --git a/Lake/Config/ModuleFacetConfig.lean b/Lake/Config/ModuleFacetConfig.lean
index 48c12bf7d4..adb4f310c4 100644
--- a/Lake/Config/ModuleFacetConfig.lean
+++ b/Lake/Config/ModuleFacetConfig.lean
@@ -26,13 +26,13 @@ instance : Inhabited ModuleFacetConfig := ⟨{
   name := Module.leanBinFacet
   resultType := PUnit
   build := default
-  data_eq_target := eq_dynamic_type
+  data_eq_target := family_key_eq_type
 }⟩
 
 hydrate_opaque_type OpaqueModuleFacetConfig ModuleFacetConfig
 
 instance {cfg : ModuleFacetConfig}
-: DynamicType ModuleData cfg.name (ActiveBuildTarget cfg.resultType) :=
+: FamilyDef ModuleData cfg.name (ActiveBuildTarget cfg.resultType) :=
   ⟨cfg.data_eq_target⟩
 
 /-- Try to find a module facet configuration in the package with the given name . -/
diff --git a/Lake/Config/PackageFacetConfig.lean b/Lake/Config/PackageFacetConfig.lean
index 83fc6f954a..56ff4f485b 100644
--- a/Lake/Config/PackageFacetConfig.lean
+++ b/Lake/Config/PackageFacetConfig.lean
@@ -25,13 +25,13 @@ instance : Inhabited PackageFacetConfig := ⟨{
   name := &`extraDep
   resultType := PUnit
   build := default
-  data_eq_target := eq_dynamic_type
+  data_eq_target := family_key_eq_type
 }⟩
 
 hydrate_opaque_type OpaquePackageFacetConfig PackageFacetConfig
 
 instance (cfg : PackageFacetConfig)
-: DynamicType PackageData cfg.name (ActiveBuildTarget cfg.resultType) :=
+: FamilyDef PackageData cfg.name (ActiveBuildTarget cfg.resultType) :=
   ⟨cfg.data_eq_target⟩
 
 /-- Try to find a package configuration in the package with the given name . -/
diff --git a/Lake/Config/TargetConfig.lean b/Lake/Config/TargetConfig.lean
index 3cd0ee39f4..551c06c330 100644
--- a/Lake/Config/TargetConfig.lean
+++ b/Lake/Config/TargetConfig.lean
@@ -25,13 +25,13 @@ instance : Inhabited TargetConfig := ⟨{
   name := &`_nil_
   resultType := PUnit
   target := default
-  data_eq_target := eq_dynamic_type
+  data_eq_target := family_key_eq_type
 }⟩
 
 hydrate_opaque_type OpaqueTargetConfig TargetConfig
 
-instance dynamicTypeOfTargetConfig {cfg : TargetConfig}
-: DynamicType CustomData cfg.name (ActiveBuildTarget cfg.resultType) :=
+instance FamilyDefOfTargetConfig {cfg : TargetConfig}
+: FamilyDef CustomData cfg.name (ActiveBuildTarget cfg.resultType) :=
   ⟨cfg.data_eq_target⟩
 
 /-- Try to find a target configuration in the package with the given name . -/
diff --git a/Lake/Util/DynamicType.lean b/Lake/Util/DynamicType.lean
deleted file mode 100644
index 5e98283fb7..0000000000
--- a/Lake/Util/DynamicType.lean
+++ /dev/null
@@ -1,44 +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
--/
-import Lean.Parser.Command
-
-open Lean
-namespace Lake
-
-class DynamicType {α : Type u} (Δ : α → Type v) (a : α) (β : outParam $ Type v) : Prop where
-  eq_dynamic_type : Δ a = β
-
-export DynamicType (eq_dynamic_type)
-
-attribute [simp] eq_dynamic_type
-
-@[inline] def toDynamic (a : α) [DynamicType Δ a β] (b : β) : Δ a :=
-  cast eq_dynamic_type.symm b
-
-@[inline] def ofDynamic (a : α) [DynamicType Δ a β] (b : Δ a) : β :=
-  cast eq_dynamic_type b
-
-/--
-The syntax:
-
-```lean
-dynamic_data foo : Data 0 := Nat
-```
-
-Declares a new alternative for the dynamic `Data` type via the
-production of an axiom `foo : Data 0 = Nat` and an instance of `DynamicType`
-that uses this axiom for key `0`.
--/
-scoped macro (name := dynamicDataDecl) doc?:optional(Parser.Command.docComment)
-"dynamic_data " id:ident " : " dty:ident key:term " := " ty:term : command => do
-  let tid := extractMacroScopes dty.getId |>.name
-  if let (tid, _) :: _ ← Macro.resolveGlobalName tid then
-    let app := Syntax.mkApp dty #[key]
-    let axm := mkIdentFrom dty <| `_root_ ++ tid ++ id.getId
-    `($[$doc?]? @[simp] axiom $axm : $app = $ty
-    instance : DynamicType $dty $key $ty := ⟨$axm⟩)
-  else
-    Macro.throwErrorAt dty s!"unknown identifier '{tid}'"
diff --git a/Lake/Util/Family.lean b/Lake/Util/Family.lean
new file mode 100644
index 0000000000..8c226d60c8
--- /dev/null
+++ b/Lake/Util/Family.lean
@@ -0,0 +1,170 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lean.Parser.Command
+
+/-!
+# Open Type Families in Lean
+
+This module contains utilities for defining **open type families** in Lean.
+
+The concept of type families originated in Haskell with the paper
+(*Type checking with open type functions*](https://doi.org/10.1145/1411204.1411215)
+by Schrijvers *et al.* and is essentially just a fancy name for a function from
+an input *index* to an output type. However, it tends to imply some additional
+restrictions on syntax or functionality as opposed to a proper type function.
+The design here has some such limitations so the name was similarly adopted.
+
+Type families come in two forms: open and closed.
+A *closed* type family is an ordinary total function.
+An *open* type family, on the other hand, is a partial function that allows
+additional input to output mappings to be defined as needed.
+
+Lean does not (currently) directly support open type families.
+However, it does support type class *functional dependencies* (via `outParam`),
+and simple open type families can be modeled through functional dependencies,
+which is what we do here.
+
+## Defining Families
+
+In this approach, to define an open type family, one first defines an `opaque`
+type function with a single argument that serves as the key:
+
+```lean
+opaque FooFam (key : WfName) : Type
+```
+
+Note that, unlike Haskell, the key need not be a type. Lean's dependent type
+theory does not have Haskell's strict separation of types and data and thus
+we can use data as an index as well.
+
+Then, to add a mapping to this family, one defines an axioms:
+
+```lean
+axiom FooFam.bar : FooFam &`bar = Nat
+```
+
+To finish, one also defines an instance of the `FamilyDef` type class
+defined in this module using the axiom like so:
+
+```lean
+instance : FamilyDef FooFam &`bar Nat := ⟨FooFam.bar⟩
+```
+
+This module provides a `family_def` macro to define both the axiom and the
+instance in one go like so:
+
+```lean
+family_def bar : FooFam &`bar := Nat
+```
+
+## Type Inference
+
+The signature of the type class `FamilyDef` is
+
+```
+FamilyDef {α : Type u} (Fam : α → Type v) (a : α) (β : outParam $ Type v) : Prop
+```
+
+The key part being that `β` is an `outParam` so Lean's type class synthesis will
+smartly infer the defined type `Nat` when given the key of ``&`bar``. Thus, if
+we have a function define like so:
+
+```
+def foo (key : α) [FamilyDef FooFam key β] : β := ...
+```
+
+Lean will smartly infer that the type of ``foo &`bar`` is `Nat`.
+
+However, filling in the right hand side of `foo` is not quite so easy.
+``FooFam &`bar = Nat`` is only true propositionally, so we have to manually
+`cast` a `Nat` to ``FooFam &`bar``and provide the proof (and the same is true
+vice versa). Thus, this module provides two definitions, `toFamily : β → Fam a`
+and `ofFamily : Fam a → β`, to help with this conversion.
+
+## Full Example
+
+Putting this all together, one can do something like the following:
+
+```lean
+opaque FooFam (key : WfName) : Type
+
+abbrev FooMap := DRBMap WfName FooFam WfName.quickCmp
+def FooMap.insert (self : FooMap) (key : WfName) [FamilyDef FooFam key α] (a : α) : FooMap :=
+  DRBMap.insert self key (toFamily a)
+def FooMap.find? (self : FooMap) (key : WfName) [FamilyDef FooFam key α] : Option α :=
+  ofFamily <$> DRBMap.find? self key
+
+family_def bar : FooFam &`bar := Nat
+family_def baz : FooFam &`baz := String
+def foo := Id.run do
+  let mut map : FooMap := {}
+  map := map.insert &`bar 5
+  map := map.insert &`baz "str"
+  return map.find? &`bar
+
+#eval foo -- 5
+```
+
+## Type Safety
+
+In order to maintain type safety, `a = b → Fam a = Fam b` must actually hold.
+That is, one must not define mapping to two different types with equivalent
+keys. Since mappings are defined through axioms, Lean WILL NOT catch violations
+of this rule itself, so extra care must be taken when defining mappings.
+
+In Lake, this is solved by having its open type families be indexed by a
+`WfName` and defining each mapping using a name literal `name` and the
+declaration ``axiom Fam.name : Fam &`name = α`` thus causing a name clash
+if two keys overlap and thereby producing an error.
+-/
+
+open Lean
+namespace Lake
+
+/-! ## API Documentation -/
+
+/--
+Defines a single mapping of the **open type family** `Fam`, namely `Fam a = β`.
+See the module documentation of `Lake.Util.Family` for details what an open type
+family is in Lake.
+-/
+class FamilyDef {α : Type u} (Fam : α → Type v) (a : α) (β : outParam $ Type v) : Prop where
+  family_key_eq_type : Fam a = β
+
+export FamilyDef (family_key_eq_type)
+
+-- Simplifies proofs involving open type families.
+attribute [simp] family_key_eq_type
+
+/-- Cast a datum from its individual type to its general family. -/
+@[macroInline] def toFamily [FamilyDef Fam a β] (b : β) : Fam a :=
+  cast family_key_eq_type.symm b
+
+/-- Cast a datum from its general family to its individual type. -/
+@[macroInline] def ofFamily [FamilyDef Fam a β] (b : Fam a) : β :=
+  cast family_key_eq_type b
+
+/--
+The syntax:
+
+```lean
+family_def foo : Fam 0 := Nat
+```
+
+Declares a new mapping for the open type family `Fam` type via the
+production of an axiom `Fam.foo : Data 0 = Nat` and an instance of `FamilyDef`
+that uses this axiom for key `0`.
+-/
+scoped macro (name := familyDef) doc?:optional(Parser.Command.docComment)
+"family_def " id:ident " : " fam:ident key:term " := " ty:term : command => do
+  let tid := extractMacroScopes fam.getId |>.name
+  if let (tid, _) :: _ ← Macro.resolveGlobalName tid then
+    let app := Syntax.mkApp fam #[key]
+    let axm := mkIdentFrom fam <| `_root_ ++ tid ++ id.getId
+    `($[$doc?]? @[simp] axiom $axm : $app = $ty
+    instance : FamilyDef $fam $key $ty := ⟨$axm⟩)
+  else
+    Macro.throwErrorAt fam s!"unknown family '{tid}'"
diff --git a/Lake/Util/StoreInsts.lean b/Lake/Util/StoreInsts.lean
index 4774dfa516..84b901747e 100644
--- a/Lake/Util/StoreInsts.lean
+++ b/Lake/Util/StoreInsts.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Util.DRBMap
-import Lake.Util.DynamicType
+import Lake.Util.Family
 import Lake.Util.Store
 
 open Std
@@ -18,6 +18,6 @@ instance [Monad m] : MonadStore κ α (StateT (RBMap κ α cmp) m) where
   fetch? k := return (← get).find? k
   store k a := modify (·.insert k a)
 
-@[inline] instance [MonadDStore κ β m] [t : DynamicType β k α] : MonadStore1 k α m where
-  fetch? := cast (by rw [t.eq_dynamic_type]) <| fetch? (m := m) k
-  store a := store k <| cast t.eq_dynamic_type.symm a
+@[inline] instance [MonadDStore κ β m] [t : FamilyDef β k α] : MonadStore1 k α m where
+  fetch? := cast (by rw [t.family_key_eq_type]) <| fetch? (m := m) k
+  store a := store k <| cast t.family_key_eq_type.symm a