New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Poor error message on unbound variable #217

Closed
ocharles opened this Issue Jan 20, 2018 · 5 comments

Comments

Projects
None yet
2 participants
@ocharles
Collaborator

ocharles commented Jan 20, 2018

Given

    let GitHubProject : Type = { owner : Text, repo : Text }

in  let gitHubProject =
            λ(github : GitHubProject)
          →     let gitHubRoot =
                          "https://github.com/"
                      ++  github.owner
                      ++  "/"
                      ++  github.repo
                      ++  ""
            
            in    ./empty-package.dhall 
                ⫽ { bugReports = gitHubRoot ++ "/issues", name = repo }

in  gitHubProject

I get:

dhall-to-cabal: 
↳ ./dhall/gitHubProject.dhall 

majorVersion : List Natural → VersionRange
VersionRange : Type
anyVersion : VersionRange
github : { owner : Text, repo : Text }

Error: Unbound variable

Explanation: Expressions can only reference previously introduced (i.e. "bound")
variables that are still "in scope"                                           
                                                                                
For example, the following valid expressions introduce a "bound" variable named
❰x❱:                                                                            
                                                                                
                                                                                
    ┌─────────────────┐                                                         
    │ λ(x : Bool) → x │  Anonymous functions introduce "bound" variables      
    └─────────────────┘                                                         
        ⇧                                                                       
        This is the bound variable                                              
                                                                                
                                                                                
    ┌─────────────────┐                                                         
    │ let x = 1 in x  │  ❰let❱ expressions introduce "bound" variables        
    └─────────────────┘                                                         
          ⇧                                                                     
          This is the bound variable                                            
                                                                                
                                                                                
However, the following expressions are not valid because they all reference a   
variable that has not been introduced yet (i.e. an "unbound" variable):       
                                                                                
                                                                                
    ┌─────────────────┐                                                         
    │ λ(x : Bool) → y │  The variable ❰y❱ hasn't been introduced yet            
    └─────────────────┘                                                         
                    ⇧                                                           
                    This is the unbound variable                                
                                                                                
                                                                                
    ┌──────────────────────────┐                                                
    │ (let x = True in x) && x │  ❰x❱ is undefined outside the parentheses      
    └──────────────────────────┘                                                
                             ⇧                                                  
                             This is the unbound variable                       
                                                                                
                                                                                
    ┌────────────────┐                                                          
    │ let x = x in x │  The definition for ❰x❱ cannot reference itself          
    └────────────────┘                                                          
              ⇧                                                                 
              This is the unbound variable                                      
                                                                                
                                                                                
Some common reasons why you might get this error:                               
                                                                                
● You misspell a variable name, like this:                                      
                                                                                
                                                                                
    ┌────────────────────────────────────────────────────┐                      
    │ λ(empty : Bool) → if emty then "Empty" else "Full" │                  
    └────────────────────────────────────────────────────┘                      
                           ⇧                                                    
                           Typo                                                 
                                                                                
                                                                                
● You misspell a reserved identifier, like this:                                
                                                                                
                                                                                
    ┌──────────────────────────┐                                                
    │ foral (a : Type) → a → a │                                                
    └──────────────────────────┘                                                
      ⇧                                                                         
      Typo                                                                      
                                                                                
                                                                                
● You tried to define a recursive value, like this:                             
                                                                                
                                                                                
    ┌─────────────────────┐                                                     
    │ let x = x + +1 in x │                                                     
    └─────────────────────┘                                                     
              ⇧                                                                 
              Recursive definitions are not allowed                             
                                                                                
                                                                                
● You accidentally forgot a ❰λ❱ or ❰∀❱/❰forall❱                                 
                                                                                
                                                                                
        Unbound variable                                                        
        ⇩                                                                       
    ┌─────────────────┐                                                         
    │  (x : Bool) → x │                                                         
    └─────────────────┘                                                         
      ⇧                                                                         
      A ❰λ❱ here would transform this into a valid anonymous function           
                                                                                
                                                                                
        Unbound variable                                                        
        ⇩                                                                       
    ┌────────────────────┐                                                      
    │  (x : Bool) → Bool │                                                      
    └────────────────────┘                                                      
      ⇧                                                                         
      A ❰∀❱ or ❰forall❱ here would transform this into a valid function type    

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

let GitHubProject : Type = { owner : Text, repo : Text }

in  let gitHubProject =
            λ(github : GitHubProject)
          →     let gitHubRoot =
                          "https://github.com/"
                      ++  github.owner
                      ++  "/"
                      ++  github.repo
                      ++  ""
            
            in    ./empty-package.dhall 
                ⫽ { bugReports = gitHubRoot ++ "/issues", name = repo }

in  gitHubProject

dhall/gitHubProject.dhall:1:5

The unbound variable is repo, but the error message doesn't tell me that.

@Gabriel439

This comment has been minimized.

Collaborator

Gabriel439 commented Jan 20, 2018

Yeah, we can add the variable name to the error message.

For some context: https://github.com/dhall-lang/dhall-haskell/blob/master/src/Dhall/TypeCheck.hs#L743-L744

The original reason I recommended against the error message having the variable name is because the source span for the error should be localized to exactly the unbound variable. However, for some reason it looks like that didn't work here, so it's probably worth including the variable name in the error message as a fallback.

@Gabriel439

This comment has been minimized.

Collaborator

Gabriel439 commented Jan 21, 2018

Actually, I think I found the root cause for why the source span localization was so bad. This was related to the recent support for type synonyms and it's pretty simple fix, which produces this much better output:

dhall <<< './yourExample' 

Use "dhall --explain" for detailed errors

↳ ./yourExample 

github : { owner : Text, repo : Text }

Error: Unbound variable

repo

foo:12:66

Once I fix that would that satisfy your concerns or would you still like to see the name of the unbound variable on the Error: line?

Gabriel439 added a commit that referenced this issue Jan 21, 2018

Fix error localization
Related to #217

Two type-checking steps shift and substitute expressions:

* Function application
* `let` expressions (only more recently, in acd06c)

However, the `shift` and `subst` functions have the undesirable property
that they (unnecessarily) strip `Note` constructors.  As a result, any
type-checking step that involves either `Let` or `App` may produce poor error
localization.

The solution is to modify `shift` and `subst` to note remove `Note`
constructors and instead split that functionality out into a new
`denote` function.  Fixing this greatly improves error localization.
@Gabriel439

This comment has been minimized.

Collaborator

Gabriel439 commented Jan 21, 2018

Fix up in #218

Try that out and see if that improves the error messages for you. If it does, then I'll merge

@ocharles

This comment has been minimized.

Collaborator

ocharles commented Jan 21, 2018

Gabriel439 added a commit that referenced this issue Jan 21, 2018

Fix error localization (#218)
Related to #217

Two type-checking steps shift and substitute expressions:

* Function application
* `let` expressions (only more recently, in acd06c)

However, the `shift` and `subst` functions have the undesirable property
that they (unnecessarily) strip `Note` constructors.  As a result, any
type-checking step that involves either `Let` or `App` may produce poor error
localization.

The solution is to modify `shift` and `subst` to note remove `Note`
constructors and instead split that functionality out into a new
`denote` function.  Fixing this greatly improves error localization.
@Gabriel439

This comment has been minimized.

Collaborator

Gabriel439 commented Jan 21, 2018

In that case I will go ahead and close this since it should print the source span equivalent to the unbound variable now (assuming no other bugs in source span localizaiton)

@Gabriel439 Gabriel439 closed this Jan 21, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment