{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreia7byvp4la2mn746luqpnsur2lckhrntziadkhgjb7gq4xwuf4kku",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mijstfxpzg72"
  },
  "path": "/t/type-equality-in-gadt-typefamily-context/13876#post_4",
  "publishedAt": "2026-04-02T16:46:45.000Z",
  "site": "https://discourse.haskell.org",
  "textContent": "In Agda you would write it like this (I’ve used `Char` instead of `String` because that felt simpler while still presenting the same problems):\n\n\n    open import Data.Char\n    open import Data.List\n    open import Relation.Nullary.Decidable\n    open import Relation.Binary.PropositionalEquality\n\n    data N : List Char → Set where\n      [] : N []\n      _∷_ : ∀{xs} → (x : Char) → N xs → N (x ∷ xs)\n\n    popHelper : {x c : Char} → Dec (x ≡ c) → List Char → List Char → List Char\n    popHelper (yes refl) _ n = n\n    popHelper (no _) l _ = l\n\n    pop : (n : List Char) (c : Char) → List Char\n    pop [] _ = []\n    pop l@(x ∷ n) c = popHelper (x ≟ c) l n\n\n    popNHelper : ∀ {xs} {x} {c} (w : Dec (x ≡ c)) → N (x ∷ xs) → N xs → N (popHelper w (x ∷ xs) xs)\n    popNHelper (yes refl) l n = n\n    popNHelper (no _) l n = l\n\n    popN : ∀{n} → N n → (c : Char) → N (pop n c)\n    popN [] _ = []\n    popN l@(x ∷ n) c = popNHelper (x ≟ c) l n\n\n\nThey also use this `Dec` type instead of `Maybe` which includes an explicit proof of refutation:\n\n\n    data Dec (a : Set) : Set where\n      yes : a → Dec a\n      no : (a → ⊥) → Dec a\n\n\nBut I don’t think that’s very relevant here. I think a more important problem is the nonlinear matching that type families allow you to do. This is not allowed in Agda and in my opinion questionable in general.",
  "title": "Type equality in GADT/TypeFamily context"
}