Why does hs-to-coq CPS transform type class dictionaries?

```
Record Functor_Dict F := { fmap : ... }.
Class Functor F :=
fdict : forall R, (Functor_Dict F -> R) -> R.
```

The CPS transform helps Coq see the termination argument for some instances. See the "Recursion through Instances" section of the Total Haskell is Reasonable Coq paper. https://arxiv.org/pdf/1711.09286.pdf

Last updated: Feb 06 2023 at 05:03 UTC