Example of non-trivial equivalence

increment.dhall

{- If I remember correctly, one consequence of Gödel's second incompleteness
   theorem is that extensional equivalence is not decidable in general for
   any programming language that can encode Peano numerals.

   The exact case that a programming language fails on may differ from language
   to language (depending on how many tricks they add to try to detect
   non-trivial equivalences).  However, many of them will typically fail to
   detect the equivalence between two ways to encode `increment` for Peano
   numerals.

   This is the case for Dhall, which will not detect that `increment0` and
   `increment1` are equivalence because they have different normal forms and
   Dhall doesn't do anything special to simplify them further.  This is a valid
   Dhall file and `increment0` and `increment1` are already both in normal
   form.

   However, `increment0` and `increment1` are extensionally equal, even if Dhall
   can't tell, because they will return the same result for all Peano numerals.
-}

let Peano = ∀(Peano : Type) → ∀(Succ : Peano → Peano) → ∀(Zero : Peano) → Peano

let increment0
    : Peano → Peano
    =   λ(n : Peano)
      → λ(Peano : Type)
      → λ(Succ : Peano → Peano)
      → λ(Zero : Peano)
      → n Peano Succ (Succ Zero)

let increment1
    : Peano → Peano
    =   λ(n : Peano)
      → λ(Peano : Type)
      → λ(Succ : Peano → Peano)
      → λ(Zero : Peano)
      → Succ (n Peano Succ Zero)

in  { increment0 = increment0, increment1 = increment1 }