Dolmen's Typechecker is sometimes too smart for the SMTLIB

[Gbury]

Consider the following problem:

(set-logic QF_UFLIA)
(declare-datatypes ((list 1)) ((par (alpha) ((nil) (cons (head (list alpha)))))))
(assert (= (as nil (list Int)) nil))
(check-sat)

Dolmen's tff typechecker is able to infer the type of the second nil because it knows the type of the first one, whereas cvc4 will complain. I don't know how much of a problem that is.