Solution (source code)

= Solution

The <principal type> needs an <equality type class> constraint:
``
isPrefix :: Eq a => [a] -> [a] -> Bool
isPrefix [] _ = True
isPrefix (_:_) [] = False
isPrefix (x:xs) (y:ys) = x == y && isPrefix xs ys
``
The empty <list> is a <prefix> of every <list>, witnessed by the second list itself as the remaining suffix. A nonempty prefix cannot fit in the empty <list>. Otherwise the first elements must agree, and the remaining first list must be a <prefix> of the remaining second list. These cases prove correctness by <structural induction> on the candidate prefix. The `Eq a` constraint is required by `x == y`; no ordering constraint is needed.