Return the value from the right component. The behavior is undefined
if passed a left value, i.e., it can return any value.
>>> fromRight (sRight (literal 'a') :: SEither Integer Char)
'a' :: SChar
>>> prove $ \x -> fromRight (sRight x :: SEither Char Integer) .== (x :: SInteger)
Q.E.D.
>>> sat $ \x -> x .== (fromRight (sLeft (literal 2) :: SEither Integer Char))
Satisfiable. Model:
s0 = 'A' :: Char
Note how we get a satisfying assignment in the last case: The behavior
is unspecified, thus the SMT solver picks whatever satisfies the
constraints, if there is one.