Colors.cr

struct Red    end 
struct Yellow end
struct Green  end
alias Color = Red | Yellow | Green

def take_red_green(xs : Array(Color)) : Array(Red | Green)
  xs.select(Red | Green)
end

def expand_type(x : U, t : T.class) : U | T forall U, T
  x.as U | T
end

all_colors : Array(Color) 
all_colors = [ Red.new, Yellow.new, Green.new ]

red_or_green : Array(Red | Green) 
red_or_green = take_red_green all_colors

restored : Array(Red | Green | Yellow) 
restored = red_or_green.map { |x| expand_type x, Yellow } << Yellow.new

Colors.idr

-- Equivalent(ish) Idris Code
module Colors
import Data.List.Elem

data Color' 
    = Red' 
    | Yellow' 
    | Green' 

Show Color' where
    show Red'    = "Red'"
    show Yellow' = "Yellow'"
    show Green'  = "Green'"

data Color : {allowed : List Color'} -> Type where
    Red    : {allowed : _} -> {color : _}
                -> {auto prf1 : color = Red'}
                -> {auto prf2 : Elem color allowed} 
                -> Color {allowed}

    Yellow : {allowed : _} -> {color : _}
                -> {auto prf1 : color = Yellow'}
                -> {auto prf : Elem color allowed} 
                -> Color {allowed}

    Green  : {allowed : _} -> {color : _}
                -> {auto prf1 : color = Green'}
                -> {auto prf2 : Elem color allowed} 
                -> Color {allowed}

Show Color where
    show Red    = "Red"
    show Yellow = "Yellow"
    show Green  = "Green"

takeRedGreen : List (Color {allowed}) -> List (Color {allowed=[Red', Green']})
takeRedGreen [] = []
takeRedGreen (x :: xs) = case x of 
                              Red   => Red   {color=Red'}   :: takeRedGreen xs
                              Green => Green {color=Green'} :: takeRedGreen xs
                              _     => takeRedGreen xs

allColors : List (Color {allowed = [Red', Yellow', Green']})
allColors = [Red, Yellow, Green]

redOrGreen : List (Color {allowed = [Red', Green']})
redOrGreen = takeRedGreen allColors