diff --git a/src/Juvix/Compiler/Abstract/Data/Name.hs b/src/Juvix/Compiler/Abstract/Data/Name.hs
index a62d53320..d826d6532 100644
--- a/src/Juvix/Compiler/Abstract/Data/Name.hs
+++ b/src/Juvix/Compiler/Abstract/Data/Name.hs
@@ -47,15 +47,16 @@ instance Pretty Name where
       <> "@"
       <> pretty (n ^. nameId)
 
+addNameIdTag :: Bool -> NameId -> Doc a -> Doc a
+addNameIdTag showNameId nid
+  | showNameId = (<> ("@" <> pretty nid))
+  | otherwise = id
+
 prettyName :: HasNameKindAnn a => Bool -> Name -> Doc a
 prettyName showNameId n =
   annotate
     (annNameKind (n ^. nameKind))
-    (pretty (n ^. namePretty) <>? uid)
-  where
-    uid
-      | showNameId = Just ("@" <> pretty (n ^. nameId))
-      | otherwise = Nothing
+    (addNameIdTag showNameId (n ^. nameId) (pretty (n ^. namePretty)))
 
 type FunctionName = Name
 
diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs
index 713958d5c..229f94dd0 100644
--- a/src/Juvix/Compiler/Internal/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs
@@ -104,7 +104,9 @@ instance PrettyCode Function where
     return $ funParameter' <+> kwArrow <+> funReturn'
 
 instance PrettyCode Hole where
-  ppCode _ = return kwHole
+  ppCode h = do
+    showNameId <- asks (^. optShowNameIds)
+    return (addNameIdTag showNameId (h ^. holeId) kwHole)
 
 instance PrettyCode InductiveConstructorDef where
   ppCode c = do
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
index 53c438075..2d45dbd5f 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
@@ -529,7 +529,8 @@ inferExpression' hint e = case e of
   ExpressionLambda l -> goLambda l
   where
     goHole :: Hole -> Sem r TypedExpression
-    goHole h =
+    goHole h = do
+      void (queryMetavar h)
       return
         TypedExpression
           { _typedExpression = ExpressionHole h,
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
index a34f5a1d6..cd89fd518 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
@@ -1,4 +1,3 @@
--- TODO: RENAME!
 module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Inference
   ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Inference,
     module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.FunctionsTable,
@@ -7,6 +6,7 @@ where
 
 import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Internal.Extra
+import Juvix.Compiler.Internal.Pretty
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.FunctionsTable
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
@@ -63,9 +63,14 @@ closeState = \case
       Sem r' ()
     f m = mapM_ goHole (HashMap.keys m)
       where
+        getState :: Hole -> MetavarState
+        getState h = fromMaybe err (m ^. at h)
+          where
+            err :: a
+            err = error ("Impossible: could not find the state for the hole " <> ppTrace h)
         goHole :: Hole -> Sem r' Expression
         goHole h =
-          let st = fromJust (m ^. at h)
+          let st = getState h
            in case st of
                 Fresh -> throw (ErrUnsolvedMeta (UnsolvedMeta h))
                 Refined t -> do
diff --git a/test/Internal/Eval/Positive.hs b/test/Internal/Eval/Positive.hs
index 15003e4d2..7767da0c8 100644
--- a/test/Internal/Eval/Positive.hs
+++ b/test/Internal/Eval/Positive.hs
@@ -69,11 +69,6 @@ tests =
       $(mkRelDir ".")
       $(mkRelFile "IdenFunctionArgsImplicit.juvix")
       $(mkRelFile "out/IdenFunctionArgsImplicit.out"),
-    PosTest
-      "A function with no explicit arguments"
-      $(mkRelDir ".")
-      $(mkRelFile "IdenFunctionArgsNoExplicit.juvix")
-      $(mkRelFile "out/IdenFunctionArgsNoExplicit.out"),
     PosTest
       "A module that imports another"
       $(mkRelDir "Import")
diff --git a/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs
index 69365e581..6130f6f9c 100644
--- a/test/Typecheck/Negative.hs
+++ b/test/Typecheck/Negative.hs
@@ -119,6 +119,13 @@ tests =
       $(mkRelFile "WrongReturnTypeTooManyArguments.juvix")
       $ \case
         ErrExpectedFunctionType {} -> Nothing
+        _ -> wrongError,
+    NegTest
+      "Ambiguous hole"
+      $(mkRelDir "Internal")
+      $(mkRelFile "IdenFunctionArgsNoExplicit.juvix")
+      $ \case
+        ErrUnsolvedMeta {} -> Nothing
         _ -> wrongError
   ]
 
diff --git a/test/Typecheck/Positive.hs b/test/Typecheck/Positive.hs
index 8ae65df95..f864b7f9d 100644
--- a/test/Typecheck/Positive.hs
+++ b/test/Typecheck/Positive.hs
@@ -173,5 +173,9 @@ tests =
     PosTest
       "As Patterns"
       $(mkRelDir "Internal")
-      $(mkRelFile "AsPattern.juvix")
+      $(mkRelFile "AsPattern.juvix"),
+    PosTest
+      "Issue 1693 (Inference and higher order functions)"
+      $(mkRelDir "issue1693")
+      $(mkRelFile "M.juvix")
   ]
diff --git a/tests/Internal/positive/out/IdenFunctionArgsNoExplicit.out b/tests/Internal/positive/out/IdenFunctionArgsNoExplicit.out
deleted file mode 100644
index 26af6a865..000000000
--- a/tests/Internal/positive/out/IdenFunctionArgsNoExplicit.out
+++ /dev/null
@@ -1 +0,0 @@
-zero
diff --git a/tests/Internal/positive/IdenFunctionArgsNoExplicit.juvix b/tests/negative/Internal/IdenFunctionArgsNoExplicit.juvix
similarity index 100%
rename from tests/Internal/positive/IdenFunctionArgsNoExplicit.juvix
rename to tests/negative/Internal/IdenFunctionArgsNoExplicit.juvix
diff --git a/tests/positive/issue1693/M.juvix b/tests/positive/issue1693/M.juvix
new file mode 100644
index 000000000..9030510a6
--- /dev/null
+++ b/tests/positive/issue1693/M.juvix
@@ -0,0 +1,21 @@
+module M;
+  open import Stdlib.Prelude;
+
+  S : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → (A → B) → A → C;
+  S x y z := x z (y z);
+
+  K : {A : Type} → {B : Type} → A → B → A;
+  K x y := x;
+
+  I : {A : Type} → A → A;
+  I := S K (K {_} {Bool});
+
+  main : IO;
+  main := printNatLn
+    $ I {Nat} 1
+      + I I 1
+      + I (I 1)
+      + I 1
+      + I (I I) I (I I I) 1
+      + I I I (I I I (I I)) I (I I) I I I 1;
+end;
diff --git a/tests/positive/issue1693/juvix.yaml b/tests/positive/issue1693/juvix.yaml
new file mode 100644
index 000000000..e69de29bb