fix generic new_ids

2 files changed, 17 insertions, 3 deletions

diff --git a/lib/Wayland/Display.lean b/lib/Wayland/Display.lean
index 9ba60bc..70f5c67 100644
--- a/lib/Wayland/Display.lean
+++ b/lib/Wayland/Display.lean
@@ -101,7 +101,7 @@ class Interface (ι : InterfaceName) where
   version : UInt32
 
 /-- Interface where all dependency interfaces can be resolvew. -/
-class ResolvedInterface (ι : InterfaceName) where
+class ResolvedInterface (ι : InterfaceName) extends Interface ι where
   referencedInterfaces : Array ((ι' : InterfaceName) × Interface ι')
   contains_self : ∃ α, ⟨ι, α⟩ ∈ referencedInterfaces := by exists inferInstance; simp
   -- TODO: Verify that dependencies of interfaces are in referencedInterfaces
@@ -367,8 +367,7 @@ private def DisplayM.ensureInterface (ι : InterfaceName) [iface : ResolvedInter
           events := iface'.events.map MessageDesc.toNative }
         (setComplete := if ι' == ι then 1 else 0)
 
-/-- Get the `wl_display` instance within the display monad. -/
-def DisplayM.getDisplay : DisplayM σ (Object "wl_display") := do
+def DisplayM.getDisplay' : DisplayM σ (Object "wl_display") := do
   let proxy ← Native.Proxy.fromDisplay (← read).disp
   return ⟨proxy⟩
 
diff --git a/lib/Wayland/Helpers.lean b/lib/Wayland/Helpers.lean
new file mode 100644
index 0000000..7230fc2
--- /dev/null
+++ b/lib/Wayland/Helpers.lean
@@ -0,0 +1,15 @@
+import Wayland.Display
+import Wayland.Protocols
+
+-- Helpers that depend on the protocols and can thus not be included in `Display.lean`.
+
+namespace Wayland
+
+open Protocols
+
+variable {σ : Type}
+
+/-- Get the `wl_display` instance within the display monad. -/
+def DisplayM.getDisplay : DisplayM σ WlDisplay := getDisplay'
+
+end Wayland