tutorial006a.idr:5:23-25:
When elaborating right hand side of vapp:
When elaborating argument xs to constructor Data.VectType.Vect.:::
        Can't unify
                Vect (n + n) a (Type of vapp xs xs)
        with
                Vect (plus n m) a (Expected type)
        
        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)) (Type of even)
with
        Parity (S (S (plus j j))) (Expected type)

Specifically:
        Can't unify
                plus (S j) (S j)
        with
                S (S (plus j j))