Remove wildcard patterns from Internal (#1724)

This pr removes wildcard patterns from the Internal language.
Wildcards are translated to variables with generated names.
This should resolve the issue of having unbound names after inference

src/Juvix/Compiler/Abstract/Data/Name.hs

@@ -23,6 +23,15 @@ data Name = Name
 
 makeLenses ''Name
 
+varFromWildcard :: Members '[NameIdGen] r => Wildcard -> Sem r VarName
+varFromWildcard w = do
+  _nameId <- freshNameId
+  let _nameText :: Text = "_ω" <> prettyText _nameId
+      _nameKind = KNameLocal
+      _namePretty = _nameText
+      _nameLoc = getLoc w
+  return Name {..}
+
 instance HasAtomicity Name where
   atomicity = const Atom
 

src/Juvix/Compiler/Backend/C/Data/Base.hs

@@ -219,7 +219,6 @@ buildPatternInfoTable argTyps c =
           [(v ^. Internal.nameText, BindingInfo {_bindingInfoExpr = exp, _bindingInfoType = typ})]
       Internal.PatternConstructorApp Internal.ConstructorApp {..} ->
         goConstructorApp exp _constrAppConstructor _constrAppParameters
-      Internal.PatternWildcard {} -> return []
 
     goConstructorApp :: Expression -> Internal.Name -> [Internal.PatternArg] -> Sem r [(Text, BindingInfo)]
     goConstructorApp exp constructorName ps = do

src/Juvix/Compiler/Backend/C/Translation/FromInternal.hs

@@ -342,7 +342,6 @@ goFunctionClause funSig argTyps clause = do
                 )
         fmap (isCtor :) subConditions
       Micro.PatternVariable {} -> return []
-      Micro.PatternWildcard {} -> return []
 
     clauseCondition :: Sem r (Maybe Expression)
     clauseCondition = fmap (foldr1 f) . nonEmpty <$> conditions

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

@@ -397,7 +397,6 @@ fromPattern ::
   Internal.Pattern ->
   Sem r Pattern
 fromPattern = \case
-  Internal.PatternWildcard {} -> return wildcard
   Internal.PatternVariable n -> return $ PatBinder (PatternBinder (Binder (n ^. nameText) (Just (n ^. nameLoc)) mkDynamic') wildcard)
   Internal.PatternConstructorApp c -> do
     let n = c ^. Internal.constrAppConstructor
@@ -424,7 +423,6 @@ fromPattern = \case
 
 getPatternVars :: Internal.Pattern -> [Name]
 getPatternVars = \case
-  Internal.PatternWildcard {} -> []
   Internal.PatternVariable n -> [n]
   Internal.PatternConstructorApp c ->
     concatMap getPatternVars explicitPatterns

src/Juvix/Compiler/Internal/Extra.hs

@@ -330,7 +330,6 @@ patternVariables :: Traversal' Pattern VarName
 patternVariables f p = case p of
   PatternVariable v -> PatternVariable <$> f v
   PatternConstructorApp a -> PatternConstructorApp <$> goApp f a
-  PatternWildcard {} -> pure p
   where
     goApp :: Traversal' ConstructorApp VarName
     goApp g = traverseOf constrAppParameters (traverse (patternArgVariables g))

src/Juvix/Compiler/Internal/Language.hs

@@ -167,7 +167,6 @@ instance Hashable PatternArg
 data Pattern
   = PatternVariable VarName
   | PatternConstructorApp ConstructorApp
-  | PatternWildcard Wildcard
   deriving stock (Eq, Generic)
 
 instance Hashable Pattern
@@ -269,7 +268,6 @@ instance HasAtomicity Pattern where
   atomicity p = case p of
     PatternConstructorApp a -> atomicity a
     PatternVariable {} -> Atom
-    PatternWildcard {} -> Atom
 
 instance HasLoc InductiveParameter where
   getLoc (InductiveParameter n) = getLoc n
@@ -319,7 +317,6 @@ instance HasLoc Pattern where
   getLoc = \case
     PatternVariable v -> getLoc v
     PatternConstructorApp a -> getLoc a
-    PatternWildcard i -> getLoc i
 
 instance HasLoc PatternArg where
   getLoc a = fmap getLoc (a ^. patternArgName) ?<> getLoc (a ^. patternArgPattern)

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

@@ -149,7 +149,6 @@ instance PrettyCode Pattern where
   ppCode p = case p of
     PatternVariable v -> ppCode v
     PatternConstructorApp a -> ppCode a
-    PatternWildcard {} -> return kwWildcard
 
 instance PrettyCode FunctionDef where
   ppCode f = do

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

@@ -36,7 +36,7 @@ iniState =
 makeLenses ''TranslationState
 
 fromAbstract ::
-  Members '[Error JuvixError] r =>
+  Members '[Error JuvixError, NameIdGen] r =>
   Abstract.AbstractResult ->
   Sem r InternalResult
 fromAbstract abstractResults = do
@@ -71,13 +71,11 @@ fromAbstract abstractResults = do
         . E.entryPointNoTermination
     depInfo = buildDependencyInfo (abstractResults ^. Abstract.resultModules) (abstractResults ^. Abstract.resultExports)
 
-fromAbstractExpression ::
-  Abstract.Expression ->
-  Sem r Expression
+fromAbstractExpression :: Members '[NameIdGen] r => Abstract.Expression -> Sem r Expression
 fromAbstractExpression = goExpression
 
 goModule ::
-  Members '[Reader ExportsTable, State TranslationState] r =>
+  Members '[Reader ExportsTable, State TranslationState, NameIdGen] r =>
   Abstract.TopModule ->
   Sem r Module
 goModule m = do
@@ -117,7 +115,7 @@ unsupported :: Text -> a
 unsupported thing = error ("Abstract to Internal: Not yet supported: " <> thing)
 
 goModuleBody ::
-  Members '[Reader ExportsTable, State TranslationState] r =>
+  Members '[Reader ExportsTable, State TranslationState, NameIdGen] r =>
   [NonEmpty Abstract.FunctionDef] ->
   Abstract.ModuleBody ->
   Sem r ModuleBody
@@ -129,7 +127,7 @@ goModuleBody mutualBlocks b = do
       { _moduleStatements = statements' <> mutualBlocks'
       }
 
-goImport :: Members '[Reader ExportsTable, State TranslationState] r => Abstract.TopModule -> Sem r (Maybe Include)
+goImport :: Members '[Reader ExportsTable, State TranslationState, NameIdGen] r => Abstract.TopModule -> Sem r (Maybe Include)
 goImport m = do
   inc <- gets (HashSet.member (m ^. Abstract.moduleName) . (^. translationStateIncluded))
   if
@@ -145,7 +143,7 @@ goImport m = do
             )
 
 goStatement ::
-  Members '[Reader ExportsTable, State TranslationState] r =>
+  Members '[Reader ExportsTable, State TranslationState, NameIdGen] r =>
   Abstract.Statement ->
   Sem r (Maybe Statement)
 goStatement = \case
@@ -195,7 +193,7 @@ goFunction (Abstract.Function l r) = do
   r' <- goType r
   return (Function l' r')
 
-goFunctionDef :: Abstract.FunctionDef -> Sem r FunctionDef
+goFunctionDef :: Members '[NameIdGen] r => Abstract.FunctionDef -> Sem r FunctionDef
 goFunctionDef f = do
   _funDefClauses' <- mapM (goFunctionClause _funDefName') (f ^. Abstract.funDefClauses)
   _funDefType' <- goType (f ^. Abstract.funDefTypeSig)
@@ -212,7 +210,7 @@ goFunctionDef f = do
     _funDefName' :: Name
     _funDefName' = f ^. Abstract.funDefName
 
-goExample :: Abstract.Example -> Sem r Example
+goExample :: Members '[NameIdGen] r => Abstract.Example -> Sem r Example
 goExample e = do
   e' <- goExpression (e ^. Abstract.exampleExpression)
   return
@@ -221,7 +219,7 @@ goExample e = do
         _exampleId = e ^. Abstract.exampleId
       }
 
-goFunctionClause :: Name -> Abstract.FunctionClause -> Sem r FunctionClause
+goFunctionClause :: Members '[NameIdGen] r => Name -> Abstract.FunctionClause -> Sem r FunctionClause
 goFunctionClause n c = do
   _clauseBody' <- goExpression (c ^. Abstract.clauseBody)
   _clausePatterns' <- mapM goPatternArg (c ^. Abstract.clausePatterns)
@@ -232,7 +230,7 @@ goFunctionClause n c = do
         _clauseBody = _clauseBody'
       }
 
-goPatternArg :: Abstract.PatternArg -> Sem r PatternArg
+goPatternArg :: Members '[NameIdGen] r => Abstract.PatternArg -> Sem r PatternArg
 goPatternArg p = do
   pat' <- goPattern (p ^. Abstract.patternArgPattern)
   return
@@ -242,14 +240,14 @@ goPatternArg p = do
         _patternArgPattern = pat'
       }
 
-goPattern :: Abstract.Pattern -> Sem r Pattern
+goPattern :: Members '[NameIdGen] r => Abstract.Pattern -> Sem r Pattern
 goPattern p = case p of
   Abstract.PatternVariable v -> return (PatternVariable v)
   Abstract.PatternConstructorApp c -> PatternConstructorApp <$> goConstructorApp c
-  Abstract.PatternWildcard i -> return (PatternWildcard i)
+  Abstract.PatternWildcard w -> PatternVariable <$> varFromWildcard w
   Abstract.PatternEmpty -> unsupported "pattern empty"
 
-goConstructorApp :: Abstract.ConstructorApp -> Sem r ConstructorApp
+goConstructorApp :: Members '[NameIdGen] r => Abstract.ConstructorApp -> Sem r ConstructorApp
 goConstructorApp c = do
   _constrAppParameters' <- mapM goPatternArg (c ^. Abstract.constrAppParameters)
   return
@@ -281,7 +279,7 @@ goType e = case e of
   Abstract.ExpressionHole h -> return (ExpressionHole h)
   Abstract.ExpressionLambda {} -> unsupported "lambda in types"
 
-goLambda :: forall r. Abstract.Lambda -> Sem r Lambda
+goLambda :: forall r. Members '[NameIdGen] r => Abstract.Lambda -> Sem r Lambda
 goLambda (Abstract.Lambda cl) = case nonEmpty cl of
   Nothing -> unsupported "empty lambda"
   Just cl' -> Lambda <$> mapM goClause cl'
@@ -297,7 +295,7 @@ goLambda (Abstract.Lambda cl) = case nonEmpty cl of
           Explicit -> p
           Implicit -> unsupported "implicit patterns in lambda"
 
-goApplication :: Abstract.Application -> Sem r Application
+goApplication :: Members '[NameIdGen] r => Abstract.Application -> Sem r Application
 goApplication (Abstract.Application f x i) = do
   f' <- goExpression f
   x' <- goExpression x
@@ -311,7 +309,7 @@ goIden i = case i of
   Abstract.IdenAxiom a -> IdenAxiom (a ^. Abstract.axiomRefName)
   Abstract.IdenInductive a -> IdenInductive (a ^. Abstract.inductiveRefName)
 
-goExpressionFunction :: forall r. Abstract.Function -> Sem r Function
+goExpressionFunction :: forall r. Members '[NameIdGen] r => Abstract.Function -> Sem r Function
 goExpressionFunction f = do
   l' <- goParam (f ^. Abstract.funParameter)
   r' <- goExpression (f ^. Abstract.funReturn)
@@ -324,7 +322,7 @@ goExpressionFunction f = do
           return (FunctionParameter (p ^. Abstract.paramName) (p ^. Abstract.paramImplicit) ty')
       | otherwise = unsupported "usages"
 
-goExpression :: Abstract.Expression -> Sem r Expression
+goExpression :: Members '[NameIdGen] r => Abstract.Expression -> Sem r Expression
 goExpression e = case e of
   Abstract.ExpressionIden i -> return (ExpressionIden (goIden i))
   Abstract.ExpressionUniverse u -> return (ExpressionUniverse (goUniverse u))
@@ -346,29 +344,26 @@ goInductiveParameter f =
     (Just {}, _, _) -> unsupported "only type variables of small types are allowed"
     (Nothing, _, _) -> unsupported "unnamed inductive parameters"
 
-goInductiveDef ::
-  Abstract.InductiveDef ->
-  Sem r InductiveDef
-goInductiveDef i =
-  if
-      | not (isSmallType (i ^. Abstract.inductiveType)) -> unsupported "inductive indices"
-      | otherwise -> do
-          inductiveParameters' <- mapM goInductiveParameter (i ^. Abstract.inductiveParameters)
-          let indTypeName = i ^. Abstract.inductiveName
-          inductiveConstructors' <-
-            mapM
-              goConstructorDef
-              (i ^. Abstract.inductiveConstructors)
-          examples' <- mapM goExample (i ^. Abstract.inductiveExamples)
-          return
-            InductiveDef
-              { _inductiveName = indTypeName,
-                _inductiveParameters = inductiveParameters',
-                _inductiveBuiltin = i ^. Abstract.inductiveBuiltin,
-                _inductiveConstructors = inductiveConstructors',
-                _inductiveExamples = examples',
-                _inductivePositive = i ^. Abstract.inductivePositive
-              }
+goInductiveDef :: forall r. Members '[NameIdGen] r => Abstract.InductiveDef -> Sem r InductiveDef
+goInductiveDef i
+  | not (isSmallType (i ^. Abstract.inductiveType)) = unsupported "inductive indices"
+  | otherwise = do
+      inductiveParameters' <- mapM goInductiveParameter (i ^. Abstract.inductiveParameters)
+      let indTypeName = i ^. Abstract.inductiveName
+      inductiveConstructors' <-
+        mapM
+          goConstructorDef
+          (i ^. Abstract.inductiveConstructors)
+      examples' <- mapM goExample (i ^. Abstract.inductiveExamples)
+      return
+        InductiveDef
+          { _inductiveName = indTypeName,
+            _inductiveParameters = inductiveParameters',
+            _inductiveBuiltin = i ^. Abstract.inductiveBuiltin,
+            _inductiveConstructors = inductiveConstructors',
+            _inductiveExamples = examples',
+            _inductivePositive = i ^. Abstract.inductivePositive
+          }
   where
     goConstructorDef :: Abstract.InductiveConstructorDef -> Sem r InductiveConstructorDef
     goConstructorDef c = do

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

@@ -187,11 +187,12 @@ checkLhs loc guessedBody ariSignature pats = do
     -- between explicit parameters already in the pattern.
     goLhs :: Arity -> [PatternArg] -> Sem (State LocalVars ': r) ([PatternArg], Arity)
     goLhs a = \case
-      [] -> return $ case tailHelper a of
-        Nothing -> ([], a)
-        Just tailUnderscores ->
+      [] -> case tailHelper a of
+        Nothing -> return ([], a)
+        Just tailUnderscores -> do
+          wildcard <- genWildcard
           let a' = foldArity (over ufoldArityParams (drop tailUnderscores) (unfoldArity' a))
-           in (replicate tailUnderscores wildcard, a')
+          return (replicate tailUnderscores wildcard, a')
       lhs@(p : ps) -> case a of
         ArityUnit ->
           throw
@@ -216,14 +217,17 @@ checkLhs loc guessedBody ariSignature pats = do
                         _wrongPatternIsImplicitActual = p
                       }
                 )
-            (Explicit, ParamImplicit) ->
+            (Explicit, ParamImplicit) -> do
+              wildcard <- genWildcard
               first (wildcard :) <$> goLhs r lhs
             (Explicit, ParamExplicit pa) -> do
               p' <- checkPattern pa p
               first (p' :) <$> goLhs r ps
       where
-        wildcard :: PatternArg
-        wildcard = PatternArg Implicit Nothing (PatternWildcard (Wildcard loc))
+        genWildcard :: forall r'. Members '[NameIdGen] r' => Sem r' PatternArg
+        genWildcard = do
+          var <- varFromWildcard (Wildcard loc)
+          return (PatternArg Implicit Nothing (PatternVariable var))
 
     -- This is an heuristic and it can have an undesired result.
     -- Sometimes the outcome may even be confusing.
@@ -259,7 +263,6 @@ checkPattern ari = traverseOf (patternArgName . each) nameAri >=> traverseOf pat
     patternAri :: Pattern -> Sem r Pattern
     patternAri = \case
       PatternVariable v -> addArity v ari $> PatternVariable v
-      PatternWildcard i -> return (PatternWildcard i)
       PatternConstructorApp c -> case ari of
         ArityUnit -> PatternConstructorApp <$> checkConstructorApp c
         ArityUnknown -> PatternConstructorApp <$> checkConstructorApp c

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

@@ -360,7 +360,6 @@ checkPattern = go
           name = patArg ^. patternArgName
       whenJust name (\n -> addVar n ty argTy)
       case pat of
-        PatternWildcard {} -> return ()
         PatternVariable v -> addVar v ty argTy
         PatternConstructorApp a -> do
           s <- checkSaturatedInductive ty

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

@@ -363,11 +363,8 @@ matchPatterns (PatternArg impl1 name1 pat1) (PatternArg impl2 name2 pat2) =
     goName _ _ = err
     goPattern :: Pattern -> Pattern -> Sem r Bool
     goPattern p1 p2 = case (p1, p2) of
-      (PatternWildcard {}, PatternWildcard {}) -> ok
       (PatternVariable v1, PatternVariable v2) -> modify (HashMap.insert v1 v2) $> True
       (PatternConstructorApp c1, PatternConstructorApp c2) -> goConstructor c1 c2
-      (PatternWildcard {}, _) -> err
-      (_, PatternWildcard {}) -> err
       (PatternVariable {}, _) -> err
       (_, PatternVariable {}) -> err
     goConstructor :: ConstructorApp -> ConstructorApp -> Sem r Bool