Pretty-printer improvements

The pretty-printer now correctly annotates the output of :t when it's applied to a name, which means that IDE clients can now support normalization and selective showing of implicits.

Additionally, pretty-printing (=) now correctly shows implicits when that option is enabled:
```
λΠ> (a : Type) -> (n,m,o : Nat) -> (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect o a) -> xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
(a : Type) ->
(n : Nat) ->
(m : Nat) ->
(o : Nat) ->
(xs : Vect n a) ->
(ys : Vect m a) -> (zs : Vect o a) -> xs ++ ys ++ zs = (xs ++ ys) ++ zs : Type
λΠ> :set showimplicits
λΠ> (a : Type) -> (n,m,o : Nat) -> (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect o a) -> xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
(a : Type) ->
(n : Prelude.Nat.Nat) ->
(m : Prelude.Nat.Nat) ->
(o : Prelude.Nat.Nat) ->
(xs : Prelude.Vect.Vect n a) ->
(ys : Prelude.Vect.Vect m a) ->
(zs : Prelude.Vect.Vect o a) ->
(=) {A = Prelude.Vect.Vect (Prelude.Nat.plus n (Prelude.Nat.plus m o)) a}
    {B = Prelude.Vect.Vect (Prelude.Nat.plus (Prelude.Nat.plus n m) o) a}
    (Prelude.Vect.(++) {m = n}
                       {a = a}
                       {n = Prelude.Nat.plus m o}
                       xs
                       (Prelude.Vect.(++) {m = m} {a = a} {n = o} ys zs))
    (Prelude.Vect.(++) {m = Prelude.Nat.plus n m}
                       {a = a}
                       {n = o}
                       (Prelude.Vect.(++) {m = n} {a = a} {n = m} xs ys)
                       zs) : Type
```
This fixes #1410.