There's a related issue with type holes:

module Main where

import Prelude
import Effect (Effect)
import Effect.Console (log)

f :: forall @a. a -> a
f = identity

x :: { x :: Int }
x = f @{ x :: ?Help } { x: 42 }

main = log "Done"

produces:

  tests/TestCompiler.hs:140:18: 
  1) compiler, Passing examples, 'VTAsHole.purs' should compile and run without error
       Error found:
       in module Main
       at tests/purs/passing/VTAsHole.purs:11:15 - 11:20 (line 11, column 15 - line 11, column 20)
       
         Hole 'Help' has the inferred type
              
           Int
              
       
       in value declaration x
       
       See https://github.com/purescript/documentation/blob/master/errors/HoleInferredType.md for more information,
       or to contribute content related to this error.
       

  To rerun use: --match "/compiler/Passing examples/'VTAsHole.purs' should compile and run without error/"

Randomized with seed 194657359

How should this case be handled?

Holes are an explicit request for information; I think that behavior's correct.

But aren't type applications a user-supplied piece of information?

AFAICT, wildcards are only allowed in VTAs as a means of skipping the next type variable because there's not an alternative syntax.

But aren't type applications a user-supplied piece of information?

Yes. Let me restate: a hole is the user asking the compiler for information. No program with a hole anywhere in the source should compile, because the hole doesn't say ‘I don't care’ like a wildcard does; it says ‘tell me what I should put here (instead of completing the compilation)’.

I understand that. I'm asking, "Just because VTAs can be used to do that, should they?"

🤔 Perhaps my understanding of VTAs' purpose is too limited. I guess there's really no difference between these two mechanisms for instructing the compiler what the type with which to unify a is aside from which mechanism one uses:

f :: forall @a. a -> a
f = identity

bar = f @Int

baz = (f :: Int -> _)

They are different in that

• VTAs specify one part that may or may not affect the expression's type whereas type annotations can affect part (e.g. f :: Int -> _) or all (e.g. f :: Int -> Int) of the expression's type
• VTAs are order-dependent whereas type annotations are not
• VTAs are opt-in whereas type annotations are not.
• VTAs are less verbose than type annotations

If I'm arguing that VTAs should not allow type holes, then you could counter by asking, "Why can type annotations have them? If we want to be consistent, we should remove type holes from type annotations as well."

Well... all that to say... It feels weird to me to allow them here, but I can't disagree with them being there anymore based on the previous paragraph.