Agda のドキュメントには、Data.AVLモジュールの使用方法の例がいくつか示されています。
http://darcsden.com/abel/AgdaPrelude/browse/README/AVL.agda
例では、モジュールは、ツリーに格納されている値のタイプとキー タイプの順序を指定する引数を使用して、インポート時に 1 回インスタンス化されます。
同じクライアント モジュールで異なる値の型 (文字列のツリーと数値のツリーの両方) で AVL ツリーを使用するにはどうすればよいですか?