Unclear error message for (second x) expression

[srcreigh]

Thank you so much for typed racket.. I hope to be able to help improve it

What version of Racket are you using?

7.6

What program did you run?

#lang typed/racket

(provide Text Header Paragraph ToplevelElement Title PageAttribute Page
         load-page)

(define-type Text String)
(define-type Header (List 'header Text))
(define-type Paragraph (List 'paragraph Text))
(define-type ToplevelElement (U Header Paragraph))
(define-type Title (List 'title String))
(define-type PageAttribute (U Title))
(define-type Page (List 'page (Listof PageAttribute) (Listof ToplevelElement)))

(: load-page (String . -> . Page))
(define (load-page id)
  `(page
    ((title "Test page"))
    ((header "Test page") (paragraph "This is a test. How does it look?"))))

(: page-attr (Page (U 'title) . -> . (U #f PageAttribute)))
(define (page-attr p t)
  (assoc t (second p)))

(: page-title (Page . -> . (U Title #f)))
(define (page-title p)
  (let ([title (page-attr p 'title)])
    (if title (second title) #f)))

What should have happened?

provide clear error message for fixing type error at (second title) in last line

If you got an error message, please include it here.

Polymorphic function `second' could not be applied to arguments:
Types: (List* a r (Listof t)) -> (r : ((! (cadr (0 0)) False) | (: (cadr (0 0)) False)) : (cadr (0 0))
       (Listof a) -> a
Arguments: Title
Expected result: (U False Title)

Discussion

In hindsight the problem was very simple, the (second title) returns a String but the function need a Title or #f. The bug was in the function as I meant it to return a String or #f.

I have a few highly naive ideas to improve the error message:

1. Making the (cadr (0 0)) type easier to learn about. I searched the docs website, grepped this repo looking for type declarations of second or of cadr but couldn't find any. I still haven't found info about what the (cadr (0 0)) type means. I also tried copying it out to a define-type to track down the cadr type via xref, but it fails to parse at the |

(define-type second (List* a r (Listof t)) -> (r : ((! (cadr (0 0)) False) | (: (cadr (0 0)) False)) : (cadr (0 0))))

2. You probably hear this too much, but if it displayed the type it was inferring for the expression (ex: Expected (U False Title) but got String) that would have made the issue very clear.

[samth]

For 1, that portion of the type just shouldn't be printed at all (and when it is printed, it should print in the way you can write it). It isn't involved in the problem you actually had.

For 2, it would definitely be better to include that information in the error message. Unfortunately, the algorithm that Typed Racket uses doesn't have that information, so a pretty substantial revision of the inference code is needed to fix that.