wip

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

@@ -98,6 +98,16 @@ instance (SingI s) => HasNameSignature s (InductiveDef s) where
     mapM_ addInductiveParams (a ^. inductiveParameters)
     whenJust (a ^. inductiveType) addExpressionType
 
+instance (SingI s) => HasNameSignature s (InductiveDef s, RecordField s) where
+  addArgs ::
+    forall r.
+    (Members '[NameSignatureBuilder s] r) =>
+    (InductiveDef s, RecordField s) ->
+    Sem r ()
+  addArgs (i, f) = do
+    mapM_ addConstructorParams (i ^. inductiveParameters)
+
+
 mkNameSignature ::
   forall s d r.
   (SingI s, Members '[Error ScoperError] r, HasNameSignature s d) =>

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

@@ -1208,8 +1208,19 @@ checkInductiveDef InductiveDef {..} = do
   registerNameSignature (inductiveName' ^. S.nameId) indDef
   forM_ inductiveConstructors' $ \c -> do
     registerNameSignature (c ^. constructorName . S.nameId) (indDef, c)
+    registerRecordFieldSignatures indDef c
   registerInductive @$> indDef
   where
+    registerRecordFieldSignatures :: InductiveDef 'Scoped -> ConstructorDef 'Scoped -> Sem r ()
+    registerRecordFieldSignatures indDef c =
+      case c ^. constructorRhs of
+        ConstructorRhsRecord r ->
+          forM_ (r ^. rhsRecordStatements) $ \case
+            RecordStatementField f -> do
+              registerNameSignature (f ^. fieldName . S.nameId) (indDef, f)
+            _ -> return ()
+        _ -> return ()
+
     -- note that the constructor name is not bound here
     checkConstructorDef :: S.Symbol -> S.Symbol -> ConstructorDef 'Parsed -> Sem r (ConstructorDef 'Scoped)
     checkConstructorDef inductiveName' constructorName' ConstructorDef {..} = do

tests/Compilation/positive/test061.juvix

@@ -33,15 +33,15 @@ g : {A : Type} → {{Show A}} → Nat := 5;
 instance
 showListI {A} {{Show' A}} : Show (List A) :=
   mkShow@{
-    show {A} : {{Show' A}} → List A → String
+    show : List A → String
       | nil := "nil"
       | (h :: t) := Show.show h ++str " :: " ++str show t
   };
 
 instance
 showMaybeI {A} {{Show A}} : Show (Maybe A) :=
   mkShow@{
-    show {A} {{Show A}} : Maybe A → String
+    show : Maybe A → String
       | (just x) := "just (" ++str Show.show x ++str ")"
       | nothing := "nothing"
   };