How to solve the type mismatch error in this currying function?

Question

I tried to define a polymorphic type:

(define-type (listt a)
  (U Empty
     (Cons a)))

(struct Empty ()) (struct (a) Cons ([v : a] [w : (listt a)]))

and a currying function:

;; a better name for subst-c is subst-currying
(: subst-c : (∀ (a) ((-> a Boolean) -> a (listt a) -> (listt a))))
(define (subst-c pred)
  (lambda (n listt)
    (match listt
      [(Empty)
       (Empty)]
      [(Cons e t)
       (if (pred e)
           (Cons n ((subst-c pred) n t))
           (Cons e ((subst-c pred) n t)))])))

but got error

;Type Checker: type mismatch
;   expected: Nothing
;   given: a
;   in: n
;Type Checker: type mismatch
;   expected: (U Empty (Cons Nothing))
;   given: (U Empty (Cons a))
;   in: t

I'm confused about it， what did I do wrong?

Asumu Takikawa Asumu Takikawa · Accepted Answer · 2016-04-17T16:46:25

If you add a few type variable instantiations manually, this code actually type-checks. Like this:

(: subst-c : (∀ (a) ((-> a Boolean) -> a (listt a) -> (listt a))))
(define (subst-c pred)
  (lambda (n listt)
    (match listt
      [(Empty)
       (Empty)]
      [(Cons e t)
       (if (pred e)
           (Cons n (((inst subst-c a) pred) n t))      ;; <-- Right here
           (Cons e (((inst subst-c a) pred) n t)))]))) ;; <-- and here

The inst operator is for instantiating a type variable. In this case, for the recursive use of subst-c. I'm not sure why this needs to be manually instantiated here. I think it might be a bug/limitation with Typed Racket's type inference.

I was able to figure out where to put these in by looking at the type tooltips that pop up in DrRacket (hover your mouse over an expression to see the type) and seeing where the Nothing came from.

How to solve the type mismatch error in this currying function?

1 Answers