Mimicking Haskell canonicity (one-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 p p where I'd prefer ...| refl or a full rewrite into normal form instead.

Any help is appreciated!

Solution

With newer versions of Agda you could use the Prop universe to get definitional uniqueness of a type:

{-# OPTIONS --prop #-}
module UniquenessUsingProp where
open import Data.Nat.Base
open import Relation.Binary.PropositionalEquality

-- Convert a Set to a Prop. This could be avoided if e.g.
-- we defined > as a Prop (like in the example in the docs
-- linked above)
data Squash {ℓ} (A : Set ℓ) : Prop ℓ where
  squash : A → Squash A

-- record Yo (n : ℕ) : Prop where -- Both variants works
record Yo (n : ℕ) : Set where
  field
    sem : Squash (n + 1 > n * 2)

-- Since `Yo n` is a Prop and not a set, it can't be the
-- direct argument of ≡. This is not a problem since 
-- it's definitionally equal anyways.
UniqueYo : ∀ {n} (P : Yo n → Set) (p q : Yo n) → P p ≡ P q
UniqueYo P p q = refl

Another alternative that produces similar results is using proof irrelevant record fields:

module UniqunessUsingProofIrrelevance where
open import Data.Nat.Base
open import Relation.Binary.PropositionalEquality

record Yo (n : ℕ) : Set where
  field
    .sem : n + 1 > n * 2

open Yo {{...}}

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

In both cases, actually using the value in Yo can be difficult, since you need to convince Agda that your code does not depend on the concrete value in sem, e.g. by only using absurd pattern matches on it or by producing values in Prop or respectively, providing it as an argument to irrelevant functions.