Either magic

data AB = A|B

data D : (ab:AB)->Type where 
     MkD : String -> D ab
  
dA: D A
dA = MkD "A"

dB: D B 
dB = MkD "B"

dA2Int: D A -> Int
dA2Int (MkD s) = 2

dB2String: D B ->String
dB2String (MkD s) = "bla"

main : IO ()
main =do
   l <- getLine 
   
   let m_ab : Maybe (Either (D A) (D B)) = case l of
      "A" => Just (Left dA) 
      "B" => Just (Right dB)
      _  => Nothing
   
   putStrLn $ case m_ab of 
     Just ab => case ab of 
       Left  da => show $ dA2Int da 
       Right db => dB2String db 
     Nothing => "Nothing"