module PrivateBug where

open import Relation.Binary.PropositionalEquality
open import Data.Nat

record R : Set where
  private
    field
      i : ℕ

r : R
r = record { i = 42 }

j : ℕ
j = {!R.i r!} -- R.i r doesn't work here, as expected

-- but, with a little effort, we can get i out of r despite its privacy:
get-i : R → ℕ
get-i r = F r refl
  where
    F : {n : ℕ}(r : R) → (r ≡ record { i = n }) → ℕ
    F {n} .(record { i = n }) refl = n

k : ℕ
k = get-i r

k-is-42 : k ≡ 42
k-is-42 = refl