If anyone is confused by how the author uses "proof" in this article, they are referring to the Curry-Howard isomorphism that types represent propositions in a

If anyone is confused by how the author uses "proof" in this article, they are referring to the Curry-Howard isomorphism that types represent propositions in a constructive logic and well-typed terms inhabiting those types can be considered as proofs. a :~: b is the type that a and b are "equal", i.e. they are the same type. the functions convert1 and convert2 witness the isomorphism between a and b. The core reason why GHC didn't allow the naïve recursive definition in the first place is because the definition failed the occurs check[0], so using type families and explicitly labeling the types circumvents the problem. [0] https://en.wikipedia.org/wiki/Occurs_check https://en.wikipedia.org/wiki/Occurs_check