I agree that τ : ∀ σ. σ is the usual meaning of a typed hole; but the "typed hole" could ostensibly also generate a fresh type that fits and then panic at run-time in some circumstances. It's does not have the same exact semantics, but I think it's purpose is roughly the same (i.e. "Hi rustc, please, can you just let me get away with not giving you all the info right now? Thanks."). It seems also reminiscent of GHC's -fdefer-type-errors and these work well with GHC's typed holes.
This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.