程式語言與理論- Agda 的 instance resolution

最近這裡好像比較熱鬧，希望有大大能看到我的問題 orz

廢話有點多，如果想直接看問題的話請直接拉到最下面


假設有一個 Id : String → Set，用來表示 Minecraft 中的各種不同物品

data Id : String → Set where
　id : (rawId : String) → Id rawId


對於一種物品我們須要知道的事只有三個，名字、物品欄中的可堆疊數量、是否能在創造模式物品欄中直接獲得

record Item {rawId : String} (_ : Id rawId) : Set where
　field
　　displayName : Id rawId → String
　　stacks : Id rawId → Fin 65
　　obtainable : Bool


開始新增物品種類到 Minecraft 世界中

instance

用 'minecraft:stone' 建立的 Id 當作石頭的 ID，石頭可以堆疊 64 個，可從創造模式物品欄直接活獲得

　Stone : Item (id 'minecraft:stone')
　Stone =
　　record {
　　　displayName = 'Stone';
　　　stacks = # 64;
　　　obtainable = true
　　}

盔甲座 ID 是 'minecraft:armor_stand'，可堆疊 16 個，可以從創造模式物品欄直接獲得

　ArmorStand : Item (Id 'minecraft:armor_stand')
　ArmorStand =
　　record {
　　　displayName = 'Armor Stand';
　　　stacks = # 16;
　　　obtainable = true
　　}



-- Normal form 是 'Stone'
stoneDisplayName : String
stoneDisplayName = displayName (Id 'minecraft:stone')

-- Normal form 是 'Armor Stand'
armorStandDisplayName : String
armorStandDisplayName = displayName (Id 'minecraft:armor_stand')










以上程式都還沒有問題，我想問的是下面這個

itemDisplayName : String → String
itemDisplayName rawId = displayName (Id rawId)

會報錯，因為不是所有 rawId 都有一個 Item 的 instance

我想問的是，在 Agda 裡要怎麼保證所有用來呼叫 itemDisplayName 的 String 都有一個 Item 的 instance？
(is it even possible? what should I be searching for?)

例如有什麼辦法可以弄到一個 proof 之類的，然後編譯器就不會報錯了嗎？

謝謝！

（目前想到的方法就只有枚舉所有 instance 來 pattern matching，但顯然在 instance
數量很多的情況下不是什麼好方法）

--