Faked overloaded strings

fakechar.idr

data FakeChar = A | B | C
  
data ValidMyString : List Char -> Type where
     VA : ValidMyString xs -> ValidMyString ('a' :: xs)
     VB : ValidMyString xs -> ValidMyString ('b' :: xs)
     VC : ValidMyString xs -> ValidMyString ('c' :: xs)
     VNil : ValidMyString []
  
implicit fromString : (x : String) -> {auto p : ValidMyString (unpack x)}
                      -> List FakeChar
fromString x {p} = fromListChar p
    where
      fromListChar : ValidMyString xs -> List FakeChar
      fromListChar (VA x) = A :: fromListChar x
      fromListChar (VB x) = B :: fromListChar x
      fromListChar (VC x) = C :: fromListChar x
      fromListChar VNil = []
  
foo : List FakeChar
foo = "abcab"