Line 16 was necessary because if unitpropagate clears out the formula then chooseLiteral will return Nothing which causes it to say a solvable formula was unsolvable. I'd love more Haskell pointers to help though!
-- if formula is a null list, this clause will match:
dpll (SolverState [] r) = return r
-- otherwise this one will match:
dpll (SolverState f r) =
-- so it is never the case that null f is true here:
if null f then return r
> solve [[1],[2]]
You'll get "Nothing" when in fact the answer is [2,1].
The reason is that unitpropagate could potentially empty the list before chooseLiteral gets at it. However, I run unitpropagate first because it cuts down the search space dramatically.
In that case, I would probably turn the whole thing into a case on "unitpropagate s", and get rid of the outer where, but my advice is clearly best taken with a pinch of salt.