if-then-else which can return different types in the two branches

bla.hs

module Bla where

-- declare constants to minimise example
-- just assume Set == Type
postulate
  -- there is a type called String
  String : Set
  -- it has a value called 'hey' in it
  hey : String
  -- there is a type called Int
  Int : Set
  -- it has a value called 'one' in it
  one : Int


-- declare booleans
data Bool : Set where
  ff tt : Bool

-- calculate which type of the given two we should return based on a boolean
-- actually we can use the traditional if-then-else instead
-- but we need to generalise it a bit, so I omitted doing so
If : Bool -> Set -> Set -> Set
If ff A B = B
If tt A B = A

if_then_else_ :
  -- for any two types 'A' and 'B'
  {A B : Set}
  -- and a boolean value 'b'
  (b : Bool) ->
  -- given values of those types
  A -> B ->
  -- return the value of the correct type
  If b A B
if ff then t else e = e
if tt then t else e = t

-- example usage
-- > if ff then hey else one
-- one
-- > if tt then hey else one
-- hey