-- I haven't been able to actually run the program (broken archlinux packages), but it typechecks

open import Data.String
open import Function
open import IO.Primitive

Either : Set → Set → Set₁
Either l r = {a : Set} → (l → a) → (r → a) → a 

Left  : { l r : Set } → l → Either l r
Left  val l _ = l val

Right : { l r : Set } → r → Either l r
Right val _ r = r val

main = putStrLn (toCostring (Right {String} "lol" (const "") id))