Allow instance field declarations (#2916)

- Closes #2897

---------

Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>

src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs

@@ -10,7 +10,6 @@ module Juvix.Compiler.Concrete.Data.NameSignature.Builder
   )
 where
 
-import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Concrete.Data.NameSignature.Error
 import Juvix.Compiler.Concrete.Extra (symbolParsed)
 import Juvix.Compiler.Concrete.Gen qualified as Gen
@@ -215,6 +214,7 @@ addSymbol' impl mdef sym ty = do
             NameItem
               { _nameItemDefault = mdef,
                 _nameItemSymbol = sym,
+                _nameItemImplicit = impl,
                 _nameItemIndex = idx,
                 _nameItemType = ty
               }
@@ -241,10 +241,16 @@ endBuild' = get @(BuilderState s) >>= throw
 mkRecordNameSignature :: forall s. (SingI s) => RhsRecord s -> RecordNameSignature s
 mkRecordNameSignature rhs =
   RecordNameSignature $
-    HashMap.fromList
-      [ (symbolParsed _nameItemSymbol, NameItem {..})
+    hashMap
+      [ ( symbolParsed _nameItemSymbol,
+          NameItem
+            { _nameItemSymbol,
+              _nameItemIndex,
+              _nameItemType = field ^. fieldType,
+              _nameItemImplicit = fromIsImplicitField (field ^. fieldIsImplicit),
+              _nameItemDefault = Nothing
+            }
+        )
         | (Indexed _nameItemIndex field) <- indexFrom 0 (toList (rhs ^.. rhsRecordStatements . each . _RecordStatementField)),
           let _nameItemSymbol :: SymbolType s = field ^. fieldName
-              _nameItemType = field ^. fieldType
-              _nameItemDefault :: Maybe (ArgDefault s) = Nothing
       ]

src/Juvix/Compiler/Concrete/Extra.hs

@@ -12,7 +12,6 @@ module Juvix.Compiler.Concrete.Extra
   )
 where
 
-import Data.IntMap.Strict qualified as IntMap
 import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Language
@@ -93,11 +92,8 @@ flattenStatement = \case
   StatementModule m -> concatMap flattenStatement (m ^. moduleBody)
   s -> [s]
 
-recordNameSignatureByIndex :: forall s. (SingI s) => RecordNameSignature s -> IntMap Symbol
-recordNameSignatureByIndex = IntMap.fromList . (^.. recordNames . each . to mkAssoc)
-  where
-    mkAssoc :: NameItem s -> (Int, Symbol)
-    mkAssoc NameItem {..} = (_nameItemIndex, symbolParsed _nameItemSymbol)
+recordNameSignatureByIndex :: RecordNameSignature s -> IntMap (NameItem s)
+recordNameSignatureByIndex = indexedByInt (^. nameItemIndex) . (^. recordNames)
 
 getExpressionAtomIden :: ExpressionAtom 'Scoped -> Maybe S.Name
 getExpressionAtomIden = \case

src/Juvix/Compiler/Concrete/Language/Base.hs

@@ -158,6 +158,7 @@ type ParsedPragmas = WithLoc (WithSource Pragmas)
 data NameItem (s :: Stage) = NameItem
   { _nameItemSymbol :: SymbolType s,
     _nameItemIndex :: Int,
+    _nameItemImplicit :: IsImplicit,
     _nameItemType :: ExpressionType s,
     _nameItemDefault :: Maybe (ArgDefault s)
   }
@@ -304,6 +305,7 @@ deriving stock instance Ord (Statement 'Scoped)
 data ProjectionDef s = ProjectionDef
   { _projectionConstructor :: S.Symbol,
     _projectionField :: SymbolType s,
+    _projectionKind :: ProjectionKind,
     _projectionFieldIx :: Int,
     _projectionFieldBuiltin :: Maybe (WithLoc BuiltinFunction),
     _projectionDoc :: Maybe (Judoc s),
@@ -734,6 +736,7 @@ deriving stock instance Ord (RecordUpdateField 'Scoped)
 
 data RecordField (s :: Stage) = RecordField
   { _fieldName :: SymbolType s,
+    _fieldIsImplicit :: IsImplicitField,
     _fieldColon :: Irrelevant (KeywordRef),
     _fieldType :: ExpressionType s,
     _fieldBuiltin :: Maybe (WithLoc BuiltinFunction),
@@ -2210,7 +2213,7 @@ deriving stock instance Ord (ArgumentBlock 'Scoped)
 data RecordUpdateExtra = RecordUpdateExtra
   { _recordUpdateExtraConstructor :: S.Symbol,
     -- | Implicitly bound fields sorted by index
-    _recordUpdateExtraVars :: [S.Symbol]
+    _recordUpdateExtraVars :: IntMap (IsImplicit, S.Symbol)
   }
   deriving stock (Generic)
 

src/Juvix/Compiler/Concrete/Print/Base.hs

@@ -1298,10 +1298,14 @@ instance (SingI s) => PrettyPrint (RecordField s) where
     let doc' = ppCode <$> _fieldDoc
         pragmas' = ppCode <$> _fieldPragmas
         builtin' = (<> line) . ppCode <$> _fieldBuiltin
+        mayBraces :: forall r'. (Members '[ExactPrint] r') => Sem r' () -> Sem r' ()
+        mayBraces = case _fieldIsImplicit of
+          ExplicitField -> id
+          ImplicitInstanceField -> doubleBraces
     doc'
       ?<> pragmas'
       ?<> builtin'
-      ?<> ppSymbolType _fieldName
+      ?<> mayBraces (ppSymbolType _fieldName)
       <+> ppCode _fieldColon
       <+> ppExpressionType _fieldType
 

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs

@@ -170,6 +170,7 @@ checkProjectionDef p = do
         _projectionConstructor = p ^. projectionConstructor,
         _projectionFieldBuiltin = p ^. projectionFieldBuiltin,
         _projectionPragmas = p ^. projectionPragmas,
+        _projectionKind = p ^. projectionKind,
         _projectionField,
         _projectionDoc
       }
@@ -1643,10 +1644,16 @@ checkSections sec = topBindings helper
                                 { _projectionConstructor = headConstr,
                                   _projectionField = field ^. fieldName,
                                   _projectionFieldIx = idx,
+                                  _projectionKind = kind,
                                   _projectionFieldBuiltin = field ^. fieldBuiltin,
                                   _projectionDoc = field ^. fieldDoc,
                                   _projectionPragmas = field ^. fieldPragmas
                                 }
+                              where
+                                kind :: ProjectionKind
+                                kind = case field ^. fieldIsImplicit of
+                                  ExplicitField -> ProjectionExplicit
+                                  ImplicitInstanceField -> ProjectionCoercion
 
                             getFields :: Sem (Fail ': s') [RecordStatement 'Parsed]
                             getFields = case i ^. inductiveConstructors of
@@ -2665,8 +2672,8 @@ checkRecordUpdate RecordUpdate {..} = do
   tyName' <- getNameOfKind KNameInductive _recordUpdateTypeName
   info <- getRecordInfo tyName'
   let sig = info ^. recordInfoSignature
-  (vars', fields') <- withLocalScope $ do
-    vs <- mapM bindVariableSymbol (toList (recordNameSignatureByIndex sig))
+  (vars' :: IntMap (IsImplicit, S.Symbol), fields') <- withLocalScope $ do
+    vs <- mapM bindRecordUpdateVariable (recordNameSignatureByIndex sig)
     fs <- mapM (checkUpdateField sig) _recordUpdateFields
     return (vs, fs)
   let extra' =
@@ -2682,6 +2689,11 @@ checkRecordUpdate RecordUpdate {..} = do
         _recordUpdateAtKw,
         _recordUpdateDelims
       }
+  where
+    bindRecordUpdateVariable :: NameItem 'Parsed -> Sem r (IsImplicit, S.Symbol)
+    bindRecordUpdateVariable NameItem {..} = do
+      v <- bindVariableSymbol _nameItemSymbol
+      return (_nameItemImplicit, v)
 
 checkUpdateField ::
   (Members '[HighlightBuilder, Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) =>

src/Juvix/Compiler/Concrete/Translation/FromSource.hs

@@ -1409,12 +1409,27 @@ axiomDef _axiomBuiltin = do
 -- Function expression
 --------------------------------------------------------------------------------
 
+implicitOpenField ::
+  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  ParsecS r (KeywordRef, IsImplicitField)
+implicitOpenField =
+  (,ImplicitInstanceField) <$> kw delimDoubleBraceL
+    <|> (,ExplicitField) <$> kw delimParenL
+
 implicitOpen :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (KeywordRef, IsImplicit)
 implicitOpen =
   (,ImplicitInstance) <$> kw delimDoubleBraceL
     <|> (,Implicit) <$> kw delimBraceL
     <|> (,Explicit) <$> kw delimParenL
 
+implicitCloseField ::
+  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  IsImplicitField ->
+  ParsecS r KeywordRef
+implicitCloseField = \case
+  ExplicitField -> kw delimParenR
+  ImplicitInstanceField -> kw delimDoubleBraceR
+
 implicitClose :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => IsImplicit -> ParsecS r KeywordRef
 implicitClose = \case
   Implicit -> kw delimBraceR
@@ -1529,7 +1544,10 @@ recordField = do
   _fieldDoc <- optional stashJudoc >> getJudoc
   _fieldPragmas <- optional stashPragmas >> getPragmas
   _fieldBuiltin <- optional builtinRecordField
+  mayImpl <- optional (snd <$> implicitOpenField)
   _fieldName <- symbol
+  whenJust mayImpl (void . implicitCloseField)
+  let _fieldIsImplicit = fromMaybe ExplicitField mayImpl
   _fieldColon <- Irrelevant <$> kw kwColon
   _fieldType <- parseExpressionAtoms
   return RecordField {..}

src/Juvix/Compiler/Internal/Data/InfoTable.hs

@@ -190,7 +190,7 @@ lookupConstructor f = do
           <> "\nThe registered constructors are: "
           <> ppTrace (HashMap.keys tbl)
 
-lookupConstructorArgTypes :: (Member (Reader InfoTable) r) => Name -> Sem r ([InductiveParameter], [Expression])
+lookupConstructorArgTypes :: (Member (Reader InfoTable) r) => Name -> Sem r ([InductiveParameter], [FunctionParameter])
 lookupConstructorArgTypes = fmap constructorArgTypes . lookupConstructor
 
 lookupInductive :: forall r. (Member (Reader InfoTable) r) => InductiveName -> Sem r InductiveInfo

src/Juvix/Compiler/Internal/Extra.hs

@@ -7,15 +7,14 @@ module Juvix.Compiler.Internal.Extra
 where
 
 import Data.HashMap.Strict qualified as HashMap
-import Data.Stream qualified as Stream
 import Juvix.Compiler.Internal.Extra.Base
 import Juvix.Compiler.Internal.Extra.Clonable
 import Juvix.Compiler.Internal.Extra.DependencyBuilder
 import Juvix.Compiler.Internal.Language
 import Juvix.Compiler.Store.Internal.Data.InfoTable
 import Juvix.Prelude
 
-constructorArgTypes :: ConstructorInfo -> ([InductiveParameter], [Expression])
+constructorArgTypes :: ConstructorInfo -> ([InductiveParameter], [FunctionParameter])
 constructorArgTypes i =
   ( i ^. constructorInfoInductiveParameters,
     constructorArgs (i ^. constructorInfoType)
@@ -42,7 +41,7 @@ constructorType info =
   let (inductiveParams, constrArgs) = constructorArgTypes info
       args =
         map inductiveToFunctionParam inductiveParams
-          ++ map unnamedParameter constrArgs
+          ++ constrArgs
       saturatedTy = constructorReturnType info
    in foldFunType args saturatedTy
 
@@ -54,10 +53,6 @@ inductiveToFunctionParam InductiveParameter {..} =
       _paramType = _inductiveParamType
     }
 
-constructorImplicity :: ConstructorInfo -> IsImplicit
-constructorImplicity info =
-  if info ^. constructorInfoTrait then ImplicitInstance else Explicit
-
 patternArgFromVar :: IsImplicit -> VarName -> PatternArg
 patternArgFromVar i v =
   PatternArg
@@ -66,19 +61,32 @@ patternArgFromVar i v =
       _patternArgPattern = PatternVariable v
     }
 
--- | Given `mkPair`, returns (mkPair a b, [a, b])
-genConstructorPattern :: (Members '[NameIdGen] r) => Interval -> ConstructorInfo -> Sem r (PatternArg, [VarName])
-genConstructorPattern loc info = genConstructorPattern' impl loc (info ^. constructorInfoName) (length (snd (constructorArgTypes info)))
-  where
-    impl = constructorImplicity info
+-- | Given `mkApplicative`, returns {{mkApplicative {{funct}}}} var_pure var_ap, [var_pure, var_ap]
+genConstructorPattern ::
+  (Members '[NameIdGen] r) =>
+  Interval ->
+  IsImplicit ->
+  ConstructorInfo ->
+  Sem r (PatternArg, [VarName])
+genConstructorPattern loc traitImplicity info =
+  genConstructorPattern' traitImplicity loc (info ^. constructorInfoName) (snd (constructorArgTypes info))
 
 -- | Given `mkPair`, returns (mkPair a b, [a, b])
-genConstructorPattern' :: (Members '[NameIdGen] r) => IsImplicit -> Interval -> Name -> Int -> Sem r (PatternArg, [VarName])
-genConstructorPattern' impl loc cname cargs = do
-  vars <- mapM (freshVar loc) (Stream.take cargs allWords)
-  return (mkConstructorVarPattern impl cname vars, vars)
+genConstructorPattern' ::
+  (Members '[NameIdGen] r) =>
+  IsImplicit ->
+  Interval ->
+  Name ->
+  [FunctionParameter] ->
+  Sem r (PatternArg, [VarName])
+genConstructorPattern' traitImplicity loc concstrName cargs = do
+  vars :: [(IsImplicit, VarName)] <- runStreamOf allWords . forM cargs $ \p -> do
+    varTxt <- maybe yield return (p ^? paramName . _Just . nameText)
+    var <- freshVar loc varTxt
+    return (p ^. paramImplicit, var)
+  return (mkConstructorVarPattern traitImplicity concstrName vars, snd <$> vars)
 
-mkConstructorVarPattern :: IsImplicit -> Name -> [VarName] -> PatternArg
+mkConstructorVarPattern :: IsImplicit -> Name -> [(IsImplicit, VarName)] -> PatternArg
 mkConstructorVarPattern impl c vars =
   PatternArg
     { _patternArgIsImplicit = impl,
@@ -88,33 +96,33 @@ mkConstructorVarPattern impl c vars =
           ConstructorApp
             { _constrAppConstructor = c,
               _constrAppType = Nothing,
-              _constrAppParameters = map (patternArgFromVar Explicit) vars
+              _constrAppParameters = map (uncurry patternArgFromVar) vars
             }
     }
 
--- | Assumes the constructor does not have implicit arguments (which is not
--- allowed at the moment).
+-- | Generates a projection function for the given constructor and field index.
 genFieldProjection ::
   forall r.
   (Members '[NameIdGen] r) =>
+  ProjectionKind ->
   FunctionName ->
   Maybe BuiltinFunction ->
   Maybe Pragmas ->
   ConstructorInfo ->
   Int ->
   Sem r FunctionDef
-genFieldProjection _funDefName _funDefBuiltin mpragmas info fieldIx = do
+genFieldProjection kind _funDefName _funDefBuiltin mpragmas info fieldIx = do
   body' <- genBody
   let (inductiveParams, constrArgs) = constructorArgTypes info
-      implicity = constructorImplicity info
-      saturatedTy = unnamedParameter' implicity (constructorReturnType info)
+      saturatedTy :: FunctionParameter = unnamedParameter' constructorImplicity (constructorReturnType info)
       inductiveArgs = map inductiveToFunctionParam inductiveParams
-      retTy = constrArgs !! fieldIx
+      param = constrArgs !! fieldIx
+      retTy = param ^. paramType
   cloneFunctionDefSameName
     FunctionDef
       { _funDefTerminating = False,
         _funDefInstance = False,
-        _funDefCoercion = False,
+        _funDefCoercion = kind == ProjectionCoercion,
         _funDefArgsInfo = mempty,
         _funDefPragmas =
           maybe
@@ -127,9 +135,14 @@ genFieldProjection _funDefName _funDefBuiltin mpragmas info fieldIx = do
         _funDefBuiltin
       }
   where
+    constructorImplicity :: IsImplicit
+    constructorImplicity
+      | info ^. constructorInfoTrait = ImplicitInstance
+      | otherwise = Explicit
+
     genBody :: Sem r Expression
     genBody = do
-      (pat, vars) <- genConstructorPattern (getLoc _funDefName) info
+      (pat, vars) <- genConstructorPattern (getLoc _funDefName) constructorImplicity info
       let body = toExpression (vars !! fieldIx)
           cl =
             LambdaClause
@@ -265,5 +278,10 @@ substitutionE m expr
         Just e -> clone e
         Nothing -> return (toExpression n)
 
-substituteIndParams :: forall r. (Member NameIdGen r) => [(InductiveParameter, Expression)] -> Expression -> Sem r Expression
+substituteIndParams ::
+  forall r expr.
+  (Member NameIdGen r, HasExpressions expr) =>
+  [(InductiveParameter, Expression)] ->
+  expr ->
+  Sem r expr
 substituteIndParams = substitutionE . HashMap.fromList . map (first (^. inductiveParamName))

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

@@ -367,10 +367,10 @@ foldFunType l r = go l
 foldFunTypeExplicit :: [Expression] -> Expression -> Expression
 foldFunTypeExplicit = foldFunType . map unnamedParameter
 
-viewConstructorType :: Expression -> ([Expression], Expression)
-viewConstructorType = first (map (^. paramType)) . unfoldFunType
+viewConstructorType :: Expression -> ([FunctionParameter], Expression)
+viewConstructorType = unfoldFunType
 
-constructorArgs :: Expression -> [Expression]
+constructorArgs :: Expression -> [FunctionParameter]
 constructorArgs = fst . viewConstructorType
 
 unfoldLambdaClauses :: Expression -> Maybe (NonEmpty (NonEmpty PatternArg, Expression))