-- "basic" or "regular" sum type
type Nat
    O
    S (n:Nat)

-- structural subtype of a sum type
type EvenNat (< Nat)
    O
    S (S (n:EvenNat))

type Positive (< Nat)
    S O
    S (p:Positive)

-- another basic type
type Reward
    Nothing
    Coins(num:Positive)
    Item(id:String)

-- supertype of a sum type
-- by adding more constructor
type LootReward (> Reward)
    Exp(amount:Positive)

-- subtype of a sum type (adding extra field to each constructor)
type RewardWithPostcard (< Reward)
    + message:String

    -- Nothing(message:String)
    -- Coins(num:Positive, message:String)
    -- Item(id:String, message:String)

-- propositional subtyping
 Subtype A B ==
    exists coerce : A -> B,
        downcast : B -> maybe A,
        forall a:A, downcast (coerce a) = Some a
    -- there is one caveat with propositional subtyping
    -- it is not necessarily transitive, i.e. for A, B, C, if there are coercions A->B, B->C and A->C,
    -- it could be "coerce_B_C (coerce_A_B a) <> coerce_A_C a"