The introduction of the Data Kinds and Type families GHC extensions has allowed a powerful technique for writing Haskell data structures which are Correct-by-Construction: GADTs indexed by Algebraic Data Types.

However, when defining operations on such data structures, there often arise type equalities that GHC is unable to prove. Furthermore, proving these equalities manually in Haskell is often a difficult or even impossible task.

Even when it is possible to write such proofs, they are usually “relevant” proofs, which must be executed at runtime. This is an unfortunate situation, as correctness should not come at the cost of speed.

This paper presents a typechecker plugin for GHC which can assert such equalities, while simultaneously translating their statements into Coq theorems, which can be proven and checked to ensure their correctness.