0mm

# Functional Extensionality for Refinement Types

Niki Vazou<EMAIL_ADDRESS>IMDEA Software InstituteMadridSpain and
Michael Greenberg<EMAIL_ADDRESS>Pomona CollegeClaremontCAUSA

(2020)

###### Abstract.

Refinement type checkers are a powerful way to reason about functional
programs. For example, one can prove properties of a slow, specification
implementation, porting the proofs to an optimized implementation that behaves
the same. Without functional extensionality, proofs must relate functions that
are fully applied. When data itself has a higher-order representation, fully
applied proofs face serious impediments! When working with first-order data,
fully applied proofs lead to noisome duplication when using higher-order
functions.

While dependent type theories are typically consistent with functional
extensionality axioms, refinement type systems with semantic subtyping treat
naive phrasings of functional extensionality inconsistently, leading to
_unsoundness_. We demonstrate this unsoundness and develop a new approach to
equality in Liquid Haskell: we define a propositional equality in a library we
call PEq. Using PEq avoids the unsoundness while still proving useful
equalities at higher types; we demonstrate its use in several case studies. We
validate PEq by building a small model and developing its metatheory.
Additionally, we prove metaproperties of PEq inside Liquid Haskell itself
using an unnamed folklore technique, which we dub ‘classy induction’.

††copyright: acmcopyright††journalyear: 2020††doi:
10.1145/1122445.1122456††copyright: none

##  1\. Introduction

Refinement types have been extensively used to reason about functional
programs (Rushby et al., 1998; Xi and Pfenning, 1998; Constable and Smith,
1987; Rondon et al., 2008; Swamy et al., 2016). Higher-order functions are a
key ingredient of functional programming, so reasoning about function equality
within refinement type systems is unavoidable. For example, Vazou et al.
(2018a) prove function optimizations correct by specifying equalities between
fully applied functions. Do these equalities hold in the context of higher
order functions (e.g., maps and folds) or do the proofs need to be redone for
each fully applied context? Without functional extensionality (a/k/a funext),
one must duplicate proofs for each higher-order function. Worse still, all
reasoning about higher-order representations of data requires first-order
observations.

Most verification systems allow for function equality by way of functional
extensionality, either built-in (e.g., Lean) or as an axiom (e.g., Agda, Coq).
Liquid Haskell and F∗, two major, SMT-based verification systems built on
refinement types, are no exception: function equalities come up regularly.
But, in both these systems, the first attempt to give an axiom for functional
extensionality was wrong.111 See
https://github.com/FStarLang/FStar/issues/1542 for F∗’s initial, wrong
encoding and §7 for F∗’s different solution. We explain the situation in
Liquid Haskell in §2.  A naive funext axiom proves equalities between unequal
functions.

Our first contribution is to expose why a naive encoding of unfext is
inconsistent (§2). At first sight, function equality can be encoded as a
refinement type stating that for functions f and g, if we can prove that f x
equals g x for all x, then the functions f and g are equal:

⬇

funext :: $\forall$ a b. f:(a $\rightarrow$ b) $\rightarrow$ g:(a
$\rightarrow$ b) $\rightarrow$ (x:a $\rightarrow$ {f x = g x}) $\rightarrow$
{f = g}

(The ‘refinement proposition’ {e} is equivalent to {_:() $\mid$ e}.) On closer
inspection, funext does not encode function equality, since it is not
reasoning about equality on the domains of the functions. What if we
instantiate the domain type parameter a’s refinement to an intersection of the
domains of the input functions or, worse, to an uninhabited type? Would such
an instantiation of funext still prove equality of the two input functions? It
turns out that this naive extensionality axiom is inconsistent with refinement
types: in §2 we assume this naive funext and prove false—disaster! We work in
Liquid Haskell, but the problem generalizes to any refinement type system that
allows for semantic subtyping along with refinement polymorphism, i.e.,
refinements inferred from constraints (Rondon et al., 2008). To be sound,
proofs of function equality must carry information about the domain type on
which the compared functions are equal.

Our second contribution is to define a type-indexed propositional equality as
a Liquid Haskell library (§3), where the type indexing uses Haskell’s GADTs
and Liquid Haskell’s refinement types. We call the propositional equality PEq
and find that it adequately reasons about function equality: we can prove the
theorems we want, and we can’t prove the (non-)theorems we _don’t_ want.
Further, we prove in Liquid Haskell _itself_ that the implementation of PEq is
an equivalence relation, i.e., it is reflexive, symmetric, and transitive. To
conduct these proofs—which go by induction on the structure of the type
index—we applied a heretofore-unnamed folklore proof methodology, which we dub
classy induction (§3.3).

Our third contribution is to use PEq to prove equalities between functions
(§4). As simple examples, we prove optimizations correct as equalities between
functions (i.e., reverse), work carefully with functions that only agree on
certain domains and dependent codomains, lift equalities to higher-order
contexts (i.e., map), prove equivalences with multi-argument higher-order
functions (i.e., fold), and showcase how higher-order, propositional
equalities can co-exist with and speedup executable code. We also provide a
more substantial case study, proving the monad laws for reader monads.

Our fourth and final contribution is to formalize $\lambda^{RE}$, a core
calculus modeling PEq’s two important features: type-indexed, functionally
extensional propositional equality and refinement types with semantic
subtyping (§5). We prove that $\lambda^{RE}$ is sound and that propositional
equality implies equality in a term model of equivalence (§6).

##  2\. Functional Extensionality is Inconsistent in Refinement Types

Functional extensionality states that two functions are equal, if their values
are equal at every argument: $\forall f,g:A\rightarrow B,\forall x\in
A,f(x)=g(x)\Rightarrow f=g$. Most theorem provers consistently admit
functional extensionality as an axiom, which we call funext throughout.
Admitting funext is a convenient way to generate equalities on functions and
reuse higher order proofs. For example, Agda defines functional extensionality
as below in the standard library:

⬇

Extensionality : (a b : Level) $\rightarrow$ Set _ \--
Axiom.Extensionality.Propositional

Extensionality a b =

{A : Set a} {B : A $\rightarrow$ Set b} {f g : (x : A) $\rightarrow$ B x}
$\rightarrow$ ($\forall$ x $\rightarrow$ f x $\equiv$ g x) $\rightarrow$ f
$\equiv$ g

Having seen funext’s success in other dependently typed languages, we naively
admitted the funext axiom below in Liquid Haskell:

⬇

{-@ assume funext :: $\forall$ a b. f:(a$\rightarrow$b) $\rightarrow$
g:(a$\rightarrow$b) $\rightarrow$ (x:a $\rightarrow$ {f x = g x})
$\rightarrow$ {f = g} @-}

funext :: (a $\rightarrow$ b) $\rightarrow$ (a $\rightarrow$ b) $\rightarrow$
(a $\rightarrow$ ()) $\rightarrow$ ()

funext _f _g _pf = ()

The assume keyword introduces an axiom: Liquid Haskell will accept the
refinement signature of funext wholesale and ignore its definition. Also, note
that the = symbol in the refinements refers to SMT equality (see §3.4). Our
encoding certainly looks like Agda’s Extensionality axiom. But looks can be
deceiving: in Liquid Haskell, we can use funext to prove false. Why?

Consider two functions on Integers: the incrInt function increases all
integers by one; the incrPos function increases positive numbers by one,
returning 0 otherwise:

⬇

incrInt, incrPos :: Integer $\rightarrow$ Integer

incrInt n = n + 1

incrPos n = if 0 < n then n + 1 else 0

Liquid Haskell easily proves that these two functions behave the same on
positive numbers:

⬇

{-@ type Pos = {n:Integer | 0 < n } @-}

{-@ incrSamePos :: n:Pos $\rightarrow$ {incrPos n = incrInt n} @-}

incrSamePos :: Integer $\rightarrow$ ()

incrSamePos _n = ()

We can use funext to show that incrPos and incrInt are equal, using our proof
incrSamePos on the domain of positive numbers.

⬇

{-@ incrExt :: {incrPos = incrInt} @-}

incrExt :: ()

incrExt = funext incrPos incrInt incrSamePos

Having incrExt to hand, it’s easy to prove that every higher-order use of
incrPos can be replaced with incrInt, which is much more efficient—it saves us
a conditional branch! For example, incrMap shows that mapping over a list with
incrPos is just the same as mapping over it with incrInt.

⬇

{-@ incrMap :: xs:[Pos] $\rightarrow$ {map incrPos xs = map incrInt xs} @-}

incrMap :: [Integer] $\rightarrow$ ()

incrMap xs = incrExt

We could prove incrMap without function equality, i.e., if we only knew
incrSamePos. To do so, we would write an inductive proof—and we’d have to redo
the proof for every context in which we would rewrite incrPos to incrInt. So
funext is in part about _modularity_ and _reuse_ in theorem proving. We don’t
give a full example here, but funext is particularly critical when trying to
equate structures that are themselves higher order, like difference lists or
streams.

Unfortunately, incrExt makes it _too_ easy to prove equivalences… our system
is inconsistent! Here’s a proof that 0 is equal to -4:

⬇

{-@ inconsistencyI :: {incrPos (-5) = incrInt (-5)} @-} \-- 0 = -4

inconsistencyI :: ()

inconsistencyI = incrExt

What happened here? How can we have that equality… that 0 = -4? Liquid Haskell
looked at incrExt and saw the two functions were equal… without any regard to
the domain on which incrExt proved incrPos and incrInt equal! We _forgot_ the
domain, and so incrExt generates a proof in SMT that those two functions are
equal on any domain.

So funext is inconsistent in Liquid Haskell! The problem is that Liquid
Haskell forgets the domain on which the two functions are proved equal,
remembering only the equality itself.

We can exploit funext to find equalities between _any_ two functions that
share the same Haskell type on the _empty_ domain, and Liquid Haskell will
treat these functions as _universally_ equal. Ouch!

For example, plus2 below defines a function that increases its input by 2 and
is obviously not equal to incrInt on any nontrivial domain.

⬇

plus2 :: Integer $\rightarrow$ Integer

plus2 x = x + 2

Even so, we can use funext to prove that plus2 behaves the same as incrInt on
the empty domain, i.e., for all inputs n that satisfy false.

⬇

{-@ type Empty = {v:Integer | false } @-}

{-@ incrSameEmpty :: n:Empty $\rightarrow$ {incrInt n = plus2 n} @-}

incrSameEmpty :: Integer $\rightarrow$ ()

incrSameEmpty _n = ()

Now incrSameEmpty provides enough evidence for funext to show that incrInt
equals plus2, which we use to prove another egregious inconsistency.

⬇

{-@ incrPlus2Ext :: {incrInt = plus2} @-}

incrPlus2Ext :: ()

incrPlus2Ext = funext incrInt plus2 incrSameEmpty

{-@ inconsistencyII :: {incrInt 0 = plus2 0} @-} \-- 1 = 2

inconsistencyII :: ()

inconsistencyII = incrPlus2Ext

Liquid Haskell isn’t like most other dependent type theories: we can’t just
admit funext as phrased. But we still want to prove equalities between higher-
order values! What can we do?

###  2.1. Refined, Type-Indexed, Extensional, Propositional Equality

If we’re going to reason using functional extensionality in Liquid Haskell,
we’ll need to be careful to remember the type at which we show the functions
produce equal results. What domains are involved when we use functional
extensionality?

To prove two functions $f$ and $g$ extensionally equal, we must reason about
_four_ domains. Let $\mathcal{D}_{f}$ and $\mathcal{D}_{g}$ be the domains on
which the functions $f$ and $g$ are respectively defined. Let
$\mathcal{D}_{p}$ be the domain on which the two functions are proved equal
and $\mathcal{D}_{e}$ the domain on which the resulting equality between the
two functions is found. In our incrExt example above, the function domains are
Integer ($\mathcal{D}_{f}$ = $\mathcal{D}_{g}$ = Integer), as specified by the
function definitions, the domain of the proof is positive numbers
($\mathcal{D}_{p}$ = Pos), as specified by incrSamePos, and, disastrously, the
domain of the equality itself is unspecified in funext. Liquid Haskell will
implicitly set the domain on which the functions are equal to the most general
one where both functions can be called ($\mathcal{D}_{e}$ = Integer).

Our funext encoding naively imposes no real constraints between these domains.
In fact, funext only requires that $\mathcal{D}_{f}$, $\mathcal{D}_{g}$, and
$\mathcal{D}_{p}$ are supertypes of the empty domain (§5), which trivially
holds for all types, leaving $\mathcal{D}_{e}$ underconstrained.

To be consistent, we need a functional extensionality axiom that (1) captures
the domain of function equality $\mathcal{D}_{e}$ explicitly, (2) requires
that the domain of the equality, $\mathcal{D}_{e}$, is a subtype of the domain
of the proof, $\mathcal{D}_{p}$, which should be a subtype of the functions
domains, $\mathcal{D}_{f}$ and $\mathcal{D}_{g}$, and (3) ensures that the
resulting equality between functions is only used on subdomains of
$\mathcal{D}_{e}$.

Our solution is to define a refined, type-indexed, extensional propositional
equality. We do so in the Liquid Haskell library PEq, which defines a
propositional equality also called PEq. We write PEq a {el} {er} to mean that
the expressions el and er are propositionally equal and of type a. We
carefully crafted PEq’s definition as a refined GADT (§3) to meet our three
criteria.

##### 1\. PEq is Type-Indexed

The type index a in PEq a {el} {er} makes it easy to track types explicitly.
PEq’s constructor axiomatizing functional extensionality keeps careful track
of types:

⬇

XEq :: f:(a $\rightarrow$ b) $\rightarrow$ g:(a $\rightarrow$ b) $\rightarrow$
(x:a $\rightarrow$ PEq b {f x} {g x}) $\rightarrow$ PEq (a $\rightarrow$ b)
{f} {g}

The result type of XEq explicitly captures the equality domain as the domain
of the return type (i.e., a). The standard variance and type checking rules of
Liquid Haskell ensure that the domains $\mathcal{D}_{f}$, $\mathcal{D}_{g}$,
and $\mathcal{D}_{p}$ are supertypes of $\mathcal{D}_{e}$. (See §5 for more
detail on type checking.)

##### 2\. Generating Function Equalities

The XEq case of PEq generates equalities at function types using functional
extensionality. Liquid Haskell will check the domains appropriately: it won’t
prove equality between functions at an inappropriate domain.

Returning to our concrete example of incrPos and incrInt, we can use XEq to
find these functions equal on the domain Pos:

⬇

{-@ incrExtGood :: PEq (Pos $\rightarrow$ Integer) {incrPos} {incrInt} @-}

incrExtGood :: PEq (Integer $\rightarrow$ Integer)

incrExtGood = XEq incrPos incrInt incrEq

XEq checks that the domains of the functions incrPos and incrInt are
supertypes of Pos, i.e., Pos <: Integer. Further it checks that the domain of
the proof incrEq is supertype of Pos.

What might we define for incrEq? Here are three alternatives. Each alternative
is either accepted or rejected by XEq as appropriate for the Pos $\rightarrow$
Integer type index; each alternative is also possible or impossible to prove.
(See §3 for more on how incrEq can be defined.)

⬇

incrEq :: n:Pos $\rightarrow$ PEq Integer {incrPos n} {incrInt n} \-- ACCEPTED
and POSSIBLE

incrEq :: n:Integer $\rightarrow$ PEq Integer {incrPos n} {incrInt n} \--
ACCEPTED and IMPOSSIBLE

incrEq :: n:Empty $\rightarrow$ PEq Integer {incrPos n} {incrInt n} \--
REJECTED and POSSIBLE

The first two alternatives, n:Pos and n:Integer, will be accepted by XEq,
since both Pos and Integer are supertypes of Pos… though it is impossible to
actually construct a proof for the second alternative, i.e., a proof that
incrPos n equals incrInt n for all integers n. On the other hand, the last
proof on n:Empty is trivial, but XEq rejects it, because Empty is not a
supertype of Pos. Liquid Haskell’s checks on XEq’s type indices prevents
inconsistencies like inconsistencyII.

##### 3\. Using Function Equalities

Just as PEq’s XEq constructor ensures that the right domains are checked and
tracked for functional extensionality, we have a constructor for ensuring
these equalities are used appropriately. The constructor CEq characterizes
equality as valid in all contexts, i.e., if x and y are equal, they can be
substituted in any context ctx and the results ctx x and ctx y will be equal:

⬇

CEq :: x:a $\rightarrow$ y:a $\rightarrow$ PEq a {x} {y} $\rightarrow$ ctx:(a
$\rightarrow$ b) $\rightarrow$ PEq b {ctx x} {ctx y}

It is easy to use CEq to apply functional equalities in higher order contexts.
For example, we can prove that map incrPos equals map incrInt:

⬇

{-@ incrMapProp :: PEq ([Pos] $\rightarrow$ [Integer]) {map incrPos} {map
incrInt} @-}

incrMapProp :: PEq ([Integer] $\rightarrow$ [Integer])

incrMapProp = CEq incrPos incrInt incrExtGood (map)

We can more generally show that propositionally equal functions produce equal
results on equal inputs. The trick is to _flip_ the context, defining a
function app that takes as input two functions f and g, a proof these
functions are equal, and an argument x, returning a proof that f x = g x:

⬇

{-@ app :: f:(a $\rightarrow$ b) $\rightarrow$ g:(a $\rightarrow$ b)
$\rightarrow$ PEq (a $\rightarrow$ b) {f} {g}

$\rightarrow$ x:a $\rightarrow$ PEq b {f x} {g x} @-}

app :: (a $\rightarrow$ b) $\rightarrow$ (a $\rightarrow$ b) $\rightarrow$ PEq
(a $\rightarrow$ b) $\rightarrow$ a $\rightarrow$ PEq b

app f g eq x = CEq f g eq (flip x)

flip x f = f x

The app lemma makes it easy to use function equalities while still checking
the domain on which the function is applied. These checks prevent
inconsistencies like inconsistencyI. For instance, we can try to apply the
functional equality incrExtGood to a bad and a good input.

⬇

{-@ badFO ::PEq Integer {incrPos 0} {incrInt 0} @-}

badFO = app incrPos incrInt incrExtGood 0 \-- REJECTED

{-@ goodFO :: x:{Integer | 42 < x } $\rightarrow$ PEq Integer {incrPos x} {incrNat x} @-}

goodFO x = app incrPos incrInt incrExtGood x \-- ACCEPTED

Liquid Haskell rejects the bad input in badFO: the number $0$ isn’t in the Pos
domain on which incrExtGood was proved. Liquid Haskell accepts the good input
in goodFO, since any x greater than 42 is certainly positive. The goodFO proof
yields a first-order equality on any such x, here on Integer. Such first order
equalities correspond neatly with the notion of equality used in the SMT
solvers that buttress all of Liquid Haskell’s reasoning. (For more information
on how SMT equality relates to notions of equality in Liquid Haskell, see §3.
For an example of how these first-order equalities can lead to runtime
optimizations, see §4.5.)

###  2.2. Why Isn’t funext Inconsistent in Agda?

At the beginning of §2, we present Agda’s Extensionality axiom, whose return
type is f $\equiv$ g. Agda’s equality appears to lack a type index. Why
doesn’t Agda also suffer from inconsistency?

Agda’s equality only seems to be unindexed. In fact, Agda’s built-in equality
is the standard, type-indexed Leibniz equality used in most dependent type
theories (omitting Level polymorphism):

⬇

data _$\equiv$_ {A : Set} (x : A) : A $\rightarrow$ Set a where

refl : x $\equiv$ x

The curly braces around the type index A marks it as _implicit_ , i.e., to be
inferred. If we were to explicitly give implicit arguments by wrapping them in
curly braces, Agda’s extensionality axiom returns (_$\equiv$_)
{a$\rightarrow$b} f g.

Our XEq axiom recovers the type indexing in Agda’s equivalence that’s missing
in our original funext encoding. Of course, (Liquid) Haskell’s lack of
implicit type indices makes reasoning about function equalities verbose. On
the other hand, Liquid Haskell’s subtyping can reinterpret functions at many
domains (see §4.2). In Agda, however, it is much more complex to reinterpret
functions and to generate heterogeneous equality relating incrInt and incrPos
only on positive inputs.

##  3\. PEq: a Library and GADT for Extensional Equality

We define the PEq library in Liquid Haskell, implementing the type-indexed
propositional equality, also called PEq. First, we axiomatize equality for
base types in the AEq typeclass (§3.1). Next, we define propositional equality
for base and function types with the PEq GADT (Xi et al., 2003; Cheney and
Hinze, 2003) (§3.2). Refinements on the GADT enforce the typing rules of our
formal model (§6), but we prove some of the metatheory in Liquid Haskell
itself (§3.3). Finally, we discuss how AEq and PEq interact with Haskell’s and
SMT’s equalities (§3.4).

###  3.1. The AEq typeclass, for axiomatized equality

We begin with by axiomatizing equality that can be ported to SMT: such an
equality should be an equivalence relation that implies SMT equality. We use
refinements on typeclasses (Liu et al., 2020) to define a typeclass AEq, which
contains the (operational) equality method $\equiv$, three methods that encode
the equality laws, and one method that encodes correspondence with SMT
equality.

⬇

{-@ class AEq a where

($\equiv$) :: x:a $\rightarrow$ y:a $\rightarrow$ Bool

reflP :: x:a $\rightarrow$ {${x}\equiv{x}$}

symmP :: x:a $\rightarrow$ y:a $\rightarrow$ { ${x}\equiv{y}$ $\Rightarrow$
${y}\equiv{x}$ }

transP :: x:a $\rightarrow$ y:a $\rightarrow$ z:a $\rightarrow$ {
(${x}\equiv{y}$ && ${y}\equiv{z}$) $\Rightarrow$ ${x}\equiv{z}$ }

smtP :: x:a $\rightarrow$ y:a $\rightarrow$ { ${x}\equiv{y}$ } $\rightarrow$ {
x = y } @-}

To define an instance of AEq one has to define the method ($\equiv$) and
provide explicit proofs that it is reflexive, symmetric, and transitive
(reflP, symmP, and transP resp.); thus $\equiv$ is, by construction, an
equality. Finally, we require the proof smtP that captures that ($\equiv$)
implies equality provable by SMT (e.g., structural equality).222 The three
axioms of equality alone are not enough to ensure SMT’s structural equality,
e.g., one can define an instance x $\equiv$ y = True which satisfies the
equality laws, but does not correspond to SMT equality.

###  3.2. The PBEq GADT and its PEq Refinement

⬇

\-- (1) Plain GADT

data PBEq :: * $\rightarrow$ * where

BEq :: AEq a $\Rightarrow$ a $\rightarrow$ a $\rightarrow$ () $\rightarrow$
PBEq a

XEq :: (a $\rightarrow$ b) $\rightarrow$ (a $\rightarrow$ b) $\rightarrow$ (a
$\rightarrow$ PEq b) $\rightarrow$ PBEq (a $\rightarrow$ b)

CEq :: a $\rightarrow$ a $\rightarrow$ PBEq a $\rightarrow$ (a $\rightarrow$
b) $\rightarrow$ PBEq b

\-- (2) Uninterpreted equality between terms e1 and e2

{-@ type PEq a e1 e2 = {v:PBEq a | e1 $\backsimeq$ e2} @-}

{-@ measure ($\backsimeq$) :: a $\rightarrow$ a $\rightarrow$ Bool @-}

\-- (3) Type refinement of the GADT

{-@ data PBEq :: * $\rightarrow$ * where

BEq :: AEq a $\Rightarrow$ x:a $\rightarrow$ y:a $\rightarrow$ {v:() | ${x}\equiv{y}$}

$\rightarrow$ PEq a {x} {y}

XEq :: f:(a $\rightarrow$ b) $\rightarrow$ g:(a $\rightarrow$ b) $\rightarrow$
(x:a $\rightarrow$ PEq b {f x} {g x})

$\rightarrow$ PEq (a $\rightarrow$ b) {f} {g}

CEq :: x:a $\rightarrow$ y:a $\rightarrow$ PEq a {x} {y} $\rightarrow$ ctx:(a
$\rightarrow$ b)

$\rightarrow$ PEq b {ctx x} {ctx y} @-}

Figure 1. Implementation of the propositional equality PEq as a refinement of
Haskell’s GADT PBEq.

We use AEq to define our type-indexed propositional equality PEq a {e1} {e2}
in three steps (Figure 1): (1) structure as a GADT, (2) definition of the
refined type PEq, and (3) axiomatization of equality by refining of the GADT.

First, we define the structure of our proofs of equality as PBEq, an
unrefined, i.e., Haskell, GADT (Figure 1, (1)). The plain GADT defines the
structure of derivations in our propositional equality (i.e., which proofs are
well formed), but none of the constraints on derivations (i.e., which proofs
are valid). There are three ways to prove our propositional equality, each
corresponding to a constructor of PBEq: using an AEq instance (constructor
BEq); using funext (constructor XEq); and by congruence closure (constructor
CEq).

Next, we define the refinement type PEq to be our propositional equality
(Figure 1, (2)). Two terms e1 and e2 of type a are propositionally equal when
(a) there is a well formed and valid PBEq proof and (b) we have e1
$\backsimeq$ e2, where ($\backsimeq$) is an uninterpreted SMT function. Liquid
Haskell uses curly braces for expression arguments in type applications, e.g.,
in PEq a {x} {y}, x and y are expressions, but a is a type.

Finally, we refine the type constructors of PBEq to axiomatize the
uninterpreted ($\backsimeq$) and generate proofs of PEq (Figure 1, (3)). Each
constructor of PBEq is refined to return something of type PEq, where PEq a
{e1} {e2} means that terms e1 and e2 are considered equal at type a. BEq
constructs proofs that two terms, x and y of type a, are equal when
${x}\equiv{y}$ according to the AEq instance for a. XEq is the (type-indexed)
funext axiom. Given functions f and g of type a $\rightarrow$ b, a proof of
equality via extensionality also needs a PEq-proof that f x and g x are equal
for all x of type a. Such a proof has refined type x:a $\rightarrow$ PEq b {f
x} {g x}. Critically, we don’t lose any type information about f or g! CEq
implements congruence closure: for x and y of type a that are equal—i.e., PEq
a {x} {y}—and an arbitrary context with an a-shaped hole (ctx :: a
$\rightarrow$ b), filling the context with x and y yields equal results, i.e.,
PEq b {ctx x} {ctx y}.

##### Design Alternatives

The first design choice we made was to define PEq as a GADT and not an
axiomatized opaque type. While there’s no reason to pattern match on PEq
terms, there’s also no harm in it. A GADT provides a clean interface on how
PEq can be generated: it collects all the axioms as data contructors and
prevents the user from arbitrarily adding new constructors. The second choice
we made was to define the type PEq using a fresh uninterpreted equality symbol
(Figure 1, (2)) instead of SMT equality. Again, we made this decision to
ensure that all PEq terms are constructed via the constructors and not
implicit SMT automation. The final choice we made was to define the base case
using the AEq constraints. We considered two alternatives:

⬇

BEq :: x:a $\rightarrow$ y:a $\rightarrow$ {v:() | x = y } $\rightarrow$ PEq a {x} {y} \-- alternative I

BEq :: Eq a $\Rightarrow$ x:a $\rightarrow$ y:a $\rightarrow$ {v:() | x = y } $\rightarrow$ PEq a {x} {y} \-- alternative II

We rejected the first to ensure that the base case does not include functions
(which don’t generally have Eq instances) and to support our metatheory
(§3.3). We rejected the second to exclude user-defined Eq instances that do
not correspond to SMT equality (since in §3.4 we define a machanism to turn
PEq to SMT equalities).

##### Example:

Having seen AEq and the BEq case of PEq, we can define the incrEq function
from §2:

⬇

{-@ incrEq :: x:Pos $\rightarrow$ PEq Integer {incrPos x} {incrInt x} @-}

incrEq x = BEq (incrPos x) (incrInt x) (reflP (incrPos x))

We start from reflP (incrPos x) :: {incrPos x${}\equiv{}$incrPos x}, since x
is positive, the SMT derives incrPos x = incrInt x, generating the BEq proof
term {incrPos x${}\equiv{}$incrInt x}.

###  3.3. Equivalence Properties and Classy Induction

We can prove metaproperties of the actual implementation of PEq—reflexivity,
symmetry, and transitivity—within Liquid Haskell itself.

Our proofs in Liquid Haskell go by induction on types. But “induction” in
Liquid Haskell means writing a recursive function, which necessarily has a
single, fixed type. To express that PEq is reflexive, we want a Liquid Haskell
theorem refl :: x:a $\rightarrow$ PEq a {x} {x}, but its proof goes by
induction on the type a, which is not possible in ordinary Haskell
functions.333A variety of GHC extensions allow case analysis on types (e.g.,
type families and generics), but, unfortunately, Liquid Haskell doesn’t
support such fancy type-level programming.

The essence of our proofs is a folklore method we call _classy induction_ (see
§7 for the history). To prove a theorem using classy induction on the PEq
GADT, one must: (1) define a typeclass with a method whose refined type
corresponds to the theorem; (2) prove the base case for types with AEq
instances; and (3) prove the inductive case for function types, where
typeclass constraints on smaller types generate inductive hypotheses. All
three of our proofs follow this pattern. Here’s the proof for reflexivity.

⬇

\-- (1) Refined typeclass

{-@ class Reflexivity a where

refl :: x:a $\rightarrow$ PEq a {x} {x} @-}

\-- (2) Base case (AEq types)

instance AEq a $\Rightarrow$ Reflexivity a where

refl a = BEq a a (reflP a)

\-- (3) Inductive case (function types)

instance Reflexivity b $\Rightarrow$ Reflexivity (a $\rightarrow$ b) where

refl f = XEq f f (\a $\rightarrow$ refl (f a))

For (1), the typeclass Reflexivity simply states the desired theorem type,
refl :: x:a $\rightarrow$ PEq a {x} {x}. For (2), given an AEq a instance, BEq
and the reflP method are combined to define the refl method. To define such a
general instance, we enabled the GHC extensions FlexibleInstances and
UndecidableInstances. For (3), XEq can show that f is equal to itself by using
the refl instance from the codomain constraint: the Reflexivity b constraint
generates a method refl :: x:b $\rightarrow$ PEq b {x} {x}. The codomain
constraint Reflexivity b corresponds exactly to the inductive hypothesis on
the codomain: we are doing induction!

At compile time, any use of refl x when x has type a asks the compiler to find
a Reflexivity instance for a. If a has an AEq instance, the proof of refl x
will simply be BEq x x (reflP a). If a is a function of type b $\rightarrow$
c, then the compiler will try to find a Reflexivity instance for the codomain
c—and if it finds one, generate a proof using XEq and c’s proof. The
compiler’s constraint resolver does the constructive proof for us, assembling
the ‘inductive tower’ to give us a refl for our chosen type. That is, even
though Liquid Haskell can’t mechanically check that our inductive proofs are
in general complete (i.e., the base and inductive cases cover all types), our
refl proofs will work for types where the codomain bottoms out with an AEq
instance, i.e., any type consisting of functions and AEq-equable types.

Our proofs of symmetry and transitivity follow the same pattern, but both also
make use congruence closure. The full proofs can be found in supplementary
material (2021). Here is the inductive case from symmetry:

⬇

instance Symmetry b $\Rightarrow$ Symmetry (a $\rightarrow$ b) where

\-- sym :: l:(a$\rightarrow$b) $\rightarrow$ r:(a$\rightarrow$b) $\rightarrow$
PEq (a$\rightarrow$b) {l} {r} $\rightarrow$ PEq (a$\rightarrow$b) {r} {l}

sym l r pf = XEq r l $\$$ \a $\rightarrow$ sym (l a) (r a) (CEq l r pf ($\$$
a) ? ($\$$ a l) ? ($\$$ a r)))

Here l and r are functions of type a $\rightarrow$ b and we know that l
$\backsimeq$ r; we must prove that r $\backsimeq$ l. We do so using: (a) XEq
for extensionality, letting a of type a be given; (b) sym (l a) (r a) as the
IH on the codomain b on (c) CEq for congruence closure on l $\backsimeq$ r in
the context ($\$$ a). The last step is the most interesting: if l is equal to
r, then plugging them into the same context yields equal results; as our
context, we pick ($\$$ a), i.e., \f $\rightarrow$ f a, showing that l a
$\backsimeq$ r a; the IH on the codomain b yields r a $\backsimeq$ l a, and
extensionality shows that r $\backsimeq$ l, as desired. The operator ?,
defined as x ? p = x, asks Liquid Haskell to encode ‘p‘ into the SMT solver to
help prove ‘x‘. Our use of ? unfolds the definitions $\$$ a l and $\$$ a r to
help CEq.

###  3.4. Interaction of the different equalities.

We have four equalities in our system (Figure 2): SMT equality ($=$), the
($\equiv$) method of the AEq typeclass(§3.1), the refined GADT PEq (§3.2), and
the (==) method of Haskell’s Eq typeclass.

##### SMT Equality

The single equal sign ($=$) represents SMT equality, which satisfies the three
equality axioms and is syntactically defined for data types. The SMT-LIB
standard (Barrett et al., 2010) permits the equality symbol on functions but
does not specify its behavior. Implementations vary. CVC4 allows for
functional extensionality and higher-order reasoning (Barbosa et al., 2019).
When Z3 compares functions for equality, it treats them as arrays, using the
extensional array theory to incompletely perform the comparison. When asked if
two functions are equal, Z3 typically answers unknown. To avoid this
unpredictability, our system avoids SMT equality on functions.

##### Interactions of Equalities

SMT equalities are internally generated by Liquid Haskell using the reflection
and PLE tactic of Vazou et al. (2018b) (see also §4.1). An
${e_{1}}\equiv{e_{2}}$ equality can be generated one of three ways: (1) If SMT
can prove an SMT equality $e_{1}=e_{2}$, then the reflexivity reflP method can
generate that equality, i.e., reflP $e_{1}$ proves ${e_{1}}\equiv{e_{1}}$,
which is enough to show ${e_{1}}\equiv{e_{2}}$. (2) Our system provides AEq
instances for the primitive Haskell types using the Haskell equality that we
assume satisfies the four laws, e.g., the instance AEq Int is provided. (3)
Using refinements in typeclasses (Liu et al., 2020) one can explicitly define
instances of AEq, which may or may not coincide with Haskell Eq instances.

Constructors generate PEq proofs, bottoming out at AEq: BEq combined with an
AEq term and XEq or CEq combined with other PEq terms.

Finally, we define a mechanism to convert PEq into an SMT equality. This
conversion is useful when we want to derive an SMT equality $f\ e=g\ e$ from a
function equality PEq (a $\rightarrow$ b) {f} {g} (see §4.5). The derivation
requires that the domain b admits the axiomatized equality, AEq. To capture
this requirement we define toSMT that converts PEq to SMT equality as a method
of a class that requires an AEq constraint:

⬇

class AEq a $\Rightarrow$ SMTEq a where

toSMT :: x:a $\rightarrow$ y:a $\rightarrow$ PEq a {x} {y} $\rightarrow$ {x =
y}

Figure 2. The four different equalities and their interactions. Haskell
equality is in red to highlight its potential for unsoundness.

##### Non-interaction

Liquid Haskell maps Haskell’s (==) to SMT equality by default. It is surely
unsound to do so, as users can define their own Eq instances with (==) methods
that do arbitrarily strange things. To avoid this built-in unsoundness, our
implementation and case studies don’t directly use Haskell’s equality.

##### Equivalence Relation Axioms

Each of the four equalities has a different relationship to th equivalence
relation axioms (reflexivity, symmetry, transitivity). AEq comes with explicit
proof methods that capture the axioms. For PEq, we prove the equality axioms
using classy induction (§3.3). For SMT equality, we simply trust
implementation of the underlying solver. For Haskell’s equality, there’s no
general way to enforce the equality axioms, though users can choose to prove
them.

##### Computability

Finally, the Eq and AEq classes define the computable equalities used in
programs, (==) and ($\equiv$) respectively. The PEq equality only contains
proof terms, while the SMT equality lives entirely inside the refinements;
neither can be meaningfully used in programs.

##  4\. Case Studies

We demonstrate our propositional equality in seven case studies. We start by
moving from first-order equalities to equalities between functions (reverse,
§4.1). Next, we show how PEq’s type indices reason about refined domains and
dependent codomains of functions (succ, §4.2). Proofs about higher-order
functions demonstrate the contextual equivalence axiom (map, §4.3). Then, we
see that PEq plays well with multi-argument functions (foldl, §4.4). Next, we
present how a PEq proof can speedup code (spec, §4.5). Finally, we present two
bigger case studies that prove the monoid laws for endofunctions (§4.6) and
the monad laws for reader monads (§4.7). Complete code is available in the
(supplementary material, 2021).

###  4.1. Reverse: from First- to Higher-Order Equality

Consider three candidate definitions of the list-reverse function (Figure
LABEL:fig:reverse, top): a ‘fast’ one in accumulator-passing style, a ‘slow’
one in direct style, and a ‘bad’ one that is the identity.

##### First-Order Proofs

The reverseEq theorem neatly relates the two list reversals (Figure
LABEL:fig:reverse). The final theorem reverseEq is a corollary of a lemma and
rightId, which shows that [] is a right identity for list append, (++). The
lemma is the core induction, relating the accumulating fastGo and the direct
slow. The lemma itself uses the inductive lemma assoc to show associativity of
(++). All the equalities in the first order statements use the SMT equality,
since they are automatically proved by Liquid Haskell’s reflection and PLE
tactic (Vazou et al., 2018b).

##### Higher-Order Proofs

Plain SMT equality isn’t enough to prove that fast and slow are themselves
equal. We need functional extensionality: the XEq constructor of the PEq GADT.

⬇

reverseHO :: PEq ([a] $\rightarrow$ [a]) {fast} {slow}

reverseHO = XEq fast slow reversePf

The job of the reversePf lemma is to prove fast xs propositionally equal to
slow xs for all xs:

⬇

reversePf :: xs:[a] $\rightarrow$ PEq [a] {fast xs} {slow xs}

There are several different ways to construct such a proof.

##### Style 1: Lifting First-Order Proofs

The first order equality proof reverseEq lifts directly into propositional
equality, using the BEq constructor and the reflexivity property of AEq.

⬇

reversePf1 :: AEq [a] $\Rightarrow$ xs:[a] $\rightarrow$ PEq [a] {fast xs}
{slow xs}

reversePf1 xs = BEq (fast xs) (slow xs) (reverseEq xs ? reflP (fast xs))

Such proofs rely on SMT equality, which the reflP call turns into axiomatized
equality (AEq).

##### Style 2: Inductive Proofs

Alternatively, inductive proofs can be directly performed in the propositional
setting, eliminating the AEq constraint. To give a sense of what these proofs
are like, we translate lemma into lemmaP:

⬇

lemmaP :: (Reflexivity [a], Transitivity [a])

$\Rightarrow$ rest:[a] $\rightarrow$ xs:[a] $\rightarrow$ PEq [a] {fastGo rest
xs} {slow xs ++ rest}

lemmaP rest [] = refl rest

lemmaP rest (x:xs) = trans (fastGo rest (x:xs)) (slow xs ++ (x:rest))

(slow (x:xs) ++ rest)

(lemmaP (x:rest) xs) (assocP (slow xs) [x] rest)

The proof goes by induction and uses the Reflexivity and Transitivity
properties of PEq encoded as typeclasses (§3.3) along with assocP and
rightIdP, the propositional versions of assoc and rightId (not shown). These
typeclass constraints propagate to the reverseHO proof, via reversePf2.

⬇

reversePf2 :: (Reflexivity [a], Transitivity [a])

$\Rightarrow$ xs:[a] $\rightarrow$ PEq [a] {fast xs} {slow xs}

reversePf2 xs = trans (fast xs) (slow xs ++ [])

(slow xs)

(lemmaP [] xs) (rightIdP (slow xs))

##### Style 3: Combinations

One can combine the easy first order inductive proofs with the typeclass-
encoded properties. Here refl sets up the propositional context; lemma and
rightId complete the proof.

⬇

reversePf3 :: (Reflexivity [a]) $\Rightarrow$ xs:[a] $\rightarrow$ PEq [a]
{fast xs} {slow xs}

reversePf3 xs = refl (fast xs) ? lemma xs [] ? rightId (slow xs)

##### Bad Proofs

We could not use any of these styles to generate a bad (non-)proof: neither
PEq ([a] $\rightarrow$ [a]) {fast} {bad} nor PEq ([a] $\rightarrow$ [a])
{slow} {bad} are provable.

###  4.2. Succ: Refined Domains and Dependent Codomains

Our propositional equality PEq naturally reasons about functions with refined
domains and dependent codomains. For example, recall the functions incrInt and
incrPos from §2:

⬇

incrInt, incrPos :: Integer $\rightarrow$ Integer

incrInt n = n + 1

incrPos n = if 0 < n then n + 1 else 0

In §2 we proved that the two functions are equal on the domain of positive
numbers:

⬇

type Pos = {x:Integer | 0 < x }

posDom :: PEq (Pos $\rightarrow$ Integer) {incrInt} {incrPos}

posDom = XEq incrInt incrPos $\x->$\BEq (incrInt x) (incrPos x) (reflP
(incrInt x))

We can also reason about how each function’s domain affects its codomain. For
example, we can prove that these functions are equal _and_ they take Pos
inputs to natural numbers.

⬇

posRng :: PEq (Pos $\rightarrow$ {v:Integer | 0 <= v}) {incrInt} {incrPos}

posRng = XEq incrInt incrPos $\x->$\BEq (incrInt x) (incrPos x) (reflP
(incrInt x))

Finally, we can prove properties of the function’s codomain that depend on the
inputs. Below we show that on positive arguments, the result is always
increased by one.

⬇

type SPos x = {v:Pos | v = x + 1}

depRng :: PEq (x:Pos $\rightarrow$ SPos {x}) {incrInt} {incrPos}

depRng = XEq incrInt incrPos $\x->$\BEq (incrInt x) (incrPos x) (reflP
(incrInt x))

##### Equalities Rejected by Our System

Liquid Haskell correctly rejects various wrong, (non-)proofs of equality
between the functions incrInt and incrPos. We highlight three:

⬇

badDom :: PEq ( Integer $\rightarrow$ Integer) {incrInt} {incrPos}

badCod :: PEq ( Pos $\rightarrow$ {v:Integer | v < 0}) {incrInt} {incrPos}

badDCod :: PEq (x:Pos $\rightarrow$ {v:Integer | v = x+2}) {incrInt} {incrPos}

badDom expresses that incrInt and incrPos are equal for any Integer input,
which is wrong, e.g., incrInt (-2) yields -1, but incrPos (-2) yields 0.
Correctly constrained to positive domains, badCod specifies a negative
codomain (wrong) while badDCod specifies that the result is increased by 2
(also wrong). Our system rejects all three with a refinement type error.

###  4.3. Map: Putting Equality in Context

Our propositional equality can be used in higher order settings: we prove that
if f and g are propositionally equal, then map f and map g are also equal. Our
proofs use the congruence closure equality constructor/axiom CEq.

##### Equivalence on the Last Argument

Direct application of CEq ports a proof of equality to the last argument of
the context (a function). For example, mapEqP below states that if two
functions f and g are equal, then so are the partially applied functions map f
and map g.

⬇

mapEqP :: f:(a $\rightarrow$ b) $\rightarrow$ g:(a $\rightarrow$ b)
$\rightarrow$ PEq (a $\rightarrow$ b) {f} {g}

$\rightarrow$ PEq ([a] $\rightarrow$ [b]) {map f} {map g}

mapEqP f g pf = CEq f g pf map

##### Equivalence on an Arbitrary Argument

To show that map f xs and map g xs are equal for all xs, we use CEq with
flipMap, i.e., a context that puts f and g in a ‘flipped’ context.

⬇

mapEq :: f:(a $\rightarrow$ b) $\rightarrow$ g:(a $\rightarrow$ b)
$\rightarrow$ PEq (a $\rightarrow$ b) {f} {g}

$\rightarrow$ xs:[a] $\rightarrow$ PEq [b] {map f xs} {map g xs}

mapEq f g pf xs = CEq f g pf (flipMap xs) ? fMapEq f xs ? fMapEq g xs

fMapEq :: f:_ $\rightarrow$ xs:[a] $\rightarrow$ {map f xs = flipMap xs f}

fMapEq f xs = ()

flipMap xs f = map f xs

The mapEq proof relies on CEq with the flipped context and needs to know that
map f xs = flipMap xs f. Liquid Haskell won’t infer this fact on its own in
the higher order setting of this proof; we explicitly provide this evidence
with the fMapEq calls.

##### Proof Reuse in Context

Finally, we use the posDom proof (§4.2) to show how existing proofs can be
reused with map.

⬇

client :: xs:[Pos] $\rightarrow$ PEq [Integer] {map incrInt xs} {map incrPos
xs}

client = mapEq incrInt incrPos posDom

clientP :: PEq ([Pos] $\rightarrow$ [Integer]) {map incrInt} {map incrPos}

clientP = mapEqP incrInt incrPos posDom

client proves that map incrInt xs is equivalent to map incrPos xs for each
list xs of positive numbers, while clientP proves that the partially applied
functions map incrInt and map incrPos are equivalent on the domain of lists of
positive numbers.

###  4.4. Fold: Equality of Multi-Argument Functions

As an example of equality proofs on multi-argument functions, we show that the
directly tail-recursive foldl is equal to foldl’, a foldr encoding of a left-
fold via CPS. The first-order equivalence theorem is expressed as follows:

⬇

thm :: f:(b $\rightarrow$ a $\rightarrow$ b) $\rightarrow$ b:b $\rightarrow$
xs:[a] $\rightarrow$ { foldl f b xs = foldl’ f b xs }

We lifted the first-order property into a multi-argument function equality by
using XEq for all but the last arguments and BEq for the last, as below:

⬇

foldEq :: AEq b $\Rightarrow$ PEq ((b $\rightarrow$ a $\rightarrow$ b)
$\rightarrow$ b $\rightarrow$ [a] $\rightarrow$ b) {foldl} {foldl’}

foldEq = XEq foldl foldl’ $\$$ \f $\rightarrow$

XEq (foldl f) (foldl’ f) $\$$ \b $\rightarrow$

XEq (foldl f b) (foldl’ f b) $\$$ \xs $\rightarrow$

BEq (foldl f b xs) (foldl’ f b xs)

(thm f b xs ? reflP (foldl f b xs))

One can avoid the first-order proof and the AEq constraint, by using the
second, typeclass-oriented style of §4.1, (see supplementary material (2021)
for details).

###  4.5. Spec: Function Equality for Program Efficiency

Function equality can be used to prove optimizations sound. For example,
consider a critical function that, for safety, can only run on inputs that
satisfy a specification spec, and fastSpec, a fast implementation to check
spec.

⬇

spec, fastSpec :: a $\rightarrow$ Bool

critical :: x:{ a | spec x } $\rightarrow$ a

A client function can soundly call critical for any input x by performing the
runtime fastSpec x check, given a PEq proof that the functions fastSpec and
spec are equal.

⬇

client :: PEq (a $\rightarrow$ Bool) {fastSpec} {spec} $\rightarrow$ a
$\rightarrow$ Maybe a

client pf x =

if fastSpec x ? toSMT (fastSpec x) (spec x) (CEq fastSpec spec pf (\x f
$\rightarrow$ f x))

then Just (critical x)

else Nothing

The toSMT call generates the SMT equality that fastSpec x = spec x, which,
combined with the branch condition check fastSpec x, lets the path-sensitive
refinement type checker decide that the call to critical x is safe in the then
branch.

Our propositional equality (1) co-exists with practical features of refinement
types, e.g., path sensitivity, and (2) can help optimize executable code.

###  4.6. Monoid Laws for Endofunctions

Endofunctions form a law-abiding monoid. A function $f$ is an _endofunction_
when its domain and codomain types are the same. A _monoid_ is an algebraic
structure comprising an identity element (mempty) and an associative operation
(mappend). For the monoid of endofunctions, mempty is the identity function
and mappend is function composition (Figure 4; top).

Monoid Instance for Endofunctions

⬇

type Endo a = a $\rightarrow$ a

mempty :: Endo a

mempty a = a

⬇

_ =~= y = y

mappend :: Endo a $\rightarrow$ Endo a $\rightarrow$ Endo a

mappend f g a = f (g a) \-- a/k/a (<>)

Endofunction Monoid Laws

⬇

mLeftIdentity :: (Reflexivity a, Transitivity a)

$\Rightarrow$ x:Endo a $\rightarrow$ PEq (Endo a) {mappend mempty x} {x}

mRightIdentity :: (Reflexivity a, Transitivity a)

$\Rightarrow$ x:Endo a $\rightarrow$ PEq (Endo a) {x} {mappend x mempty}

mAssociativity :: (Reflexivity a, Transitivity a)

$\Rightarrow$ x:(Endo a) $\rightarrow$ y:(Endo a) $\rightarrow$ z:(Endo a)

$\rightarrow$ PEq (Endo a) {mappend (mappend x y) z} {mappend x (mappend y z)}

Proofs By Reflexivity and Transitivity

⬇

mLeftIdentity x = XEq (mappend mempty x) x $\$$ \a $\rightarrow$

refl (mappend mempty x a) ? (mappend mempty x a =~= mempty (x a) =~= x a ***
QED)

mRightIdentity x = XEq x (mappend x mempty) $\$$ \a $\rightarrow$

refl (x a) ? (x a =~= x (mempty a) =~= mappend x mempty a *** QED)

mAssociativity x y z =

XEq (mappend (mappend x y) z) (mappend x (mappend y z)) $\$$ \a $\rightarrow$

refl (mappend (mappend x y) z a) ?

(mappend (mappend x y) z a =~= (mappend x y) (z a) =~= x (y (z a))

=~= x (mappend y z a)

=~= mappend x (mappend y z) a *** QED)

Figure 4. Case study: Endofunction Monoid Proofs.

To be a monoid, mempty must really be an identity with respect to mappend
(mLeftIdentity and mRightIdentity) and mappend must really be associative
(mAssociativity) (Figure 4; middle).

Proving the monoid laws for endofunctions demands functional extensionality
(Figure 4; bottom). For example, consider the proof that mempty is a left
identity for mappend, i.e., mappend mempty x = x. To prove this equation
between _functions_ , we can’t use SMT equality. With functional
extensionality, each proof reduces to three parts: XEq to take an input of
type a; reflon the left-hand side of the equation, to generate an equality
proof; and (=~=) to give unfolding hints to the SMT solver. The (=~=) operator
is defined as _ =~= y = y, and it is unrefined, i.e., it is not checking
equality of its arguments.

The Reflexivity constraints on the theorems make our proofs general in the
underlying type a: endofunctions on the type a form a monoid whether a admits
SMT equality or if it’s a complex higher-order type (whose ultimate result
admits equality). Haskell’s typeclass resolution ensures that an appropriate
refl method will be constructed whatever type a happens to be.

###  4.7. Monad Laws for Reader Monads

A _reader_ is a function with a fixed domain r, i.e., the partially applied
type Reader r (Figure 5, top left). Readers form a monad and their composition
is a useful way of defining and composing functions that take some fixed
information, like command-line arguments or configuration files. Our
propositional equality can prove the monad laws for readers.

Monad Instance for Readers ⬇ type Reader r a = r $\rightarrow$ a kleisli :: (a
$\rightarrow$ Reader r b) $\rightarrow$ (b $\rightarrow$ Reader r c)
$\rightarrow$ a $\rightarrow$ Reader r c kleisli f g x = bind (f x) g ⬇ pure
:: a $\rightarrow$ Reader r a pure a _r = a bind :: Reader r a $\rightarrow$
(a $\rightarrow$ Reader r b) $\rightarrow$ Reader r b bind fra farb = \r
$\rightarrow$ farb (fra r) r

Reader Monad Laws

⬇

monadLeftIdentity :: Reflexivity b $\Rightarrow$ a:a

$\rightarrow$ f:(a $\rightarrow$ Reader r b) $\rightarrow$ PEq (Reader r b)
{bind (pure a) f} {f a}

monadRightIdentity :: Reflexivity a

$\Rightarrow$ m:(Reader r a) $\rightarrow$ PEq (Reader r a) {bind m pure} {m}

monadAssociativity :: (Reflexivity c, Transitivity c)

$\Rightarrow$ m:(Reader r a) $\rightarrow$ f:(a $\rightarrow$ Reader r b)
$\rightarrow$ g:(b $\rightarrow$ Reader r c)

$\rightarrow$ PEq (Reader r c) {bind (bind m f) g} {bind m (kleisli f g)}

Identity Proofs By Reflexivity ⬇ monadLeftIdentity a f = XEq (bind (pure a) f)
(f a) $\$$ \r $\rightarrow$ refl (bind (pure a) f r) ? (bind (pure a) f r =~=
f (pure a r) r =~= f a r *** QED) ⬇ monadRightIdentity m = XEq (bind m pure) m
$\$$ \r $\rightarrow$ refl (bind m pure r) ? (bind m pure r =~= pure (m r) r
=~= m r *** QED) Associativity Proof By Transitivity and Reflexivity

⬇

monadAssociativity m f g = XEq (bind (bind m f) g) (bind m (kleisli f g)) $\$$
\r $\rightarrow$

let { el = bind (bind m f) g r ; eml = g (bind m f r) r ; em = (bind (f (m r))
g) r

; emr = kleisli f g (m r) r ; er = bind m (kleisli f g) r }

in trans el em er (trans el eml em (refl el) (refl eml))

(trans em emr er (refl em) (refl emr))

Figure 5. Case study: Reader Monad Proofs.

The monad instance for the reader type is defined using function composition
(Figure 5, top). We also define Kleisli composition of monads as a convenience
for specifying the monad. We prove that readers are in fact monads, i.e.,
their operations satisfy the monad laws (Figure 5, bottom). We also prove that
they satisfy the functor and applicative laws in supplementary material
(2021). The reader monad laws are expressed as refinement type specifications
using PEq. We prove the left and right identities following the pattern of
§4.6, i.e., XEq, followed by reflexivity with (=~=) for function unfolding
(Figure 5, middle). We use transitivity to conduct the more complicated proof
of associativity (Figure 5, bottom).

##### Proof by Associativity and Error Locality

As noted earlier, the use of (=~=) in proofs by reflexivity is not checking
intermediate equational steps. So, the proof either succeeds or fails without
explanation. To address this problem, during proof construction, we employed
transitivity. For instance, in the monadAssociativity proof, our goal is to
construct the proof PEq _ {el} {er}. To do so, we pick an intermediate term
em; we might attempt an equivalence proof as follows:

⬇

trans el em er

(refl el) \-- proof of el = em; local error

(trans em emr er \-- proof of em = er

(refl em) \-- proof of em = emr

(refl emr)) \-- proof of emr = er

The refl el proof will produce a type error; replacing that proof with an
appropriate trans to connect el and em via eml completes the
monadAssociativity proof (Figure 5, bottom). Writing proofs in this trans/refl
style works well: start with refl and where the SMT solver can’t figure things
out, a local refinement type error tells you to expand with trans (or look for
a counterexample).

Our reader proofs use the Reflexivity and Transitivity typeclasses to ensure
that readers are monads whatever the return type a may be (with the type of
‘read’ values fixed to r). Having generic monad laws is critical: readers are
typically used to compose functions that take configuration information, but
such functions usually have other arguments, too! For example, an interpreter
might run readFile >>= parse >>= eval, where readFile :: Config $\rightarrow$
String and parse :: String $\rightarrow$ Config $\rightarrow$ Expr and eval ::
Expr $\rightarrow$ Config $\rightarrow$ Value. With our generic proof of
associativity, we can rewrite the above to readFile >>= (kleisli parse eval)
even though parse and eval are higher-order terms without Eq instances. Doing
so could, in theory, trigger inlining/fusion rules that would combine the
parser and the interpreter.

##  5\. Type Checking XEq: Did We Get It Right?

We’ve seen that XEq is effective at proving equalities between functions (§4)
and we’ve argued that we avoid the inconsistency with funext. Things _seem_ to
work in Liquid Haskell. But: Why do things go so wrong with funext? Does XEq
really avoid funext’s issues? We give a schematic example showing why Liquid
Haskell works with XEq consistently but works with funext inconsistently. (We
give a detailed, formal model of our propositional equality in §6.)

Suppose we have two functions h and k, defined on domains $d_{\texttt{h}}$ and
$d_{\texttt{k}}$ and codomains $r_{\texttt{h}}$ and $r_{\texttt{k}}$,
respectively. Let’s also assume we have some lemma that proves, for all $x$ in
some domain $d_{p}$, we have an equality $e_{l}\backsimeq e_{r}$, where
$e_{l}$ and $e_{r}$ are arbitrary expressions of type {v:$\beta$ $\mid$
$r_{p}$}.

⬇

h :: x:{$\alpha$ | $d_{\texttt{h}}$} $\rightarrow$ {v:$\beta$ | $r_{\texttt{h}}$}

k :: x:{$\alpha$ | $d_{\texttt{k}}$} $\rightarrow$ {v:$\beta$ | $r_{\texttt{k}}$}

lemma :: x:{$\alpha$ | $d_{p}$} $\rightarrow$ PEq {v:$\beta$ | $r_{p}$} {$e_{l}$} {$e_{r}$}

We can pass these along to our XEq constructor (of §3) to form a proof that h
equals k on some domain $d_{e}$:

⬇

XEq h k lemma :: PEq ({v:$\alpha$ | $d_{e}$} $\rightarrow$ {v:$\beta$ | $r_{e}$}) {h} {k}

When type checking this use of XEq, we need to check that the lemma equates
the right expressions (i.e., forall $x$. $e_{l}\backsimeq e_{r}$ implies
$\texttt{h}\ x\backsimeq\texttt{k}\ x$). Critically, type checking must also
ensure that the final equality domain ($d_{e}$) is stronger than the domains
for the functions ($d_{\texttt{h}}$, $d_{\texttt{k}}$) and for the lemma
($d_{p}$).

Typing Environmennt

$\begin{array}[]{rcll}\Gamma&\doteq&\\{&\texttt{XEq}:\forall\alpha\beta.f:(\alpha\rightarrow\beta)\rightarrow
g:(\alpha\rightarrow\beta)\rightarrow(x:\alpha\rightarrow\texttt{PEq}\
\beta\\{f\ x\\}\\{g\ x\\})\rightarrow\texttt{PEq}\
(\alpha\rightarrow\beta)\\{f\\}\\{g\\}\\\
&&,&\texttt{h}:x:\\{\\!\mid\\!\\!{d_{\texttt{h}}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{r_{\texttt{h}}}\\!\\!\mid\\!\\},\texttt{k}:x:\\{\\!\mid\\!\\!{d_{\texttt{k}}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{r_{\texttt{k}}}\\!\\!\mid\\!\\},\texttt{lemma}:x:\\{\\!\mid\\!\\!{d_{p}}\\!\\!\mid\\!\\}\rightarrow\texttt{PEq}\
\\{\\!\mid\\!\\!{r_{p}}\\!\\!\mid\\!\\}\\{e_{l}\\}\\{e_{r}\\}\quad\\}\\\
\end{array}$

Type Checking

$\begin{array}[]{l}1.\Gamma\vdash\texttt{XEq}\mathrel{\text{::}}\forall\alpha\beta.{f}\text{:}({\alpha}\\!\rightarrow\\!{\beta})\rightarrow{g}\text{:}({\alpha}\\!\rightarrow\\!{\beta})\rightarrow({x}\text{:}{\alpha}\\!\rightarrow\\!{\texttt{PEq}\
\beta\ \\{f\ x\\}\\{g\ x\\})}\rightarrow\texttt{PEq}\
(\alpha\rightarrow\beta)\\{f\\}\\{g\\}\\\ \hline\cr
2.\Gamma\vdash\texttt{XEq}\
@\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\mathrel{\text{::}}\forall\beta.{f}\text{:}({\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\\!\rightarrow\\!{\beta})\rightarrow{g}\text{:}({\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\\!\rightarrow\\!{\beta})\rightarrow({x}\text{:}{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\\!\rightarrow\\!{\texttt{PEq}\
\beta\ \\{f\ x\\}\\{g\ x\\})}\rightarrow\texttt{PEq}\
(\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\beta)\\{f\\}\\{g\\}\\\
\hline\cr 3.\Gamma\vdash\texttt{XEq}\
@\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\
@\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}\mathrel{\text{::}}{f}\text{:}({\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\\!\rightarrow\\!{\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}})\rightarrow{g}\text{:}({\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\\!\rightarrow\\!{\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}})\rightarrow({x}\text{:}{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\\!\rightarrow\\!{\texttt{PEq}\
\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}\ \\{f\ x\\}\\{g\
x\\})}\rightarrow\texttt{PEq}\
(\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\})\\{f\\}\\{g\\}\\\
\hline\cr 4.\Gamma\vdash\texttt{XEq}\
@\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\
@\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}\
\texttt{h}\mathrel{\text{::}}g:(\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\})\rightarrow(x\colon\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\texttt{PEq}\
\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}\\{\texttt{h}\ x\\}\\{g\
x\\})\rightarrow\texttt{PEq}\
(\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\})\\{\texttt{h}\\}\\{g\\}\quad{\framebox{$\textsc{Sub-H}$}}\\\
\hline\cr 5.\Gamma\vdash\texttt{XEq}\
@\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\
@\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}\ \texttt{h}\
\texttt{k}\mathrel{\text{::}}(x:\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\texttt{PEq}\
\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}\\{\texttt{h}\
x\\}\\{\texttt{k}\ x\\})\rightarrow\texttt{PEq}\
(\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\})\\{\texttt{h}\\}\\{\texttt{k}\\}\quad{\framebox{$\textsc{Sub-K}$}}\\\
\hline\cr 6.\Gamma\vdash\texttt{XEq}\
@\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\
@\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}\ \texttt{h}\ \texttt{k}\
\texttt{lemma}{}\mathrel{\text{::}}\texttt{PEq}\
(\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\})\\{\texttt{h}\\}\\{\texttt{k}\\}\quad{\framebox{$\textsc{Sub-L}$}}\\\
\hline\cr 7.\Gamma\vdash\texttt{XEq}\
@\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\
@\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}\ \texttt{h}\ \texttt{k}\
\texttt{lemma}{}\mathrel{\text{::}}\texttt{PEq}\
(\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\})\\{\texttt{h}\\}\\{\texttt{k}\\}\quad{\framebox{$\textsc{Sub-
Sub}$}}\\\ \hline\cr 8.\Gamma\vdash\texttt{XEq}\
@\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\
@\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}\ \texttt{h}\ \texttt{k}\
\texttt{lemma}\mathrel{\text{::}}\texttt{PEq}\
(\\{\\!\mid\\!\\!{d_{e}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{r_{e}}\\!\\!\mid\\!\\})\\{\texttt{h}\\}\\{\texttt{k}\\}\\\
\end{array}$

Subtyping Derivation Leaves

i. $\kappa_{\alpha}$ ⇒$d_{\texttt{h}}$
${\Gamma}\vdash{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\ \preceq\
{\\{\\!\mid\\!\\!{d_{\texttt{h}}}\\!\\!\mid\\!\\}}$ & $\kappa_{\alpha}$
⇒$r_{\texttt{h}}$ ⇒$\kappa_{\beta}$
${\Gamma,x:\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\vdash{\\{\\!\mid\\!\\!{r_{\texttt{h}}}\\!\\!\mid\\!\\}}\
\preceq\ {\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}}$
${\Gamma}\vdash{x:\\{\\!\mid\\!\\!{d_{\texttt{h}}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{r_{\texttt{h}}}\\!\\!\mid\\!\\}}\
\preceq\
{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}}$
[Sub-H ] ii. $\kappa_{\alpha}$ ⇒$d_{\texttt{k}}$
${\Gamma}\vdash{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\ \preceq\
{\\{\\!\mid\\!\\!{d_{\texttt{k}}}\\!\\!\mid\\!\\}}$ & $\kappa_{\alpha}$
⇒$r_{\texttt{k}}$ ⇒$\kappa_{\beta}$
${\Gamma,x:\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\vdash{\\{\\!\mid\\!\\!{r_{\texttt{k}}}\\!\\!\mid\\!\\}}\
\preceq\ {\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}}$
${\Gamma}\vdash{x:\\{\\!\mid\\!\\!{d_{\texttt{k}}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{r_{\texttt{k}}}\\!\\!\mid\\!\\}}\
\preceq\
{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}}$
[Sub-K ]

iii. $\kappa_{\alpha}$ ⇒$d_{p}$
${\Gamma}\vdash{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\ \preceq\
{\\{\\!\mid\\!\\!{d_{p}}\\!\\!\mid\\!\\}}$ & $\kappa_{\alpha}$ ⇒r_p
⇒$\kappa_{\beta}$
${\Gamma,x:\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\vdash{\\{\\!\mid\\!\\!{r_{p}}\\!\\!\mid\\!\\}}\
\preceq\ {\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}}$ $\kappa_{\alpha}$
⇒$\kappa_{\beta}$ ⇒r_p
${\Gamma,x:\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\vdash{\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}}\
\preceq\ {\\{\\!\mid\\!\\!{r_{p}}\\!\\!\mid\\!\\}}$ iv. $\kappa_{\alpha}$
⇒$e_{l}\backsimeq e_{r}$ ⇒$\texttt{h}\ x\backsimeq\texttt{k}\ x$
${\Gamma,x:\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\vdash{\texttt{PEq}\
\\{\\!\mid\\!\\!{r_{p}}\\!\\!\mid\\!\\}\\{e_{l}\\}\\{e_{r}\\}}\ \preceq\
{\texttt{PEq}\ \\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}\\{\texttt{h}\
x\\}\\{\texttt{k}\ x\\}}$
${\Gamma}\vdash{x:\\{\\!\mid\\!\\!{d_{p}}\\!\\!\mid\\!\\}\rightarrow\texttt{PEq}\
\\{\\!\mid\\!\\!{r_{p}}\\!\\!\mid\\!\\}\\{e_{l}\\}\\{e_{r}\\}}\ \preceq\
{x:\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\texttt{PEq}\
\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}\\{\texttt{h}\
x\\}\\{\texttt{k}\ x\\}}$ [Sub-L ]

vi. $d_{e}$ ⇒$\kappa_{\alpha}$
${\Gamma}\vdash{\\{\\!\mid\\!\\!{d_{e}}\\!\\!\mid\\!\\}}\ \preceq\
{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}$ & $\kappa_{\alpha}$
⇒$\kappa_{\beta}$ ⇒r_e
${\Gamma,x:\\{\\!\mid\\!\\!{d_{e}}\\!\\!\mid\\!\\}}\vdash{\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}}\
\preceq\ {\\{\\!\mid\\!\\!{r_{e}}\\!\\!\mid\\!\\}}$
${\Gamma}\vdash{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}}\
\preceq\
{\\{\\!\mid\\!\\!{d_{e}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{r_{e}}\\!\\!\mid\\!\\}}$
& v. $\kappa_{\alpha}$ ⇒$d_{e}$
${\Gamma}\vdash{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\ \preceq\
{\\{\\!\mid\\!\\!{d_{e}}\\!\\!\mid\\!\\}}$ $\kappa_{\alpha}$ ⇒r_e
⇒$\kappa_{\beta}$
${\Gamma,x:\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\vdash{\\{\\!\mid\\!\\!{r_{e}}\\!\\!\mid\\!\\}}\
\preceq\ {\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}}$
${\Gamma}\vdash{\\{\\!\mid\\!\\!{d_{e}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{r_{e}}\\!\\!\mid\\!\\}}\
\preceq\
{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}}$
$\texttt{h}\backsimeq\texttt{k}$ ⇒$\texttt{h}\backsimeq\texttt{k}$
${\Gamma}\vdash{\texttt{PEq}\
(\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\})\\{\texttt{h}\\}\\{\texttt{k}\\}}\
\preceq\ {\texttt{PEq}\
(\\{\\!\mid\\!\\!{d_{e}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{r_{e}}\\!\\!\mid\\!\\})\\{\texttt{h}\\}\\{\texttt{k}\\}}$
[Sub-Sub ]

Figure 6. Type checking XEq h k lemma. For space, we write
$\\{\\!\mid\\!\\!{d}\\!\\!\mid\\!\\}$ to mean the refined type
$\\{{v}:{t}\mid{d}\\}$.

Liquid Haskell goes through a complex series of steps to enforce both required
checks (Figure 6). We haven’t modified Liquid Haskell’s typing rules or
implementation _at all_ ; we merely defined PEq in such a way that the
existing type checking rules in Liquid Haskell implement the right checks to
soundly show extensional equality between functions.

It’s easiest to understand how type checking works from top to bottom (“Type
Checking”, Figure 6). First, we look up XEq’s type in the environment (1).
Since the XEq is polymorphic, we instantiate the type arguments with the
types, $\\{{v}:{\alpha}\mid{\kappa_{\alpha}}\\}$ (2) and
$\\{{v}:{\beta}\mid{\kappa_{\beta}}\\}$ (3). (We write
$\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}$ as a short for
$\\{{v}:{\alpha}\mid{\kappa_{\alpha}}\\}$, since we focus on the refinements
assuming the Haskell types match.) Here $\kappa_{\alpha}$ and $\kappa_{\beta}$
are refinement type variables; type checking will generate constraints on them
that liquid type inference will try to resolve (Rondon et al., 2008). Next we
apply each of the arguments: h (4), k (5), and lemma (6). Each application
applies standard dependent function application, with consideration for
subtyping. That is, each application (a) substitutes the applied argument in
the codomain type and (b) checks that the type of the argument is a subtype of
the function’s domain type. Application leads to the subtyping constraints
Sub-H, Sub-K, and Sub-L set off in boxes, resolved below. Now Liquid Haskell
has inferred a type for the checked expression (7). To conclude the check, it
introduces the final subtype constraint Sub-Sub: the inferred type should be a
subtype of the type the user specified (8).

The four instances of subtyping during type checking generate 13 logical
implications to resolve for the original expression to type check (“Subtyping
Derivation Leaves”, Figure 6). The six purple implications with Roman numerals
place requirements on the domain; we’ll ignore the others, which impose less
interesting constraints on the functions’ codomains. The Sub-H and Sub-K
derivations require (via contravariance) that the refinement variable
$\kappa_{\alpha}$ implies the refinements on the functions’ domains,
$d_{\texttt{h}}$ and $d_{\texttt{k}}$. Similarly, the derivation Sub-L
requires that $\kappa_{\alpha}$ implies the proof domain $d_{p}$. Since PEq is
defined as refined type alias (§3), Sub-L also checks that the refinements
given imply the top level refinements of PEq, i.e., that the result of the
lemma is sufficient to show XEq’s precondition. The Sub-Sub derivation checks
subtyping of two PEq types, by treating the type arguments _invariantly_. (We
mark covariant implications in red and contravariant implications in blue.)
Liquid Haskell treats checks invariantly because PEq’s definition uses its
type parameter in both positive and negative positions. Sub-Sub will
ultimately require that the refinement variable $\kappa_{\alpha}$ is
_equivalent_ to the equality domain $d_{e}$.

To sum up, type checking imposes the following six implications as
constraints:

$\begin{array}[]{r@{\quad}lr<EMAIL_ADDRESS>d_{\texttt{h}}&ii.&\kappa_{\alpha}\Rightarrow
d_{\texttt{k}}&iii.&\kappa_{\alpha}\Rightarrow d_{p}\\\
iv.&\kappa_{\alpha}\Rightarrow e_{l}\backsimeq e_{r}\Rightarrow\texttt{h}\
x\backsimeq\texttt{k}\ x&v.&\kappa_{\alpha}\Rightarrow
d_{e}&vi.&d_{e}\Rightarrow\kappa_{\alpha}\\\ \end{array}$

Implications _v_ and _vi_ require the refinement variable $\kappa_{\alpha}$ to
be equivalent to the equality domain $d_{e}$. Given that equality,
implications _i_ – _iii_ state that the equality domain $d_{e}$ should imply
the domains of the functions (_i_ and _ii_) and lemma (_iii_). Implication
_iv_ requires that the lemma’s domain implies equality of the two functions
for each argument x that satisfies the domain $d_{e}$. All together, these
constraints exactly capture the requirements of functional extensionality.

##### Naive Functional Extensionality with funext

When, in §2, we use the non-type-indexed funext in Liquid Haskell, the typing
derivation looks almost exactly the same, but one critical thing changes: the
type-indexed PEq t {$e_{l}$} {$e_{r}$} is replaced by a refined unit {v:()
$\mid$ $e_{l}$ = $e_{r}$}. This only affects the Sub-L and Sub-Sub
derivations, which lose the red and blue parts and become:

$\inference{\inference{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}{iii}^{\prime}.\
\kappa_{\alpha}\Rightarrow
d_{p}}}{{\Gamma}\vdash{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\
\preceq\
{\\{\\!\mid\\!\\!{d_{p}}\\!\\!\mid\\!\\}}}&\inference{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}{iv}^{\prime}.\
\kappa_{\alpha}\Rightarrow e_{l}=e_{r}\Rightarrow h\ x=k\
x}}{{\Gamma,x:\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\vdash{\\{{v}:{\texttt{()}}\mid{e_{l}=e_{r}}\\}}\
\preceq\ {\\{{v}:{\texttt{()}}\mid{h\ x=k\
x}\\}}}}{{\Gamma}\vdash{{x}\text{:}{\\{\\!\mid\\!\\!{d_{p}}\\!\\!\mid\\!\\}}\\!\rightarrow\\!{\\{{v}:{\texttt{()}}\mid{e_{l}=e_{r}}\\}}}\
\preceq\
{{x}\text{:}{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\\!\rightarrow\\!{\\{{v}:{\texttt{()}}\mid{h\
x=k\ x}\\}}}}[\textsc{Sub-L}-\textsc{Naive}]$ $\inference{h\ x=k\ x\Rightarrow
h\ x=k\ x}{{\Gamma}\vdash{\\{{v}:{\texttt{()}}\mid{h\ x=k\ x}\\}}\ \preceq\
{\\{{v}:{\texttt{()}}\mid{h\ x=k\ x}\\}}}[\textsc{Sub-Sub}-\textsc{Naive}]$

Sub-L-Naive generates the implications ${iii}^{\prime}$ and ${iv}^{\prime}$
that are essentially the same as before. But, Sub-Sub-Naive won’t generate any
meaningful checks, because equality is just a unit type. We lost implications
${v}$ and ${vi}$! We are now left with an implication system in which the
refinement variable $\kappa_{\alpha}$ only appears in the assumptions. Since
Liquid Haskell always tries to infer the most specific refinement possible, it
will find a very specific refinement for $\kappa_{\alpha}$: false! Having
inferred false for $\kappa_{\alpha}$, the entire use of funext trivially holds
and can be used on other, nontrivial domains—with inconsistent results.

##  6\. A Refinement Calculus with Built-in Type-Indexed Equality

Because funext is inconsistent in Liquid Haskell (§2), we developed PEq to
reason consistently about extensional equality, using the GADT PBEq and the
uninterpreted equality PEq (§3). We’re able to prove some interesting
equalities (§4) and Liquid Haskell’s type checking seems to be doing the right
thing (§5). But how do we know that our definitions suffice? Formalizing _all_
of Liquid Haskell is a challenge, but we can build a model to check the
features we use. We formalize a core calculus $\lambda^{RE}$ with $R$efinement
types, semantic subtyping, and type-indexed propositional $E$quality.

$\lambda^{RE}$ contains just enough to check the core interactions between
refinement types and a type-indexed propositional equality resembling our PBEq
definition (§6.1). We omit plenty of important features from Liquid Haskell
(e.g., algebraic data types): our purpose here is not to develop a complete
formal model, but to check that our implementation holds together.

Using $\lambda^{RE}$’s static semantics (§6.2), we prove several metatheorems
(§6.3). Most importantly, we define a logical relation that characterizes
$\lambda^{RE}$ equivalence and reflects $\lambda^{RE}$’s propositional
equality. Propositional equivalence in $\lambda^{RE}$ implies equivalence in
the logical relation (Theorem 6.2); both are reflexive, symmetric, and
transitive (Theorems 6.3 and 6.4).

###  6.1. Syntax and Semantics of $\lambda^{RE}$

$\begin{array}[]{rrcl}\textit{Constants}&c&::=&\texttt{true}\mid\texttt{false}\mid\texttt{unit}\mid(==_{b})\mid(==_{(c,b)})\\\\[2.84526pt]
\textit{Expressions}&e&::=&c\mid x\mid e\ e\mid\lambda
x\mathord{:}\tau.~{}e\mid\texttt{bEq}_{b}\ e\ e\ e\ \mid\
\texttt{xEq}_{{x}\text{:}{\tau}\rightarrow\tau}\ e\ e\ e\\\\[2.84526pt]
\textit{Values}&v&::=&c\mid\lambda x\mathord{:}\tau.~{}e\mid\texttt{bEq}_{b}\
e\ e\ v\ \mid\ \texttt{xEq}_{{x}\text{:}{\tau}\rightarrow\tau}\ e\ e\
v\\\\[2.84526pt] \textit{Refinements}&r&::=&e\\\\[2.84526pt] \textit{Basic
Types}&b&::=&\texttt{Bool}\mid\texttt{()}\\\\[2.84526pt]
\textit{Types}&\tau&::=&\\{{x}\text{:}{b}\mid{r}\\}\mid{x}\text{:}{\tau}\rightarrow\tau\mid\texttt{PEq}_{\tau}\
\\{e\\}\ \\{e\\}\\\\[2.84526pt] \textit{Typing
Environment}&\Gamma&::=&\emptyset\mid\Gamma,x:\tau\\\\[2.84526pt]
\textit{Closing Substitutions}&\theta&::=&\emptyset\mid\theta,x\mapsto
v\\\\[2.84526pt] \textit{Equivalence
Environments}&\delta&::=&\emptyset\mid\delta,(v,v)/x\\\\[2.84526pt]
\textit{Evaluation Contexts}&\mathcal{E}&::=&\bullet\mid\mathcal{E}\ e\mid v\
\mathcal{E}\mid\texttt{bEq}_{b}\ e\ e\
\mathcal{E}\mid\texttt{xEq}_{{x}\text{:}{\tau}\rightarrow\tau}\ e\ e\
\mathcal{E}\\\\[2.84526pt] \end{array}$

Reduction $e\hookrightarrow e$

$\begin{array}[]{rcll}\mathcal{E}[e]&\hookrightarrow&\mathcal{E}[e^{\prime}],&\text{if}\
e\hookrightarrow e^{\prime}\\\ (\lambda x\mathord{:}\tau.~{}e)\
v&\hookrightarrow&e[v/x]&\\\ (==_{b})\
c_{1}&\hookrightarrow&(==_{(c_{1},b)})&\\\ (==_{(c_{1},b)})\
c_{2}&\hookrightarrow&c_{1}=c_{2},&\textit{syntactic equality on constants}\\\
\end{array}$

Figure 7. Syntax and Dynamic Semantics of $\lambda^{RE}$.

We present $\lambda^{RE}$, a core calculus with $R$efinement types and type-
indexed $E$quality (Figure 7).

##### Expressions

$\lambda^{RE}$ expressions include constants (booleans, unit, and equality
operations on base types), variables, lambda abstraction, and application.
There are also two primitives to prove propositional equality:
$\texttt{bEq}_{b}$ and $\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}$
construct proofs of equality at base and function types, respectively.
Equality proofs take three arguments: the two expressions equated and a proof
of their equality; proofs at base type are trivial, of type (), but higher
types use functional extensionality. These two primitives correspond to BEq
and XEq constructors of §3; we did not encode congruence closure since it can
be proved by induction on expressions, which is impossible in Haskell.

##### Values

The values of $\lambda^{RE}$ are constants, functions, and equality proofs
with converged proofs.

##### Types

$\lambda^{RE}$’s _basic types_ are booleans and unit. Basic types are refined
with boolean expressions $r$ in _refinement types_
$\\{{x}\text{:}{b}\mid{r}\\}$, which denote all expressions of base type $b$
that satisfy the refinement $r$. In addition to refinements, $\lambda^{RE}$’s
types also include _dependent function types_
${x}\text{:}{\tau_{x}}\rightarrow\tau$ with arguments of type $\tau_{x}$ and
result type $\tau$, where $\tau$ can refer back to the argument $x$. Finally,
types include our _propositional equality_ $\texttt{PEq}_{\tau}\ \\{e_{1}\\}\
\\{e_{2}\\}$, which denotes a proof of equality between the two expressions
$e_{1}$ and $e_{2}$ of type $\tau$. We write $b$ to mean the trivial
refinement type $\\{{x}\text{:}{b}\mid{\texttt{true}}\\}$. We omit polymorphic
types to avoid known and resolved metatheoretical problems (Sekiyama et al.,
2017). Yet, xEq equality primitive is defined as a family of operators, one
for each refinement function type, capturing the essence of polymorphic
function equality.

##### Environments

The typing environment $\Gamma$ binds variables to types, the (semantic
typing) closing substitution $\theta$ binds variables to values, and the
(logical relation) pending substitution $\delta$ binds variables to pairs of
equivalent values.

##### Runtime Semantics

The relation $\cdot\hookrightarrow\cdot$ evaluates $\lambda^{RE}$ expressions
using contextual, small step, call-by-value semantics (Figure 7, bottom). The
semantics are standard with $\texttt{bEq}_{b}$ and
$\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}$ evaluating proofs but
not the equated terms. Let $\cdot\hookrightarrow^{*}\cdot$ be the reflexive,
transitive closure of $\cdot\hookrightarrow\cdot$.

##### Type Interpretations

$\begin{array}[]{rcr@{~}c@{~}l}\left[\\!\left|\\{{x}\text{:}{b}\mid{r}\\}\right|\\!\right]&\doteq&\\{e~{}&\mid\hfil~{}&\
e\hookrightarrow^{*}v\wedge\vdash_{B}e\,\mathrel{::}\,b\wedge
r[e/x]\hookrightarrow^{*}\texttt{true}\\}\\\
\left[\\!\left|{x}\text{:}{\tau_{x}}\rightarrow\tau\right|\\!\right]&\doteq&\\{e~{}&\mid\hfil~{}&\forall
e_{x}\in\left[\\!\left|\tau_{x}\right|\\!\right]\\!.\ e\
e_{x}\in\left[\\!\left|\tau[e_{x}/x]\right|\\!\right]\\}\\\
\left[\\!\left|\texttt{PEq}_{b}\ \\{e_{l}\\}\
\\{e_{r}\\}\right|\\!\right]&\doteq&\\{e~{}&\mid\hfil~{}&\
\vdash_{B}e\,\mathrel{::}\,\texttt{PBEq}_{b}\wedge
e\hookrightarrow^{*}\texttt{bEq}_{b}\ {e_{l}}\ {e_{r}}\ {e_{pf}}\wedge
e_{l}==_{b}e_{r}\hookrightarrow^{*}\texttt{true}\\}\\\
\left[\\!\left|\texttt{PEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\
\\{e_{l}\\}\ \\{e_{r}\\}\right|\\!\right]&\doteq&\\{e~{}&\mid\hfil~{}&\
\vdash_{B}e\,\mathrel{::}\,\texttt{PBEq}_{\lfloor{x}\text{:}{\tau_{x}}\rightarrow\tau\rfloor}\wedge
e\hookrightarrow^{*}\texttt{xEq}_{\\_}\ {e_{l}}\ {e_{r}}\ {e_{pf}}\\\
&&~{}&\wedge\hfil~{}&e_{l},e_{r}\in\left[\\!\left|{x}\text{:}{\tau_{x}}\rightarrow\tau\right|\\!\right]\wedge\forall
e_{x}\in\left[\\!\left|\tau_{x}\right|\\!\right].e_{pf}\
e_{x}\in\left[\\!\left|\texttt{PEq}_{\tau[e_{x}/x]}\ \\{e_{l}\ e_{x}\\}\
\\{e_{r}\ e_{x}\\}\right|\\!\right]\\}\\\ \end{array}$ Figure 8. Semantic
typing: a unary syntactic logical relation interprets types.

Semantic typing uses a unary logical relation to interpret types in a
syntactic term model (closed terms, Figure 8; open terms, Figure 9).

The interpretation of the base type $\\{{x}\text{:}{b}\mid{r}\\}$ includes all
expressions which yield $b$-value $v$ that satisfy the refinement, i.e., $r$
evaluates to true on $v$. To decide the unrefined type of an expression we use
$\vdash_{B}e\,\mathrel{::}\,b$ (defined in §B.1). The interpretation of
function types ${x}\text{:}{\tau_{x}}\rightarrow\tau$ is _logical_ : it
includes all expressions that yield $\tau$-results when applied to $\tau_{x}$
arguments. The interpretation of base-type equalities $\texttt{PEq}_{b}\
\\{e_{l}\\}\ \\{e_{r}\\}$ includes all expressions that satisfy the basic
typing ($\texttt{PBEq}_{\tau}$ is the unrefined version of
$\texttt{PEq}_{\tau}\ \\{e_{l}\\}\ \\{e_{r}\\}$) and reduce to a basic
equality proof whose first arguments reduce to equal $b$-constants. Finally,
the interpretation of the function equality type
$\texttt{PEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ \\{e_{l}\\}\
\\{e_{r}\\}$ includes all expressions that satisfy the basic typing (based on
the $\lfloor\cdot\rfloor$ operator; §B.1). These expressions reduce to a proof
whose first two arguments are functions of type
${x}\text{:}{\tau_{x}}\rightarrow\tau$ and the third, proof argument takes
$\tau_{x}$ arguments to equality proofs of type $\texttt{PEq}_{\tau[e_{x}/x]}\
\\{e_{l}\ e_{x}\\}\ \\{e_{r}\ e_{x}\\}$. We write these proofs as
$\texttt{xEq}_{\\_}$, since the type index does not need to be syntactically
equal to the index of the type.

##### Constants

For simplicity, $\lambda^{RE}$ constants are only the two boolean values,
unit, and equality operators for basic types. For each basic type $b$, we
define the type indexed “computational” equality $==_{b}$. For two constants
$c_{1}$ and $c_{2}$ of basic type $b$, $c_{1}\ ==_{b}\ c_{2}$ evaluates in one
step to $(==_{(c_{1},b)})\ c_{2}$, which then steps to true when $c_{1}$ and
$c_{2}$ are the same and false otherwise.

Each constant $c$ has the type $\texttt{TyCon}(c)$ , as defined below.

$\begin{array}[]{rcl}\texttt{TyCon}(\texttt{true})&\doteq&\\{{x}\text{:}{\texttt{Bool}}\mid{x==_{\texttt{Bool}}\texttt{true}}\\}\\\
\texttt{TyCon}(\texttt{false})&\doteq&\\{{x}\text{:}{\texttt{Bool}}\mid{x==_{\texttt{Bool}}\texttt{false}}\\}\\\
\texttt{TyCon}(\texttt{unit})&\doteq&\\{{x}\text{:}{\texttt{()}}\mid{x==_{\texttt{()}}\texttt{unit}}\\}\\\
\texttt{TyCon}(==_{b})&\doteq&{x}\text{:}{b}\rightarrow{y}\text{:}{b}\rightarrow\\{{z}\text{:}{\texttt{Bool}}\mid{z==_{\texttt{Bool}}(x==_{b}y)}\\}\end{array}$

Our system could of course be extended with further constants, as long as they
belong in the interpretation of their type. This requirement is formally
defined by the Property 1 which, for the four constants of our system is
proved in Theorem B.1

###### Property 1 (Constants).

$c\in\left[\\!\left|\texttt{TyCon}(c)\right|\\!\right]$

###  6.2. Static Semantics of $\lambda^{RE}$

$\lambda^{RE}$’s static semantics comes in two parts: as typing judgments
(§6.2.1) and as a binary logical relation characterizing equivalence (§6.2.2).

####  6.2.1. Typing of $\lambda^{RE}$

Type checking in $\lambda^{RE}$ uses three mutually recursive judgments
(Figure 9): _type checking_ , $\Gamma\vdash e\mathrel{\text{::}}\tau$, for
when $e$ has type $\tau$ in $\Gamma$; _well formedness_ , $\Gamma\vdash\tau$,
for when when $\tau$ is well formed in $\Gamma$; and _subtyping_ ,
${\Gamma}\vdash{\tau_{l}}\ \preceq\ {\tau_{r}}$ , for when when $\tau_{l}$ is
a subtype of $\tau_{r}$ in $\Gamma$.

Type checking $\Gamma\vdash e\mathrel{\text{::}}\tau$

$\inference{\Gamma\vdash e\mathrel{\text{::}}\tau&{\Gamma}\vdash{\tau}\
\preceq\ {\tau^{\prime}}}{\Gamma\vdash
e\mathrel{\text{::}}\tau^{\prime}}[\textsc{TSub}]\quad\inference{\Gamma\vdash
e\mathrel{\text{::}}\\{{z}\text{:}{b}\mid{r}\\}}{\Gamma\vdash
e\mathrel{\text{::}}\\{{z}\text{:}{b}\mid{z==_{b}e}\\}}[\textsc{TSelf}]\quad\inference{}{\Gamma\vdash
c\mathrel{\text{::}}\texttt{TyCon}(c)}[\textsc{TCon}]$

$\inference{x:\tau\in\Gamma}{\Gamma\vdash
x\mathrel{\text{::}}\tau}[\textsc{TVar}]\quad\inference{\Gamma\vdash\tau_{x}&\Gamma,x:\tau_{x}\vdash
e\mathrel{\text{::}}\tau}{\Gamma\vdash\lambda
x\mathord{:}\tau_{x}.~{}e\mathrel{\text{::}}{x}\text{:}{\tau_{x}}\rightarrow\tau}[\textsc{TLam}]\quad\inference{\Gamma\vdash
e_{x}\mathrel{\text{::}}\tau_{x}&\Gamma\vdash
e\mathrel{\text{::}}{x}\text{:}{\tau_{x}}\rightarrow\tau}{\Gamma\vdash e\
e_{x}\mathrel{\text{::}}\tau[e_{x}/x]}[\textsc{TApp}]$

$\inference{\Gamma\vdash
e_{l}\mathrel{\text{::}}\tau_{l}&{\Gamma}\vdash{\tau_{l}}\ \preceq\
{\\{{x}\text{:}{b}\mid{\texttt{true}}\\}}\\\ \Gamma\vdash
e_{r}\mathrel{\text{::}}\tau_{r}{\Gamma}\vdash{\tau_{r}}\ \preceq\
{\\{{x}\text{:}{b}\mid{\texttt{true}}\\}}\\\
\Gamma,l:\tau_{l},r:\tau_{r}\vdash
e\mathrel{\text{::}}\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}}{\Gamma\vdash\texttt{bEq}_{b}\
e_{l}\ e_{r}\ e\mathrel{\text{::}}\texttt{PEq}_{b}\ \\{e_{l}\\}\
\\{e_{r}\\}}[\textsc{TEqBase}]\quad\inference{\Gamma\vdash
e_{l}\mathrel{\text{::}}\tau_{l}&{\Gamma}\vdash{\tau_{l}}\ \preceq\
{{x}\text{:}{\tau_{x}}\rightarrow\tau}\\\ \Gamma\vdash
e_{r}\mathrel{\text{::}}\tau_{r}{\Gamma}\vdash{\tau_{r}}\ \preceq\
{{x}\text{:}{\tau_{x}}\rightarrow\tau}\Gamma\vdash{x}\text{:}{\tau_{x}}\rightarrow\tau\\\
\Gamma,l:\tau_{l},r:\tau_{r}\vdash
e\mathrel{\text{::}}({x}\text{:}{\tau_{x}}\rightarrow\texttt{PEq}_{\tau}\
\\{l\ x\\}\ \\{r\
x\\})}{\Gamma\vdash\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e_{l}\
e_{r}\
e\mathrel{\text{::}}\texttt{PEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\
\\{e_{l}\\}\ \\{e_{r}\\}}[\textsc{TEqFun}]$

Well-formedness $\Gamma\vdash\tau$ $\vdash\Gamma$

$\inference{\lfloor\Gamma\rfloor,x:b\vdash_{B}r\,\mathrel{::}\,\texttt{Bool}}{\Gamma\vdash\\{{x}\text{:}{b}\mid{r}\\}}[\textsc{WFBase}]\quad\inference{\Gamma\vdash\tau_{x}&\Gamma,x:\tau_{x}\vdash\tau}{\Gamma\vdash{x}\text{:}{\tau_{x}}\rightarrow\tau}[\textsc{WFFun}]$

$\inference{\Gamma\vdash\tau&\Gamma\vdash
e_{l}\mathrel{\text{::}}\tau\Gamma\vdash
e_{r}\mathrel{\text{::}}\tau}{\Gamma\vdash\texttt{PEq}_{\tau}\ \\{e_{l}\\}\
\\{e_{r}\\}}[\textsc{WFEq}]\quad\inference{}{\vdash\emptyset}[\textsc{WFEmp}]\quad\inference{\vdash\Gamma&\Gamma\vdash\tau}{\vdash\Gamma,x:\tau}[\textsc{WFBind}]$

Subtyping ${\Gamma}\vdash{\tau}\ \preceq\ {\tau}$

$\inference{\forall\theta\in\left[\\!\left|\Gamma\right|\\!\right],~{}\left[\\!\left|{\theta}\cdot{\\{{x}\text{:}{b}\mid{r}\\}}\right|\\!\right]\subseteq\left[\\!\left|{\theta}\cdot{\\{{x^{\prime}}\text{:}{b}\mid{r^{\prime}}\\}}\right|\\!\right]}{{\Gamma}\vdash{\\{{x}\text{:}{b}\mid{r}\\}}\
\preceq\
{\\{{x^{\prime}}\text{:}{b}\mid{r^{\prime}}\\}}}[\textsc{SBase}]\quad\inference{{\Gamma}\vdash{\tau^{\prime}_{x}}\
\preceq\ {\tau_{x}}&{\Gamma,x:\tau^{\prime}_{x}}\vdash{\tau}\ \preceq\
{\tau^{\prime}}}{{\Gamma}\vdash{{x}\text{:}{\tau_{x}}\rightarrow\tau}\
\preceq\
{{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime}}}[\textsc{SFun}]$

$\inference{{\Gamma}\vdash{\tau}\ \preceq\
{\tau^{\prime}}&{\Gamma}\vdash{\tau^{\prime}}\ \preceq\
{\tau}}{{\Gamma}\vdash{\texttt{PEq}_{\tau}\ \\{e_{l}\\}\ \\{e_{r}\\}}\
\preceq\ {\texttt{PEq}_{\tau^{\prime}}\ \\{e_{l}\\}\
\\{e_{r}\\}}}[\textsc{SEq}]$

Semantic typing and closing substitutions
$\theta\in\left[\\!\left|\Gamma\right|\\!\right]$ $\Gamma\models e\in\tau$

$\inference{}{\emptyset\in\left[\\!\left|\emptyset\right|\\!\right]}[\textsc{CEmp}]\quad\inference{v\in\left[\\!\left|\tau\right|\\!\right]&\theta\in\left[\\!\left|\Gamma[v/x]\right|\\!\right]}{x\mapsto
v,\theta\in\left[\\!\left|x:\tau,\Gamma\right|\\!\right]}[\textsc{CSub}]\quad\begin{array}[]{c}\Gamma\models
e\in\tau\Leftrightarrow\forall\theta\in\left[\\!\left|\Gamma\right|\\!\right],~{}{\theta}\cdot{e}\in\left[\\!\left|{\theta}\cdot{\tau}\right|\\!\right]\end{array}$

Figure 9. Typing of $\lambda^{RE}$.

##### Type Checking

Beyond the conventional rules for refinement type systems (Ou et al., 2004;
Knowles and Flanagan, 2010; Rondon et al., 2008), the interesting rules are
concerned with equality (TEqBase, TEqFun).

The rule TEqBase assigns to the expression $\texttt{bEq}_{b}\ e_{l}\ e_{r}\ e$
the type $\texttt{PEq}_{b}\ \\{e_{l}\\}\ \\{e_{r}\\}$. To do so, we guess
types $\tau_{l}$ and $\tau_{r}$ that fit $e_{l}$ and $e_{r}$, respectively.
Both these types should be subtypes of $b$ that are _strong_ enough to derive
that if $l:\tau_{l}$ and $r:\tau_{r}$, then the proof argument $e$ has type
$\\{{\\_}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}$. Our formal model allows
checking of strong, selfified types (rule TSelf), but does not define an
algorithmic procedure to generate them. In Liquid Haskell, type inference
(Rondon et al., 2008) automatically and algorithmically derives such strong
types. We don’t encumber $\lambda^{RE}$ with inference, since, formally
speaking, we can always guess any type that inference can derive.

The rule TEqFun gives the expression
$\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e_{l}\ e_{r}\ e$ type
$\texttt{PEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ \\{e_{l}\\}\
\\{e_{r}\\}$. As in TEqBase, we guess strong types $\tau_{l}$ and $\tau_{r}$
to stand for $e_{l}$ and $e_{r}$ such that with $l:\tau_{l}$ and $r:\tau_{r}$,
the proof argument $e$ should have type
${x}\text{:}{\tau_{x}}\rightarrow\texttt{PEq}_{\tau}\ \\{l\ x\\}\ \\{r\ x\\}$,
i.e., it should prove that $l$ and $r$ are extensionally equal. We require
that the index ${x}\text{:}{\tau_{x}}\rightarrow\tau$ is well formed as
technical bookkeeping.

##### Well Formedness

Refinements should be booleans (WFBase); functions are treated in the usual
way (WFFun); and the propositional equality $\texttt{PEq}_{\tau}\ \\{e_{l}\\}\
\\{e_{r}\\}$ is well formed when the expressions $e_{l}$ and $e_{r}$ are typed
at the index $\tau$, which is also well formed (WFEq).

##### Subtyping

Basic types are related by set inclusion on the interpretation of those types
(SBase, and Figure 8). Concretely, for all closing substitutions (CEmp, CSub)
the interpretation of the left-hand side type should be a subset of the right-
hand side type. The rule SFun implements the usual (dependent) function
subtyping. Finally, SEq reduces subtyping of equality types to subtyping of
the type indices, while the expressions to be equated remain unchanged. Even
though covariant treatment of the type index would suffice for our metatheory,
we treat the type index invariantly to be consistent with the implementation
(§5) where the GADT encoding of PEq is invariant. Our subtyping rule allows
equality proofs between functions with convertible types (§4.2).

####  6.2.2. Equivalence Logical Relation for $\lambda^{RE}$

$\begin{array}[]{r@{~}c@{~}l@{~}lcl}\lx@intercol\textit{Value equivalence
<EMAIL_ADDRESS>c~{}&\mathrel{\sim}\hfil~{}&c\hfil~{}&\mathrel{::}\\{{x}\text{:}{b}\mid{r}\\};{\delta}&\quad\doteq&\vdash_{B}c\,\mathrel{::}\,b\wedge{\delta_{1}}\cdot{r[c/x]}\hookrightarrow^{*}\texttt{true}\wedge{\delta_{2}}\cdot{r[c/x]}\hookrightarrow^{*}\texttt{true}\\\
v_{1}~{}&\mathrel{\sim}\hfil~{}&v_{2}\hfil~{}&\mathrel{::}{x}\text{:}{\tau_{x}}\rightarrow\tau;{\delta}&\quad\doteq&\forall
v_{3}\mathrel{\sim}v_{4}\mathrel{::}\tau_{x};{\delta}.~{}v_{1}\
v_{3}\mathrel{\sim}v_{2}\ v_{4}\mathrel{::}\tau;{\delta,(v_{3},v4_{4})/x}\\\
v_{1}~{}&\mathrel{\sim}\hfil~{}&v_{2}\hfil~{}&\mathrel{::}\texttt{PEq}_{\tau}\
\\{e_{l}\\}\
\\{e_{r}\\}\mathord{;}\,\delta&\quad\doteq&{\delta_{1}}\cdot{e_{l}}\mathrel{\sim}{\delta_{2}}\cdot{e_{r}}\mathrel{::}\tau;{\delta}\\\\[8.53581pt]
\lx@intercol\textit{Expression equivalence
<EMAIL_ADDRESS>e_{1}~{}&\mathrel{\sim}\hfil~{}&e_{2}\hfil~{}&\mathrel{::}\tau;{\delta}&\quad\doteq&e_{1}\hookrightarrow^{*}v_{1},\quad
e_{2}\hookrightarrow^{*}v_{2},\quad
v_{1}\mathrel{\sim}v_{2}\mathrel{::}\tau;{\delta}\\\\[8.53581pt]
\lx@intercol\textit{Open expression equivalence
relation}\hfill\framebox{$\delta\in\Gamma$}\qquad\framebox{$\Gamma\vdash
<EMAIL_ADDRESS>\lx@intercol\hfil{\delta\in\Gamma}~{}~{}\doteq~{}~{}\forall x:\tau\in\Gamma,\
\delta_{1}(x)\mathrel{\sim}\delta_{2}(x)\mathrel{::}\tau;{\delta}\par\qquad\quad\par{\Gamma\vdash
e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,\tau}~{}~{}\doteq~{}~{}\forall\delta\in\Gamma,\
{\delta_{1}}\cdot{e_{1}}\mathrel{\sim}{\delta_{2}}\cdot{e_{2}}\mathrel{::}\tau;{\delta\par}\hfil\lx@intercol\\\
\end{array}$ Figure 10. Definition of equivalence logical relation.

We characterize equivalence with a term-model binary logical relation. We lift
a relation on closed values to closed and then open expressions (Figure 10).
Instead of directly substituting in type indices, all three relations use
_pending substitutions_ $\delta$, which map variables to pairs of equivalent
values.

##### Closed Values and Expressions

We read $v_{1}\mathrel{\sim}v_{2}\mathrel{::}\tau;{\delta}$ as saying that
values $v_{1}$ and $v_{2}$ are related under the type $\tau$ with pending
substitutions $\delta$. The relation is defined as a fixpoint on types, noting
that the propositional equality on a type, $\texttt{PEq}_{\tau}\ \\{e_{1}\\}\
\\{e_{2}\\}$, is structurally larger than the type $\tau$.

For refinement types $\\{{x}\text{:}{b}\mid{r}\\}$, related values must be the
same constant $c$. Further, this constant should actually be a $b$-constant
and it should actually satisfy the refinement $r$, i.e., substituting $c$ for
$x$ in $r$ should evaluate to true under either pending substitution
($\delta_{1}$ or $\delta_{2}$). Two values of function type are equivalent
when applying them to equivalent arguments yield equivalent results. Since we
have dependent types, we record the arguments in the pending substitution for
later substitution in the codomain. Two proofs of equality are equivalent when
the two equated expressions are equivalent in the logical relation at type-
index $\tau$—equality proofs ‘reflect’ the logical relation. Since the equated
expressions appear in the type itself, they may be open, referring to
variables in the pending substitution $\delta$. Thus we use $\delta$ to close
these expressions, using the logical relation on ${\delta_{1}}\cdot{e_{l}}$
and ${\delta_{2}}\cdot{e_{r}}$. Following the proof irrelevance notion of
refinement typing, the equivalence of equality proofs does not relate the
proof terms—in fact, it doesn’t even _inspect_ the proofs $v_{1}$ and $v_{2}$.

Two closed expressions $e_{1}$ and $e_{2}$ are equivalent on type $\tau$ with
pending substitions $\delta$, written
$e_{1}\mathrel{\sim}e_{2}\mathrel{::}\tau;{\delta}$, iff they respectively
evaluate to equivalent values $v_{1}$ and $v_{2}$.

##### Open Expressions

A pending substitution $\delta$ satisfies a typing environment $\Gamma$ when
its bindings are relates pairs of values at the type in $\Gamma$. Two open
expressions, with variables from $\Gamma$ are equivalent on type $\tau$,
written $\Gamma\vdash e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,\tau$, iff for
each $\delta$ that satisfies $\Gamma$, we have
${\delta_{1}}\cdot{e_{1}}\mathrel{\sim}{\delta_{2}}\cdot{e_{2}}\mathrel{::}\tau;{\delta}$.
The expressions $e_{1}$ and $e_{2}$ and the type $\tau$ might refer to
variables in the environment $\Gamma$. We use $\delta$ to close the
expressions eagerly, while we close the type lazily: we apply $\delta$ in the
refinement and equality cases of the closed value equivalence relation.

###  6.3. Metaproperties: PEq is an Equivalence Relation

Finally, we show various metaproperties of $\lambda^{RE}$. Theorem 6.1 proves
soundness of syntactic typing with respect to semantic typing. Theorem 6.2
proves that propositional equality implies equivalence in the term model.
Theorems 6.3 and 6.4 prove that both the equivalence relation and
propositional equality define equivalences, i.e., satisfy the three equality
axioms. All the proofs are in Appendix B.

$\lambda^{RE}$ is semantically sound: syntactically well typed programs are
also semantically well typed.

###### Theorem 6.1 (Typing is Sound).

If $\Gamma\vdash e\mathrel{\text{::}}\tau$, then $\Gamma\models e\in\tau$.

The proof goes by induction on the derivation tree. Our system could not be
proved sound using purely syntactic techniques, like progress and preservation
(Wright and Felleisen, 1994), for two reasons. First, and most essentially,
SBase needs to quantify over all closing substitutions and purely syntactic
approaches flirt with non-monotonicity (though others have attempted syntactic
approaches in similar systems (Zalewski et al., 2020)). Second, and merely
coincidentally, our system does not enjoy subject reduction. In particular,
SEq allows us to change the type index of propositional equality, but not the
term index. Why? Consider the term:

$(\lambda
x\mathord{:}\\{{x}\text{:}{\texttt{Bool}}\mid{\texttt{true}}\\}.~{}\texttt{bEq}_{\texttt{Bool}}\
x\ x\ ())\ e$

such that $e\hookrightarrow e^{\prime}$ for some $e^{\prime}$. The whole
application has type $\texttt{PEq}_{\texttt{Bool}}\ \\{e\\}\ \\{e\\}$; after
we take a step, it will have type $\texttt{PEq}_{\texttt{Bool}}\
\\{e^{\prime}\\}\ \\{e^{\prime}\\}$. Subject reduction demands that the latter
is a subtype of the former. We have

$\texttt{PEq}_{\texttt{Bool}}\ \\{e\\}\
\\{e\\}\rightrightarrows\texttt{PEq}_{\texttt{Bool}}\ \\{e^{\prime}\\}\
\\{e^{\prime}\\}$

so we could recover subject reduction by allowing a supertype’s terms to
parallel reduce (or otherwise convert) to a subtype’s terms. Adding this
condition would not be hard: the logical relations’ metatheory already demands
a variety of lemmas about parallel reduction, relegated to supplementary
material(Appendix C) to avoid distraction and preserve space for our main
contributions. We haven’t made this change because subject reduction isn’t
necessary for our purposes.

###### Theorem 6.2 (PEq is Sound).

If $\Gamma\vdash e\mathrel{\text{::}}\texttt{PEq}_{\tau}\ \\{e_{1}\\}\
\\{e_{2}\\}$, then $\Gamma\vdash
e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,\tau$.

The proof (see Theorem B.13)is a corollary of the fundamental property of the
logical relation(Theorem B.22), i.e., if $\Gamma\vdash
e\mathrel{\text{::}}\tau$ then $\Gamma\vdash
e\mathrel{\sim}e\,\mathrel{::}\,\tau$, which is proved in turn by induction on
the typing derivation.

###### Theorem 6.3 (The logical relation is an Equivalence).

$\Gamma\vdash e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,\tau$ is reflexive,
symmetric, and transitive:

  * •

Reflexivity: If $\Gamma\vdash e\mathrel{\text{::}}\tau$, then $\Gamma\vdash
e\mathrel{\sim}e\,\mathrel{::}\,\tau$.

  * •

Symmetry: If $\Gamma\vdash e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,\tau$, then
$\Gamma\vdash e_{2}\mathrel{\sim}e_{1}\,\mathrel{::}\,\tau$.

  * •

Transitivity: If $\Gamma\vdash e_{2}\mathrel{\text{::}}\tau$, $\Gamma\vdash
e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,\tau$, and $\Gamma\vdash
e_{2}\mathrel{\sim}e_{3}\,\mathrel{::}\,\tau$, then $\Gamma\vdash
e_{1}\mathrel{\sim}e_{3}\,\mathrel{::}\,\tau$.

Reflexivity is also called the _fundamental property_ of the logical relation.
The other proofs go by structural induction on $\tau$ (Theorem B.23).
Transitivity requires reflexivity on $e_{2}$, so we also assume that
$\Gamma\vdash e_{2}\mathrel{\text{::}}\tau$.

###### Theorem 6.4 (PEq is an Equivalence).

$\texttt{PEq}_{\tau}\ \\{e_{1}\\}\ \\{e_{2}\\}$ is reflexive, symmetric, and
transitive on equable types. That is, for all $\tau$ that do not contain
equalities themselves:

  * •

Reflexivity: If $\Gamma\vdash e\mathrel{\text{::}}\tau$, then there exists $v$
such that $\Gamma\vdash v\mathrel{\text{::}}\texttt{PEq}_{\tau}\ \\{e\\}\
\\{e\\}$.

  * •

Symmetry: If $\Gamma\vdash v_{12}\mathrel{\text{::}}\texttt{PEq}_{\tau}\
\\{e_{1}\\}\ \\{e_{2}\\}$, then there exists $v_{21}$ such that $\Gamma\vdash
v_{21}\mathrel{\text{::}}\texttt{PEq}_{\tau}\ \\{e_{2}\\}\ \\{e_{1}\\}$.

  * •

Transitivity: If $\Gamma\vdash v_{12}\mathrel{\text{::}}\texttt{PEq}_{\tau}\
\\{e_{1}\\}\ \\{e_{2}\\}$ and $\Gamma\vdash
v_{23}\mathrel{\text{::}}\texttt{PEq}_{\tau}\ \\{e_{2}\\}\ \\{e_{3}\\}$, then
there exists $v_{13}$ such that $\Gamma\vdash
v_{13}\mathrel{\text{::}}\texttt{PEq}_{\tau}\ \\{e_{1}\\}\ \\{e_{3}\\}$.

The proofs go by induction on $\tau$(Theorem B.24). Reflexivity requires us to
generalize the inductive hypothesis to generate appropriate $\tau_{l}$ and
$\tau_{r}$ for the PEq proofs.

##  7\. Related Work

##### Functional Extensionality and Subtyping with an SMT Solver

F∗also uses a type-indexed funext axiom after having run into similar
unsoundness issues (FStarLang, 2018). Their extensionality axiom makes a more
roundabout connection with SMT: function equality uses ==, a proof-irrelevant,
propositional Leibniz equality. They assume that their Leibniz equality
coincides with SMT equality. Liquid Haskell can’t just copy F∗: there are no
dependent, inductive type definitions, nor a dedicated notion of propositions.
Our PEq GADT approximates F∗’s approach, with different compromises.

Dafny’s SMT encoding axiomatizes extensionality for data, but not for
functions (Leino, 2012). Function equality is utterable but neither provable
nor disprovable in their encoding into Z3.

Ou et al. (2004) introduce _selfification_ , which assigns singleton types
using equality (as in our TSelf rule). SAGE assigns selfified types to _all_
variables, implying equality on functions (Knowles et al., 2006). Dminor
avoids the question: it lacks first-class functions (Bierman et al., 2012).

##### Extensionality in Dependent Type Theories

Functional extensionality (funext) has a rich history of study. Martin-Löf
type theory comes in a decidable, intensional flavor (ITT) (Martin-Löf, 1975)
as well as an undecidable, extensional one (ETT) (Martin-Löf, 1984). NuPRL
implements ETT (Constable et al., 1986), while Coq and Agda implement ITT
(2020; 2008). Lean’s quotient-based reasoning can _prove_ funext (de Moura et
al., 2015). Extensionality axioms are independent of the rules of ITT; funext
is a common axiom, but is not consistent in every model of type theory (von
Glehn, 2014). Hofmann (1996) shows that ETT is a conservative but less
computational extension of ITT with funext and UIP. Pfenning (2001) and
Altenkirch and McBride (2006) try to reconcile ITT and ETT.

Dependent type theories often care about equalities between equalities, with
axioms like UIP (all identity proofs are the same), K (all identity proofs are
refl), and univalence (identity proofs are isomorphisms, and so not the same).
If we allowed equalities between equalities, we could add UIP. Our
propositional equality isn’t exactly Leibniz equality, so axiom K would be
harder to encode.

Zombie’s type theory uses an adaptation of a congruence closure algorithm to
automatically reason about equality (Sjöberg and Weirich, 2015). Zombie can do
some reasoning about equalities on functions but cannot show equalities based
on bound variables. Zombie is careful to omit a $\lambda$-congruence rule,
which could be used to prove funext, “which is not compatible with [their]
‘very heterogeneous’ treatment of equality” [Ibid., §9].

Cubical type theory offers alternatives to our propositional equality
(Sterling et al., 2019). Such approaches may play better with F∗’s approach
using dependent, inductive types than the ‘flatter’ approach we used for
Liquid Haskell. Univalent systems like cubical type theory get funext ‘for
free’—that is, for the price of the univalence axiom or of cubical
foundations.

##### Classy Induction: Inductive Proofs Using Typeclasses

We used ‘classy induction’ to prove metaproperties of PEq inside Liquid
Haskell (§3.3), using ad-hoc polymorphism and general instances to generate
proofs that ‘cover’ some class of types. We did not _invent_ classy
induction—it is a folklore technique that we named. We have seen five
independent uses of “classy induction” in the literature (Guillemette and
Monnier, 2008; Weirich, 2017; Boulier et al., 2017; Dagand et al., 2018;
Tabareau et al., 2019).

Any typeclass system that accommodates ad-hoc polymorphism and a notion of
proof can use classy induction. Sozeau (2008) generates proofs of nonzeroness
using something akin to classy induction, though it goes by induction on the
operations used to build up arithmetic expressions in the (dependent!) host
language (§6.3.2); he calls this the ‘programmation logique’ aspect of
typeclasses. Instance resolution is characterized as proof search over lemmas
(§7.1.3). Sozeau and Oury (2008) introduce typeclasses to Coq; their system
can do induction by typeclasses, but they do not demonstrate the idea in the
paper. Earlier work on typeclasses focused on overloading (Wadler and Blott,
1989; Nipkow and Snelting, 1991; Nipkow and Prehofer, 1993), with no notion of
classy induction even in settings with proofs (Wenzel, 1997).

##  8\. Conclusion

In a refinement type system with subtyping a naive encoding of funext is
inconsistent. We explained the inconsistency by examples (that proved false)
and by standard type checking (where the equality domain is inferred as
false). We implemented a type-indexed propositional equality that avoids this
inconsistency and validated it with a model calculus. Several case studies
demonstrate the range, effectiveness, and power of our work.

###### Acknowledgements.

We thank Conal Elliott for his help in exposing the inadequacy of the naive
functional extensionality encoding. Stephanie Weirich, Éric Tanter, and
Nicolas Tabareau offered valuable insights into the folklore of classy
induction.

## References

  * (1)
  * Altenkirch and McBride (2006) Thorsten Altenkirch and Conor McBride. 2006.  Towards observational type theory.  Unpublished manuscript.
  * Barbosa et al. (2019) Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, and Clark Barrett. 2019\.  Extending SMT Solvers to Higher-Order Logic. In _Automated Deduction – CADE 27_ , Pascal Fontaine (Ed.). Springer International Publishing, Cham, 35–54.
  * Barrett et al. (2010) Clark Barrett, Aaron Stump, and Cesare Tinelli. 2010\.  _The SMT-LIB Standard: Version 2.0_.  Technical Report. Department of Computer Science, The University of Iowa.  Available at www.SMT-LIB.org.
  * Bierman et al. (2012) Gavin M. Bierman, Andrew D. Gordon, Catalin Hritcu, and David E. Langworthy. 2012.  Semantic subtyping with an SMT solver.  _J. Funct. Program._ 22, 1 (2012), 31–105.  https://doi.org/10.1017/S0956796812000032
  * Boulier et al. (2017) Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau. 2017.  The next 700 syntactical models of type theory. In _Certified Programs and Proofs (CPP 2017)_. Paris, France, 182 – 194.  https://doi.org/10.1145/3018610.3018620
  * Cheney and Hinze (2003) James Cheney and Ralf Hinze. 2003.  _First-Class Phantom Types_.  Technical Report. Cornell University.
  * Constable et al. (1986) Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, R. W. Harper, Douglas J. Howe, Todd B. Knoblock, N. P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith. 1986.  _Implementing mathematics with the Nuprl proof development system_.  Prentice Hall.  http://dl.acm.org/citation.cfm?id=10510
  * Constable and Smith (1987) Robert L Constable and Scott Fraser Smith. 1987.  _Partial objects in constructive type theory_.  Technical Report. Cornell University.
  * Dagand et al. (2018) Pierre-Évariste Dagand, Nicolas Tabareau, and Éric Tanter. 2018.  Foundations of dependent interoperability.  _J. Funct. Program._ 28 (2018), e9.  https://doi.org/10.1017/S0956796818000011
  * de Moura et al. (2015) Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015.  The Lean Theorem Prover (System Description). In _Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings_ _(Lecture Notes in Computer Science, Vol. 9195)_ , Amy P. Felty and Aart Middeldorp (Eds.). Springer, 378–388.  https://doi.org/10.1007/978-3-319-21401-6_26
  * FStarLang (2018) Github FStarLang. 2018\.  Functional Equality Discussions in F*.  https://github.com/FStarLang/FStar/blob/cba5383bd0e84140a00422875de21a8a77bae116/ulib/FStar.FunctionalExtensionality.fsti#L133-L134 and https://github.com/FStarLang/FStar/issues/1542 and https://github.com/FStarLang/FStar/wiki/SMT-Equality-and-Extensionality-in-F%2A.
  * Guillemette and Monnier (2008) Louis-Julien Guillemette and Stefan Monnier. 2008.  A Type-Preserving Compiler in Haskell. In _Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming_ (Victoria, BC, Canada) _(ICFP ’08)_. Association for Computing Machinery, New York, NY, USA, 75–86.  https://doi.org/10.1145/1411204.1411218
  * Hofmann (1996) Martin Hofmann. 1996\.  Conservativity of equality reflection over intensional type theory. In _Types for Proofs and Programs_ , Stefano Berardi and Mario Coppo (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 153–164.
  * Knowles and Flanagan (2010) Kenneth Knowles and Cormac Flanagan. 2010.  Hybrid Type Checking.  _ACM Trans. Program. Lang. Syst._ 32, 2, Article 6 (Feb. 2010), 34 pages.  https://doi.org/10.1145/1667048.1667051
  * Knowles et al. (2006) Kenneth Knowles, Aaron Tomb, Jessica Gronski, Stephen N. Freund, and Cormac Flanagan. 2006\.  Sage: Hybrid checking for flexible specifications. In _Scheme and Functional Programming Workshop_.
  * Leino (2012) K. Rustan M. Leino. 2012\.  Developing verified programs with Dafny. In _Proceedings of the 2012 ACM Conference on High Integrity Language Technology, HILT ’12, December 2-6, 2012, Boston, Massachusetts, USA_ , Ben Brosgol, Jeff Boleng, and S. Tucker Taft (Eds.). ACM, 9–10.  https://doi.org/10.1145/2402676.2402682
  * Liu et al. (2020) Yiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, and Niki Vazou. 2020\.  Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell. In _Proceedings of the ACM Conference on Object-Oriented Programming Languages, Systems, and Applications (OOPSLA)_.
  * Martin-Löf (1975) Per Martin-Löf. 1975\.  An Intuitionistic Theory of Types: Predicative Part.  In _Logic Colloquium ’73_ , H.E. Rose and J.C. Shepherdson (Eds.). Studies in Logic and the Foundations of Mathematics, Vol. 80. Elsevier, 73 – 118.  https://doi.org/10.1016/S0049-237X(08)71945-1
  * Martin-Löf (1984) Per Martin-Löf. 1984\.  _Intuitionistic Type Theory_.  Bibliopolis.  https://books.google.com/books?id=_D0ZAQAAIAAJ As recorded by Giovanni Sambin.
  * Nipkow and Prehofer (1993) Tobias Nipkow and Christian Prehofer. 1993.  Type Checking Type Classes. In _Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (Charleston, South Carolina, USA) _(POPL ’93)_. Association for Computing Machinery, New York, NY, USA, 409–418.  https://doi.org/10.1145/158511.158698
  * Nipkow and Snelting (1991) Tobias Nipkow and Gregor Snelting. 1991.  Type Classes and Overloading Resolution via Order-Sorted Unification. In _Proceedings of the 5th ACM Conference on Functional Programming Languages and Computer Architecture_. Springer-Verlag, Berlin, Heidelberg, 1–14.
  * Norell (2008) Ulf Norell. 2008\.  Dependently Typed Programming in Agda. In _Proceedings of the 6th International Conference on Advanced Functional Programming_ (Heijen, The Netherlands) _(AFP’08)_. Springer-Verlag, Berlin, Heidelberg, 230–266.
  * Ou et al. (2004) Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker. 2004\.  Dynamic Typing with Dependent Types. In _Exploring New Frontiers of Theoretical Informatics, IFIP 18th World Computer Congress, TC1 3rd International Conference on Theoretical Computer Science (TCS2004), 22-27 August 2004, Toulouse, France_ _(IFIP, Vol. 155)_ , Jean-Jacques Lévy, Ernst W. Mayr, and John C. Mitchell (Eds.). Kluwer/Springer, 437–450.  https://doi.org/10.1007/1-4020-8141-3_34
  * Pfenning (2001) F. Pfenning. 2001\.  Intensionality, extensionality, and proof irrelevance in modal type theory. In _Proceedings 16th Annual IEEE Symposium on Logic in Computer Science_. 221–230.
  * Rondon et al. (2008) Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. 2008\.  Liquid Types. In _Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Tucson, AZ, USA) _(PLDI ’08)_. ACM, New York, NY, USA, 159–169.  https://doi.org/10.1145/1375581.1375602
  * Rushby et al. (1998) John Rushby, Sam Owre, and Natarajan Shankar. 1998.  Subtypes for specifications: Predicate subtyping in PVS.  _IEEE Transactions on Software Engineering_ 24, 9 (1998), 709–720.
  * Sekiyama et al. (2017) Taro Sekiyama, Atsushi Igarashi, and Michael Greenberg. 2017\.  Polymorphic Manifest Contracts, Revised and Resolved.  _ACM Trans. Program. Lang. Syst._ 39, 1, Article 3 (Feb. 2017), 36 pages.  https://doi.org/10.1145/2994594
  * Sjöberg and Weirich (2015) Vilhelm Sjöberg and Stephanie Weirich. 2015.  Programming up to Congruence. In _Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (Mumbai, India) _(POPL ’15)_. Association for Computing Machinery, New York, NY, USA, 369–382.  https://doi.org/10.1145/2676726.2676974
  * Sozeau (2008) Matthieu Sozeau. 2008\.  _Un environnement pour la programmation avec types dépendants_.  Ph.D. Dissertation. Université Paris 11, Orsay, France.
  * Sozeau and Oury (2008) Matthieu Sozeau and Nicolas Oury. 2008.  First-Class Type Classes. In _Theorem Proving in Higher Order Logics_ , Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 278–293.
  * Sterling et al. (2019) Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. 2019\.  Cubical Syntax for Reflection-Free Extensional Equality.  _CoRR_ abs/1904.08562 (2019).  arXiv:1904.08562 http://arxiv.org/abs/1904.08562
  * supplementary material (2021) supplementary material. 2021\.  Supplementary Material for Functional Extensionality for Refinement Types.
  * Swamy et al. (2016) Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, and Santiago Zanella-Béguelin. 2016\.  Dependent Types and Multi-Monadic Effects in F*. In _43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)_. ACM, 256–270.  https://www.fstar-lang.org/papers/mumon/
  * Tabareau et al. (2019) Nicolas Tabareau, Éric Tanter, and Matthieu Sozeau. 2019.  The Marriage of Univalence and Parametricity.  _arXiv e-prints_ , Article arXiv:1909.05027 (Sept. 2019), arXiv:1909.05027 pages.  arXiv:1909.05027 [cs.PL]
  * Takahashi (1989) Masako Takahashi. 1989\.  Parallel Reductions in lambda-Calculus.  _J. Symb. Comput._ 7, 2 (1989), 113–123.  https://doi.org/10.1016/S0747-7171(89)80045-8
  * Team (2020) The Coq Development Team. 2020\.  _The Coq Proof Assistant, version 8.11.0_.  https://doi.org/10.5281/zenodo.3744225
  * Vazou et al. (2018a) Niki Vazou, Joachim Breitner, Rose Kunkel, David Van Horn, and Graham Hutton. 2018a.  Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl). In _Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell_ (St. Louis, MO, USA) _(Haskell 2018)_. ACM, New York, NY, USA, 132–144.  https://doi.org/10.1145/3242744.3242756
  * Vazou et al. (2018b) Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala. 2018b.  Refinement reflection: complete verification with SMT.  _PACMPL_ 2, POPL (2018), 53:1–53:31.  https://doi.org/10.1145/3158141
  * von Glehn (2014) Tamara von Glehn. 2014\.  _Polynomials and Models of Type Theory_.  Ph.D. Dissertation. Magdalene College, University of Cambridge.
  * Wadler and Blott (1989) P. Wadler and S. Blott. 1989.  How to Make Ad-Hoc Polymorphism Less Ad Hoc. In _Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (Austin, Texas, USA) _(POPL ’89)_. Association for Computing Machinery, New York, NY, USA, 60–76.  https://doi.org/10.1145/75277.75283
  * Weirich (2017) Stephanie Weirich. 2017\.  The Influence of Dependent Types (Keynote). In _Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages_ (Paris, France) _(POPL 2017)_. Association for Computing Machinery, New York, NY, USA, 1\.  https://doi.org/10.1145/3009837.3009923
  * Wenzel (1997) Markus Wenzel. 1997\.  Type classes and overloading in higher-order logic. In _Theorem Proving in Higher Order Logics_ , Elsa L. Gunter and Amy Felty (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 307–322.
  * Wright and Felleisen (1994) Andrew K. Wright and Matthias Felleisen. 1994.  A Syntactic Approach to Type Soundness.  _Information and Computation_ 115 (1994), 38–94.  Issue 1.
  * Xi et al. (2003) Hongwei Xi, Chiyan Chen, and Gang Chen. 2003.  Guarded Recursive Datatype Constructors. In _Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (New Orleans, Louisiana, USA) _(POPL ’03)_. Association for Computing Machinery, New York, NY, USA, 224–235.  https://doi.org/10.1145/604131.604150
  * Xi and Pfenning (1998) Hongwei Xi and Frank Pfenning. 1998.  Eliminating array bound checking through dependent types. In _Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation_. 249–257.
  * Zalewski et al. (2020) Jakub Zalewski, James McKinna, J. Garrett Morris, and Philip Wadler. 2020.  Blame tracking at higher fidelity. In _Workshop on Gradual Typing (WGT)_.

##  Appendix A Complete Type Checking of Extensionality Example

$\Gamma(\texttt{funext})\ =\ \forall a\ b.\texttt{Eq }b\Rightarrow
f:(a\rightarrow b)\rightarrow g:(a\rightarrow
b)\rightarrow(x:a\rightarrow\\{f\ x\ \text{==}\ g\
x\\})\rightarrow\\{f\backsimeq g\\}$
$\Gamma\vdash\texttt{funext}\mathrel{\text{::}}\forall a\ b.\texttt{Eq
}b\Rightarrow f:(a\rightarrow b)\rightarrow g:(a\rightarrow
b)\rightarrow(x:a\rightarrow\\{f\ x\ \text{==}\ g\
x\\})\rightarrow\\{f\backsimeq g\\}$ $\Gamma\vdash\texttt{funext}\
@\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\mathrel{\text{::}}\forall
b.\texttt{Eq }b\Rightarrow
f:(\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow b)\rightarrow
g:(\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow
b)\rightarrow(x:\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{f\
x\ \text{==}\ g\ x\\})\rightarrow\\{f\backsimeq g\\}$
$\Gamma\vdash\texttt{funext}\
@\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\
@\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}\mathrel{\text{::}}\texttt{Eq
}\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}\Rightarrow
f:(\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\})\rightarrow
g:(\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\})\rightarrow(x:\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{f\
x\ \text{==}\ g\ x\\})\rightarrow\\{f\backsimeq g\\}$
$\Gamma(\texttt{d})\ =\ \texttt{Eq }\alpha$
$\Gamma\vdash\texttt{d}\mathrel{\text{::}}\texttt{Eq }\alpha$ &
${\Gamma}\vdash{\texttt{Eq }\alpha}\ \preceq\ {\texttt{Eq
}\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}}$ [Sub-D ]
$\Gamma\vdash\texttt{funext}\
@\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\
@\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}\
\texttt{d}\mathrel{\text{::}}f:(\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\})\rightarrow
g:(\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\})\rightarrow(x:\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{f\
x\ \text{==}\ g\ x\\})\rightarrow\\{f\backsimeq g\\}$
$\Gamma(\texttt{h})\ =\
x:\\{\\!\mid\\!\\!{d_{\texttt{h}}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{r_{\texttt{h}}}\\!\\!\mid\\!\\}$
$\Gamma\vdash\texttt{h}\mathrel{\text{::}}x:\\{\\!\mid\\!\\!{d_{\texttt{h}}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{r_{\texttt{h}}}\\!\\!\mid\\!\\}$
& …
${\Gamma}\vdash{x:\\{\\!\mid\\!\\!{d_{\texttt{h}}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{r_{\texttt{h}}}\\!\\!\mid\\!\\}}\
\preceq\
{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}}$
[Sub-H ] $\Gamma\vdash\texttt{funext}\
@\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\
@\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}\ \texttt{d}\
\texttt{h}\mathrel{\text{::}}g:(\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\})\rightarrow(x:\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\texttt{h}\
x\ \text{==}\ g\ x\\})\rightarrow\\{\texttt{h}\backsimeq g\\}$
$\Gamma(\texttt{k})\ =\
x:\\{\\!\mid\\!\\!{d_{\texttt{k}}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{r_{\texttt{k}}}\\!\\!\mid\\!\\}$
$\Gamma\vdash\texttt{k}\mathrel{\text{::}}x:\\{\\!\mid\\!\\!{d_{\texttt{k}}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{r_{\texttt{k}}}\\!\\!\mid\\!\\}$
& …
${\Gamma}\vdash{x:\\{\\!\mid\\!\\!{d_{\texttt{k}}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{r_{\texttt{k}}}\\!\\!\mid\\!\\}}\
\preceq\
{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}}$
[Sub-K ] $\Gamma\vdash\texttt{funext}\
@\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\
@\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}\ \texttt{d}\ \texttt{h}\
\texttt{k}\mathrel{\text{::}}(x:\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\texttt{h}\
x\ \text{==}\ \texttt{k}\
x\\})\rightarrow\\{\texttt{h}\backsimeq\texttt{k}\\}$
$\Gamma(\texttt{lemma})\ =\
x:\\{\\!\mid\\!\\!{d_{p}}\\!\\!\mid\\!\\}\rightarrow\\{p\\}$
$\Gamma\vdash\texttt{lemma}\mathrel{\text{::}}x:\\{\\!\mid\\!\\!{d_{p}}\\!\\!\mid\\!\\}\rightarrow\\{p\\}$
& …
${\Gamma}\vdash{x:\\{\\!\mid\\!\\!{d_{p}}\\!\\!\mid\\!\\}\rightarrow\\{p\\}}\
\preceq\
{x:\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\texttt{h}\
x\ \text{==}\ \texttt{k}\ x\\}}$ [Sub-L ] $\Gamma\vdash\texttt{funext}\
@\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\
@\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}\ \texttt{d}\ \texttt{h}\
\texttt{k}\ \texttt{lemma}\mathrel{\text{::}}\\{h\backsimeq k\\}$

$\inference{\inference{\kappa_{\alpha}\Rightarrow
d_{\texttt{h}}}{{\Gamma}\vdash{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\
\preceq\ {\\{v:\alpha\mid
d_{\texttt{h}}\\}}}&\inference{\kappa_{\alpha}\Rightarrow
r_{\texttt{h}}\Rightarrow\kappa_{\beta}}{{\Gamma,x:\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\vdash{\\{v:\beta\mid
r_{\texttt{h}}\\}}\ \preceq\
{\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}}}}{{\Gamma}\vdash{x:\\{\\!\mid\\!\\!{d_{\texttt{h}}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{r_{\texttt{h}}}\\!\\!\mid\\!\\}}\
\preceq\
{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}}}[\textsc{Sub-H}]$

$\inference{\inference{\kappa_{\alpha}\Rightarrow
d_{\texttt{k}}}{{\Gamma}\vdash{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\
\preceq\ {\\{v:\alpha\mid
d_{\texttt{k}}\\}}}&\inference{\kappa_{\alpha}\Rightarrow
r_{\texttt{k}}\Rightarrow\kappa_{\beta}}{{\Gamma,x:\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\vdash{\\{v:\beta\mid
r_{\texttt{k}}\\}}\ \preceq\
{\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}}}}{{\Gamma}\vdash{x:\\{\\!\mid\\!\\!{d_{\texttt{k}}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{r_{\texttt{k}}}\\!\\!\mid\\!\\}}\
\preceq\
{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\\!\mid\\!\\!{\kappa_{\beta}}\\!\\!\mid\\!\\}}}[\textsc{Sub-K}]$

$\inference{\inference{\kappa_{\alpha}\Rightarrow\texttt{true}}{{\Gamma}\vdash{\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\
\preceq\ {\alpha}}&\inference{\kappa_{\alpha}\Rightarrow p\Rightarrow h\ x\
\text{==}\ k\
x}{{\Gamma,x:\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}}\vdash{\\{p\\}}\
\preceq\ {\\{h\ x\ \text{==}\ k\
x\\}}}}{{\Gamma}\vdash{x:\\{\\!\mid\\!\\!{d_{p}}\\!\\!\mid\\!\\}\rightarrow\\{p\\}}\
\preceq\
{x:\\{\\!\mid\\!\\!{\kappa_{\alpha}}\\!\\!\mid\\!\\}\rightarrow\\{\texttt{h}\
x\ \text{==}\ \texttt{k}\ x\\}}}[\textsc{Sub-L}]$

Figure 11. Complete type checking of naive extensionality in theoremEq.

##  Appendix B Proofs and Definitions for Metatheory

In this section we provide proofs and definitions ommitted from §6.

###  B.1. Base Type Checking

For completeness, we defined $\lambda^{E}$, the unrefined version of
$\lambda^{RE}$, that ignores the refinements on basic types and the expression
indices from the typed equality.

The function $\lfloor\cdot\rfloor$ is defined to turn $\lambda^{RE}$ types to
their unrefined counterparts.

$\begin{array}[]{rcl}\lfloor\texttt{Bool}\rfloor&\doteq&\texttt{Bool}\\\
\lfloor\texttt{()}\rfloor&\doteq&\texttt{()}\\\ \lfloor\texttt{PEq}_{\tau}\
\\{e_{1}\\}\
\\{e_{2}\\}\rfloor&\doteq&\texttt{PBEq}_{\lfloor\tau\rfloor}{}{}\\\\[5.69054pt]
\lfloor\\{{v}\text{:}{b}\mid{r}\\}\rfloor&\doteq&b\\\
\lfloor{x}\text{:}{\tau_{x}}\rightarrow\tau\rfloor&\doteq&{\lfloor\tau_{x}\rfloor}\rightarrow\lfloor\tau\rfloor\\\
\end{array}$

Figure 12 defines the syntax and typing of $\lambda^{E}$ that we use to define
type denotations of $\lambda^{RE}$.

$\begin{array}[]{rrcl}\textit{Expressions}&e&::=&\text{as in
}\lambda^{RE}\\\\[2.84526pt]
\textit{Types}&t&::=&\texttt{Bool}\mid\texttt{()}\mid\texttt{PBEq}_{t}{e}{e}\mid{t}\rightarrow
t\\\\[2.84526pt] \textit{Typing Environment}&G&::=&\emptyset\mid
G,x:t\\\\[2.84526pt] \end{array}$

Basic Type checking $G\vdash_{B}e\,\mathrel{::}\,t$

$\inference{}{G\vdash_{B}c\,\mathrel{::}\,\lfloor\texttt{TyCon}(c)\rfloor}[\textsc{BTCon}]\quad\inference{x:t\in
G}{G\vdash_{B}x\,\mathrel{::}\,t}[\textsc{BTVar}]$

$\inference{G\vdash_{B}e\,\mathrel{::}\,{t_{x}}\rightarrow
t&G\vdash_{B}e_{x}\,\mathrel{::}\,t_{x}}{G\vdash_{B}e\
e_{x}\,\mathrel{::}\,t}[\textsc{BTApp}]\quad\inference{G,x:\lfloor\tau_{x}\rfloor\vdash_{B}e\,\mathrel{::}\,t}{G\vdash_{B}\lambda
x\mathord{:}\tau_{x}.~{}e\,\mathrel{::}\,{\lfloor\tau_{x}\rfloor}\rightarrow
t}[\textsc{BTLam}]$

$\inference{G\vdash_{B}e\,\mathrel{::}\,\texttt{()}\\\
G\vdash_{B}e_{1}\,\mathrel{::}\,b&G\vdash_{B}e_{2}\,\mathrel{::}\,b}{G\vdash_{B}\texttt{bEq}_{b}\
e_{1}\ e_{2}\
e\,\mathrel{::}\,\texttt{PBEq}_{b}{e_{1}}{e_{2}}}[\textsc{BTEqBase}]\quad\inference{G\vdash_{B}e\,\mathrel{::}\,\texttt{()}\\\
G\vdash_{B}e_{1}\,\mathrel{::}\,\lfloor{\tau_{x}}\rightarrow\tau\rfloor&G\vdash_{B}e_{2}\,\mathrel{::}\,\lfloor{\tau_{x}}\rightarrow\tau\rfloor}{G\vdash_{B}\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\
e_{1}\ e_{2}\
e\,\mathrel{::}\,\texttt{PBEq}_{\lfloor{\tau_{x}}\rightarrow\tau\rfloor}{e_{1}}{e_{2}}}[\textsc{BTEqFun}]$

Figure 12. Syntax and Typing of $\lambda^{E}$.

###  B.2. Constant Property

###### Theorem B.1.

For the constants $c=\texttt{true},\texttt{false},\texttt{unit},$ and
$==_{b}$, Property 1 holds, i.e.,
$c\in\left[\\!\left|\texttt{TyCon}(c)\right|\\!\right]$.

###### Proof.

Below are the proofs for each of the four constants.

  * •

$e\equiv\texttt{true}$ and
$e\in\left[\\!\left|\\{{x}\text{:}{\texttt{Bool}}\mid{x==_{\texttt{Bool}}\texttt{true}}\\}\right|\\!\right]$.
We need to prove the below three requirements of membership in the
interpretation of basic types:

    * –

$e\hookrightarrow^{*}v$, which holds because true is a value, thus
$v=\texttt{true}$;

    * –

$\vdash_{B}e\,\mathrel{::}\,\texttt{Bool}$, which holds by the typing rule
BTCon; and

    * –

$(x==_{\texttt{Bool}}\texttt{true})[e/x]\hookrightarrow^{*}\texttt{true}$,
which holds because

$\begin{array}[]{rcl}(x==_{\texttt{Bool}}\texttt{true})[e/x]&=&\texttt{true}==_{\texttt{Bool}}\texttt{true}\\\
&\hookrightarrow&(==_{(\texttt{true},\texttt{Bool})})\ \texttt{true}\\\
&\hookrightarrow&\texttt{true}=\texttt{true}\\\ &=&\texttt{true}\end{array}$

  * •

$e\equiv\texttt{false}$ and
$e\in\left[\\!\left|\\{{x}\text{:}{\texttt{Bool}}\mid{x==_{\texttt{Bool}}\texttt{false}}\\}\right|\\!\right]$.
We need to prove the below three requirements of membership in the
interpretation of basic types:

    * –

$e\hookrightarrow^{*}v$, which holds because false is a value, thus
$v=\texttt{false}$;

    * –

$\vdash_{B}e\,\mathrel{::}\,\texttt{Bool}$, which holds by the typing rule
BTCon; and

    * –

$(x==_{\texttt{Bool}}\texttt{false})[e/x]\hookrightarrow^{*}\texttt{true}$,
which holds because

$\begin{array}[]{rcl}(x==_{\texttt{Bool}}\texttt{false})[e/x]&=&\texttt{false}==_{\texttt{Bool}}\texttt{false}\\\
&\hookrightarrow&(==_{(\texttt{false},\texttt{Bool})})\ \texttt{false}\\\
&\hookrightarrow&\texttt{false}=\texttt{false}\\\ &=&\texttt{true}\end{array}$

  * •

$e\equiv\texttt{unit}$ and
$e\in\left[\\!\left|\\{{x}\text{:}{\texttt{()}}\mid{x==_{\texttt{()}}\texttt{unit}}\\}\right|\\!\right]$.
We need to prove the below three requirements of membership in the
interpretation of basic types:

    * –

$e\hookrightarrow^{*}v$, which holds because unit is a value, thus
$v=\texttt{unit}$;

    * –

$\vdash_{B}e\,\mathrel{::}\,\texttt{()}$, which holds by the typing rule
BTCon; and

    * –

$(x==_{\texttt{()}}\texttt{unit})[e/x]\hookrightarrow^{*}\texttt{true}$, which
holds because