tutorial006a.idr:3:23:When elaborating right hand side of vapp: When elaborating argument xs to constructor Prelude.Vect.::: Can't unify Vect (n + n) a with Vect (plus n m) a Specifically: Can't unify plus n n with plus n m tutorial006b.idr:10:10:When elaborating right hand side of with block in Main.parity: Can't unify Parity (plus (S j) (S j)) with Parity (S (S (plus j j))) Specifically: Can't unify plus (S j) (S j) with S (S (plus j j))