Non-Auto Implicits get Deferred as Holes and not checked on REPL Evaluation

[fabianhjr]

Steps to Reproduce

Load the following into a repl idris2 Test.idr

module Test

data TNat = TZ | TS TNat

data IsZero : TNat -> Type where
  ItIsZero : IsZero TZ

isZero : (n: TNat) -> {ok: IsZero n} -> Bool
isZero _ = True

isZero' : (n: TNat) -> {auto ok: IsZero n} -> Bool
isZero' _ = True

Expected Behavior

Test> isZero TZ
True
Test> isZero (TS TZ)
(interactive):1:1--1:16:Can't find an implementation for IsZero (TS TZ)
Test> isZero' TZ
True
Test> isZero' (TS TZ)    
(interactive):1:1--1:16:Can't find an implementation for IsZero (TS TZ)
Test> 
Bye for now!

Observed Behavior

Test> isZero TZ
True
Test> isZero (TS TZ)
True                                  <<<<<
Test> isZero' TZ
True
Test> isZero' (TS TZ)    
(interactive):1:1--1:16:Can't find an implementation for IsZero (TS TZ)
Test> 
Bye for now!

Aparently it is treating the evaluation of isZero as having a hole:

test : Bool
test = isZero (TS TZ)

Test.idr:12:8--13:1:Unsolved holes:
Test.{ok:174} introduced at Test.idr:12:8--13:1

[edwinb]

I suspect this is just that it's not checking whether there are holes left over after checking at the REPL (via checkUserHoles), and given that the missing argument isn't checked or used at all in the definition, it can still successfully evaluate it.