MAIN-PASS
Faulty.idr:6:9-11:
  |
6 | fault : num = Z
  |         ~~~
num is bound as an implicit
	Did you mean to refer to A.num?

Faulty.idr:7:9-12:
  |
7 | fault = Refl
  |         ~~~~
When checking right hand side of fault with expected type
        num = 0

Type mismatch between
        0 = 0 (Type of Refl)
and
        num = 0 (Expected type)

Specifically:
        Type mismatch between
                0
        and
                num

Multiple.idr:3:21:
  |
3 | import Data.Vect as X
  |                     ^
import alias not unique: "X"