checkHole : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref EST (EState vars) => RigCount -> ElabInfo -> NestedNames vars -> Env Term vars -> FC -> UserName -> Maybe (Glued vars) -> Core (Term vars, Glued vars)