This is something I do not like. The algorithms of the type system should be understandable, written in a page that you could perform yourself on paper. They should be meaningful for the user.
They shouldn't be opaque.
It is an interesting experiment for someone that is not a logician.
@apostolis Welcome to the wonderful world of epistemic opacity!
@khinsen Apart from not being a logician, the error messages do not explain the algorithms.
Also, Agda is a research project, meaning that new theories are always introduced. This is good and bad. A lot of errors can be found later.
This has led many to limit themselves to a well understood part of theory, check for example @MartinEscardo typetopology .
In the same vein, I use univalent mathematics, math in general, well understood concepts, instead of Agda 's features.
@apostolis Limiting oneself to a well understood subset is a wise move. Tools like Agda should support it.
The fundamental issue I see, and which I address in the preprint, is that we don't make enough effort in digital science to separate mature from experimental methods. There is a place for both of course.
Most features can be disabled, and there is also the `--safe` flag.
I agree, it would be better if we could control more precisely the type theory we want to work with by suitable flags, but there are already many flags that can be used.
See e.g. the flags we use in TypeTopology:
https://github.com/martinescardo/TypeTopology/blob/master/typetopology.agda-lib