Dependently typed Haskell in industry

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