Something.v

Module Type OpaqueSomething.
    Parameter T : Type.
    Parameter t : T.
End OpaqueSomething.

Module OpaqueNat : OpaqueSomething with Definition T := nat.
    Definition T := nat.
    Definition t := 0.
End OpaqueNat.

Class Something (T : Type) := {
    something : T
}.

Instance NatSomething : Something nat := {
    something := OpaqueNat.t
}.

(* We can not show that [something] of type nat is equal to 0.
Lemma undefined_nat_is_zero: 0 = (something : nat).
Proof.
    apply eq_refl.
    (* Fails with:
        > apply eq_refl.
        >       ^^^^^^^
        Error: Unable to unify "something" with "0".
    *)
*)

Module OpaqueBool : OpaqueSomething with Definition T := bool.
    Definition T := bool.
    Definition t := false.
End OpaqueBool.

Instance BoolSomething : Something bool := {
    something := OpaqueBool.t
}.

Definition constOrId b :=
    match b with
    | true => true
    | false => something
    end.

Definition funeq {A}{B} (f g : A -> B) : Prop :=
    forall a, f a = g a.

Lemma l : funeq constOrId (fun x => x) \/ funeq constOrId (fun _ => true).
    unfold constOrId, funeq.
    case (something : bool); [right | left]; intros []; auto.
Qed.

Definition fromSome {T : Type} {_ : Something T} (o : option T) : T :=
    match o with
    | Some x => x
    | None => something
    end.