mismatch.idr

data Zzz : List Nat -> List Nat -> Type
    where
        SameArg : Zzz l l
        DiffArg : Zzz a b

helperFunc : (xs, ys : List Nat) -> Zzz xs ys
helperFunc = ?helperFunc

thisWorks : (xs, ys : List Nat) -> Nat
thisWorks xs ys =
    let qs = xs ++ xs in
    let ws = ys ++ ys in
    let ddd = helperFunc qs ws in
    case ddd of
        SameArg => Z
        DiffArg => Z

thisDoesntWork : (xs, ys : List Nat) -> Nat
thisDoesntWork xs ys =
    let ddd = helperFunc (xs ++ xs) (ys ++ ys) in
    case ddd of
        SameArg => Z -- error is here
        DiffArg => Z