Continuing a bit on the subject posted on this thread, I have run into two cases where a function produces identical outcomes for all input but has different hashes. Both came up when I was refactoring dhall code, which gave me the spooks as I was pretty sure my logic hadn’t changed, so I had to run several examples a la quickcheck just to convince myself it hadn’t.

## Case 1

```
let Natural/equal : Natural -> Natural -> Bool =
https://prelude.dhall-lang.org/Natural/equal
sha256:7f108edfa35ddc7cebafb24dc073478e93a802e13b5bc3fd22f4768c9b066e60
let neq: Natural -> Natural -> Bool = \(n0: Natural) -> \(n1: Natural) -> Natural/equal n0 n1
in neq
```

yields a hash `sha256:7f108edfa35ddc7cebafb24dc073478e93a802e13b5bc3fd22f4768c9b066e60`

, whereas

```
let Natural/equal : Natural -> Natural -> Bool =
https://prelude.dhall-lang.org/Natural/equal
sha256:7f108edfa35ddc7cebafb24dc073478e93a802e13b5bc3fd22f4768c9b066e60
let neq: Natural -> Natural -> Bool = \(n0: Natural) -> \(n1: Natural) -> Natural/equal n1 n0
in neq
```

yields a hash `sha256:9e0e952e097a2a974ca4ed3e65bcf395cda2bb54382c8ecc3963bca50bfff124`

.

## Case 2

```
let Natural/equal : Natural -> Natural -> Bool =
https://prelude.dhall-lang.org/Natural/equal
sha256:7f108edfa35ddc7cebafb24dc073478e93a802e13b5bc3fd22f4768c9b066e60
let User: Type = { id : Natural, name : Text }
let userEq: User -> User -> Bool = \(u0: User) -> \(u1: User) -> Natural/equal u0.id u1.id
in userEq
```

Yields a hash of `sha256:9dd6204f24c38fec828b454492d37086018b2781b2189f5e270d824055a2fe20`

whereas

```
let Natural/equal : Natural -> Natural -> Bool =
https://prelude.dhall-lang.org/Natural/equal
sha256:7f108edfa35ddc7cebafb24dc073478e93a802e13b5bc3fd22f4768c9b066e60
let User: Type = { id : Natural, name : Text, email : Text }
let userEq: User -> User -> Bool = \(u0: User) -> \(u1: User) -> Natural/equal u0.id u1.id
in userEq
```

yields a hash of `sha256:9c5e711166f46d9c69f6fc1d2cf4dd2dc7c14495f9ae60259fa27f468c1cc1f0`

.

## Comments

The two cases are different, and perhaps this is intended behavior, but it caught me by surprise so maybe there is a way to document it? In general, like my first post, it is getting at issues of extensionality in Dhall. Basically, I’m trying to avoid experimenting with heavier solutions like `z3`

or `coq`

for verifying that certain configurations haven’t changed, and if I can bend dhall to do this that’d be great as my configurations are in dhall anyway and it’d prevent me from using another tool/language.

Thanks for your help!