To me, the inability of these "haskell to hardware" systems to handle general recursion shows that they are fundamentally missing the most important part of the mapping from functional computation to combinational logic plus registers. They don't easily permit the "unrolling" of recursively-written code, so your recursive programs must squirrel away their state between every iteration, even when they could potentially be performed in parallel. In trying to sum a list in parallel in hardware, how do you know how many per-element operations to do at once? This determines the number of gates you'll need, and the buffer size for storing the rest of the list until those gates are free.

One way to get around this is to use termination proofs to bound the size of input data, which is exactly what's done in total functional programming. In total programs, no term is a bottom, so laziness vs. strictness is moot (both give the same answer for all programs with no exceptions or infinite loops in either evaluation strategy). Which is what you would expect since you're modelling hardware which has a clock and will clock out results into its output pins each cycle anyhow.

How can we bridge the mapping? Well, you could write a totality checker which searches for a recursion principle which is well-founded, and use this to bound data/iteration sizes and determine the shape of necessary hardware. Or you could build a theorem-proving language whose constructs enable extraction of these sizing bounds, and have humans write the proof with application of tactics.

What I really think we should be doing is writing specifications (aka, type signatures, per Curry-Howard), which do not themselves impose a particular mode of execution of the program which fulfills the specification, but only completely specify its results (and effects, if in an effectful language), and then do (constrained, by the desirable properties of the resulting programs/hardware designs) searches for proofs of those theorems.