From d99673088a1bf045308fd507c4e6438f4537c2e1 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 9 Jan 2023 15:18:58 +0100
Subject: [PATCH] fix #1693

---
 src/Juvix/Compiler/Abstract/Data/Name.hs      | 11 +++++-----
 src/Juvix/Compiler/Internal/Pretty/Base.hs    |  4 +++-
 .../Analysis/TypeChecking/Checker.hs          |  3 ++-
 .../Analysis/TypeChecking/Data/Inference.hs   |  9 ++++++--
 test/Typecheck/Positive.hs                    |  6 +++++-
 tests/positive/issue1693/M.juvix              | 21 +++++++++++++++++++
 tests/positive/issue1693/juvix.yaml           |  0
 7 files changed, 44 insertions(+), 10 deletions(-)
 create mode 100644 tests/positive/issue1693/M.juvix
 create mode 100644 tests/positive/issue1693/juvix.yaml

diff --git a/src/Juvix/Compiler/Abstract/Data/Name.hs b/src/Juvix/Compiler/Abstract/Data/Name.hs
index a62d53320a..d826d6532c 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 713958d5ca..229f94dd03 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 53c4380756..2d45dbd5f6 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 a34f5a1d6d..cd89fd5187 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/Typecheck/Positive.hs b/test/Typecheck/Positive.hs
index 8ae65df950..f864b7f9d5 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/positive/issue1693/M.juvix b/tests/positive/issue1693/M.juvix
new file mode 100644
index 0000000000..122e719a8c
--- /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 {A} := 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 0000000000..e69de29bb2