Coinductive Soundness of Corecursive Type Class Resolution

František Farka, Ekaterina Komendantskaya, Kevin Hammond

Horn clauses and first-order resolution are commonly used to implement type classes in Haskell. Several corecursive extensions to type class resolution have recently been proposed,…