instance only) of typeclasses in Agda

Agda's mixiture of records and the instance keyword give us behaviour similar to that of Haskell's typeclasses. Moreover, ignoring the instance keyword, we can have more than one instance for the same type --- something we cannot do in Haskell.

I am at a point where I need Haskell's one-instance only requirement, but in Agda. Is there an compiler option or some trick/heuristic to enforce this?

Right now the approach I am taking is,

record Yo (n : ℕ) : Set where
  field
    sem : (some interesting property involving n)

open Yo {{...}}

postulate UniqueYo: ∀ {n} (p q : Yo n) → p ≡ q

However, whenever I actually use UniqueYo the lack of computation leaves my goals littered with things like ...| UniqueYo pp ...| UniqueYo pp where I'd prefer ...| refl ...| refl or a full rewrite into normal form instead.

Any help is appreciated!

链接地址: http://www.djcxy.com/p/33172.html

上一篇: 为什么GHC在这里发出错误的“冗余约束”警告？

下一篇: Agda中的类型类的实例）