Fix #1693

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
 

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

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,

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

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")

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
   ]
 

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")
   ]

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;