Idris 如何避免将点图案用于无法访问的图案？

Question

在 Agda 中，必须使用点模式来告诉编译器不能检查函数定义的哪些部分，特别是哪些变量可以用于模式匹配，哪些不能（在新版本中，点模式似乎只是可选的，可以使用新变量代替）。

Idris 显然不使用任何此类机制，那么 idris 编译器如何猜测哪些模式可以访问，哪些模式不在函数定义中？它如何获得哪个模式匹配的参数？

提前致谢。