Unify type signature declaration syntax (#3178)

* Closes #2990 
* Allows type signatures for constructors, record fields and axioms to
have the same form as in function definitions, e.g.,
```
field {A} {{M A}} (arg1 arg2 : A) : List A
```
* For constructors, this introduces an ambiguity between record and GADT
syntax with names. For example,
```
ctr {
  A : Type
}
```
can be confused by the parser with initial part of GADT type signature:
```
ctr {A : Type} : A -> C A
```
For now, this is resolved by preferring the record syntax. Hence, it's
currently not possible to use type signatures with implicit arguments
for constructors. Ultimately, the `@` in record syntax should be made
mandatory, which would resolve the ambiguity:
```
ctr@{
  A : Type
}
```

---------

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>

include/package/PackageDescription/V2.juvix

@@ -4,7 +4,7 @@ import Juvix.Builtin.V1 open public;
 
 --- A ;Package; defines the configuration for a Juvix package
 type Package :=
-  mkPackage {
+  mkPackage@{
     -- The name of the package
     name : String;
     -- The version for the package
@@ -19,7 +19,7 @@ type Package :=
 
 --- A ;SemVer; defines a version that conforms to the Semantic Versioning specification.
 type SemVer :=
-  mkSemVer {
+  mkSemVer@{
     major : Nat;
     minor : Nat;
     patch : Nat;
@@ -30,9 +30,9 @@ type SemVer :=
 --- A ;Dependency; defines a Juvix package dependency.
 type Dependency :=
   | --- A filesystem path to another Juvix Package.
-    path {path : String}
+    path@{path : String}
   | --- A ;git; repository containing a Juvix package at its root
-    git {
+    git@{
       -- A name for this dependency
       name : String;
       -- The URL to the git repository

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

@@ -54,14 +54,17 @@ addSymbol isImplicit mdefault sym ty = addArgument isImplicit mdefault (Just sym
 class HasNameSignature (s :: Stage) d | d -> s where
   addArgs :: (Members '[NameSignatureBuilder s] r) => d -> Sem r ()
 
+instance (SingI s) => HasNameSignature s (TypeSig s) where
+  addArgs a = do
+    mapM_ addSigArg (a ^. typeSigArgs)
+    whenJust (a ^. typeSigRetType) addExpressionType
+
 instance (SingI s) => HasNameSignature s (AxiomDef s) where
   addArgs :: (Members '[NameSignatureBuilder s] r) => AxiomDef s -> Sem r ()
-  addArgs a = addExpressionType (a ^. axiomType)
+  addArgs a = addArgs (a ^. axiomTypeSig)
 
 instance (SingI s) => HasNameSignature s (FunctionDef s) where
-  addArgs a = do
-    mapM_ addSigArg (a ^. signArgs)
-    whenJust (a ^. signRetType) addExpressionType
+  addArgs a = addArgs (a ^. signTypeSig)
 
 instance (SingI s) => HasNameSignature s (InductiveDef s, ConstructorDef s) where
   addArgs ::
@@ -89,7 +92,7 @@ instance (SingI s) => HasNameSignature s (InductiveDef s, ConstructorDef s) wher
 
       addRhs :: ConstructorRhs s -> Sem r ()
       addRhs = \case
-        ConstructorRhsGadt g -> addExpressionType (g ^. rhsGadtType)
+        ConstructorRhsGadt g -> addArgs (g ^. rhsGadtTypeSig)
         ConstructorRhsRecord g -> addRecord g
         ConstructorRhsAdt {} -> return ()
 

src/Juvix/Compiler/Concrete/Extra.hs

@@ -110,4 +110,4 @@ isBodyExpression = \case
 
 isFunctionLike :: FunctionDef a -> Bool
 isFunctionLike = \case
-  FunctionDef {..} -> not (null _signArgs) || not (isBodyExpression _signBody)
+  FunctionDef {..} -> not (null (_signTypeSig ^. typeSigArgs)) || not (isBodyExpression _signBody)

src/Juvix/Compiler/Concrete/Gen.hs

@@ -29,9 +29,12 @@ simplestFunctionDef funName funBody =
   FunctionDef
     { _signName = funName,
       _signBody = SigBodyExpression funBody,
-      _signColonKw = Irrelevant Nothing,
-      _signArgs = [],
-      _signRetType = Nothing,
+      _signTypeSig =
+        TypeSig
+          { _typeSigColonKw = Irrelevant Nothing,
+            _typeSigArgs = [],
+            _typeSigRetType = Nothing
+          },
       _signDoc = Nothing,
       _signPragmas = Nothing,
       _signBuiltin = Nothing,
@@ -137,30 +140,45 @@ functionDefExpression ::
   Sem r (FunctionDefBody 'Parsed)
 functionDefExpression exp = SigBodyExpression <$> expressionAtoms' exp
 
+mkFun :: forall s. (SingI s) => FunctionParameters s -> ExpressionType s -> ExpressionType s
+mkFun params tgt = case sing :: SStage s of
+  SParsed -> mkFunParsed params tgt
+  SScoped -> mkFunScoped params tgt
+
+mkFunction :: forall s. (SingI s) => FunctionParameters s -> ExpressionType s -> Function s
+mkFunction params tgt =
+  Function
+    { _funParameters = params,
+      _funReturn = tgt,
+      _funKw = funkw
+    }
+  where
+    funkw =
+      KeywordRef
+        { _keywordRefKeyword = kwRightArrow,
+          _keywordRefInterval = case sing :: SStage s of
+            SParsed -> getLoc tgt
+            SScoped -> getLoc tgt,
+          _keywordRefUnicode = Ascii
+        }
+
+mkFunParsed :: FunctionParameters 'Parsed -> ExpressionType 'Parsed -> ExpressionType 'Parsed
+mkFunParsed params tgt =
+  mkExpressionAtoms
+    . NonEmpty.singleton
+    . AtomFunction
+    $ mkFunction params tgt
+
+mkFunScoped :: FunctionParameters 'Scoped -> ExpressionType 'Scoped -> ExpressionType 'Scoped
+mkFunScoped params tgt =
+  ExpressionFunction $ mkFunction params tgt
+
 mkProjectionType :: InductiveDef 'Parsed -> ExpressionType 'Parsed -> ExpressionType 'Parsed
 mkProjectionType i indTy =
   foldr mkFun target indParams
   where
     indParams = map mkFunctionParameters $ i ^. inductiveParameters
-    target = mkFun (mkRecordParameter (i ^. inductiveTypeApplied)) indTy
-
-    mkFun :: FunctionParameters 'Parsed -> ExpressionType 'Parsed -> ExpressionType 'Parsed
-    mkFun params tgt =
-      mkExpressionAtoms
-        . NonEmpty.singleton
-        . AtomFunction
-        $ Function
-          { _funParameters = params,
-            _funReturn = tgt,
-            _funKw = funkw
-          }
-      where
-        funkw =
-          KeywordRef
-            { _keywordRefKeyword = kwRightArrow,
-              _keywordRefInterval = getLoc (i ^. inductiveName),
-              _keywordRefUnicode = Ascii
-            }
+    target = mkFunParsed (mkRecordParameter (i ^. inductiveTypeApplied)) indTy
 
     mkFunctionParameters :: InductiveParameters 'Parsed -> FunctionParameters 'Parsed
     mkFunctionParameters InductiveParameters {..} =
@@ -230,3 +248,65 @@ mkProjectionType i indTy =
               _keywordRefInterval = getLoc (i ^. inductiveName),
               _keywordRefUnicode = Ascii
             }
+
+mkWildcardKw :: Interval -> KeywordRef
+mkWildcardKw loc =
+  KeywordRef
+    { _keywordRefKeyword = kwWildcard,
+      _keywordRefUnicode = Ascii,
+      _keywordRefInterval = loc
+    }
+
+mkWildcardParsed :: Interval -> ExpressionType 'Parsed
+mkWildcardParsed loc =
+  mkExpressionAtoms
+    . NonEmpty.singleton
+    . AtomHole
+    $ mkWildcardKw loc
+
+mkTypeSigType :: forall s r. (SingI s, Member NameIdGen r) => TypeSig s -> Sem r (ExpressionType s)
+mkTypeSigType ts = do
+  wildcard <-
+    case sing :: SStage s of
+      SParsed ->
+        return $ mkWildcardParsed defaultLoc
+      SScoped -> do
+        ExpressionHole
+          . mkHole defaultLoc
+          <$> freshNameId
+  return $ mkTypeSigType' wildcard ts
+  where
+    defaultLoc :: Interval
+    defaultLoc = singletonInterval (mkInitialLoc sourcePath)
+
+    sourcePath :: Path Abs File
+    sourcePath = $(mkAbsFile "/<source>")
+
+mkTypeSigType' :: forall s. (SingI s) => ExpressionType s -> TypeSig s -> (ExpressionType s)
+mkTypeSigType' wildcard TypeSig {..} =
+  foldr mkFun rty (map mkFunctionParameters _typeSigArgs)
+  where
+    rty = fromMaybe wildcard _typeSigRetType
+
+    univ :: Interval -> ExpressionType s
+    univ loc = run (runReader loc smallUniverseExpression)
+
+    mkFunctionParameters :: SigArg s -> FunctionParameters s
+    mkFunctionParameters arg@SigArg {..} =
+      FunctionParameters
+        { _paramNames = getSigArgNames arg,
+          _paramImplicit = _sigArgImplicit,
+          _paramDelims = fmap Just _sigArgDelims,
+          _paramColon = Irrelevant $ maybe Nothing (Just . (^. unIrrelevant)) _sigArgColon,
+          _paramType = fromMaybe (univ (getLoc arg)) _sigArgType
+        }
+
+    getSigArgNames :: SigArg s -> [FunctionParameter s]
+    getSigArgNames arg = case arg ^. sigArgNames of
+      SigArgNames ns -> map getArgName (toList ns)
+      SigArgNamesInstance -> [FunctionParameterWildcard (mkWildcardKw (getLoc arg))]
+
+    getArgName :: Argument s -> FunctionParameter s
+    getArgName = \case
+      ArgumentSymbol n -> FunctionParameterName n
+      ArgumentWildcard (Wildcard loc) -> FunctionParameterWildcard (mkWildcardKw loc)

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

@@ -592,6 +592,33 @@ deriving stock instance Ord (SigArg 'Parsed)
 
 deriving stock instance Ord (SigArg 'Scoped)
 
+data TypeSig (s :: Stage) = TypeSig
+  { _typeSigArgs :: [SigArg s],
+    _typeSigColonKw :: Irrelevant (Maybe KeywordRef),
+    _typeSigRetType :: Maybe (ExpressionType s)
+  }
+  deriving stock (Generic)
+
+instance Serialize (TypeSig 'Scoped)
+
+instance NFData (TypeSig 'Scoped)
+
+instance Serialize (TypeSig 'Parsed)
+
+instance NFData (TypeSig 'Parsed)
+
+deriving stock instance Show (TypeSig 'Parsed)
+
+deriving stock instance Show (TypeSig 'Scoped)
+
+deriving stock instance Eq (TypeSig 'Parsed)
+
+deriving stock instance Eq (TypeSig 'Scoped)
+
+deriving stock instance Ord (TypeSig 'Parsed)
+
+deriving stock instance Ord (TypeSig 'Scoped)
+
 data FunctionClause (s :: Stage) = FunctionClause
   { _clausenPipeKw :: Irrelevant KeywordRef,
     _clausenPatterns :: NonEmpty (PatternAtomType s),
@@ -647,9 +674,7 @@ deriving stock instance Ord (FunctionDefBody 'Scoped)
 
 data FunctionDef (s :: Stage) = FunctionDef
   { _signName :: FunctionName s,
-    _signArgs :: [SigArg s],
-    _signColonKw :: Irrelevant (Maybe KeywordRef),
-    _signRetType :: Maybe (ExpressionType s),
+    _signTypeSig :: TypeSig s,
     _signDoc :: Maybe (Judoc s),
     _signPragmas :: Maybe ParsedPragmas,
     _signBuiltin :: Maybe (WithLoc BuiltinFunction),
@@ -685,9 +710,8 @@ data AxiomDef (s :: Stage) = AxiomDef
     _axiomDoc :: Maybe (Judoc s),
     _axiomPragmas :: Maybe ParsedPragmas,
     _axiomName :: SymbolType s,
-    _axiomColonKw :: Irrelevant KeywordRef,
-    _axiomBuiltin :: Maybe (WithLoc BuiltinAxiom),
-    _axiomType :: ExpressionType s
+    _axiomTypeSig :: TypeSig s,
+    _axiomBuiltin :: Maybe (WithLoc BuiltinAxiom)
   }
   deriving stock (Generic)
 
@@ -768,7 +792,7 @@ deriving stock instance Ord (RecordUpdateField 'Scoped)
 data RecordField (s :: Stage) = RecordField
   { _fieldName :: SymbolType s,
     _fieldIsImplicit :: IsImplicitField,
-    _fieldColon :: Irrelevant (KeywordRef),
+    _fieldTypeSig :: TypeSig s,
     _fieldType :: ExpressionType s,
     _fieldBuiltin :: Maybe (WithLoc BuiltinFunction),
     _fieldDoc :: Maybe (Judoc s),
@@ -836,8 +860,7 @@ deriving stock instance Ord (RhsRecord 'Parsed)
 deriving stock instance Ord (RhsRecord 'Scoped)
 
 data RhsGadt (s :: Stage) = RhsGadt
-  { _rhsGadtColon :: Irrelevant KeywordRef,
-    _rhsGadtType :: ExpressionType s
+  { _rhsGadtTypeSig :: TypeSig s
   }
   deriving stock (Generic)
 
@@ -2809,12 +2832,11 @@ data FunctionLhs (s :: Stage) = FunctionLhs
     _funLhsInstance :: Maybe KeywordRef,
     _funLhsCoercion :: Maybe KeywordRef,
     _funLhsName :: FunctionName s,
-    _funLhsArgs :: [SigArg s],
-    _funLhsColonKw :: Irrelevant (Maybe KeywordRef),
-    _funLhsRetType :: Maybe (ExpressionType s)
+    _funLhsTypeSig :: TypeSig s
   }
 
 makeLenses ''SideIfs
+makeLenses ''TypeSig
 makeLenses ''FunctionLhs
 makeLenses ''Statements
 makeLenses ''NamedArgumentFunctionDef
@@ -2910,9 +2932,7 @@ functionDefLhs FunctionDef {..} =
       _funLhsInstance = _signInstance,
       _funLhsCoercion = _signCoercion,
       _funLhsName = _signName,
-      _funLhsArgs = _signArgs,
-      _funLhsColonKw = _signColonKw,
-      _funLhsRetType = _signRetType
+      _funLhsTypeSig = _signTypeSig
     }
 
 fixityFieldHelper :: SimpleGetter (ParsedFixityFields s) (Maybe a) -> SimpleGetter (ParsedFixityInfo s) (Maybe a)
@@ -3060,7 +3080,7 @@ instance HasLoc (InductiveDef s) where
   getLoc i = (getLoc <$> i ^. inductivePositive) ?<> getLoc (i ^. inductiveKw)
 
 instance (SingI s) => HasLoc (AxiomDef s) where
-  getLoc m = getLoc (m ^. axiomKw) <> getLocExpressionType (m ^. axiomType)
+  getLoc m = getLoc (m ^. axiomKw) <> getLocExpressionType (fromJust (m ^. axiomTypeSig . typeSigRetType))
 
 getLocPublicAnn :: PublicAnn -> Maybe Interval
 getLocPublicAnn p = getLoc <$> p ^? _Public