better error message from checkPLam

[Rotsor]

Improve error message from checkPLam. The following is an example program that triggers the error:

module test where

Path (A : U) (a0 a1 : A) : U = PathP (<i> A) a0 a1

bad (A B : U) (x y : A) (q : Path A x y) : Path (Path A x y) q q =
  <i> comp (<_> Path A x y) q [(i=0) -> q]

[mortberg]

Thanks!