Extracting Programs with Exceptions in an Impredicative Type System