Interesting experience paper by Galois, which also raises some interesting related questions for Coq:
- Extraction to dependently typed haskell
- Extension of hs-to-coq to dependent types
- Convenience of Equations vs DT haskell
- Addition of rewriting to Coq’s type checking
- …