Extract data from Maybe/Either with a proof

ResolveMaybe.agda

module ResolveMaybe where

data Maybe (A : Set) : Set where
  none : Maybe A
  some : A → Maybe A

data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where
  refl : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

resolveMaybe : {A : Set} {x : A} {m : Maybe A} → (m ≡ (some x)) → A
resolveMaybe {x = x} refl = x

data MaybeConstructor : Set where
  none some : MaybeConstructor

getConstructor : ∀ {A} → Maybe A → MaybeConstructor
getConstructor none = none
getConstructor (some x) = some

resolveMaybe' : ∀ {A} {x : A} {m : Maybe A} → (getConstructor m ≡ some) → A
resolveMaybe' {m = none} ()
resolveMaybe' {m = some x} refl = x


data Either (A B : Set) : Set where
  left : A → Either A B
  right : B → Either A B

resolveEither : {A B : Set} {x : B} {e : Either A B} → (e ≡ right x) → B
resolveEither {x = x} refl = x



data Single : Set where
  single : Single

myMaybe : Maybe Single
myMaybe = some single

propMyMaybe : myMaybe ≡ some single
propMyMaybe = refl

myMaybeResult : Single
myMaybeResult = resolveMaybe propMyMaybe


data Other : Set where
  other : Other

myEither : Either Other Single
myEither = right single

propMyEither : myEither ≡ right single
propMyEither = refl

myEitherResult : Single
myEitherResult = resolveEither propMyEither