Compiling Agda to Haskell with fewer coercions

Abstract

The Agda programming language is most often used as a theorem prover. Agda programs can also be compiled using the GHC backend, which translates an Agda program to a Haskell program that can be compiled by the GHC compiler. Because the Agda programming language has multiple features that are difficult to translate to Haskell automatically, the GHC backend creates simple Haskell programs that may contain type errors. Coercions (using the Haskell unsafeCoerce function) are then inserted to avoid these type errors.

This thesis changes the GHC backend so that it only inserts coercions where necessary, by utilizing the type errors that GHC reports and inserting coercions at those locations. To further lower the number of needed coercions, the translation of Agda data types is improved by retaining more type information in the generated Haskell data types.