Unbound implicits are absent from the context

[spcfox]

Steps to Reproduce

X : Type
Y : X -> Type
Z : X -> Type

failing "While processing type of f. Can't find an implementation for X"
  f : Y x -> Z %search

f : {0 x : _} -> Y x -> Z %search

failing "While processing constructor MkD. Can't find an implementation for X"
  data D : Type where
    MkD : Y x -> Z %search -> D

data D : Type where
  MkD : {0 x : _} -> Y x -> Z %search -> D

Expected Behavior

An unbound x is equivalent to {0 x : _} ->

Observed Behavior

%search finds x in the second case, but not in the first case

[spcfox]

x is also not in context

f : Y x -> Z ?holeF
g : {0 x : _} -> Y x -> Z ?holeG

Main> :ti holeF
Main.holeF : X
Main> :ti holeG
 0 {x : X}
------------------------------
holeG : X

[spcfox]

Also they can't be used in let

failing "Undefined name a"
  f : (x : a) -> let y = a in y

g : {0 a : _} -> (x : a) -> let y = a in y