Refinement type checkers are a powerful way to reason about functional programs. % For example, one can prove properties of a slow, specification implementation and port the proofs to an optimized pure implementation that behaves the same. % But to reason about higher-order programs, we must reason about equalities between functions: we need a consistent encoding of functional extensionality.

A natural but naive phrasing of the functional extensionality axiom ($\texttt{funExt}$) is inconsistent in refinement type systems with semantic subtyping and polymorphism, that is, if we assume $\texttt{funExt}$, then we can prove false. We demonstrate the inconsistency and develop a new approach to equality in Liquid Haskell: we define a propositional equality in a library we call $\texttt{PEq}$. Using $\texttt{PEq}$ avoids the inconsistency while still proving useful equalities at higher types; we demonstrate its use in several case studies. We validate $\texttt{PEq}$ by building a small model and developing its metatheory. Additionally, we prove metaproperties of $\texttt{PEq}$ inside Liquid Haskell itself using an unnamed folklore technique, which we dub `classy induction’.