From 3b452e7d7638ff515cede0f1f14831dd6f1fe51e Mon Sep 17 00:00:00 2001 From: janmasrovira Date: Mon, 9 Jan 2023 18:56:28 +0100 Subject: [PATCH] Fix #1693 (#1708) --- 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/Internal/Eval/Positive.hs | 5 ----- test/Typecheck/Negative.hs | 7 +++++++ test/Typecheck/Positive.hs | 6 +++++- .../out/IdenFunctionArgsNoExplicit.out | 1 - .../IdenFunctionArgsNoExplicit.juvix | 0 tests/positive/issue1693/M.juvix | 21 +++++++++++++++++++ tests/positive/issue1693/juvix.yaml | 0 11 files changed, 51 insertions(+), 16 deletions(-) delete mode 100644 tests/Internal/positive/out/IdenFunctionArgsNoExplicit.out rename tests/{Internal/positive => negative/Internal}/IdenFunctionArgsNoExplicit.juvix (100%) 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 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