MAIN-PASS Faulty.idr:6:9-12:WARNING: num is bound as an implicit Did you mean to refer to A.num? Faulty.idr:7:7: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:1:import alias not unique: "X"