Related to #20, in that this should be triggered with a --verbose-errors flag.

Types containing global variables of the form VPar a.b.c.d.e_1 0 are useful to us, but just line noise for end users. We should try to keep track of where these variables are defined from. I suspect there's often a good name in terms of user variables.

I.e. if a user binds a type variable (:: #) as n, we should call references to it n in error messages. If a user writes succ(n), we should print out n and n + 1 as appropriate