Agda のモジュール読み込みのエラー

Agda 2.5.2 で import my-module-file as M のようにしてファイルを開こうとすると、

Module cannot be imported since it has open interaction points
when scope checking the declaration
  import my-module-file as M

というエラーが出ますが、これは元ファイル (my-module-file.agda) に示すべき Goal が残っているのが原因のようです。 Hole を埋めてあげて、*All Done* の状態にしてあげればモジュールとして読み込めました。