Skip to content
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

Add --censor flag support for censoring type errors #1329

Merged
merged 5 commits into from
Sep 22, 2019

Conversation

Gabriella439
Copy link
Collaborator

Fixes #1294

@Gabriella439
Copy link
Collaborator Author

Example output:

$ dhall --explain --censor <<< '"ABC" : Natural'
Error: Expression doesn't match annotation

- Natural
+ Text

Explanation: You can annotate an expression with its type or kind using the     
❰:❱ symbol, like this:                                                          
                                                                                
                                                                                
    ┌───────┐                                                                   
    │ x : t │  ❰x❱ is an expression and ❰t❱ is the annotated type or kind of ❰x❱
    └───────┘                                                                   
                                                                                
The type checker verifies that the expression's type or kind matches the        
provided annotation                                                             
                                                                                
For example, all of the following are valid annotations that the type checker   
accepts:                                                                        
                                                                                
                                                                                
    ┌─────────────┐                                                             
    │ 1 : Natural │  ❰1❱ is an expression that has type ❰Natural❱, so the type  
    └─────────────┘  checker accepts the annotation                             
                                                                                
                                                                                
    ┌───────────────────────┐                                                   
    │ Natural/even 2 : Bool │  ❰Natural/even 2❱ has type ❰Bool❱, so the type    
    └───────────────────────┘  checker accepts the annotation                   
                                                                                
                                                                                
    ┌────────────────────┐                                                      
    │ List : Type → Type │  ❰List❱ is an expression that has kind ❰Type → Type❱,
    └────────────────────┘  so the type checker accepts the annotation          
                                                                                
                                                                                
    ┌──────────────────┐                                                        
    │ List Text : Type │  ❰List Text❱ is an expression that has kind ❰Type❱, so 
    └──────────────────┘  the type checker accepts the annotation               
                                                                                
                                                                                
However, the following annotations are not valid and the type checker will
reject them:                                                                    
                                                                                
                                                                                
    ┌──────────┐                                                                
    │ 1 : Text │  The type checker rejects this because ❰1❱ does not have type  
    └──────────┘  ❰Text❱                                                        
                                                                                
                                                                                
    ┌─────────────┐                                                             
    │ List : Type │  ❰List❱ does not have kind ❰Type❱                           
    └─────────────┘                                                             
                                                                                
                                                                                
Some common reasons why you might get this error:                               
                                                                                
● The Haskell Dhall interpreter implicitly inserts a top-level annotation       
  matching the expected type                                                    
                                                                                
  For example, if you run the following Haskell code:                           
                                                                                
                                                                                
    ┌───────────────────────────────┐                                           
    │ >>> input auto "1" :: IO Text │                                         
    └───────────────────────────────┘                                           
                                                                                
                                                                                
  ... then the interpreter will actually type check the following annotated     
  expression:                                                                   
                                                                                
                                                                                
    ┌──────────┐                                                                
    │ 1 : Text │                                                                
    └──────────┘                                                                
                                                                                
                                                                                
  ... and then type-checking will fail                                          
                                                                                
────────────────────────────────────────────────────────────────────────────────
                                                                                
You or the interpreter annotated this expression:                               
                                                                                
↳ "   "
                                                                                
... with this type or kind:                                                     
                                                                                
↳ Natural
                                                                                
... but the inferred type or kind of the expression is actually:                
                                                                                
↳ Text

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

1│                 

(stdin):1:1

Copy link
Collaborator

@sjakobi sjakobi left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM apart from a few wibbles! 👍

censorSrc :: Src -> Src
censorSrc (Src { srcText = oldText, .. }) = Src { srcText = newText, .. }
where
newText = Data.Text.map (\_ -> ' ') oldText
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
newText = Data.Text.map (\_ -> ' ') oldText
newText = censorText oldText

@@ -27,7 +28,7 @@ hash censor = do

resolvedExpression <- State.evalStateT (Dhall.Import.loadWith parsedExpression) status

case Dhall.TypeCheck.typeOf resolvedExpression of
case Dhall.TypeCheck.typeWith Context.empty resolvedExpression of
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't mind, but what's the motivation for this change?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's a mistake which I'll undo. I made this change as part of a refactor to add a new argument to typeWith, but then realized that I could restructure this change to not require argument passing. However, I forgot to undo this change along the way

xys' = [ (censorText x, censorExpression y) | (x, y) <- xys ]

censorText :: Text -> Text
censorText = Data.Text.map (\_ -> ' ')
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can we reuse this for censoring parser errors, too?

... as caught by @sjakobi
... as caught by @sjakobi

This is a vestige of a refactor that I reverted incompletely
@mergify mergify bot merged commit 183cc92 into master Sep 22, 2019
@mergify mergify bot deleted the gabriel/censor_type_error branch September 22, 2019 04:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

[Feature Request] CLI flag to censor record values while printing error
2 participants