Union type in Idris

Union.idr

module Data.Union

import Data.Vect

data Sum : {n: Nat} -> Vect n Type -> Type where
  isA: t -> {auto e: Elem t ts} -> Sum ts

data Orange = AnOrange String
data Apple = AnApple String

fruit : Type
fruit = Sum [Orange, Apple]

-- Usage:
-- the fruit isA $ AnOrange "foo"
-- the fruit isA $ AnApple "bar"