-- Non-deterministic list insertion.
-- Both rules are overlapping. Thus, if the Curry evaluator
-- decides to take the second rule, the evaluation fails on the
-- empty list.
ins :: a -> [a] -> [a]
ins x ys     = x : ys
ins x (y:ys) = y : ins x ys
-- Therefore, the following non-fail condition is required:
-- ins'nonfail :: a -> [a] -> Bool
-- ins'nonfail _ _ = False

-- To provide a non-failing version of list insertion, we define
-- a non-deterministic list insertion by pattern matching:
insP :: a -> [a] -> [a]
insP x []     = [x]
insP x (y:ys) = x : y : ys  ?  y : insP x ys

-- Exploiting non-deterministic list insertion, one can easily define
-- list permutations:
perm :: [a] -> [a]
perm []     = []
perm (x:xs) = insP x (perm xs)