Add error for ill-scoped inferred variables

anoma · Dec 14, 2023 · f3bdd72 · f3bdd72
1 parent 170a4d3
commit f3bdd72
Show file tree

Hide file tree

Showing 6 changed files with 83 additions and 32 deletions.
diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@@ -15,12 +15,11 @@ import Juvix.Compiler.Core.Translation.FromInternal.Builtins.Nat
 import Juvix.Compiler.Core.Translation.FromInternal.Data
 import Juvix.Compiler.Internal.Data.Name
 import Juvix.Compiler.Internal.Extra qualified as Internal
-import Juvix.Compiler.Internal.Pretty (ppTrace)
 import Juvix.Compiler.Internal.Pretty qualified as Internal
 import Juvix.Compiler.Internal.Translation.Extra qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking qualified as InternalTyped
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
 import Juvix.Data.Loc qualified as Loc
-import Juvix.Data.PPOutput
 import Juvix.Extra.Strings qualified as Str
 
 type MVisit = Visit Internal.ModuleIndex
@@ -50,8 +49,8 @@ unsupported thing = error ("Internal to Core: Not yet supported: " <> thing)
 mkIdentIndex :: Name -> Text
 mkIdentIndex = show . (^. Internal.nameId . Internal.unNameId)
 
-fromInternal :: (Member NameIdGen k) => Internal.InternalTypedResult -> Sem k CoreResult
-fromInternal i = do
+fromInternal :: (Members '[NameIdGen, Error JuvixError] k) => Internal.InternalTypedResult -> Sem k CoreResult
+fromInternal i = mapError (JuvixError . ErrBadScope) $ do
   res <-
     execInfoTableBuilder emptyInfoTable
       . evalState (i ^. InternalTyped.resultFunctions)
@@ -63,7 +62,7 @@ fromInternal i = do
         _coreResultInternalTypedResult = i
       }
   where
-    f :: (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, State InternalTyped.FunctionsTable, NameIdGen] r) => Sem r ()
+    f :: (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, State InternalTyped.FunctionsTable, NameIdGen, Error BadScope] r) => Sem r ()
     f = do
       reserveLiteralIntToNatSymbol
       reserveLiteralIntToIntSymbol
@@ -78,7 +77,7 @@ fromInternal i = do
       setupLiteralIntToNat literalIntToNatNode
       setupLiteralIntToInt literalIntToIntNode
 
-fromInternalExpression :: (Member NameIdGen r) => CoreResult -> Internal.Expression -> Sem r Node
+fromInternalExpression :: (Members '[NameIdGen, Error BadScope] r) => CoreResult -> Internal.Expression -> Sem r Node
 fromInternalExpression res exp = do
   let modules = res ^. coreResultInternalTypedResult . InternalTyped.resultModules
   fmap snd
@@ -97,7 +96,7 @@ goModule = visit . Internal.ModuleIndex
 
 goModuleNoVisit ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen, MVisit] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen, MVisit, Error BadScope] r) =>
   Internal.ModuleIndex ->
   Sem r ()
 goModuleNoVisit (Internal.ModuleIndex m) = do
@@ -110,7 +109,7 @@ goModuleNoVisit (Internal.ModuleIndex m) = do
 -- | predefine an inductive definition
 preInductiveDef ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen, Error BadScope] r) =>
   Internal.InductiveDef ->
   Sem r PreInductiveDef
 preInductiveDef i = do
@@ -149,7 +148,7 @@ preInductiveDef i = do
 
 goInductiveDef ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen, Error BadScope] r) =>
   PreInductiveDef ->
   Sem r ()
 goInductiveDef PreInductiveDef {..} = do
@@ -163,7 +162,7 @@ goInductiveDef PreInductiveDef {..} = do
 
 goConstructor ::
   forall r.
-  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, NameIdGen] r) =>
+  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, NameIdGen, Error BadScope] r) =>
   Symbol ->
   Internal.ConstructorDef ->
   Sem r ConstructorInfo
@@ -225,7 +224,7 @@ goConstructor sym ctor = do
 
 goMutualBlock ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen, Error BadScope] r) =>
   Internal.MutualBlock ->
   Sem r ()
 goMutualBlock (Internal.MutualBlock m) = preMutual m >>= goMutual
@@ -264,7 +263,7 @@ goMutualBlock (Internal.MutualBlock m) = preMutual m >>= goMutual
 
 preFunctionDef ::
   forall r.
-  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, NameIdGen] r) =>
+  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, NameIdGen, Error BadScope] r) =>
   Internal.FunctionDef ->
   Sem r PreFunctionDef
 preFunctionDef f = do
@@ -333,7 +332,7 @@ preFunctionDef f = do
 
 goFunctionDef ::
   forall r.
-  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, NameIdGen] r) =>
+  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, NameIdGen, Error BadScope] r) =>
   PreFunctionDef ->
   Sem r ()
 goFunctionDef PreFunctionDef {..} = do
@@ -357,7 +356,7 @@ strongNormalizeHelper ty = evalState InternalTyped.iniState (InternalTyped.stron
 
 goType ::
   forall r.
-  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, NameIdGen, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, NameIdGen, Reader IndexTable, Error BadScope] r) =>
   Internal.Expression ->
   Sem r Type
 goType ty = do
@@ -366,7 +365,7 @@ goType ty = do
 
 mkFunBody ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen, Error BadScope] r) =>
   Type -> -- converted type of the function
   Internal.FunctionDef ->
   Sem r Node
@@ -378,7 +377,7 @@ mkFunBody ty f =
 
 mkBody ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen, Error BadScope] r) =>
   Type -> -- type of the function
   Location ->
   NonEmpty ([Internal.PatternArg], Internal.Expression) ->
@@ -465,7 +464,7 @@ mkBody ty loc clauses
 
 goCase ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen, Error BadScope] r) =>
   Internal.Case ->
   Sem r Node
 goCase c = do
@@ -499,7 +498,7 @@ goCase c = do
 
 goLambda ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen, Error BadScope] r) =>
   Internal.Lambda ->
   Sem r Node
 goLambda l = do
@@ -508,7 +507,7 @@ goLambda l = do
 
 goLet ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen, Error BadScope] r) =>
   Internal.Let ->
   Sem r Node
 goLet l = goClauses (toList (l ^. Internal.letClauses))
@@ -596,7 +595,7 @@ fromTopIndex = runReader initIndexTable
 
 goAxiomDef ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen, Error BadScope] r) =>
   Internal.AxiomDef ->
   Sem r ()
 goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
@@ -699,7 +698,7 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
 
 fromPatternArg ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, State IndexTable, NameIdGen] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, State IndexTable, NameIdGen, Error BadScope] r) =>
   Internal.PatternArg ->
   Sem r Pattern
 fromPatternArg pa = case pa ^. Internal.patternArgName of
@@ -783,7 +782,7 @@ fromPatternArg pa = case pa ^. Internal.patternArgName of
 
 goPatternArgs ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen, Error BadScope] r) =>
   Level -> -- the level of the first binder for the matched value
   Internal.Expression ->
   [Internal.PatternArg] ->
@@ -841,7 +840,7 @@ addPatternVariableNames p lvl vars =
 
 goIden ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, Error BadScope] r) =>
   Internal.Iden ->
   Sem r Node
 goIden i = do
@@ -857,8 +856,8 @@ goIden i = do
           )
   case i of
     Internal.IdenVar n -> do
-      let err = error ("impossible: var not found: " <> ppTrace n <> " at " <> prettyText (getLoc n))
-      k <- HashMap.lookupDefault err id_ <$> asks (^. indexTableVars)
+      let err = throw (BadScope n)
+      k <- fromMaybeM err (HashMap.lookup id_ <$> asks (^. indexTableVars))
       varsNum <- asks (^. indexTableVarsNum)
       return (mkVar (setInfoLocation (n ^. nameLoc) (Info.singleton (NameInfo (n ^. nameText)))) (varsNum - k - 1))
     Internal.IdenFunction n -> do
@@ -917,7 +916,7 @@ goIden i = do
 
 goExpression ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen, Error BadScope] r) =>
   Internal.Expression ->
   Sem r Node
 goExpression = \case
@@ -937,7 +936,7 @@ goExpression = \case
 
 goFunction ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen, Error BadScope] r) =>
   ([Internal.FunctionParameter], Internal.Expression) ->
   Sem r Node
 goFunction (params, returnTypeExpr) = go params
@@ -960,7 +959,7 @@ goFunction (params, returnTypeExpr) = go params
 
 goSimpleLambda ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen, Error BadScope] r) =>
   Internal.SimpleLambda ->
   Sem r Node
 goSimpleLambda l = do
@@ -972,7 +971,7 @@ goSimpleLambda l = do
 
 goApplication ::
   forall r.
-  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) =>
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen, Error BadScope] r) =>
   Internal.Application ->
   Sem r Node
 goApplication a = do

diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs
@@ -37,6 +37,7 @@ data TypeCheckerError
   | ErrTraitNotTerminating TraitNotTerminating
   | ErrArityCheckerError ArityCheckerError
   | ErrDefaultArgLoop DefaultArgLoop
+  | ErrBadScope BadScope
 
 instance ToGenericError TypeCheckerError where
   genericError :: (Member (Reader GenericOptions) r) => TypeCheckerError -> Sem r GenericError
@@ -64,6 +65,7 @@ instance ToGenericError TypeCheckerError where
     ErrTraitNotTerminating e -> genericError e
     ErrArityCheckerError e -> genericError e
     ErrDefaultArgLoop e -> genericError e
+    ErrBadScope e -> genericError e
 
 instance Show TypeCheckerError where
   show = \case
@@ -90,3 +92,4 @@ instance Show TypeCheckerError where
     ErrTraitNotTerminating {} -> "ErrTraitNotTerminating"
     ErrArityCheckerError {} -> "ErrArityCheckerError"
     ErrDefaultArgLoop {} -> "ErrDefaultArgLoop"
+    ErrBadScope {} -> "ErrBadScope"
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs
@@ -612,3 +612,34 @@ instance ToGenericError DefaultArgLoop where
             "Inserting default arguments caused a loop. The involved arguments are:"
               <> line
               <> itemize (ppCode opts' <$> e ^. defaultArgLoop)
+
+newtype BadScope = BadScope
+  { _badScopeVar :: VarName
+  }
+
+makeLenses ''BadScope
+
+instance ToGenericError BadScope where
+  genericError e = ask >>= generr
+    where
+      generr opts =
+        return
+          GenericError
+            { _genericErrorLoc = i,
+              _genericErrorMessage = ppOutput msg,
+              _genericErrorIntervals = [i]
+            }
+        where
+          opts' = fromGenericOptions opts
+          i = getLoc (e ^. badScopeVar)
+          var = e ^. badScopeVar
+          msg :: Doc Ann =
+            annotate AnnImportant "Oops! This is a bug of the juvix compiler."
+              <> line
+              <> "Most likely, the inference algorithm inserted the variable"
+              <+> ppCode opts' var
+              <+> "in a place where it is not in scope."
+                <> line
+                <> "As a workaround, explicitly provide a type in the place where you think the variable got inserted."
+                <> line
+                <> "More information at https://github.com/anoma/juvix/issues/2247"
diff --git a/src/Juvix/Compiler/Pipeline/Repl.hs b/src/Juvix/Compiler/Pipeline/Repl.hs
@@ -12,6 +12,7 @@ import Juvix.Compiler.Core qualified as Core
 import Juvix.Compiler.Internal qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromConcrete qualified as FromConcrete
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
 import Juvix.Compiler.Pipeline.Artifacts
 import Juvix.Compiler.Pipeline.Artifacts.PathResolver
 import Juvix.Compiler.Pipeline.EntryPoint
@@ -157,7 +158,7 @@ registerImport p =
     )
     >>= fromInternalImport
 
-fromInternalImport :: (Members '[State Artifacts] r) => Internal.Import -> Sem r ()
+fromInternalImport :: (Members '[State Artifacts, Error JuvixError] r) => Internal.Import -> Sem r ()
 fromInternalImport i = do
   artiTable <- gets (^. artifactInternalTypedTable)
   let table = Internal.buildTable [i ^. Internal.importModule . Internal.moduleIxModule] <> artiTable
@@ -167,11 +168,12 @@ fromInternalImport i = do
     . runFunctionsTableArtifacts
     . readerTypesTableArtifacts
     . runReader Core.initIndexTable
+    . mapError (JuvixError . ErrBadScope)
     -- TODO add cache in Artifacts
     . evalVisitEmpty Core.goModuleNoVisit
     $ Core.goModule (i ^. Internal.importModule . Internal.moduleIxModule)
 
-fromInternalExpression :: (Members '[State Artifacts] r) => Internal.Expression -> Sem r Core.Node
+fromInternalExpression :: (Members '[State Artifacts, Error JuvixError] r) => Internal.Expression -> Sem r Core.Node
 fromInternalExpression exp = do
   typedTable <- gets (^. artifactInternalTypedTable)
   runNameIdGenArtifacts
@@ -180,6 +182,7 @@ fromInternalExpression exp = do
     . runFunctionsTableArtifacts
     . readerTypesTableArtifacts
     . runReader Core.initIndexTable
+    . mapError (JuvixError . ErrBadScope)
     $ Core.goExpression exp
 
 data ReplPipelineResult

diff --git a/test/Compilation/Negative.hs b/test/Compilation/Negative.hs
@@ -49,5 +49,9 @@ tests =
     NegTest
       "Test005: Axiom"
       $(mkRelDir ".")
-      $(mkRelFile "test005.juvix")
+      $(mkRelFile "test005.juvix"),
+    NegTest
+      "Test006: Ill scoped term (Thi is a bug. It should be positive)"
+      $(mkRelDir ".")
+      $(mkRelFile "test006.juvix")
   ]
diff --git a/tests/Compilation/negative/test006.juvix b/tests/Compilation/negative/test006.juvix
@@ -0,0 +1,11 @@
+-- Once https://github.com/anoma/juvix/issues/2247 is fixed, this should be moved to positive tests
+module test006;
+
+type Box (A : Type) :=
+  | box : A → Box A;
+
+x : Box ((B : Type) → B → B) :=
+  box {_} λ {C x := x};
+
+-- (B : Type) → B → B
+-- (x1 : _@1) -> (x2 : _@2) -> _@3