Error reporting for list element types happens after substitution

[ocharles]

Apologies for the brevity but let me just vomit out my current context. We have this in a Dhall file:

...
      , library            =
          [   ./dhall/defaults/Library.dhall 
            ⫽ { build-dependencies =
                  [ bounded "base" [ +4, +9, +0, +0 ] [ +5 ]
                  , before "ansi-wl-pprint" [ +0, +7 ]
                  , before "base16-bytestring" [ +0, +2 ]
                  , before "bytestring" [ +0, +11 ]
                  , before "case-insensitive" [ +1, +3 ]
...

build-dependencies goes on for a while

Yet when I type check this:

    Your first ❰List❱ element has this type:                                        
                                                                                    
    ↳ { bounds : VersionRange, package : Text }                                                                
                                                                                    
    ... but the following element at index 18:                          
                                                                                    
    ↳ (λ(package : Text) → λ(min : List Natural) → λ(max : List Natural) → { bounds = intersectVersionRanges (orLaterVersion min) (earlierVersion max), package = package }) "text-format" [+0, +4]                                                                
                                                                                    
    ... has this type instead:                                                      
                                                                                    
    ↳ ∀(max : List Natural) → { bounds : VersionRange, package : Text }                                                                

The 18th element is just some function application though:

                  , bounded "text-format" [ +0, +4 ]

[Gabriel439]

Yeah, the only reason that this line of the error message is displayed at all:

 ↳ (λ(package : Text) → λ(min : List ...

... is because I had not yet improved Dhall's error messages for lists to narrow the source span to the offending list element. What I propose is fixing the source span so that the error message becomes:

    Your first ❰List❱ element has this type:                                        
                                                                                    
    ↳ { bounds : VersionRange, package : Text }                                                                
                                                                                    
    ... but the following element at index 18 has this type instead:                                                      
                                                                                    
    ↳ ∀(max : List Natural) → { bounds : VersionRange, package : Text }  

...

bounded "text-format" [ +0, +4 ]

Would that work for you?

[ocharles]

Sure, that looks good to me

…

On 27 Jan 2018 4:40 pm, "Gabriel Gonzalez" ***@***.***> wrote: Yeah, the only reason that this line of the error message is displayed at all: ↳ (λ(package : Text) → λ(min : List ... ... is because I had not yet improved Dhall's error messages for lists to narrow the source span to the offending list element. What I propose is fixing the source span so that the error message becomes: Your first ❰List❱ element has this type: ↳ { bounds : VersionRange, package : Text } ... but the following element at index 18 has this type instead: ↳ ∀(max : List Natural) → { bounds : VersionRange, package : Text } ... bounded "text-format" [ +0, +4 ] Would that work for you? — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#230 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AABRjr5fq66f10L7WvcQQ6LFhB9zpM7Fks5tO1FwgaJpZM4RqVv3> .