Use the target of aliases when resolving name signatures and iterators (#2669)

* Closes https://github.com/anoma/juvix/issues/2664

As well as this fix we rename lens scopedIdenName to scopedIdenSrcName.
`scopedIdenSrcName` refers to the name of an identifier from the source
code. The name `scopedIdenName` is confusing because users of
`ScopedIden` may think that this lens refers to the only name associated
with `ScopedIden`, they may want `scopedIdenNameFinal` instead.

src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs

@@ -106,8 +106,8 @@ anameFromScopedIden s =
     { _anameLoc = getLoc s,
       _anameKind = getNameKind s,
       _anameDocId = s ^. scopedIdenFinal . nameId,
-      _anameDefinedLoc = s ^. scopedIdenName . nameDefined,
-      _anameVerbatim = s ^. scopedIdenName . nameVerbatim
+      _anameDefinedLoc = s ^. scopedIdenSrcName . nameDefined,
+      _anameVerbatim = s ^. scopedIdenSrcName . nameVerbatim
     }
 
 lookupInfo :: (Members '[InfoTableBuilder, Reader InfoTable] r) => (InfoTable -> Maybe a) -> Sem r a

src/Juvix/Compiler/Concrete/Extra.hs

@@ -101,13 +101,13 @@ recordNameSignatureByIndex = IntMap.fromList . (^.. recordNames . each . to mkAs
 
 getExpressionAtomIden :: ExpressionAtom 'Scoped -> Maybe S.Name
 getExpressionAtomIden = \case
-  AtomIdentifier nm -> Just (nm ^. scopedIdenName)
+  AtomIdentifier nm -> Just (nm ^. scopedIdenSrcName)
   _ -> Nothing
 
 getPatternAtomIden :: PatternAtom 'Scoped -> Maybe S.Name
 getPatternAtomIden = \case
   PatternAtomIden i -> case i of
-    PatternScopedConstructor c -> Just (c ^. scopedIdenName)
+    PatternScopedConstructor c -> Just (c ^. scopedIdenSrcName)
     _ -> Nothing
   _ -> Nothing
 

src/Juvix/Compiler/Concrete/Language.hs

@@ -2285,10 +2285,10 @@ instance (SingI s) => HasAtomicity (FunctionParameters s) where
         SScoped -> atomicity (p ^. paramType)
 
 instance Pretty ScopedIden where
-  pretty = pretty . (^. scopedIdenName)
+  pretty = pretty . (^. scopedIdenSrcName)
 
 instance HasLoc ScopedIden where
-  getLoc = getLoc . (^. scopedIdenName)
+  getLoc = getLoc . (^. scopedIdenSrcName)
 
 instance (SingI s) => HasLoc (InductiveParameters s) where
   getLoc i = getLocSymbolType (i ^. inductiveParametersNames . _head1) <>? (getLocExpressionType <$> (i ^? inductiveParametersRhs . _Just . inductiveParametersType))
@@ -2668,7 +2668,7 @@ instance IsApe PatternInfixApp ApeLeaf where
         { _infixFixity = getFixity i,
           _infixLeft = toApe l,
           _infixRight = toApe r,
-          _infixIsDelimiter = isDelimiterStr (prettyText (op ^. scopedIdenName . S.nameConcrete)),
+          _infixIsDelimiter = isDelimiterStr (prettyText (op ^. scopedIdenSrcName . S.nameConcrete)),
           _infixOp = ApeLeafPattern (PatternConstructor op)
         }
 
@@ -2732,7 +2732,7 @@ instance IsApe InfixApplication ApeLeaf where
         { _infixFixity = getFixity i,
           _infixLeft = toApe l,
           _infixRight = toApe r,
-          _infixIsDelimiter = isDelimiterStr (prettyText (op ^. scopedIdenName . S.nameConcrete)),
+          _infixIsDelimiter = isDelimiterStr (prettyText (op ^. scopedIdenSrcName . S.nameConcrete)),
           _infixOp = ApeLeafExpression (ExpressionIdentifier op)
         }
 
@@ -2856,8 +2856,8 @@ _RecordStatementField f x = case x of
   RecordStatementField p -> RecordStatementField <$> f p
   _ -> pure x
 
-scopedIdenName :: Lens' ScopedIden S.Name
-scopedIdenName f n = case n ^. scopedIdenAlias of
+scopedIdenSrcName :: Lens' ScopedIden S.Name
+scopedIdenSrcName f n = case n ^. scopedIdenAlias of
   Nothing -> scopedIdenFinal f n
   Just a -> do
     a' <- f a
@@ -2871,16 +2871,16 @@ fromParsedIteratorInfo ParsedIteratorInfo {..} =
     }
 
 instance HasFixity PostfixApplication where
-  getFixity (PostfixApplication _ op) = fromMaybe impossible (op ^. scopedIdenName . S.nameFixity)
+  getFixity (PostfixApplication _ op) = fromMaybe impossible (op ^. scopedIdenSrcName . S.nameFixity)
 
 instance HasFixity InfixApplication where
-  getFixity (InfixApplication _ op _) = fromMaybe impossible (op ^. scopedIdenName . S.nameFixity)
+  getFixity (InfixApplication _ op _) = fromMaybe impossible (op ^. scopedIdenSrcName . S.nameFixity)
 
 instance HasFixity PatternInfixApp where
-  getFixity (PatternInfixApp _ op _) = fromMaybe impossible (op ^. scopedIdenName . S.nameFixity)
+  getFixity (PatternInfixApp _ op _) = fromMaybe impossible (op ^. scopedIdenSrcName . S.nameFixity)
 
 instance HasFixity PatternPostfixApp where
-  getFixity (PatternPostfixApp _ op) = fromMaybe impossible (op ^. scopedIdenName . S.nameFixity)
+  getFixity (PatternPostfixApp _ op) = fromMaybe impossible (op ^. scopedIdenSrcName . S.nameFixity)
 
 instance HasAtomicity (ListPattern s) where
   atomicity = const Atom

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

@@ -461,7 +461,7 @@ instance PrettyPrint ScopedModule where
   ppCode m = ppCode (m ^. scopedModuleName)
 
 instance PrettyPrint ScopedIden where
-  ppCode = ppCode . (^. scopedIdenName)
+  ppCode = ppCode . (^. scopedIdenSrcName)
 
 instance (SingI s) => PrettyPrint (AliasDef s) where
   ppCode AliasDef {..} =

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

@@ -1820,7 +1820,7 @@ checkRecordPattern ::
   Sem r (RecordPattern 'Scoped)
 checkRecordPattern r = do
   c' <- getNameOfKind KNameConstructor (r ^. recordPatternConstructor)
-  fields <- fromMaybeM (return (RecordNameSignature mempty)) (gets (^. scoperConstructorFields . at (c' ^. scopedIdenName . S.nameId)))
+  fields <- fromMaybeM (return (RecordNameSignature mempty)) (gets (^. scoperConstructorFields . at (c' ^. scopedIdenFinal . S.nameId)))
   l' <-
     if
         | null (r ^. recordPatternItems) -> return []
@@ -2339,7 +2339,7 @@ checkIterator ::
   Sem r (Iterator 'Scoped)
 checkIterator iter = do
   _iteratorName <- checkScopedIden (iter ^. iteratorName)
-  case _iteratorName ^. scopedIdenName . S.nameIterator of
+  case _iteratorName ^. scopedIdenFinal . S.nameIterator of
     Just IteratorInfo {..} -> do
       case _iteratorInfoInitNum of
         Just n
@@ -2422,7 +2422,7 @@ checkParens e@(ExpressionAtoms as _) = case as of
   p :| [] -> case p of
     AtomIdentifier s -> do
       scopedId <- checkScopedIden s
-      let scopedIdenNoFix = over scopedIdenName (set S.nameFixity Nothing) scopedId
+      let scopedIdenNoFix = over scopedIdenSrcName (set S.nameFixity Nothing) scopedId
       return (ExpressionParensIdentifier scopedIdenNoFix)
     AtomIterator i -> ExpressionIterator . set iteratorParens True <$> checkIterator i
     AtomCase c -> ExpressionCase . set caseParens True <$> checkCase c
@@ -2617,7 +2617,7 @@ makeExpressionTable (ExpressionAtoms atoms _) = [recordUpdate] : [appOpExplicit]
                 OpNone -> Nothing
           | otherwise = Nothing
           where
-            S.Name' {..} = iden ^. scopedIdenName
+            S.Name' {..} = iden ^. scopedIdenSrcName
 
         parseSymbolId :: S.NameId -> Parse ScopedIden
         parseSymbolId uid = P.token getIdentifierWithId mempty
@@ -2625,7 +2625,7 @@ makeExpressionTable (ExpressionAtoms atoms _) = [recordUpdate] : [appOpExplicit]
             getIdentifierWithId :: ExpressionAtom 'Scoped -> Maybe ScopedIden
             getIdentifierWithId s = case s of
               AtomIdentifier iden
-                | uid == iden ^. scopedIdenName . S.nameId -> Just iden
+                | uid == iden ^. scopedIdenSrcName . S.nameId -> Just iden
               _ -> Nothing
 
     recordUpdate :: P.Operator Parse Expression
@@ -2843,7 +2843,7 @@ parseTerm =
         identifierNoFixity :: ExpressionAtom 'Scoped -> Maybe ScopedIden
         identifierNoFixity s = case s of
           AtomIdentifier iden
-            | not (S.hasFixity (iden ^. scopedIdenName)) -> Just iden
+            | not (S.hasFixity (iden ^. scopedIdenSrcName)) -> Just iden
           _ -> Nothing
 
     parseDoubleBraces :: Parse Expression
@@ -2892,8 +2892,8 @@ makePatternTable (PatternAtoms latoms _) = [appOp] : operators
       where
         unqualifiedSymbolOp :: ScopedIden -> Maybe (Precedence, P.Operator ParsePat PatternArg)
         unqualifiedSymbolOp constr = run . runFail $ do
-          Fixity {..} <- failMaybe (constr ^. scopedIdenName . S.nameFixity)
-          let _nameId = constr ^. scopedIdenName . S.nameId
+          Fixity {..} <- failMaybe (constr ^. scopedIdenSrcName . S.nameFixity)
+          let _nameId = constr ^. scopedIdenSrcName . S.nameId
           case _fixityArity of
             OpUnary u -> return (_fixityPrecedence, P.Postfix (unaryApp <$> parseSymbolId _nameId))
               where
@@ -2916,7 +2916,7 @@ makePatternTable (PatternAtoms latoms _) = [appOp] : operators
             getConstructorRefWithId :: PatternAtom 'Scoped -> Maybe ScopedIden
             getConstructorRefWithId s = do
               ref <- getConstructorRef s
-              guard (ref ^. scopedIdenName . S.nameId == uid)
+              guard (ref ^. scopedIdenSrcName . S.nameId == uid)
               return ref
 
     -- Application by juxtaposition.
@@ -2965,7 +2965,7 @@ parsePatternTerm = do
         constructorNoFixity :: PatternAtom 'Scoped -> Maybe ScopedIden
         constructorNoFixity s = case s of
           PatternAtomIden (PatternScopedConstructor ref)
-            | not (S.hasFixity (n ^. scopedIdenName)) -> Just ref
+            | not (S.hasFixity (n ^. scopedIdenSrcName)) -> Just ref
             where
               n = ref
           _ -> Nothing

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

@@ -757,7 +757,7 @@ goExpression = \case
     goNamedApplicationNew napp extraArgs = case nonEmpty (napp ^. namedApplicationNewArguments) of
       Nothing -> return (goIden (napp ^. namedApplicationNewName))
       Just appargs -> do
-        let name = napp ^. namedApplicationNewName . scopedIdenName
+        let name = napp ^. namedApplicationNewName . scopedIdenFinal
         sig <- fromJust <$> asks (^. S.infoNameSigs . at (name ^. S.nameId))
         cls <- goArgs appargs
         let args :: [Internal.Name] = appargs ^.. each . namedArgumentNewFunDef . signName . to goSymbol

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

@@ -70,7 +70,7 @@ runNamedArguments napp extraArgs = do
   where
     mkIniBuilderState :: Sem r BuilderState
     mkIniBuilderState = do
-      let name = napp ^. namedAppName . scopedIdenName
+      let name = napp ^. namedAppName . scopedIdenFinal
       msig <- asks @NameSignatures (^. at (name ^. S.nameId))
       let sig = fromMaybe err msig
             where

test/Typecheck/Positive.hs

@@ -319,6 +319,10 @@ tests =
       "Typecheck constructor wildcard"
       $(mkRelDir ".")
       $(mkRelFile "ConstructorWildcard.juvix"),
+    posTest
+      "Typecheck record constructor alias"
+      $(mkRelDir ".")
+      $(mkRelFile "AliasRecordConstructor.juvix"),
     posTestAbsDir
       "Typecheck orphan file"
       (relToProject $(mkRelDir "tests/WithoutPackageFile"))

tests/positive/AliasRecordConstructor.juvix

@@ -0,0 +1,23 @@
+module AliasRecordConstructor;
+
+type A := a;
+
+type T := mkT {field : A};
+
+syntax alias mkT' := mkT;
+
+t : T :=
+  mkT'@{
+    field := a
+  };
+
+t1 : T -> A
+ | mkT'@{ field := x } := x;
+
+syntax iterator it {init := 0; range := 1};
+it : (A → A) → T → A
+  | _ (mkT a) := a;
+
+syntax alias it' := it;
+
+t2 (t : T) : A := it' (a in t) a;