totality013a.idr:5:3-49: | 5 | foo order x xs y ys _ = mtot order (x :: xs) ys | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Main.foo is possibly not total due to recursive path Main.foo --> Main.mtot --> Main.mtot --> Main.mtot totality013a.idr:9:3-36: | 9 | mtot order [] right = right | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Main.mtot is possibly not total due to: Main.foo