Dhall-haskell: Bug: current Prelude cannot be cached as it fails to deserialize

[f-f]

If I have a Prelude.dhall containing the following:

https://raw.githubusercontent.com/dhall-lang/dhall-lang/v7.0.0/Prelude/package.dhall

Then dhall freeze errors out:

$ dhall freeze --inplace Prelude.dhall

Use "dhall --explain" for detailed errors

_ : Bool
_ : Type
_ : _@2
_ : _@2

Error: Invalid predicate for ❰if❱

This happens with the latest release 1.22.0 and on master. Also the error with --explain is not much more helpful than this one

[f-f]

Actually the issue seems to be that the deserialization doesn't roundtrip: putting a hash on the above import works the first time you evaluate the expression, but not the second (because it deserializes from the cache)

[Gabriel439]

@f-f: It would still help me to see the error message with --explain

[f-f]

@Gabriel439 right sorry, here it is:

$ dhall --explain <<< "./Prelude.dhall"


_ : Bool
_ : Type
_ : _@2
_ : _@2

Error: Invalid predicate for ❰if❱

Explanation: Every ❰if❱ expression begins with a predicate which must have type
❰Bool❱

For example, these are valid ❰if❱ expressions:


    ┌──────────────────────────────┐
    │ if True then "Yes" else "No" │
    └──────────────────────────────┘
         ⇧
         Predicate


    ┌─────────────────────────────────────────┐
    │ λ(x : Bool) → if x then False else True │
    └─────────────────────────────────────────┘
                       ⇧
                       Predicate


... but these are not valid ❰if❱ expressions:


    ┌───────────────────────────┐
    │ if 0 then "Yes" else "No" │  ❰0❱ does not have type ❰Bool❱
    └───────────────────────────┘


    ┌────────────────────────────┐
    │ if "" then False else True │  ❰""❱ does not have type ❰Bool❱
    └────────────────────────────┘


Some common reasons why you might get this error:

● You might be used to other programming languages that accept predicates other
  than ❰Bool❱

  For example, some languages permit ❰0❱ or ❰""❱ as valid predicates and treat
  them as equivalent to ❰False❱.  However, the Dhall language does not permit
  this

────────────────────────────────────────────────────────────────────────────────

Your ❰if❱ expression begins with the following predicate:

↳ _@1

... that has type:

↳ _@2

... but the predicate must instead have type ❰Bool❱

────────────────────────────────────────────────────────────────────────────────

where the Prelude.dhall has this content:

https://raw.githubusercontent.com/dhall-lang/dhall-lang/v7.0.0/Prelude/package.dhall sha256:c5cd3e107bb2579d60084d9f7caa93b20e6230eafba4d56ce6fba100be2bc066

[Gabriel439]

I can narrow this down to ./Prelude/Bool/fold

[Gabriel439]

Here's a reproduction that doesn't involve serialization:

$ dhall <<< './dhall-lang/Prelude/Bool/fold' 
  λ(b : Bool)
→ λ(bool : Type)
→ λ(true : bool)
→ λ(false : bool)
→ if b then true else false

$ dhall --alpha <<< './dhall-lang/Prelude/Bool/fold' 
λ(_ : Bool) → λ(_ : Type) → λ(_ : _) → λ(_ : _@1) → if _@1 then _@1 else _

$ dhall --alpha <<< './dhall-lang/Prelude/Bool/fold'  | dhall

Use "dhall --explain" for detailed errors

_ : Bool
_ : Type
_ : _@2
_ : _@2

Error: Invalid predicate for ❰if❱

                                                    if _@1 then _@1 else _

(stdin):1:53

The bug appears to be due to the α-normalized form being incorrect. The reason it's triggered by serialization is due to serialization α-normalizing the expression. The next step is figuring out what is wrong with the α-normalization algorithm.

For reference, the α-normalized form should have been:

λ(_ : Bool) → λ(_ : Type) → λ(_ : _) → λ(_ : _@1) → if _@3 then _@1 else _

[AndrasKovacs]

This seems to be my bug, I'll look at it shortly.

[f-f]

@Gabriel439 thanks a lot for narrowing it down! I opened https://github.com/dhall-lang/dhall-lang/pull/521 with this case as a regression test

[Gabriel439]

Yeah, I can confirm that fcca883e00daadc377e784973f4121a28af659a0 is the commit that introduced this issue