Are there any constructive higher order logics? In particular, could one take the foundation of Isabelle/HOL remove excluded middle and choice and still have a powerful foundation of constructive math? It seems Isabelle's usage of structured proofs makes its syntax preferable to Coq but Isabelle/HOL, the by far largest Isabelle library, is entirely classical. What would the impediments be to making Isabelle/CHOL (Constructive HOL) in which all the classical theorems (T) could be rephrased as (excluded middle ==> choice ==> T)?
The answer to "are there any constructive higher-order logics" is yes. Martin-Löf type theory and its many descendants and variants are the examples that first come to mind.
However, you seem to be particularly interested in versions of simple type theory as implemented in Isabelle/HOL. In principle, the HOL logic as implemented in Isabelle is the same as that implemented in the other theorem provers in the HOL family (HOL IV, HOL Light, ProofPower, ...). John Harrison's HOL Light presents the logic in a way that clearly separates out the intuitionistic fragment (see his paper HOL Light: an overview). I suspect it would require some significant restructuring of Isabelle/HOL to adopt the HOL Light formulation. If that's something you'd like to happen, then I suggest you raise this on the Isabelle mailing list rather than here.
As a small aside: the axiom of choice implies the axiom of excluded middle in higher-order logic.