generate coercion projections

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

@@ -247,7 +247,7 @@ mkRecordNameSignature rhs =
             { _nameItemSymbol,
               _nameItemIndex,
               _nameItemType = field ^. fieldType,
-              _nameItemImplicit = field ^. fieldIsImplicit,
+              _nameItemImplicit = fromIsImplicitField (field ^. fieldIsImplicit),
               _nameItemDefault = Nothing
             }
         )

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

@@ -305,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),
@@ -735,8 +736,7 @@ deriving stock instance Ord (RecordUpdateField 'Scoped)
 
 data RecordField (s :: Stage) = RecordField
   { _fieldName :: SymbolType s,
-    -- Only Explicit and ImplicitInstance is allowed
-    _fieldIsImplicit :: IsImplicit,
+    _fieldIsImplicit :: IsImplicitField,
     _fieldColon :: Irrelevant (KeywordRef),
     _fieldType :: ExpressionType s,
     _fieldBuiltin :: Maybe (WithLoc BuiltinFunction),

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

@@ -1300,9 +1300,8 @@ instance (SingI s) => PrettyPrint (RecordField s) where
         builtin' = (<> line) . ppCode <$> _fieldBuiltin
         mayBraces :: forall r'. (Members '[ExactPrint] r') => Sem r' () -> Sem r' ()
         mayBraces = case _fieldIsImplicit of
-          Explicit -> id
-          Implicit -> impossible
-          ImplicitInstance -> doubleBraces
+          ExplicitField -> id
+          ImplicitInstanceField -> doubleBraces
     doc'
       ?<> pragmas'
       ?<> builtin'

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

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,10 +1544,10 @@ recordField = do
   _fieldDoc <- optional stashJudoc >> getJudoc
   _fieldPragmas <- optional stashPragmas >> getPragmas
   _fieldBuiltin <- optional builtinRecordField
-  mayImpl <- optional (snd <$> implicitOpen)
+  mayImpl <- optional (snd <$> implicitOpenField)
   _fieldName <- symbol
-  whenJust mayImpl (void . implicitClose)
-  let _fieldIsImplicit = fromMaybe Explicit mayImpl
+  whenJust mayImpl (void . implicitCloseField)
+  let _fieldIsImplicit = fromMaybe ExplicitField mayImpl
   _fieldColon <- Irrelevant <$> kw kwColon
   _fieldType <- parseExpressionAtoms
   return RecordField {..}

src/Juvix/Compiler/Internal/Extra.hs

@@ -104,13 +104,14 @@ mkConstructorVarPattern impl c vars =
 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
       saturatedTy :: FunctionParameter = unnamedParameter' constructorImplicity (constructorReturnType info)
@@ -121,7 +122,7 @@ genFieldProjection _funDefName _funDefBuiltin mpragmas info fieldIx = do
     FunctionDef
       { _funDefTerminating = False,
         _funDefInstance = False,
-        _funDefCoercion = False,
+        _funDefCoercion = kind == ProjectionCoercion,
         _funDefArgsInfo = mempty,
         _funDefPragmas =
           maybe

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

@@ -355,6 +355,7 @@ goProjectionDef ProjectionDef {..} = do
   info <- gets (^?! constructorInfos . at c . _Just)
   fun <-
     Internal.genFieldProjection
+      _projectionKind
       (goSymbol _projectionField)
       ( (^. withLocParam)
           <$> _projectionFieldBuiltin
@@ -668,7 +669,7 @@ goConstructorDef retTy ConstructorDef {..} = do
               Just
                 Internal.FunctionParameter
                   { _paramName = Just (goSymbol _fieldName),
-                    _paramImplicit = _fieldIsImplicit,
+                    _paramImplicit = fromIsImplicitField _fieldIsImplicit,
                     _paramType = ty'
                   }
 

src/Juvix/Data.hs

@@ -1,6 +1,7 @@
 module Juvix.Data
   ( module Juvix.Data.Effect,
     module Juvix.Data.Error,
+    module Juvix.Data.ProjectionKind,
     module Juvix.Data.NumThreads,
     module Juvix.Data.Fixity,
     module Juvix.Data.FileExt,
@@ -42,6 +43,7 @@ import Juvix.Data.NameId qualified
 import Juvix.Data.NumThreads
 import Juvix.Data.Pragmas
 import Juvix.Data.Processed
+import Juvix.Data.ProjectionKind
 import Juvix.Data.TopModulePathKey
 import Juvix.Data.Uid
 import Juvix.Data.Universe

src/Juvix/Data/InstanceHole.hs

@@ -10,7 +10,11 @@ import Juvix.Prelude.Base
 import Prettyprinter
 
 fromHole :: Hole.Hole -> InstanceHole
-fromHole (Hole.Hole a b) = InstanceHole a b
+fromHole Hole.Hole {..} =
+  InstanceHole
+    { _iholeId = _holeId,
+      _iholeKw = _holeKw
+    }
 
 data InstanceHole = InstanceHole
   { _iholeId :: NameId,

src/Juvix/Data/IsImplicit.hs

@@ -27,3 +27,24 @@ instance Pretty IsImplicit where
     Implicit -> "implicit"
     ImplicitInstance -> "implicit instance"
     Explicit -> "explicit"
+
+-- | When we support Implicit record fields we should remove this type in favour
+-- of IsImplicit
+data IsImplicitField
+  = ExplicitField
+  | ImplicitInstanceField
+  deriving stock (Show, Eq, Ord, Generic, Data)
+
+instance Hashable IsImplicitField
+
+instance Serialize IsImplicitField
+
+instance NFData IsImplicitField
+
+fromIsImplicitField :: IsImplicitField -> IsImplicit
+fromIsImplicitField = \case
+  ImplicitInstanceField -> ImplicitInstance
+  ExplicitField -> Explicit
+
+instance Pretty IsImplicitField where
+  pretty = pretty . fromIsImplicitField

src/Juvix/Data/ProjectionKind.hs

@@ -0,0 +1,10 @@
+module Juvix.Data.ProjectionKind where
+
+import Juvix.Prelude.Base
+
+data ProjectionKind
+  = -- | Projection for regular fields
+    ProjectionExplicit
+  | -- | Projection for instance fields
+    ProjectionCoercion
+  deriving stock (Show, Eq, Ord, Generic)

tests/positive/Internal/InstanceFields.juvix

@@ -1,17 +1,28 @@
 module InstanceFields;
 
-type T := t;
-
-type R := r;
+trait
+type Functor (f : Type -> Type) :=
+  mkFunctor {
+    map : {A B : Type} -> (A -> B) -> f A -> f B
+  };
 
 trait
-type HasT (y : Type) :=
-  hasT {
-    giveT : T
+type Applicative (f : Type -> Type) :=
+  mkApplicative {
+    {{ApplicativeFunctor}} : Functor f;
+    pure : {A : Type} -> A -> f A;
+    ap : {A B : Type} -> f (A -> B) -> f A -> f B
   };
 
 trait
-type HasR (x : Type) :=
-  hasR {
-    {{fieldHasT}} : HasT x;
+type Monad (f : Type -> Type) :=
+  mkMonad {
+    {{MonadApplicative}} : Applicative f;
+    bind : {A B : Type} -> f A -> (A -> f B) -> f B
   };
+
+open Functor;
+open Applicative;
+open Monad;
+
+monadMap {A B} {f : Type -> Type} {{Monad f}} (g : A -> B) (x : f A) : f B := map g x;