Curly braces are allowed nested in patterns (#1380)

src/Juvix/Syntax/Abstract/Language.hs

@@ -60,7 +60,7 @@ data FunctionDef = FunctionDef
 
 data FunctionClause = FunctionClause
   { _clauseName :: FunctionName,
-    _clausePatterns :: [Pattern],
+    _clausePatterns :: [PatternArg],
     _clauseBody :: Expression
   }
   deriving stock (Eq, Show)
@@ -152,7 +152,13 @@ instance HasAtomicity Function where
 -- | Fully applied constructor in a pattern.
 data ConstructorApp = ConstructorApp
   { _constrAppConstructor :: ConstructorRef,
-    _constrAppParameters :: [Pattern]
+    _constrAppParameters :: [PatternArg]
+  }
+  deriving stock (Eq, Show)
+
+data PatternArg = PatternArg
+  { _patternArgIsImplicit :: IsImplicit,
+    _patternArgPattern :: Pattern
   }
   deriving stock (Eq, Show)
 
@@ -161,7 +167,6 @@ data Pattern
   | PatternConstructorApp ConstructorApp
   | PatternWildcard Wildcard
   | PatternEmpty
-  | PatternBraces Pattern
   deriving stock (Eq, Show)
 
 data InductiveDef = InductiveDef
@@ -187,6 +192,7 @@ data AxiomDef = AxiomDef
   deriving stock (Eq, Show)
 
 makeLenses ''Module
+makeLenses ''PatternArg
 makeLenses ''FunctionParameter
 makeLenses ''Function
 makeLenses ''FunctionDef

src/Juvix/Syntax/Abstract/Language/Extra.hs

@@ -17,16 +17,18 @@ data ApplicationArg = ApplicationArg
 
 makeLenses ''ApplicationArg
 
-patternVariables :: Pattern -> [VarName]
+patternVariables :: Traversal' Pattern VarName
-patternVariables = \case
+patternVariables f p = case p of
-  PatternVariable v -> [v]
+  PatternVariable v -> PatternVariable <$> f v
-  PatternWildcard {} -> []
+  PatternWildcard {} -> pure p
-  PatternEmpty {} -> []
+  PatternEmpty {} -> pure p
-  PatternBraces b -> patternVariables b
+  PatternConstructorApp app -> PatternConstructorApp <$> appVariables f app
-  PatternConstructorApp app -> appVariables app
 
-appVariables :: ConstructorApp -> [VarName]
+patternArgVariables :: Traversal' PatternArg VarName
-appVariables (ConstructorApp _ ps) = concatMap patternVariables ps
+patternArgVariables f = traverseOf patternArgPattern (patternVariables f)
+
+appVariables :: Traversal' ConstructorApp VarName
+appVariables f = traverseOf constrAppParameters (traverse (patternArgVariables f))
 
 idenName :: Iden -> Name
 idenName = \case
@@ -36,25 +38,35 @@ idenName = \case
   IdenInductive (InductiveRef i) -> i
   IdenAxiom (AxiomRef a) -> a
 
-smallerPatternVariables :: Pattern -> [VarName]
+smallerPatternVariables :: Traversal' Pattern VarName
-smallerPatternVariables = \case
+smallerPatternVariables f p = case p of
-  PatternVariable {} -> []
+  PatternVariable {} -> pure p
-  PatternBraces b -> smallerPatternVariables b
+  PatternWildcard {} -> pure p
-  PatternWildcard {} -> []
+  PatternEmpty {} -> pure p
-  PatternEmpty {} -> []
+  PatternConstructorApp app -> PatternConstructorApp <$> appVariables f app
-  PatternConstructorApp app -> appVariables app
 
-viewApp :: Expression -> (Expression, [Expression])
+viewApp :: Expression -> (Expression, [ApplicationArg])
-viewApp e = case e of
+viewApp e =
-  ExpressionApplication (Application l r _) ->
+  case e of
-    second (`snoc` r) (viewApp l)
+    ExpressionApplication (Application l r i) ->
-  _ -> (e, [])
+      second (`snoc` ApplicationArg i r) (viewApp l)
+    _ -> (e, [])
+
+viewAppArgAsPattern :: ApplicationArg -> Maybe PatternArg
+viewAppArgAsPattern a = do
+  p' <- viewExpressionAsPattern (a ^. appArg)
+  return
+    ( PatternArg
+        { _patternArgIsImplicit = a ^. appArgIsImplicit,
+          _patternArgPattern = p'
+        }
+    )
 
 viewExpressionAsPattern :: Expression -> Maybe Pattern
 viewExpressionAsPattern e = case viewApp e of
   (f, args)
     | Just c <- getConstructor f -> do
-        args' <- mapM viewExpressionAsPattern args
+        args' <- mapM viewAppArgAsPattern args
         Just $ PatternConstructorApp (ConstructorApp c args')
   (f, [])
     | Just v <- getVariable f -> Just (PatternVariable v)
@@ -200,13 +212,16 @@ isSmallUniverse' = \case
   ExpressionUniverse u -> isSmallUniverse u
   _ -> False
 
-toApplicationArg :: Pattern -> ApplicationArg
+toApplicationArg :: PatternArg -> ApplicationArg
-toApplicationArg = \case
+toApplicationArg p =
-  PatternVariable v -> ApplicationArg Explicit (toExpression v)
+  set appArgIsImplicit (p ^. patternArgIsImplicit) (helper (p ^. patternArgPattern))
-  PatternConstructorApp a -> ApplicationArg Explicit (toExpression a)
+  where
-  PatternEmpty -> impossible
+    helper :: Pattern -> ApplicationArg
-  PatternBraces p -> set appArgIsImplicit Implicit (toApplicationArg p)
+    helper = \case
-  PatternWildcard _ -> error "TODO"
+      PatternVariable v -> ApplicationArg Explicit (toExpression v)
+      PatternConstructorApp a -> ApplicationArg Explicit (toExpression a)
+      PatternEmpty -> impossible
+      PatternWildcard _ -> error "TODO"
 
 clauseLhsAsExpression :: FunctionClause -> Expression
 clauseLhsAsExpression cl =

src/Juvix/Syntax/Concrete/Language.hs

@@ -83,7 +83,7 @@ type family ExpressionType s = res | res -> s where
 type PatternType :: Stage -> GHC.Type
 type family PatternType s = res | res -> s where
   PatternType 'Parsed = PatternAtom 'Parsed
-  PatternType 'Scoped = Pattern
+  PatternType 'Scoped = PatternArg
 
 type family ImportType (s :: Stage) :: GHC.Type where
   ImportType 'Parsed = TopModulePath
@@ -257,15 +257,15 @@ deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Ind
 --------------------------------------------------------------------------------
 
 data PatternApp = PatternApp
-  { _patAppLeft :: Pattern,
+  { _patAppLeft :: PatternArg,
-    _patAppRight :: Pattern
+    _patAppRight :: PatternArg
   }
   deriving stock (Show, Eq, Ord)
 
 data PatternInfixApp = PatternInfixApp
-  { _patInfixLeft :: Pattern,
+  { _patInfixLeft :: PatternArg,
     _patInfixConstructor :: ConstructorRef,
-    _patInfixRight :: Pattern
+    _patInfixRight :: PatternArg
   }
   deriving stock (Show, Eq, Ord)
 
@@ -273,7 +273,7 @@ instance HasFixity PatternInfixApp where
   getFixity (PatternInfixApp _ op _) = fromMaybe impossible (op ^. constructorRefName . S.nameFixity)
 
 data PatternPostfixApp = PatternPostfixApp
-  { _patPostfixParameter :: Pattern,
+  { _patPostfixParameter :: PatternArg,
     _patPostfixConstructor :: ConstructorRef
   }
   deriving stock (Show, Eq, Ord)
@@ -281,13 +281,18 @@ data PatternPostfixApp = PatternPostfixApp
 instance HasFixity PatternPostfixApp where
   getFixity (PatternPostfixApp _ op) = fromMaybe impossible (op ^. constructorRefName . S.nameFixity)
 
+data PatternArg = PatternArg
+  { _patternArgIsImplicit :: IsImplicit,
+    _patternArgPattern :: Pattern
+  }
+  deriving stock (Show, Eq, Ord)
+
 data Pattern
   = PatternVariable (SymbolType 'Scoped)
   | PatternConstructor ConstructorRef
   | PatternApplication PatternApp
   | PatternInfixApplication PatternInfixApp
   | PatternPostfixApplication PatternPostfixApp
-  | PatternBraces Pattern
   | PatternWildcard Wildcard
   | PatternEmpty
   deriving stock (Show, Eq, Ord)
@@ -300,7 +305,6 @@ instance HasAtomicity Pattern where
     PatternInfixApplication a -> Aggregate (getFixity a)
     PatternPostfixApplication p -> Aggregate (getFixity p)
     PatternWildcard {} -> Atom
-    PatternBraces {} -> Atom
     PatternEmpty -> Atom
 
 --------------------------------------------------------------------------------
@@ -887,8 +891,7 @@ data ExpressionAtoms (s :: Stage) = ExpressionAtoms
     _expressionAtomsLoc :: Interval
   }
 
---------------------------------------------------------------------------------
+makeLenses ''PatternArg
-
 makeLenses ''Function
 makeLenses ''InductiveDef
 makeLenses ''PostfixApplication
@@ -1048,6 +1051,11 @@ instance
 
 --------------------------------------------------------------------------------
 
+instance HasAtomicity PatternArg where
+  atomicity p
+    | Implicit <- p ^. patternArgIsImplicit = Atom
+    | otherwise = atomicity (p ^. patternArgPattern)
+
 idenOverName :: (forall s. S.Name' s -> S.Name' s) -> ScopedIden -> ScopedIden
 idenOverName f = \case
   ScopedAxiom a -> ScopedAxiom (over axiomRefName f a)

src/Juvix/Syntax/Concrete/Scoped/Pretty/Base.hs

@@ -448,6 +448,9 @@ instance PrettyCode QualifiedName where
     let symbols = _qualifiedPath ^. pathParts NonEmpty.|> _qualifiedSymbol
     dotted <$> mapM ppSymbol symbols
 
+bracesIf :: Bool -> Doc Ann -> Doc Ann
+bracesIf t = if t then braces else id
+
 ppName :: forall s r. (SingI s, Members '[Reader Options] r) => IdentifierType s -> Sem r (Doc Ann)
 ppName = case sing :: SStage s of
   SParsed -> ppCode
@@ -652,6 +655,11 @@ instance PrettyCode PatternScopedIden where
     PatternScopedVar v -> ppCode v
     PatternScopedConstructor c -> ppCode c
 
+instance PrettyCode PatternArg where
+  ppCode a = do
+    p <- ppCode (a ^. patternArgPattern)
+    return (bracesIf (Implicit == a ^. patternArgIsImplicit) p)
+
 instance SingI s => PrettyCode (PatternAtom s) where
   ppCode a = case a of
     PatternAtomIden n -> case sing :: SStage s of
@@ -750,7 +758,6 @@ instance PrettyCode Pattern where
       return $ l' <+> r'
     PatternWildcard {} -> return kwWildcard
     PatternEmpty -> return $ parens mempty
-    PatternBraces p -> braces <$> ppCode p
     PatternConstructor constr -> ppCode constr
     PatternInfixApplication i -> ppPatternInfixApp i
     PatternPostfixApplication i -> ppPatternPostfixApp i

src/Juvix/Syntax/Concrete/Scoped/Scoper.hs

@@ -1198,7 +1198,7 @@ checkParseExpressionAtoms = checkExpressionAtoms >=> parseExpressionAtoms
 checkParsePatternAtom ::
   Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   PatternAtom 'Parsed ->
-  Sem r Pattern
+  Sem r PatternArg
 checkParsePatternAtom = checkPatternAtom >=> parsePatternAtom
 
 checkStatement ::
@@ -1423,7 +1423,7 @@ parseTerm =
 type ParsePat = P.Parsec () [PatternAtom 'Scoped]
 
 makePatternTable ::
-  PatternAtom 'Scoped -> [[P.Operator ParsePat Pattern]]
+  PatternAtom 'Scoped -> [[P.Operator ParsePat PatternArg]]
 makePatternTable atom = [appOp] : operators
   where
     getConstructorRef :: PatternAtom 'Scoped -> Maybe ConstructorRef
@@ -1437,24 +1437,24 @@ makePatternTable atom = [appOp] : operators
     constructorRefs = case atom of
       PatternAtomParens (PatternAtoms atoms _) -> mapMaybe getConstructorRef (toList atoms)
       _ -> []
-    mkSymbolTable :: [ConstructorRef] -> [[P.Operator ParsePat Pattern]]
+    mkSymbolTable :: [ConstructorRef] -> [[P.Operator ParsePat PatternArg]]
     mkSymbolTable = reverse . map (map snd) . groupSortOn' fst . mapMaybe unqualifiedSymbolOp
       where
-        unqualifiedSymbolOp :: ConstructorRef -> Maybe (Precedence, P.Operator ParsePat Pattern)
+        unqualifiedSymbolOp :: ConstructorRef -> Maybe (Precedence, P.Operator ParsePat PatternArg)
         unqualifiedSymbolOp (ConstructorRef' S.Name' {..})
           | Just Fixity {..} <- _nameFixity,
             _nameKind == S.KNameConstructor = Just $
               case _fixityArity of
                 Unary u -> (_fixityPrecedence, P.Postfix (unaryApp <$> parseSymbolId _nameId))
                   where
-                    unaryApp :: ConstructorRef -> Pattern -> Pattern
+                    unaryApp :: ConstructorRef -> PatternArg -> PatternArg
                     unaryApp funName = case u of
-                      AssocPostfix -> PatternPostfixApplication . (`PatternPostfixApp` funName)
+                      AssocPostfix -> explicitP . PatternPostfixApplication . (`PatternPostfixApp` funName)
                 Binary b -> (_fixityPrecedence, infixLRN (binaryInfixApp <$> parseSymbolId _nameId))
                   where
-                    binaryInfixApp :: ConstructorRef -> Pattern -> Pattern -> Pattern
+                    binaryInfixApp :: ConstructorRef -> PatternArg -> PatternArg -> PatternArg
-                    binaryInfixApp name argLeft = PatternInfixApplication . PatternInfixApp argLeft name
+                    binaryInfixApp name argLeft = explicitP . PatternInfixApplication . PatternInfixApp argLeft name
-                    infixLRN :: ParsePat (Pattern -> Pattern -> Pattern) -> P.Operator ParsePat Pattern
+                    infixLRN :: ParsePat (PatternArg -> PatternArg -> PatternArg) -> P.Operator ParsePat PatternArg
                     infixLRN = case b of
                       AssocLeft -> P.InfixL
                       AssocRight -> P.InfixR
@@ -1470,22 +1470,30 @@ makePatternTable atom = [appOp] : operators
               return ref
 
     -- Application by juxtaposition.
-    appOp :: P.Operator ParsePat Pattern
+    appOp :: P.Operator ParsePat PatternArg
     appOp = P.InfixL (return app)
       where
-        app :: Pattern -> Pattern -> Pattern
+        app :: PatternArg -> PatternArg -> PatternArg
         app l r =
-          PatternApplication
+          explicitP
-            ( PatternApp
+            ( PatternApplication
-                { _patAppLeft = l,
+                ( PatternApp
-                  _patAppRight = r
+                    { _patAppLeft = l,
-                }
+                      _patAppRight = r
+                    }
+                )
             )
 
+explicitP :: Pattern -> PatternArg
+explicitP = PatternArg Explicit
+
+implicitP :: Pattern -> PatternArg
+implicitP = PatternArg Implicit
+
 parsePatternTerm ::
   forall r.
-  Members '[Reader (ParsePat Pattern), Embed ParsePat] r =>
+  Members '[Reader (ParsePat PatternArg), Embed ParsePat] r =>
-  Sem r Pattern
+  Sem r PatternArg
 parsePatternTerm = do
   pPat <- ask
   embed @ParsePat $
@@ -1496,9 +1504,9 @@ parsePatternTerm = do
       <|> parseWildcard
       <|> parseEmpty
   where
-    parseNoInfixConstructor :: ParsePat Pattern
+    parseNoInfixConstructor :: ParsePat PatternArg
     parseNoInfixConstructor =
-      PatternConstructor
+      explicitP . PatternConstructor
         <$> P.token constructorNoFixity mempty
       where
         constructorNoFixity :: PatternAtom 'Scoped -> Maybe ConstructorRef
@@ -1509,35 +1517,38 @@ parsePatternTerm = do
               n = ref ^. constructorRefName
           _ -> Nothing
 
-    parseWildcard :: ParsePat Pattern
+    parseWildcard :: ParsePat PatternArg
-    parseWildcard = PatternWildcard <$> P.token isWildcard mempty
+    parseWildcard = explicitP . PatternWildcard <$> P.token isWildcard mempty
       where
         isWildcard :: PatternAtom 'Scoped -> Maybe Wildcard
         isWildcard s = case s of
           PatternAtomWildcard i -> Just i
           _ -> Nothing
 
-    parseEmpty :: ParsePat Pattern
+    parseEmpty :: ParsePat PatternArg
-    parseEmpty = PatternEmpty <$ P.satisfy isEmpty
+    parseEmpty = explicitP PatternEmpty <$ P.satisfy isEmpty
       where
         isEmpty :: PatternAtom 'Scoped -> Bool
         isEmpty s = case s of
           PatternAtomEmpty -> True
           _ -> False
 
-    parseVariable :: ParsePat Pattern
+    parseVariable :: ParsePat PatternArg
-    parseVariable = PatternVariable <$> P.token var mempty
+    parseVariable = explicitP . PatternVariable <$> P.token var mempty
       where
         var :: PatternAtom 'Scoped -> Maybe S.Symbol
         var s = case s of
           PatternAtomIden (PatternScopedVar sym) -> Just sym
           _ -> Nothing
 
-    parseBraces :: ParsePat Pattern -> ParsePat Pattern
+    parseBraces :: ParsePat PatternArg -> ParsePat PatternArg
     parseBraces patternParser = do
       exprs <- P.token bracesPat mempty
       case P.parse patternParser "" exprs of
-        Right r -> return (PatternBraces r)
+        Right (PatternArg i p)
+          -- TODO proper error
+          | Implicit <- i -> error "nested braces"
+          | otherwise -> return (implicitP p)
         Left {} -> mzero
       where
         bracesPat :: PatternAtom 'Scoped -> Maybe [PatternAtom 'Scoped]
@@ -1545,7 +1556,7 @@ parsePatternTerm = do
           PatternAtomBraces (PatternAtoms ss _) -> Just (toList ss)
           _ -> Nothing
 
-    parseParens :: ParsePat Pattern -> ParsePat Pattern
+    parseParens :: ParsePat PatternArg -> ParsePat PatternArg
     parseParens patternParser = do
       exprs <- P.token parenPat mempty
       case P.parse patternParser "" exprs of
@@ -1560,22 +1571,22 @@ parsePatternTerm = do
 mkPatternParser ::
   forall r.
   Members '[Embed ParsePat] r =>
-  [[P.Operator ParsePat Pattern]] ->
+  [[P.Operator ParsePat PatternArg]] ->
-  Sem r Pattern
+  Sem r PatternArg
 mkPatternParser table = embed @ParsePat pPattern
   where
-    pPattern :: ParsePat Pattern
+    pPattern :: ParsePat PatternArg
     pPattern = P.makeExprParser pTerm table
-    pTerm :: ParsePat Pattern
+    pTerm :: ParsePat PatternArg
     pTerm = runM parseTermRec
       where
-        parseTermRec :: Sem '[Embed ParsePat] Pattern
+        parseTermRec :: Sem '[Embed ParsePat] PatternArg
         parseTermRec = runReader pPattern parsePatternTerm
 
 parsePatternAtom ::
   Members '[Error ScoperError, State Scope] r =>
   PatternAtom 'Scoped ->
-  Sem r Pattern
+  Sem r PatternArg
 parsePatternAtom sec = do
   case res of
     Left {} -> case sec of
@@ -1584,7 +1595,7 @@ parsePatternAtom sec = do
     Right r -> return r
   where
     tbl = makePatternTable sec
-    parser :: ParsePat Pattern
+    parser :: ParsePat PatternArg
     parser = runM (mkPatternParser tbl) <* P.eof
     res = P.parse parser filePath [sec]
 

src/Juvix/Syntax/IsImplicit.hs

@@ -1,8 +1,14 @@
 module Juvix.Syntax.IsImplicit where
 
 import Juvix.Prelude
+import Juvix.Prelude.Pretty
 
 data IsImplicit = Explicit | Implicit
   deriving stock (Show, Eq, Ord, Generic)
 
 instance Hashable IsImplicit
+
+instance Pretty IsImplicit where
+  pretty = \case
+    Implicit -> "implicit"
+    Explicit -> "explicit"

src/Juvix/Syntax/MicroJuvix/ArityChecker.hs

@@ -163,8 +163,8 @@ checkLhs ::
   Interval ->
   Maybe Arity ->
   Arity ->
-  [Pattern] ->
+  [PatternArg] ->
-  Sem r ([Pattern], LocalVars, Arity)
+  Sem r ([PatternArg], LocalVars, Arity)
 checkLhs loc hint ariSignature pats = do
   (locals, (pats', bodyAri)) <- runState emptyLocalVars (goLhs ariSignature pats)
   return (pats', locals, bodyAri)
@@ -173,7 +173,7 @@ checkLhs loc hint ariSignature pats = do
     -- body once all the patterns have been processed).
     -- Does not insert holes greedily. I.e. implicit wildcards are only inserted
     -- between explicit parameters already in the pattern.
-    goLhs :: Arity -> [Pattern] -> Sem (State LocalVars ': r) ([Pattern], Arity)
+    goLhs :: Arity -> [PatternArg] -> Sem (State LocalVars ': r) ([PatternArg], Arity)
     goLhs a = \case
       [] -> return $ case hint >>= tailHelper a of
         Nothing -> ([], a)
@@ -192,25 +192,26 @@ checkLhs loc hint ariSignature pats = do
           p' <- checkPattern ArityUnknown p
           first (p' :) <$> goLhs ArityUnknown ps
         ArityFunction (FunctionArity l r) ->
-          case (getPatternBraces p, l) of
+          case (p ^. patternArgIsImplicit, l) of
-            (Just b, ParamImplicit) -> do
+            (Implicit, ParamImplicit) -> do
-              b' <- checkPattern (arityParameter l) b
+              b' <- checkPattern (arityParameter l) p
               first (b' :) <$> goLhs r ps
-            (Just x, ParamExplicit {}) ->
+            (Implicit, ParamExplicit {}) ->
               throw
-                ( ErrExpectedExplicitPattern
+                ( ErrWrongPatternIsImplicit
-                    ExpectedExplicitPattern
+                    WrongPatternIsImplicit
-                      { _expectedExplicitPattern = x
+                      { _wrongPatternIsImplicitExpected = Explicit,
+                        _wrongPatternIsImplicitActual = p
                       }
                 )
-            (Nothing, ParamImplicit) ->
+            (Explicit, ParamImplicit) ->
               first (wildcard :) <$> goLhs r lhs
-            (Nothing, ParamExplicit pa) -> do
+            (Explicit, ParamExplicit pa) -> do
               p' <- checkPattern pa p
               first (p' :) <$> goLhs r ps
       where
-        wildcard :: Pattern
+        wildcard :: PatternArg
-        wildcard = PatternBraces (PatternWildcard (Wildcard loc))
+        wildcard = PatternArg Implicit (PatternWildcard (Wildcard loc))
 
     tailHelper :: Arity -> Arity -> Maybe Int
     tailHelper a target
@@ -220,30 +221,28 @@ checkLhs loc hint ariSignature pats = do
         a' = dropSuffix target' (unfoldArity a)
         target' = unfoldArity target
 
-    getPatternBraces :: Pattern -> Maybe Pattern
-    getPatternBraces p = case p of
-      PatternBraces {} -> Just p
-      _ -> Nothing
-
 checkPattern ::
+  forall r.
   Members '[Reader InfoTable, Error ArityCheckerError, State LocalVars] r =>
   Arity ->
-  Pattern ->
+  PatternArg ->
-  Sem r Pattern
+  Sem r PatternArg
-checkPattern ari = \case
+checkPattern ari = traverseOf patternArgPattern helper
-  PatternBraces p -> checkPattern ari p
+  where
-  PatternVariable v -> addArity v ari $> PatternVariable v
+    helper :: Pattern -> Sem r Pattern
-  PatternWildcard i -> return (PatternWildcard i)
+    helper = \case
-  PatternConstructorApp c -> case ari of
+      PatternVariable v -> addArity v ari $> PatternVariable v
-    ArityUnit -> PatternConstructorApp <$> checkConstructorApp c
+      PatternWildcard i -> return (PatternWildcard i)
-    ArityUnknown -> PatternConstructorApp <$> checkConstructorApp c
+      PatternConstructorApp c -> case ari of
-    ArityFunction {} ->
+        ArityUnit -> PatternConstructorApp <$> checkConstructorApp c
-      throw
+        ArityUnknown -> PatternConstructorApp <$> checkConstructorApp c
-        ( ErrPatternFunction
+        ArityFunction {} ->
-            PatternFunction
+          throw
-              { _patternFunction = c
+            ( ErrPatternFunction
-              }
+                PatternFunction
-        )
+                  { _patternFunction = c
+                  }
+            )
 
 checkConstructorApp ::
   forall r.

src/Juvix/Syntax/MicroJuvix/ArityChecker/Error.hs

@@ -10,7 +10,7 @@ import Juvix.Syntax.MicroJuvix.ArityChecker.Error.Types
 data ArityCheckerError
   = ErrWrongConstructorAppLength WrongConstructorAppLength
   | ErrLhsTooManyPatterns LhsTooManyPatterns
-  | ErrExpectedExplicitPattern ExpectedExplicitPattern
+  | ErrWrongPatternIsImplicit WrongPatternIsImplicit
   | ErrExpectedExplicitArgument ExpectedExplicitArgument
   | ErrPatternFunction PatternFunction
   | ErrTooManyArguments TooManyArguments
@@ -21,7 +21,7 @@ instance ToGenericError ArityCheckerError where
   genericError = \case
     ErrWrongConstructorAppLength e -> genericError e
     ErrLhsTooManyPatterns e -> genericError e
-    ErrExpectedExplicitPattern e -> genericError e
+    ErrWrongPatternIsImplicit e -> genericError e
     ErrExpectedExplicitArgument e -> genericError e
     ErrPatternFunction e -> genericError e
     ErrTooManyArguments e -> genericError e

src/Juvix/Syntax/MicroJuvix/ArityChecker/Error/Types.hs

@@ -40,7 +40,7 @@ instance ToGenericError WrongConstructorAppLength where
             | otherwise = pretty n
 
 newtype LhsTooManyPatterns = LhsTooManyPatterns
-  { _lhsTooManyPatternsRemaining :: NonEmpty Pattern
+  { _lhsTooManyPatternsRemaining :: NonEmpty PatternArg
   }
 
 makeLenses ''LhsTooManyPatterns
@@ -65,13 +65,14 @@ instance ToGenericError LhsTooManyPatterns where
         | n == 1 = "was"
         | otherwise = "were"
 
-newtype ExpectedExplicitPattern = ExpectedExplicitPattern
+data WrongPatternIsImplicit = WrongPatternIsImplicit
-  { _expectedExplicitPattern :: Pattern
+  { _wrongPatternIsImplicitExpected :: IsImplicit,
+    _wrongPatternIsImplicitActual :: PatternArg
   }
 
-makeLenses ''ExpectedExplicitPattern
+makeLenses ''WrongPatternIsImplicit
 
-instance ToGenericError ExpectedExplicitPattern where
+instance ToGenericError WrongPatternIsImplicit where
   genericError e =
     GenericError
       { _genericErrorLoc = i,
@@ -79,10 +80,17 @@ instance ToGenericError ExpectedExplicitPattern where
         _genericErrorIntervals = [i]
       }
     where
-      i = getLoc (e ^. expectedExplicitPattern)
+      i = getLoc (e ^. wrongPatternIsImplicitActual)
+      expec = e ^. wrongPatternIsImplicitExpected
+      found = e ^. wrongPatternIsImplicitActual . patternArgIsImplicit
+      pat = e ^. wrongPatternIsImplicitActual
       msg =
-        "Expected an explicit pattern but found an implicit pattern"
+        "Expected an"
-          <+> ppCode (e ^. expectedExplicitPattern)
+          <+> pretty expec
+          <+> "pattern but found an"
+          <+> pretty found
+          <+> "pattern:"
+          <+> ppCode pat
 
 data ExpectedExplicitArgument = ExpectedExplicitArgument
   { _expectedExplicitArgumentApp :: (Expression, [(IsImplicit, Expression)]),

src/Juvix/Syntax/MicroJuvix/Language.hs

@@ -57,7 +57,7 @@ data FunctionDef = FunctionDef
 
 data FunctionClause = FunctionClause
   { _clauseName :: FunctionName,
-    _clausePatterns :: [Pattern],
+    _clausePatterns :: [PatternArg],
     _clauseBody :: Expression
   }
 
@@ -113,14 +113,18 @@ instance Hashable Application where
 -- | Fully applied constructor in a pattern.
 data ConstructorApp = ConstructorApp
   { _constrAppConstructor :: Name,
-    _constrAppParameters :: [Pattern]
+    _constrAppParameters :: [PatternArg]
+  }
+
+data PatternArg = PatternArg
+  { _patternArgIsImplicit :: IsImplicit,
+    _patternArgPattern :: Pattern
   }
 
 data Pattern
   = PatternVariable VarName
   | PatternConstructorApp ConstructorApp
   | PatternWildcard Wildcard
-  | PatternBraces Pattern
 
 newtype InductiveParameter = InductiveParameter
   { _inductiveParamName :: VarName
@@ -157,6 +161,7 @@ data Function = Function
 instance Hashable Function
 
 makeLenses ''Module
+makeLenses ''PatternArg
 makeLenses ''Include
 makeLenses ''FunctionDef
 makeLenses ''FunctionClause
@@ -191,12 +196,16 @@ instance HasAtomicity ConstructorApp where
     | null args = Atom
     | otherwise = Aggregate appFixity
 
+instance HasAtomicity PatternArg where
+  atomicity p
+    | Implicit <- p ^. patternArgIsImplicit = Atom
+    | otherwise = atomicity (p ^. patternArgPattern)
+
 instance HasAtomicity Pattern where
   atomicity p = case p of
     PatternConstructorApp a -> atomicity a
     PatternVariable {} -> Atom
     PatternWildcard {} -> Atom
-    PatternBraces {} -> Atom
 
 instance HasLoc FunctionParameter where
   getLoc f = v (getLoc (f ^. paramType))
@@ -232,9 +241,11 @@ instance HasLoc Pattern where
   getLoc = \case
     PatternVariable v -> getLoc v
     PatternConstructorApp a -> getLoc a
-    PatternBraces p -> getLoc p
     PatternWildcard i -> getLoc i
 
+instance HasLoc PatternArg where
+  getLoc = getLoc . (^. patternArgPattern)
+
 instance HasLoc ConstructorApp where
   getLoc (ConstructorApp c ps) =
     case last <$> nonEmpty ps of

src/Juvix/Syntax/MicroJuvix/Language/Extra.hs

@@ -244,27 +244,28 @@ renameToSubsE = fmap (ExpressionIden . IdenVar)
 renameExpression :: Rename -> Expression -> Expression
 renameExpression r = substitutionE (renameToSubsE r)
 
-patternVariables :: Pattern -> [VarName]
+patternArgVariables :: Traversal' PatternArg VarName
-patternVariables = \case
+patternArgVariables f = traverseOf patternArgPattern (patternVariables f)
-  PatternVariable v -> [v]
+
-  PatternConstructorApp a -> goApp a
+patternVariables :: Traversal' Pattern VarName
-  PatternBraces b -> patternVariables b
+patternVariables f p = case p of
-  PatternWildcard {} -> []
+  PatternVariable v -> PatternVariable <$> f v
+  PatternConstructorApp a -> PatternConstructorApp <$> goApp f a
+  PatternWildcard {} -> pure p
   where
-    goApp :: ConstructorApp -> [VarName]
+    goApp :: Traversal' ConstructorApp VarName
-    goApp (ConstructorApp _ ps) = concatMap patternVariables ps
+    goApp g = traverseOf constrAppParameters (traverse (patternArgVariables g))
+
+renamePatternArg :: Rename -> PatternArg -> PatternArg
+renamePatternArg = over patternArgPattern . renamePattern
 
 renamePattern :: Rename -> Pattern -> Pattern
-renamePattern m = go
+renamePattern m = over patternVariables renameVar
   where
-    go :: Pattern -> Pattern
+    renameVar :: VarName -> VarName
-    go p = case p of
+    renameVar v
-      PatternVariable v
+      | Just v' <- m ^. at v = v'
-        | Just v' <- m ^. at v -> PatternVariable v'
+      | otherwise = v
-      PatternConstructorApp a -> PatternConstructorApp (goApp a)
-      _ -> p
-    goApp :: ConstructorApp -> ConstructorApp
-    goApp (ConstructorApp c ps) = ConstructorApp c (map go ps)
 
 inductiveTypeVarsAssoc :: Foldable f => InductiveDef -> f a -> HashMap VarName a
 inductiveTypeVarsAssoc def l
@@ -275,6 +276,7 @@ inductiveTypeVarsAssoc def l
     vars :: [VarName]
     vars = def ^.. inductiveParameters . each . inductiveParamName
 
+-- TODO remove this after monojuvix is gone
 functionTypeVarsAssoc :: forall a f. Foldable f => FunctionDef -> f a -> HashMap VarName a
 functionTypeVarsAssoc def l = sig <> mconcatMap clause (def ^. funDefClauses)
   where
@@ -297,8 +299,8 @@ functionTypeVarsAssoc def l = sig <> mconcatMap clause (def ^. funDefClauses)
         clauseVars :: [Maybe VarName]
         clauseVars = take n (map patternVar (c ^. clausePatterns))
           where
-            patternVar :: Pattern -> Maybe VarName
+            patternVar :: PatternArg -> Maybe VarName
-            patternVar = \case
+            patternVar a = case a ^. patternArgPattern of
               PatternVariable v -> Just v
               _ -> Nothing
 

src/Juvix/Syntax/MicroJuvix/Pretty/Base.hs

@@ -199,6 +199,11 @@ instance PrettyCode InductiveDef where
     rhs <- indent' $ align $ concatWith (\a b -> a <> line <> kwPipe <+> b) inductiveConstructors'
     return $ kwData <+> inductiveName' <+?> params <+> kwEquals <> line <> rhs
 
+instance PrettyCode PatternArg where
+  ppCode a = do
+    p <- ppCode (a ^. patternArgPattern)
+    return (bracesIf (Implicit == a ^. patternArgIsImplicit) p)
+
 instance PrettyCode ConstructorApp where
   ppCode c = do
     constr' <- ppCode (c ^. constrAppConstructor)
@@ -210,7 +215,6 @@ instance PrettyCode Pattern where
     PatternVariable v -> ppCode v
     PatternConstructorApp a -> ppCode a
     PatternWildcard {} -> return kwWildcard
-    PatternBraces b -> braces <$> ppCode b
 
 instance PrettyCode FunctionDef where
   ppCode f = do
@@ -327,8 +331,11 @@ instance PrettyCode TypeCalls where
     elems' <- mapM ppCode elems
     return $ title <> line <> vsep elems' <> line
 
-parensCond :: Bool -> Doc Ann -> Doc Ann
+parensIf :: Bool -> Doc Ann -> Doc Ann
-parensCond t d = if t then parens d else d
+parensIf t = if t then parens else id
+
+bracesIf :: Bool -> Doc Ann -> Doc Ann
+bracesIf t = if t then braces else id
 
 ppPostExpression ::
   (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
@@ -358,7 +365,7 @@ ppLRExpression ::
   a ->
   Sem r (Doc Ann)
 ppLRExpression associates fixlr e =
-  parensCond (atomParens associates (atomicity e) fixlr)
+  parensIf (atomParens associates (atomicity e) fixlr)
     <$> ppCode e
 
 ppCodeAtom :: (HasAtomicity c, PrettyCode c, Members '[Reader Options] r) => c -> Sem r (Doc Ann)

src/Juvix/Syntax/MicroJuvix/TypeChecker.hs

@@ -174,9 +174,9 @@ checkFunctionClause info FunctionClause {..} = do
   where
     clauseType :: Expression
     clauseType = info ^. functionInfoDef . funDefType
-    helper :: [Pattern] -> Expression -> Sem r (LocalVars, Expression)
+    helper :: [PatternArg] -> Expression -> Sem r (LocalVars, Expression)
     helper pats ty = runState emptyLocalVars (go pats ty)
-    go :: [Pattern] -> Expression -> Sem (State LocalVars ': r) Expression
+    go :: [PatternArg] -> Expression -> Sem (State LocalVars ': r) Expression
     go pats bodyTy = case pats of
       [] -> return bodyTy
       (p : ps) -> case bodyTy of
@@ -200,26 +200,38 @@ checkFunctionClause info FunctionClause {..} = do
 typeOfArg :: FunctionParameter -> Expression
 typeOfArg = (^. paramType)
 
+matchIsImplicit :: Member (Error TypeCheckerError) r => IsImplicit -> PatternArg -> Sem r ()
+matchIsImplicit expected actual =
+  unless
+    (expected == actual ^. patternArgIsImplicit)
+    ( throw
+        ( ErrArity
+            ( ErrWrongPatternIsImplicit
+                WrongPatternIsImplicit
+                  { _wrongPatternIsImplicitExpected = expected,
+                    _wrongPatternIsImplicitActual = actual
+                  }
+            )
+        )
+    )
+
 checkPattern ::
   forall r.
   Members '[Reader InfoTable, Error TypeCheckerError, State LocalVars, Inference, NameIdGen] r =>
   FunctionName ->
   FunctionParameter ->
-  Pattern ->
+  PatternArg ->
   Sem r ()
 checkPattern funName = go
   where
-    go :: FunctionParameter -> Pattern -> Sem r ()
+    go :: FunctionParameter -> PatternArg -> Sem r ()
-    go argTy p = do
+    go argTy patArg = do
+      matchIsImplicit (argTy ^. paramImplicit) patArg
       tyVarMap <- fmap (ExpressionIden . IdenVar) . (^. localTyMap) <$> get
       ty <- normalizeType (substitutionE tyVarMap (typeOfArg argTy))
-      let unbrace = \case
+      let pat = patArg ^. patternArgPattern
-            PatternBraces b -> b
-            x -> x
-          pat = unbrace p
       case pat of
         PatternWildcard {} -> return ()
-        PatternBraces {} -> impossible
         PatternVariable v -> do
           modify (addType v ty)
           registerIden v ty

src/Juvix/Termination/FunctionCall.hs

@@ -42,7 +42,7 @@ viewCall = \case
                 return $ case s of
                   Nothing -> CallRow Nothing
                   Just s' -> CallRow (Just (s', REq))
-              _ -> return (CallRow Nothing)
+              Nothing -> return (CallRow Nothing)
   ExpressionIden (IdenFunction x) ->
     return (Just (singletonCall x))
   _ -> return Nothing

src/Juvix/Termination/Types/SizeInfo.hs

@@ -20,15 +20,16 @@ emptySizeInfo =
       _sizeSmaller = mempty
     }
 
-mkSizeInfo :: [Pattern] -> SizeInfo
+mkSizeInfo :: [PatternArg] -> SizeInfo
 mkSizeInfo ps = SizeInfo {..}
   where
-    ps' = filter (not . isBrace) ps
+    ps' :: [Pattern]
-    isBrace = \case
+    ps' = map (^. patternArgPattern) (filter (not . isBrace) ps)
-      PatternBraces {} -> True
+    isBrace :: PatternArg -> Bool
-      _ -> False
+    isBrace = (== Implicit) . (^. patternArgIsImplicit)
-    _sizeEqual = ps
+    _sizeEqual = map (^. patternArgPattern) ps
+    _sizeSmaller :: HashMap VarName Int
     _sizeSmaller =
       HashMap.fromList
-        [ (v, i) | (i, p) <- zip [0 ..] ps', v <- smallerPatternVariables p
+        [ (v, i) | (i, p) <- zip [0 ..] ps', v <- p ^.. smallerPatternVariables
         ]

src/Juvix/Translation/AbstractToMicroJuvix.hs

@@ -163,7 +163,7 @@ goFunctionDef f = do
 goFunctionClause :: Name -> Abstract.FunctionClause -> Sem r FunctionClause
 goFunctionClause n c = do
   _clauseBody' <- goExpression (c ^. Abstract.clauseBody)
-  _clausePatterns' <- mapM goPattern (c ^. Abstract.clausePatterns)
+  _clausePatterns' <- mapM goPatternArg (c ^. Abstract.clausePatterns)
   return
     FunctionClause
       { _clauseName = n,
@@ -171,17 +171,25 @@ goFunctionClause n c = do
         _clauseBody = _clauseBody'
       }
 
+goPatternArg :: Abstract.PatternArg -> Sem r PatternArg
+goPatternArg p = do
+  pat' <- goPattern (p ^. Abstract.patternArgPattern)
+  return
+    PatternArg
+      { _patternArgIsImplicit = p ^. Abstract.patternArgIsImplicit,
+        _patternArgPattern = pat'
+      }
+
 goPattern :: Abstract.Pattern -> Sem r Pattern
 goPattern p = case p of
   Abstract.PatternVariable v -> return (PatternVariable v)
   Abstract.PatternConstructorApp c -> PatternConstructorApp <$> goConstructorApp c
   Abstract.PatternWildcard i -> return (PatternWildcard i)
-  Abstract.PatternBraces b -> PatternBraces <$> goPattern b
   Abstract.PatternEmpty -> unsupported "pattern empty"
 
 goConstructorApp :: Abstract.ConstructorApp -> Sem r ConstructorApp
 goConstructorApp c = do
-  _constrAppParameters' <- mapM goPattern (c ^. Abstract.constrAppParameters)
+  _constrAppParameters' <- mapM goPatternArg (c ^. Abstract.constrAppParameters)
   return
     ConstructorApp
       { _constrAppConstructor = c ^. Abstract.constrAppConstructor . Abstract.constructorRefName,

src/Juvix/Translation/MicroJuvixToMiniC.hs

@@ -315,11 +315,17 @@ goFunctionClause funSig argTyps clause = do
             projCtor :: Text -> Expression
             projCtor ctorArg = functionCall (ExpressionVar (asProjName ctorArg ctorName)) [castToType ty arg]
             subConditions :: Sem r [Expression]
-            subConditions = fmap concat (zipWithM patternCondition (map projCtor ctorArgs) _constrAppParameters)
+            subConditions =
+              fmap
+                concat
+                ( zipWithM
+                    patternCondition
+                    (map projCtor ctorArgs)
+                    (_constrAppParameters ^.. each . Micro.patternArgPattern)
+                )
         fmap (isCtor :) subConditions
       Micro.PatternVariable {} -> return []
       Micro.PatternWildcard {} -> return []
-      Micro.PatternBraces b -> patternCondition arg b
 
     clauseCondition :: Sem r (Maybe Expression)
     clauseCondition = fmap (foldr1 f) . nonEmpty <$> conditions

src/Juvix/Translation/MicroJuvixToMiniC/Base.hs

@@ -174,7 +174,14 @@ typeOfConstructor name = do
   getInductiveCType (info ^. Micro.constructorInfoInductive)
 
 getClausePatterns :: Member (Reader Micro.TypesTable) r => Micro.FunctionClause -> Sem r [Micro.Pattern]
-getClausePatterns c = filterCompileTimeArgsOrPatterns (c ^. Micro.clauseName) (c ^. Micro.clausePatterns)
+getClausePatterns c =
+  filterCompileTimeArgsOrPatterns
+    (c ^. Micro.clauseName)
+    ( c
+        ^.. Micro.clausePatterns
+          . each
+          . Micro.patternArgPattern
+    )
 
 functionInfoPatternsNum :: Member (Reader Micro.TypesTable) r => Micro.FunctionInfo -> Sem r Int
 functionInfoPatternsNum fInfo = do
@@ -203,9 +210,8 @@ buildPatternInfoTable argTyps c =
         return
           [(v ^. Micro.nameText, BindingInfo {_bindingInfoExpr = exp, _bindingInfoType = typ})]
       Micro.PatternConstructorApp Micro.ConstructorApp {..} ->
-        goConstructorApp exp _constrAppConstructor _constrAppParameters
+        goConstructorApp exp _constrAppConstructor (_constrAppParameters ^.. each . Micro.patternArgPattern)
       Micro.PatternWildcard {} -> return []
-      Micro.PatternBraces b -> go (b, (exp, typ))
 
     goConstructorApp :: Expression -> Micro.Name -> [Micro.Pattern] -> Sem r [(Text, BindingInfo)]
     goConstructorApp exp constructorName ps = do

src/Juvix/Translation/MicroJuvixToMonoJuvix.hs

@@ -359,7 +359,7 @@ goFunctionDefConcrete n d = do
     goClause :: Micro.FunctionClause -> Sem r FunctionClause
     goClause c = do
       body' <- goExpression (c ^. Micro.clauseBody)
-      patterns' <- zipWithM goPattern' patternTys (c ^. Micro.clausePatterns)
+      patterns' <- zipWithM goPatternArg patternTys (c ^. Micro.clausePatterns)
       return
         FunctionClause
           { _clauseName = funName,
@@ -437,7 +437,7 @@ goFunctionDefPoly def poly
           pvars' <- mapM cloneName' pvars
           let localVarsRename :: Micro.Rename
               localVarsRename = HashMap.fromList (zipExact pvars pvars')
-              _clausePatterns = map (Micro.renamePattern localVarsRename) patsTail
+              _clausePatterns = map (Micro.renamePatternArg localVarsRename) patsTail
               _clauseBody =
                 Micro.substitutionE
                   (concreteSubsE <> Micro.renameToSubsE localVarsRename)
@@ -448,19 +448,21 @@ goFunctionDefPoly def poly
                 ..
               }
           where
-            patsTail :: [Micro.Pattern]
+            patsTail :: [Micro.PatternArg]
             patsTail = dropExact (length tyVars) (c ^. Micro.clausePatterns)
             pvars :: [Micro.VarName]
-            pvars = concatMap Micro.patternVariables patsTail
+            pvars = concatMap (^.. Micro.patternArgVariables) patsTail
         sig' :: Micro.ConcreteType
         sig' = Micro.substitutionConcrete (i ^. concreteTypeSubs) tyTail
 
-goPattern' :: forall r. Members '[Reader ConcreteTable, Reader Micro.InfoTable] r => Micro.ConcreteType -> Micro.Pattern -> Sem r Pattern
+goPatternArg :: forall r. Members '[Reader ConcreteTable, Reader Micro.InfoTable] r => Micro.ConcreteType -> Micro.PatternArg -> Sem r Pattern
-goPattern' ty = \case
+goPatternArg ty = goPattern ty . (^. Micro.patternArgPattern)
+
+goPattern :: forall r. Members '[Reader ConcreteTable, Reader Micro.InfoTable] r => Micro.ConcreteType -> Micro.Pattern -> Sem r Pattern
+goPattern ty = \case
   Micro.PatternVariable v -> return (PatternVariable (goName v))
   Micro.PatternConstructorApp capp -> PatternConstructorApp <$> goApp capp
   Micro.PatternWildcard {} -> return PatternWildcard
-  Micro.PatternBraces b -> goPattern' ty b
   where
     goApp :: Micro.ConstructorApp -> Sem r ConstructorApp
     goApp capp = case ty ^. Micro.unconcreteType of
@@ -469,7 +471,7 @@ goPattern' ty = \case
             c' = goName (capp ^. Micro.constrAppConstructor)
         cInfo <- Micro.lookupConstructor (capp ^. Micro.constrAppConstructor)
         let psTysConcrete = map Micro.mkConcreteType' (cInfo ^. Micro.constructorInfoArgs)
-        ps' <- zipWithM goPattern' psTysConcrete (capp ^. Micro.constrAppParameters)
+        ps' <- zipWithM goPatternArg psTysConcrete (capp ^. Micro.constrAppParameters)
         return (ConstructorApp c' ps')
       Micro.ExpressionApplication a -> do
         let getInductive :: Micro.Expression -> Micro.Name
@@ -493,7 +495,7 @@ goPattern' ty = \case
             subs = HashMap.fromList (zipExact tyParamVars (toList instanceTypes))
             psTysConcrete :: [Micro.ConcreteType]
             psTysConcrete = map (Micro.substitutionConcrete subs) psTys
-        ps' <- zipWithM goPattern' psTysConcrete (capp ^. Micro.constrAppParameters)
+        ps' <- zipWithM goPatternArg psTysConcrete (capp ^. Micro.constrAppParameters)
         return (ConstructorApp c' ps')
       _ -> impossible
 

src/Juvix/Translation/ScopedToAbstract.hs

@@ -174,7 +174,7 @@ goFunctionClause ::
   FunctionClause 'Scoped ->
   Sem r Abstract.FunctionClause
 goFunctionClause FunctionClause {..} = do
-  _clausePatterns' <- mapM goPattern _clausePatterns
+  _clausePatterns' <- mapM goPatternArg _clausePatterns
   _clauseBody' <- goExpression _clauseBody
   goWhereBlock _clauseWhere
   return
@@ -360,30 +360,44 @@ goPostfixPatternApplication ::
   Sem r Abstract.ConstructorApp
 goPostfixPatternApplication a = uncurry Abstract.ConstructorApp <$> viewApp (PatternPostfixApplication a)
 
-viewApp :: forall r. Pattern -> Sem r (Abstract.ConstructorRef, [Abstract.Pattern])
+viewApp :: forall r. Pattern -> Sem r (Abstract.ConstructorRef, [Abstract.PatternArg])
 viewApp = \case
   PatternConstructor c -> return (goConstructorRef c, [])
   PatternApplication (PatternApp l r) -> do
-    r' <- goPattern r
+    r' <- goPatternArg r
-    second (`snoc` r') <$> viewApp l
+    second (`snoc` r') <$> viewAppLeft l
   PatternInfixApplication (PatternInfixApp l c r) -> do
-    l' <- goPattern l
+    l' <- goPatternArg l
-    r' <- goPattern r
+    r' <- goPatternArg r
     return (goConstructorRef c, [l', r'])
   PatternPostfixApplication (PatternPostfixApp l c) -> do
-    l' <- goPattern l
+    l' <- goPatternArg l
     return (goConstructorRef c, [l'])
   PatternVariable {} -> err
   PatternWildcard {} -> err
-  PatternBraces {} -> err
   PatternEmpty {} -> err
   where
+    viewAppLeft :: PatternArg -> Sem r (Abstract.ConstructorRef, [Abstract.PatternArg])
+    viewAppLeft p
+      -- TODO proper error
+      | Implicit <- p ^. patternArgIsImplicit = error "An implicit pattern cannot be on the left of an application"
+      | otherwise = viewApp (p ^. patternArgPattern)
+    -- TODO proper error
     err :: a
     err = error "constructor expected on the left of a pattern application"
 
 goConstructorRef :: ConstructorRef -> Abstract.ConstructorRef
 goConstructorRef (ConstructorRef' n) = Abstract.ConstructorRef (goName n)
 
+goPatternArg :: PatternArg -> Sem r Abstract.PatternArg
+goPatternArg p = do
+  pat' <- goPattern (p ^. patternArgPattern)
+  return
+    Abstract.PatternArg
+      { _patternArgIsImplicit = p ^. patternArgIsImplicit,
+        _patternArgPattern = pat'
+      }
+
 goPattern :: Pattern -> Sem r Abstract.Pattern
 goPattern p = case p of
   PatternVariable a -> return $ Abstract.PatternVariable (goSymbol a)
@@ -393,7 +407,6 @@ goPattern p = case p of
   PatternPostfixApplication a -> Abstract.PatternConstructorApp <$> goPostfixPatternApplication a
   PatternWildcard i -> return (Abstract.PatternWildcard i)
   PatternEmpty -> return Abstract.PatternEmpty
-  PatternBraces b -> Abstract.PatternBraces <$> goPattern b
 
 goAxiom :: Members '[InfoTableBuilder, Error ScoperError, Builtins] r => AxiomDef 'Scoped -> Sem r Abstract.AxiomDef
 goAxiom a = do

test/Arity/Negative.hs

@@ -68,7 +68,7 @@ tests =
       "MicroJuvix"
       "ExpectedExplicitPattern.juvix"
       $ \case
-        ErrExpectedExplicitPattern {} -> Nothing
+        ErrWrongPatternIsImplicit {} -> Nothing
         _ -> wrongError,
     NegTest
       "Expected explicit argument"

test/TypeCheck/Negative.hs

@@ -84,6 +84,13 @@ tests =
       $ \case
         ErrWrongType {} -> Nothing
         _ -> wrongError,
+    NegTest
+      "Unexpected braces in pattern"
+      "issue1337"
+      "Braces.juvix"
+      $ \case
+        ErrArity (ErrWrongPatternIsImplicit {}) -> Nothing
+        _ -> wrongError,
     NegTest
       "Wrong return type name for a constructor of a simple data type"
       "MicroJuvix"

tests/negative/258/M.juvix

@@ -0,0 +1,11 @@
+module M;
+
+inductive Nat {
+  O : Nat;
+  S : Nat -> Nat;
+};
+
+fun : Nat -> Nat;
+fun (S {S {x}}) := x;
+
+end;

tests/negative/issue1337/Braces.juvix

@@ -0,0 +1,11 @@
+module Braces;
+
+inductive Nat {
+  O : Nat;
+  S : Nat -> Nat;
+};
+
+fun : Nat -> Nat;
+fun (S {S {x}}) := x;
+
+end;