Dependencies of Reflection.AST.Argument.Information

[MatthewDaggitt]

Type-checking the above module seems to drag in a huge amount of unnecessary stuff. It must be possible to simplify the dependencies. Also check other Reflection.AST modules!

[jamesmckinna]

The above PR is a fix to this specific issue regarding imports. A more serious effort would refactor much of this code, consisting as it does in each module of how to write a decidable equality on a non-dependent product, given decidable equality on the underlying types, and then prove injectivity of such equality, given injectivity on the underlying types etc cf #698, #799, #803. There might then be knock-on consequences regarding what should then be im/ex/ported?

[jamesmckinna]

The relevant proofs of -injective involved are all of the form λ where refl → refl , refl FWIW, but not inlined as such.

[gallais]

I have developed a new scoring system based on the size of the imported
transitive dependencies and the number of children and Reflection.AST.Term
shows up bright red because it imports so many Data.X.

We should probably wait until the first chunk of cleanups has landed but this is
indeed a good place to look into (cc @Saransh-cpp in case they're interested).

[Saransh-cpp]

I can take this up (Reflection.AST.Term and others)! A lot of the Data.X and Relation.Binary.X imports should ideally go away in the ongoing PRs.