Show that we can resolve triple instances in ECS

lean/Examples/ECS.lean

@@ -10,6 +10,9 @@ structure Position where
 structure Velocity where
   velocity : Vector2
 
+structure Magic where
+  magic : Nat
+
 axiom StoragePosition : StorageFam Position = MapStorage Position
 instance : FamilyDef StorageFam Position (MapStorage Position) := ⟨StoragePosition⟩
 
@@ -22,9 +25,16 @@ instance : FamilyDef StorageFam Velocity (MapStorage Velocity) := ⟨StorageVelo
 instance : @Component Velocity (MapStorage Velocity) Velocity _ _ where
   constraint := rfl
 
+axiom StorageMagic : StorageFam Magic = MapStorage Magic
+instance : FamilyDef StorageFam Magic (MapStorage Magic) := ⟨StorageMagic⟩
+
+instance : @Component Magic (MapStorage Magic) Magic _ _ where
+  constraint := rfl
+
 structure World where
   positionStore : MapStorage Position
   velocityStore : MapStorage Velocity
+  magicStore : MapStorage Magic
   entityStore : GlobalStorage EntityCounter
 
 instance : @Has World Position (MapStorage Position) _ where
@@ -33,28 +43,34 @@ instance : @Has World Position (MapStorage Position) _ where
 instance : @Has World Velocity (MapStorage Velocity) _ where
   getStore := (·.velocityStore) <$> read
 
+instance : @Has World Magic (MapStorage Magic) _ where
+  getStore := (·.magicStore) <$> read
+
 instance : @Has World EntityCounter (GlobalStorage EntityCounter) _ where
   getStore := (·.entityStore) <$> read
 
 def initWorld : IO World := do
   let positionStore : MapStorage Position ← ExplInit.explInit
   let velocityStore : MapStorage Velocity ← ExplInit.explInit
+  let magicStore : MapStorage Magic ← ExplInit.explInit
   let entityStore : GlobalStorage EntityCounter ← ExplInit.explInit
-  pure {positionStore,velocityStore,entityStore}
+  pure {positionStore,velocityStore,magicStore,entityStore}
 
 def update (pv : Position × Velocity) : Position :=
   let (p, v) := pv
   {position := p.position.add v.velocity}
 
 def dumpState : System World Unit := do
   IO.println "DUMP STATE"
-  cmapM_ (fun ((p, v) : Position × Velocity) =>
-    IO.println s!"position : ({p.position.x}, {p.position.y}) velocity : ({v.velocity.x}, {v.velocity.y})")
+  let globalPosition : Position ← get global
+  cmapM_ (fun ((p, v, m) : Position × Velocity × Magic) =>
+    IO.println s!"global pos: {globalPosition.position.x} position : ({p.position.x}, {p.position.y}) velocity : ({v.velocity.x}, {v.velocity.y}) magic : {m.magic}")
 
 def game : System World Unit := do
   newEntityAs_ (Position × Velocity) (⟨0,0⟩, ⟨10,11⟩)
   newEntityAs_ (Position × Velocity) (⟨1,0⟩, ⟨-5,-2⟩)
-  set' global {position := ⟨0,0⟩ : Position}
+  newEntityAs_ (Position × Velocity × Magic) (⟨1,0⟩, ⟨-5,-2⟩, ⟨1⟩)
+  set' global {position := ⟨999,0⟩ : Position}
   dumpState
   cmap update
   dumpState