It's really useful when tracking down typechecking bugs to be able to see the trace of the typechecker's decisions. This is challenging to display mostly because the input and output contexts can be very large. A simple example, omitting output contexts:
check {} -> (\x -> x) : A -> A
check {x : A} -> x : A
infer {x : A} -> x : A
subtype {x : A} -> A < A
Ideally we'd have a flag that would enable printing a debugging trace during typechecking that would help track down bugs.
It's really useful when tracking down typechecking bugs to be able to see the trace of the typechecker's decisions. This is challenging to display mostly because the input and output contexts can be very large. A simple example, omitting output contexts:
Ideally we'd have a flag that would enable printing a debugging trace during typechecking that would help track down bugs.