Check name visibility before attempting derivation

[lavrentievms]

Consider the following module:

data A = MkA

public export
data B = MkB A

Suppose we want to derive a generator for the type B. It's common to place deriveGen in a separate module. Unfortunately, this isn't possible in the example above because A is private. However, deptycheck does not correctly verify whether the name is available in the current context, so it proceeds to derive the generator anyway. After the (potentially lengthy) derivation, the elaborator fails with an error like: Name BlahBlahBlah.A is private.

In such cases, it's likely the programmer simply forgot to add public export to the definition of A. I suggest adding a proper check for name visibility before running the derivation. This would help catch such errors earlier and save a significant amount of time.