Description
I noticed (or remembered... I think we noticed this before) that long list literals take a long time to typecheck. I looked at it and I think the root cause is solving the implicit arguments of Cons.
In a synthetic file like this:
module Slow
(* let cons (x : int) (xs : list int) : list int = Cons x xs *)
let cons (x : 'a) (xs : list 'a) : list 'a = Cons x xs
let init : list int =
cons 1 <| cons 1 <| cons 1 <| cons 1 <| cons 1 <| cons 1 <| cons 1 <| cons 1 <| cons 1 <| cons 1 <|
cons 1 <| cons 1 <| cons 1 <| cons 1 <| cons 1 <| cons 1 <| cons 1 <| cons 1 <| cons 1 <| cons 1 <|
cons 1 <| cons 1 <| cons 1 <| cons 1 <| cons 1 <| cons 1 <| cons 1 <| cons 1 <| cons 1 <| cons 1 <|
....(though much longer), it takes around 20s to typecheck it. If instead we replace the definition of cons for the commented one, which just works on ints, it takes around 2s. Clearly there's an overhead to using the unifier to solve the types and instantiating the implcits, but 10x seems excessive. I think, but I didn't confirm, that the problem may come from the checking of applications not unifying the expected type as it goes through the arguments.
That is, when we check cons 1 e at expected type int, it must be the case that e <: int. But what I think happens is that we allocate a fresh ?u, check 1 against the expected type ?u, which works (with a deferred problem for int <: ?u, and then we check e against list ?u. This accumulates tons of constraints and they only get solved at the end, which probably requires much more time and memory.