If they want a dependently typed language, why not use one? Lean is good, and I don't think it has any significant downside wrt Haskell other than more limited

If they want a dependently typed language, why not use one? Lean is good, and I don't think it has any significant downside wrt Haskell other than more limited library ecosystem (but I guess AI can translate Haskell libraries to Lean very effectively).