The setup you have in mind seems alright apart from the fact I'm not sure what you want to use the Op Amp for. Perhaps you meant a transistor to decouple the Arduino's output from the 12 Volts supply?
A PID on Arduino will be good enough for the application.
Now, about the usage of the Hall sensor my answer becomes lengthy.
If you are going to use magnets as levitating object then you can indeed implement a Hall sensor instead of an ultrasonic one. But as you point out, how do you know if you are reading the right field? Magnetic fields aren't labelled.
I offer you a (little advanced, but quite cool to play with) way to deal with it: disturbance compensation.
- Mount the setup, with coils and a way to control their voltage (you can use a linear potentiometer on Arduino)
- Find a position where to put the Hall sensor (place it where it's as sensitive as possible to your magnets' field, and the least sensitive to the coil's field)
- Without having the magnet in the setup, map the readings of the Hall sensor to the voltage input to the coil. Now you know exactly what magnetic field the coils generate at each voltage setpoint.
- Magnetic fields add up linearly, so you can simply subtract the expected 'disturbance' field from the readings of the Hall sensor, and you have your clean reading
Just pay attention to the fact that instantly the voltage might fluctuate much more than the current. The current is low-passed naturally by the coil. So, alternatively, you might either average the voltage readings for the subtraction, or just assume the voltage to be constant because the current won't change much once the magnets are close to the steady-state position (especially in case your magnetic object and your sensor's position won't change)
At last, about the use of Hall sensor and linearity: a linear model should suffice. But it must be a linearized model around your object's height setpoint. Magnetic field are very non-linear (in your case it changes with 3rd power of distance I believe).
Alternatively, you could map the readings given by the Hall sensor to the magnet's position (having the coil turned off). So you can skip the complex modelling of magnetic fields.
For all mappings (look-up tables) on Arduino you should be able the MultiMap function.
Enjoy the nice choice of setup.