Fix type synonym in let (#1880)

- Closes #1879 

The issue was possibly caused by the use of `readerState`:
```
readerState :: forall a r x. (Member (State a) r) => Sem (Reader a ': r) x -> Sem r x
readerState m = get >>= (`runReader` m)
```

I originally thought it would be a good idea to "freeze" some `State`
effect into a `Reader` effect in the following situation:
- Some function `s` needs to update the state.
- Some function `f` only reads the state.
- Then you would have `g .. = ... readerState @MyState f`
- This way, it would be reflected in the type that `g` cannot update the
state. However, for some reason I have not been able to clearly
identify, this was not working as expected.

src/Juvix/Compiler/Internal/Pretty/Base.hs

@@ -336,10 +336,21 @@ ppCodeAtom c = do
   p' <- ppCode c
   return $ if isAtomic c then p' else parens p'
 
+instance PrettyCode a => PrettyCode (Maybe a) where
+  ppCode = \case
+    Nothing -> return "Nothing"
+    Just p -> ("Nothing" <+>) <$> ppCode p
+
+instance (PrettyCode a, PrettyCode b) => PrettyCode (a, b) where
+  ppCode (x, y) = do
+    x' <- ppCode x
+    y' <- ppCode y
+    return $ encloseSep "(" ")" ", " [x', y']
+
 instance (PrettyCode a) => PrettyCode [a] where
   ppCode x = do
     cs <- mapM ppCode (toList x)
-    return $ encloseSep "(" ")" ", " cs
+    return $ encloseSep "[" "]" ", " cs
 
 instance (PrettyCode a) => PrettyCode (NonEmpty a) where
   ppCode x = ppCode (toList x)

src/Juvix/Compiler/Internal/Translation/FromInternal.hs

@@ -55,7 +55,7 @@ typeCheckExpressionType ::
 typeCheckExpressionType InternalTypedResult {..} exp =
   mapError (JuvixError @TypeCheckerError)
     $ do
-      runReader _resultFunctions
+      evalState _resultFunctions
       . evalState _resultIdenTypes
       . runReader table
       . ignoreOutput @Example

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs

@@ -59,7 +59,7 @@ checkStatement ::
 checkStatement s = case s of
   StatementFunction funs -> StatementFunction <$> runReader emptyLocalVars (checkMutualBlock funs)
   StatementForeign {} -> return s
-  StatementInductive ind -> StatementInductive <$> readerState @FunctionsTable (checkInductiveDef ind)
+  StatementInductive ind -> StatementInductive <$> checkInductiveDef ind
   StatementInclude i -> StatementInclude <$> checkInclude i
   StatementAxiom ax -> do
     modify (HashMap.insert (ax ^. axiomName) (ax ^. axiomType))
@@ -67,7 +67,7 @@ checkStatement s = case s of
 
 checkInductiveDef ::
   forall r.
-  (Members '[Reader EntryPoint, Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, State NegativeTypeParameters, Output Example, Builtins] r) =>
+  (Members '[Reader EntryPoint, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, State TypesTable, State NegativeTypeParameters, Output Example, Builtins] r) =>
   InductiveDef ->
   Sem r InductiveDef
 checkInductiveDef InductiveDef {..} = runInferenceDef $ do
@@ -130,16 +130,14 @@ checkMutualBlock ::
   (Members '[Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r) =>
   MutualBlock ->
   Sem r MutualBlock
-checkMutualBlock (MutualBlock ds) =
-  readerState @FunctionsTable $
-    MutualBlock <$> runInferenceDefs (mapM checkFunctionDef ds)
+checkMutualBlock (MutualBlock ds) = MutualBlock <$> runInferenceDefs (mapM checkFunctionDef ds)
 
 checkFunctionDef ::
   (Members '[Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Inference] r) =>
   FunctionDef ->
   Sem r FunctionDef
 checkFunctionDef FunctionDef {..} = do
-  funDef <- readerState @FunctionsTable $ do
+  funDef <- do
     _funDefType' <- checkFunctionDefType _funDefType
     registerIden _funDefName _funDefType'
     _funDefClauses' <- mapM (checkFunctionClause _funDefType') _funDefClauses
@@ -150,10 +148,10 @@ checkFunctionDef FunctionDef {..} = do
           ..
         }
   registerFunctionDef funDef
-  readerState @FunctionsTable (traverseOf funDefExamples (mapM checkExample) funDef)
+  traverseOf funDefExamples (mapM checkExample) funDef
 
 checkIsType ::
-  (Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable] r) =>
+  (Members '[Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable] r) =>
   Interval ->
   Expression ->
   Sem r Expression
@@ -161,7 +159,7 @@ checkIsType = checkExpression . smallUniverseE
 
 checkFunctionDefType ::
   forall r.
-  (Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable] r) =>
+  (Members '[Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable] r) =>
   Expression ->
   Sem r Expression
 checkFunctionDefType ty = checkIsType loc ty
@@ -169,7 +167,7 @@ checkFunctionDefType ty = checkIsType loc ty
     loc = getLoc ty
 
 checkExample ::
-  (Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Output Example, State TypesTable] r) =>
+  (Members '[Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Output Example, State TypesTable] r) =>
   Example ->
   Sem r Example
 checkExample e = do
@@ -179,7 +177,7 @@ checkExample e = do
 
 checkExpression ::
   forall r.
-  (Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Reader LocalVars, Inference, Output Example, State TypesTable] r) =>
+  (Members '[Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Reader LocalVars, Inference, Output Example, State TypesTable] r) =>
   Expression ->
   Expression ->
   Sem r Expression
@@ -203,7 +201,7 @@ checkExpression expectedTy e = do
           )
 
 checkFunctionParameter ::
-  (Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable] r) =>
+  (Members '[Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable] r) =>
   FunctionParameter ->
   Sem r FunctionParameter
 checkFunctionParameter (FunctionParameter mv i e) = do
@@ -253,7 +251,7 @@ checkConstructorReturnType indType ctor = do
     )
 
 inferExpression ::
-  (Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable] r) =>
+  (Members '[Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable] r) =>
   Maybe Expression -> -- type hint
   Expression ->
   Sem r Expression
@@ -266,7 +264,7 @@ lookupVar v = HashMap.lookupDefault err v <$> asks (^. localTypes)
 
 checkFunctionClause ::
   forall r.
-  (Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Inference, Builtins, State TypesTable, Output Example, Reader LocalVars] r) =>
+  (Members '[Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Inference, Builtins, State TypesTable, Output Example, Reader LocalVars] r) =>
   Expression ->
   FunctionClause ->
   Sem r FunctionClause
@@ -281,7 +279,7 @@ checkFunctionClause clauseType FunctionClause {..} = do
 -- | helper function for function clauses and lambda functions
 checkClause ::
   forall r.
-  (Members '[Reader InfoTable, Reader FunctionsTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Builtins, Output Example, State TypesTable] r) =>
+  (Members '[Reader InfoTable, State FunctionsTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Builtins, Output Example, State TypesTable] r) =>
   -- | Type
   Expression ->
   -- | Arguments
@@ -346,7 +344,7 @@ matchIsImplicit expected actual =
 
 checkPattern ::
   forall r.
-  (Members '[Reader InfoTable, Error TypeCheckerError, State LocalVars, Inference, NameIdGen, Reader FunctionsTable] r) =>
+  (Members '[Reader InfoTable, Error TypeCheckerError, State LocalVars, Inference, NameIdGen, State FunctionsTable] r) =>
   FunctionParameter ->
   PatternArg ->
   Sem r ()
@@ -490,7 +488,7 @@ literalType lit@(WithLoc i l) = case l of
 
 inferExpression' ::
   forall r.
-  (Members '[Reader InfoTable, Reader FunctionsTable, State TypesTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output Example, Builtins] r) =>
+  (Members '[Reader InfoTable, State FunctionsTable, State TypesTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output Example, Builtins] r) =>
   Maybe Expression ->
   Expression ->
   Sem r TypedExpression
@@ -508,9 +506,8 @@ inferExpression' hint e = case e of
   where
     goLet :: Let -> Sem r TypedExpression
     goLet l = do
-      tbl <- ask
-      (tbl', _letClauses) <- runState tbl (mapM goLetClause (l ^. letClauses))
-      typedBody <- local (const tbl') (inferExpression' hint (l ^. letExpression))
+      _letClauses <- mapM goLetClause (l ^. letClauses)
+      typedBody <- inferExpression' hint (l ^. letExpression)
       return
         TypedExpression
           { _typedType = typedBody ^. typedType,
@@ -523,7 +520,7 @@ inferExpression' hint e = case e of
           }
 
     -- what about mutually recursive lets?
-    goLetClause :: LetClause -> Sem (State FunctionsTable ': r) LetClause
+    goLetClause :: LetClause -> Sem r LetClause
     goLetClause = \case
       LetFunDef f -> LetFunDef <$> checkFunctionDef f
 
@@ -670,7 +667,7 @@ inferExpression' hint e = case e of
                     )
 
 viewInductiveApp ::
-  (Members '[Error TypeCheckerError, Inference, Reader FunctionsTable] r) =>
+  (Members '[Error TypeCheckerError, Inference, State FunctionsTable] r) =>
   Expression ->
   Sem r (Either Hole (InductiveName, [Expression]))
 viewInductiveApp ty = do

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/FunctionsTable.hs

@@ -10,5 +10,5 @@ newtype FunctionsTable = FunctionsTable
 
 makeLenses ''FunctionsTable
 
-askFunctionDef :: (Member (Reader FunctionsTable) r) => FunctionName -> Sem r (Maybe Expression)
-askFunctionDef f = asks (^. functionsTable . at f)
+askFunctionDef :: (Member (State FunctionsTable) r) => FunctionName -> Sem r (Maybe Expression)
+askFunctionDef f = gets (^. functionsTable . at f)

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs

@@ -94,7 +94,7 @@ getMetavar h = do
   void (queryMetavar' h)
   gets (fromJust . (^. inferenceMap . at h))
 
-strongNormalize' :: forall r. (Members '[Reader FunctionsTable, State InferenceState] r) => Expression -> Sem r Expression
+strongNormalize' :: forall r. (Members '[State FunctionsTable, State InferenceState] r) => Expression -> Sem r Expression
 strongNormalize' = go
   where
     go :: Expression -> Sem r Expression
@@ -169,7 +169,7 @@ strongNormalize' = go
       where
         i' = ExpressionIden i
 
-weakNormalize' :: forall r. (Members '[Reader FunctionsTable, State InferenceState] r) => Expression -> Sem r Expression
+weakNormalize' :: forall r. (Members '[State FunctionsTable, State InferenceState] r) => Expression -> Sem r Expression
 weakNormalize' = go
   where
     go :: Expression -> Sem r Expression
@@ -219,7 +219,7 @@ queryMetavar' h = do
     Just (Refined e) -> return (Just e)
 
 re ::
-  (Members '[Reader FunctionsTable, Error TypeCheckerError] r) =>
+  (Members '[State FunctionsTable, Error TypeCheckerError] r) =>
   Sem (Inference ': r) a ->
   Sem (State InferenceState ': r) a
 re = reinterpret $ \case
@@ -233,14 +233,14 @@ re = reinterpret $ \case
     registerIden' i ty = modify (over inferenceIdens (HashMap.insert i ty))
 
     -- Supports alpha equivalence.
-    matchTypes' :: (Members '[State InferenceState, Reader FunctionsTable, Error TypeCheckerError] r) => Expression -> Expression -> Sem r (Maybe MatchError)
+    matchTypes' :: (Members '[State InferenceState, State FunctionsTable, Error TypeCheckerError] r) => Expression -> Expression -> Sem r (Maybe MatchError)
     matchTypes' ty = runReader ini . go ty
       where
         ini :: HashMap VarName VarName
         ini = mempty
         go ::
           forall r.
-          (Members '[State InferenceState, Reader (HashMap VarName VarName), Reader FunctionsTable, Error TypeCheckerError] r) =>
+          (Members '[State InferenceState, Reader (HashMap VarName VarName), State FunctionsTable, Error TypeCheckerError] r) =>
           Expression ->
           Expression ->
           Sem r (Maybe MatchError)
@@ -364,7 +364,7 @@ re = reinterpret $ \case
 
 matchPatterns ::
   forall r.
-  (Members '[State InferenceState, State (HashMap VarName VarName), Reader FunctionsTable] r) =>
+  (Members '[State InferenceState, State (HashMap VarName VarName), State FunctionsTable] r) =>
   PatternArg ->
   PatternArg ->
   Sem r Bool
@@ -396,7 +396,7 @@ matchPatterns (PatternArg impl1 name1 pat1) (PatternArg impl2 name2 pat2) =
     err = return False
 
 runInferenceDefs ::
-  (Members '[Error TypeCheckerError, Reader FunctionsTable, State TypesTable] r, HasExpressions funDef) =>
+  (Members '[Error TypeCheckerError, State FunctionsTable, State TypesTable] r, HasExpressions funDef) =>
   Sem (Inference ': r) (NonEmpty funDef) ->
   Sem r (NonEmpty funDef)
 runInferenceDefs a = do
@@ -406,7 +406,7 @@ runInferenceDefs a = do
   return (subsHoles subs <$> expr)
 
 runInferenceDef ::
-  (Members '[Error TypeCheckerError, Reader FunctionsTable, State TypesTable] r, HasExpressions funDef) =>
+  (Members '[Error TypeCheckerError, State FunctionsTable, State TypesTable] r, HasExpressions funDef) =>
   Sem (Inference ': r) funDef ->
   Sem r funDef
 runInferenceDef = fmap head . runInferenceDefs . fmap pure
@@ -416,10 +416,10 @@ addIdens idens = modify (HashMap.union idens)
 
 -- | Assumes the given function has been type checked
 -- | NOTE: Registers the function *only* if the result type is Type
-functionDefEval :: forall r'. (Member (Reader FunctionsTable) r') => FunctionDef -> Sem r' (Maybe Expression)
+functionDefEval :: forall r'. Member (State FunctionsTable) r' => FunctionDef -> Sem r' (Maybe Expression)
 functionDefEval = runFail . goTop
   where
-    goTop :: forall r. (Members '[Fail, Reader FunctionsTable] r) => FunctionDef -> Sem r Expression
+    goTop :: forall r. (Members '[Fail, State FunctionsTable] r) => FunctionDef -> Sem r Expression
     goTop f =
       case f ^. funDefClauses of
         c :| [] -> goClause c
@@ -429,17 +429,15 @@ functionDefEval = runFail . goTop
         goClause c = do
           let pats = c ^. clausePatterns
               n = length (c ^. clausePatterns)
-          (patsTys, _) <- splitNExplicitParams n (f ^. funDefType)
+          patsTys <- splitNExplicitParams n (f ^. funDefType)
           go (zipExact pats patsTys)
           where
-            splitNExplicitParams :: Int -> Expression -> Sem r ([Expression], Expression)
+            splitNExplicitParams :: Int -> Expression -> Sem r [Expression]
             splitNExplicitParams n fun = do
               let (params, r) = unfoldFunType fun
               unlessM (isUniverse r) fail
-              (nfirst, rest) <- failMaybe (splitAtExactMay n params)
-              sparams <- mapM simpleExplicitParam nfirst
-              let r' = foldFunType rest r
-              return (sparams, r')
+              nfirst <- failMaybe (takeExactMay n params)
+              mapM simpleExplicitParam nfirst
             isUniverse :: Expression -> Sem r Bool
             isUniverse e = do
               e' <- evalState iniState (weakNormalize' e)
@@ -461,6 +459,6 @@ functionDefEval = runFail . goTop
                 | Implicit <- p ^. patternArgIsImplicit -> fail
                 | otherwise -> go ps >>= goPattern (p ^. patternArgPattern, ty)
 
-registerFunctionDef :: (Member (State FunctionsTable) r) => FunctionDef -> Sem r ()
-registerFunctionDef f = whenJustM (readerState @FunctionsTable (functionDefEval f)) $ \e ->
+registerFunctionDef :: Member (State FunctionsTable) r => FunctionDef -> Sem r ()
+registerFunctionDef f = whenJustM (functionDefEval f) $ \e ->
   modify (over functionsTable (HashMap.insert (f ^. funDefName) e))

src/Juvix/Prelude/Base.hs

@@ -384,9 +384,6 @@ nubHashable = HashSet.toList . HashSet.fromList
 allElements :: (Bounded a, Enum a) => [a]
 allElements = [minBound .. maxBound]
 
-readerState :: forall a r x. (Member (State a) r) => Sem (Reader a ': r) x -> Sem r x
-readerState m = get >>= (`runReader` m)
-
 infixr 3 .&&.
 
 (.&&.) :: (a -> Bool) -> (a -> Bool) -> a -> Bool

test/Typecheck/Positive.hs

@@ -205,7 +205,11 @@ tests =
     posTest
       "Let shadowing"
       $(mkRelDir ".")
-      $(mkRelFile "LetShadow.juvix")
+      $(mkRelFile "LetShadow.juvix"),
+    posTest
+      "Type synonym inside let"
+      $(mkRelDir "issue1879")
+      $(mkRelFile "LetSynonym.juvix")
   ]
     <> [ compilationTest t | t <- Compilation.tests, t ^. Compilation.name /= "Self-application"
        ]

tests/positive/issue1879/LetSynonym.juvix

@@ -0,0 +1,13 @@
+module LetSynonym;
+  type T :=
+    | t : T;
+
+  main : T;
+  main :=
+    let
+      A : Type;
+      A := T;
+      x : A;
+      x := t;
+    in x;
+end;