Main.idr

module Main

main : IO ()
main = putStrLn "Hello World!"

test.erl

% Generated by the Idris -> Erlang Compiler.
% Here be dragons.

-module(test).

-compile(export_all).
-compile(nowarn_unused_function).
-compile(nowarn_shadow_vars).

'Main_main'() -> {'U_Prelude_putStr1', "Hello World!\n"}.
'mkForeignPrim'() -> 'nothing'.
'mkLazyForeignPrim'() -> 'nothing'.
'Prelude_putStr'(E0, W0) -> io:put_chars(E0).
'run__IO'(E0) -> 'APPLY0'(E0, 'TheWorld').
'unsafePerformPrimIO'() -> 'nothing'.
'APPLY0'(Fn0, Arg0) -> case Fn0 of
{'U_Prelude_putStr1', P_c0} -> 'Prelude_putStr'(P_c0, Arg0);
_Default -> 'nothing'
end.
'EVAL0'(Arg0) -> case Arg0 of
_Default -> Arg0
end.
'runMain0'() -> 'EVAL0'('APPLY0'('Main_main'(), 'TheWorld')).
'Decidable_Equality_@Decidable_Equality_DecEq$Char:!decEq:0:primitiveNotEq:0'() -> 'nothing'.
'Decidable_Equality_@Decidable_Equality_DecEq$Float:!decEq:0:primitiveNotEq:0'() -> 'nothing'.
'Decidable_Equality_@Decidable_Equality_DecEq$Int:!decEq:0:primitiveNotEq:0'() -> 'nothing'.
'Decidable_Equality_@Decidable_Equality_DecEq$Integer:!decEq:0:primitiveNotEq:0'() -> 'nothing'.
'Decidable_Equality_@Decidable_Equality_DecEq$String:!decEq:0:primitiveNotEq:0'() -> 'nothing'.
'Void_case'() -> 'nothing'.
'Void_elim'() -> 'nothing'.

Load test.erl up in an erlang shell:

$ erl
...
1> c(test).
... Warnings
{ok,test}
2> test:runMain0().
Hello World!
ok
3>

To escape the erlang shell, Ctrl-G, then q then enter.

That's actually pretty small, considering. Well done!