module Main

nat2type : Bool -> Type
nat2type False = Integer
nat2type True = List Integer

hello : (f: Bool) -> nat2type f
hello False = 10
hello True = [10, 20]

-- How do I implement 'printany' ??
-- It currently fails at typecheck
--
-- When checking an application of function Prelude.Monad.>>=:
--        Can't find implementation for Show (nat2type f)
--
-- Moreover, how do I consume an induced type?
printany : Show a => a -> IO ()
printany a = print a

main : IO ()
main = do
    putStrLn "Hello World"
    v <- getLine
    let f = if v == "True" then True else False
    let result = hello f
    printany result