O programa Simple Typed Racket não verifica o tipo

Question

Eu sou um iniciante com Typed Racket e estava brincando com o muito simples Tree tipo definido no Guia do iniciante:

#lang typed/racket
(define-type Tree (U leaf node))
(struct: leaf ([val : Number]))
(struct: node ([left : Tree] [right : Tree]))

Como exercício, decidi escrever uma função de ordem superior para descer na árvore:

(: tree-descend : All (A) (Number -> A) (A A -> A) Tree -> A)
(define (tree-descend do-leaf do-node tree)
  (if (leaf? tree)
      (do-leaf (leaf-val tree))
      (do-node (tree-descend do-leaf do-node (node-left tree))
               (tree-descend do-leaf do-node (node-right tree)))))

Este tipo verifica bem.No entanto, quando tento usá-lo para redefinir o tree-sum função que soma todas as folhas, recebo uma mensagem de erro surpreendente e detalhada:

(: tree-sum : Tree -> Number)
(define (tree-sum t)
  (tree-descend identity + t))

As mensagens de erro são

Type Checker: Polymorphic function `tree-descend' could not be applied to arguments:
  Argument 1:
    Expected: (Number -> A)
    Given:    (All (a) (a -> a))
  Argument 2:
    Expected: (A A -> A)
    Given:    (case-> (-> Zero) (Zero Zero -> Zero) (One Zero -> One) 
               (Zero One -> One) (Positive-Byte Zero -> Positive-Byte)  
               [...lots of ways of combining subtypes of Number...]
               (Index Positive-Index Index -> Positive-Fixnum) 
               (Index Index Positive-Index -> in: (tree-descend identity + t)

Agora, para meus olhos destreinados, parece que isso deve funcionar perfeitamente, porque claramente o tipo polimórfico A deveria ser apenas Number e então tudo funciona.Obviamente, a linguagem discorda de mim por algum motivo, mas não tenho certeza de qual é esse motivo.

Answer 1

Infelizmente, Typed Racket não pode inferir a instanciação adequada de funções polimórficas como tree-descend quando você os aplica a argumentos polimórficos como identity.Se você substituir identity com (inst identity Number), então o programa funciona bem.