Integerにしてもコンパイルすると32bitまたは64bit値として扱われるとかそういうのならおｋ
むしろIntegerどころか0とSuccが定義されてるなんらかのクラスのインスタンスならなんでもおｋみたいなぐらい一般化してくｒくｒ
どうせ最終的にAgdaとHaskellはシンクロする運命なんだし