Restoring Typeclass Refinement Support in LiquidHaskell

LiquidHaskell is a verification tool that allows Haskell developers to prove the correctness of their code through refinement types. This proposal aims to restore the support for type class elaboration: a feature that enables the verification of typeclasses laws and instances. The work that had been done previously to support typeclass elaboration is currently broken: typeclass methods produce "Unknown logic name" errors, hence the test suite for the feature has been disabled. The aim of this project is to restore this functionality, by fixing the elaboration mechanism responsible for making typeclass methods available during verification. I will trace the elaboration pipeline, implement the necessary fixes and extend test coverage. Additionally, the project will include an in-depth analysis of the features supported by the implementation and how they compare against the expected outcomes in the original paper. The deliverables will include successfully merged contributions on the LiquidHaskell GitHub repository, with its corresponding documentation, and a post with the solution on the Tweag blog.