Add front-end support for case expressions boolean side conditions (#2852)

- Syntax for #2804. - ⚠️ Depends on #2869. This pr introduces: 1. front-end support (parsing, printing, typechecking) for boolean side conditions for branches of case expressions. 2. Now `if` is a reserved keyword. 3. Multiway `if` is allowed to have only the `else` branch. I've also refactored the parser to be simpler. Example: ``` multiCaseBr : Nat := case 1 of | zero | if 0 < 0 := 3 | else := 4 | suc (suc n) | if 0 < 0 := 3 | else := n | suc n if 0 < 0 := 3; ``` The side if branches must satisfy the following. 1. There must be at least one `if` branch. 4. The `else` branch is optional. If present, it must be the last. Future work: 1. Translate side if conditions to Core and extend the exhaustiveness algorithm. 5. Add side if conditions to function clauses.
2024-10-03 19:47:59 +03:00 · 2024-07-04 01:16:30 +02:00 · 2024-07-04 01:16:30 +02:00 · d08bf942b6
commit d08bf942b6
parent 7c8016dbca
23 changed files with 892 additions and 179 deletions
--- a/src/Juvix/Compiler/Backend/Rust/Pretty/Keywords.hs
+++ b/src/Juvix/Compiler/Backend/Rust/Pretty/Keywords.hs
@ -6,9 +6,6 @@ import Juvix.Extra.Strings qualified as Str
 kwFn :: Doc Ann
 kwFn = keyword Str.rustFn

-kwIf :: Doc Ann
-kwIf = keyword Str.rustIf
-
 kwElse :: Doc Ann
 kwElse = keyword Str.rustElse

--- a/src/Juvix/Compiler/Backend/VampIR/Pretty/Keywords.hs
+++ b/src/Juvix/Compiler/Backend/VampIR/Pretty/Keywords.hs
@ -51,6 +51,3 @@ kwLessThan = keyword Str.vampirLessThan

 kwLessOrEqual :: Doc Ann
 kwLessOrEqual = keyword Str.vampirLessOrEqual
-
-kwIf :: Doc Ann
-kwIf = keyword Str.vampirIf
--- a/src/Juvix/Compiler/Concrete/Data/IfBranchKind.hs
+++ b/src/Juvix/Compiler/Concrete/Data/IfBranchKind.hs
@ -0,0 +1,17 @@
+module Juvix.Compiler.Concrete.Data.IfBranchKind where
+
+import Juvix.Extra.Serialize
+import Juvix.Prelude
+
+data IfBranchKind
+  = -- | Boolean condition
+    BranchIfBool
+  | -- | Default branch
+    BranchIfElse
+  deriving stock (Show, Eq, Ord, Generic)
+
+instance Serialize IfBranchKind
+
+instance NFData IfBranchKind
+
+$(genSingletons [''IfBranchKind])
--- a/src/Juvix/Compiler/Concrete/Keywords.hs
+++ b/src/Juvix/Compiler/Concrete/Keywords.hs
@ -92,6 +92,7 @@ reservedKeywords =
    kwEnd,
    kwHiding,
    kwHole,
+    kwIf,
    kwImport,
    kwIn,
    kwInductive,
--- a/src/Juvix/Compiler/Concrete/Language.hs
+++ b/src/Juvix/Compiler/Concrete/Language.hs
@ -6,6 +6,7 @@ module Juvix.Compiler.Concrete.Language
    module Juvix.Compiler.Concrete.Data.IsOpenShort,
    module Juvix.Compiler.Concrete.Data.LocalModuleOrigin,
    module Juvix.Data.IteratorInfo,
+    module Juvix.Compiler.Concrete.Data.IfBranchKind,
    module Juvix.Compiler.Concrete.Data.Name,
    module Juvix.Compiler.Concrete.Data.Stage,
    module Juvix.Compiler.Concrete.Data.NameRef,
@ -23,6 +24,7 @@ where
 import Data.Kind qualified as GHC
 import Juvix.Compiler.Backend.Markdown.Data.Types (Mk)
 import Juvix.Compiler.Concrete.Data.Builtins
+import Juvix.Compiler.Concrete.Data.IfBranchKind
 import Juvix.Compiler.Concrete.Data.IsOpenShort
 import Juvix.Compiler.Concrete.Data.Literal
 import Juvix.Compiler.Concrete.Data.LocalModuleOrigin
@ -57,6 +59,16 @@ type family FieldArgIxType s = res | res -> s where
  FieldArgIxType 'Parsed = ()
  FieldArgIxType 'Scoped = Int

+type SideIfBranchConditionType :: Stage -> IfBranchKind -> GHC.Type
+type family SideIfBranchConditionType s k = res where
+  SideIfBranchConditionType s 'BranchIfBool = ExpressionType s
+  SideIfBranchConditionType _ 'BranchIfElse = ()
+
+type IfBranchConditionType :: Stage -> IfBranchKind -> GHC.Type
+type family IfBranchConditionType s k = res where
+  IfBranchConditionType s 'BranchIfBool = ExpressionType s
+  IfBranchConditionType _ 'BranchIfElse = Irrelevant KeywordRef
+
 type ModuleIdType :: Stage -> ModuleIsTop -> GHC.Type
 type family ModuleIdType s t = res where
  ModuleIdType 'Parsed _ = ()
@ -1706,11 +1718,136 @@ deriving stock instance Ord (Let 'Parsed)

 deriving stock instance Ord (Let 'Scoped)

+data SideIfBranch (s :: Stage) (k :: IfBranchKind) = SideIfBranch
+  { _sideIfBranchPipe :: Irrelevant (Maybe KeywordRef),
+    _sideIfBranchKw :: Irrelevant KeywordRef,
+    _sideIfBranchCondition :: SideIfBranchConditionType s k,
+    _sideIfBranchAssignKw :: Irrelevant KeywordRef,
+    _sideIfBranchBody :: ExpressionType s
+  }
+  deriving stock (Generic)
+
+instance Serialize (SideIfBranch 'Scoped 'BranchIfBool)
+
+instance Serialize (SideIfBranch 'Scoped 'BranchIfElse)
+
+instance NFData (SideIfBranch 'Scoped 'BranchIfBool)
+
+instance NFData (SideIfBranch 'Scoped 'BranchIfElse)
+
+instance Serialize (SideIfBranch 'Parsed 'BranchIfBool)
+
+instance Serialize (SideIfBranch 'Parsed 'BranchIfElse)
+
+instance NFData (SideIfBranch 'Parsed 'BranchIfElse)
+
+instance NFData (SideIfBranch 'Parsed 'BranchIfBool)
+
+deriving stock instance Show (SideIfBranch 'Parsed 'BranchIfElse)
+
+deriving stock instance Show (SideIfBranch 'Parsed 'BranchIfBool)
+
+deriving stock instance Show (SideIfBranch 'Scoped 'BranchIfElse)
+
+deriving stock instance Show (SideIfBranch 'Scoped 'BranchIfBool)
+
+deriving stock instance Eq (SideIfBranch 'Parsed 'BranchIfElse)
+
+deriving stock instance Eq (SideIfBranch 'Parsed 'BranchIfBool)
+
+deriving stock instance Eq (SideIfBranch 'Scoped 'BranchIfElse)
+
+deriving stock instance Eq (SideIfBranch 'Scoped 'BranchIfBool)
+
+deriving stock instance Ord (SideIfBranch 'Parsed 'BranchIfElse)
+
+deriving stock instance Ord (SideIfBranch 'Parsed 'BranchIfBool)
+
+deriving stock instance Ord (SideIfBranch 'Scoped 'BranchIfElse)
+
+deriving stock instance Ord (SideIfBranch 'Scoped 'BranchIfBool)
+
+data SideIfs (s :: Stage) = SideIfs
+  { _sideIfBranches :: NonEmpty (SideIfBranch s 'BranchIfBool),
+    _sideIfElse :: Maybe (SideIfBranch s 'BranchIfElse)
+  }
+  deriving stock (Generic)
+
+instance Serialize (SideIfs 'Scoped)
+
+instance NFData (SideIfs 'Scoped)
+
+instance Serialize (SideIfs 'Parsed)
+
+instance NFData (SideIfs 'Parsed)
+
+deriving stock instance Show (SideIfs 'Parsed)
+
+deriving stock instance Show (SideIfs 'Scoped)
+
+deriving stock instance Eq (SideIfs 'Parsed)
+
+deriving stock instance Eq (SideIfs 'Scoped)
+
+deriving stock instance Ord (SideIfs 'Parsed)
+
+deriving stock instance Ord (SideIfs 'Scoped)
+
+data RhsExpression (s :: Stage) = RhsExpression
+  { _rhsExpressionAssignKw :: Irrelevant KeywordRef,
+    _rhsExpression :: ExpressionType s
+  }
+  deriving stock (Generic)
+
+instance Serialize (RhsExpression 'Scoped)
+
+instance NFData (RhsExpression 'Scoped)
+
+instance Serialize (RhsExpression 'Parsed)
+
+instance NFData (RhsExpression 'Parsed)
+
+deriving stock instance Show (RhsExpression 'Parsed)
+
+deriving stock instance Show (RhsExpression 'Scoped)
+
+deriving stock instance Eq (RhsExpression 'Parsed)
+
+deriving stock instance Eq (RhsExpression 'Scoped)
+
+deriving stock instance Ord (RhsExpression 'Parsed)
+
+deriving stock instance Ord (RhsExpression 'Scoped)
+
+data CaseBranchRhs (s :: Stage)
+  = CaseBranchRhsExpression (RhsExpression s)
+  | CaseBranchRhsIf (SideIfs s)
+  deriving stock (Generic)
+
+instance Serialize (CaseBranchRhs 'Scoped)
+
+instance NFData (CaseBranchRhs 'Scoped)
+
+instance Serialize (CaseBranchRhs 'Parsed)
+
+instance NFData (CaseBranchRhs 'Parsed)
+
+deriving stock instance Show (CaseBranchRhs 'Parsed)
+
+deriving stock instance Show (CaseBranchRhs 'Scoped)
+
+deriving stock instance Eq (CaseBranchRhs 'Parsed)
+
+deriving stock instance Eq (CaseBranchRhs 'Scoped)
+
+deriving stock instance Ord (CaseBranchRhs 'Parsed)
+
+deriving stock instance Ord (CaseBranchRhs 'Scoped)
+
 data CaseBranch (s :: Stage) = CaseBranch
  { _caseBranchPipe :: Irrelevant (Maybe KeywordRef),
-    _caseBranchAssignKw :: Irrelevant KeywordRef,
    _caseBranchPattern :: PatternParensType s,
-    _caseBranchExpression :: ExpressionType s
+    _caseBranchRhs :: CaseBranchRhs s
  }
  deriving stock (Generic)

@ -1818,66 +1955,58 @@ deriving stock instance Ord (NewCase 'Parsed)

 deriving stock instance Ord (NewCase 'Scoped)

-data IfBranch (s :: Stage) = IfBranch
+data IfBranch (s :: Stage) (k :: IfBranchKind) = IfBranch
  { _ifBranchPipe :: Irrelevant KeywordRef,
    _ifBranchAssignKw :: Irrelevant KeywordRef,
-    _ifBranchCondition :: ExpressionType s,
+    _ifBranchCondition :: IfBranchConditionType s k,
    _ifBranchExpression :: ExpressionType s
  }
  deriving stock (Generic)

-instance Serialize (IfBranch 'Scoped)
+instance Serialize (IfBranch 'Scoped 'BranchIfBool)

-instance NFData (IfBranch 'Scoped)
+instance Serialize (IfBranch 'Scoped 'BranchIfElse)

-instance Serialize (IfBranch 'Parsed)
+instance NFData (IfBranch 'Scoped 'BranchIfBool)

-instance NFData (IfBranch 'Parsed)
+instance NFData (IfBranch 'Scoped 'BranchIfElse)

-deriving stock instance Show (IfBranch 'Parsed)
+instance Serialize (IfBranch 'Parsed 'BranchIfBool)

-deriving stock instance Show (IfBranch 'Scoped)
+instance Serialize (IfBranch 'Parsed 'BranchIfElse)

-deriving stock instance Eq (IfBranch 'Parsed)
+instance NFData (IfBranch 'Parsed 'BranchIfElse)

-deriving stock instance Eq (IfBranch 'Scoped)
+instance NFData (IfBranch 'Parsed 'BranchIfBool)

-deriving stock instance Ord (IfBranch 'Parsed)
+deriving stock instance Show (IfBranch 'Parsed 'BranchIfElse)

-deriving stock instance Ord (IfBranch 'Scoped)
+deriving stock instance Show (IfBranch 'Parsed 'BranchIfBool)

-data IfBranchElse (s :: Stage) = IfBranchElse
-  { _ifBranchElsePipe :: Irrelevant KeywordRef,
-    _ifBranchElseAssignKw :: Irrelevant KeywordRef,
-    _ifBranchElseKw :: Irrelevant KeywordRef,
-    _ifBranchElseExpression :: ExpressionType s
-  }
-  deriving stock (Generic)
+deriving stock instance Show (IfBranch 'Scoped 'BranchIfElse)

-instance Serialize (IfBranchElse 'Scoped)
+deriving stock instance Show (IfBranch 'Scoped 'BranchIfBool)

-instance NFData (IfBranchElse 'Scoped)
+deriving stock instance Eq (IfBranch 'Parsed 'BranchIfElse)

-instance Serialize (IfBranchElse 'Parsed)
+deriving stock instance Eq (IfBranch 'Parsed 'BranchIfBool)

-instance NFData (IfBranchElse 'Parsed)
+deriving stock instance Eq (IfBranch 'Scoped 'BranchIfElse)

-deriving stock instance Show (IfBranchElse 'Parsed)
+deriving stock instance Eq (IfBranch 'Scoped 'BranchIfBool)

-deriving stock instance Show (IfBranchElse 'Scoped)
+deriving stock instance Ord (IfBranch 'Parsed 'BranchIfElse)

-deriving stock instance Eq (IfBranchElse 'Parsed)
+deriving stock instance Ord (IfBranch 'Parsed 'BranchIfBool)

-deriving stock instance Eq (IfBranchElse 'Scoped)
+deriving stock instance Ord (IfBranch 'Scoped 'BranchIfElse)

-deriving stock instance Ord (IfBranchElse 'Parsed)
-
-deriving stock instance Ord (IfBranchElse 'Scoped)
+deriving stock instance Ord (IfBranch 'Scoped 'BranchIfBool)

 data If (s :: Stage) = If
  { _ifKw :: KeywordRef,
-    _ifBranches :: NonEmpty (IfBranch s),
-    _ifBranchElse :: IfBranchElse s
+    _ifBranches :: [IfBranch s 'BranchIfBool],
+    _ifBranchElse :: IfBranch s 'BranchIfElse
  }
  deriving stock (Generic)

@ -2468,6 +2597,9 @@ deriving stock instance Ord (JudocAtom 'Parsed)

 deriving stock instance Ord (JudocAtom 'Scoped)

+makeLenses ''SideIfs
+makeLenses ''SideIfBranch
+makeLenses ''RhsExpression
 makeLenses ''PatternArg
 makeLenses ''WildcardConstructor
 makeLenses ''DoubleBracesExpression
@ -2526,7 +2658,6 @@ makeLenses ''Case
 makeLenses ''CaseBranch
 makeLenses ''If
 makeLenses ''IfBranch
-makeLenses ''IfBranchElse
 makeLenses ''PatternBinding
 makeLenses ''PatternAtoms
 makeLenses ''ExpressionAtoms
@ -2732,20 +2863,37 @@ instance HasLoc (Function 'Scoped) where
 instance HasLoc (Let 'Scoped) where
  getLoc l = getLoc (l ^. letKw) <> getLoc (l ^. letExpression)

+instance (SingI s) => HasLoc (SideIfBranch s k) where
+  getLoc SideIfBranch {..} =
+    (getLoc <$> _sideIfBranchPipe ^. unIrrelevant)
+      ?<> getLocExpressionType _sideIfBranchBody
+
+instance (SingI s) => HasLoc (SideIfs s) where
+  getLoc SideIfs {..} =
+    getLocSpan _sideIfBranches
+      <>? (getLoc <$> _sideIfElse)
+
+instance (SingI s) => HasLoc (RhsExpression s) where
+  getLoc RhsExpression {..} =
+    getLoc _rhsExpressionAssignKw
+      <> getLocExpressionType _rhsExpression
+
+instance (SingI s) => HasLoc (CaseBranchRhs s) where
+  getLoc = \case
+    CaseBranchRhsExpression e -> getLoc e
+    CaseBranchRhsIf e -> getLoc e
+
 instance (SingI s) => HasLoc (CaseBranch s) where
  getLoc c = case c ^. caseBranchPipe . unIrrelevant of
    Nothing -> branchLoc
    Just p -> getLoc p <> branchLoc
    where
      branchLoc :: Interval
-      branchLoc = getLocExpressionType (c ^. caseBranchExpression)
+      branchLoc = getLoc (c ^. caseBranchRhs)

-instance (SingI s) => HasLoc (IfBranch s) where
+instance (SingI s) => HasLoc (IfBranch s k) where
  getLoc c = getLoc (c ^. ifBranchPipe) <> getLocExpressionType (c ^. ifBranchExpression)

-instance (SingI s) => HasLoc (IfBranchElse s) where
-  getLoc c = getLoc (c ^. ifBranchElsePipe) <> getLocExpressionType (c ^. ifBranchElseExpression)
-
 instance (SingI s) => HasLoc (Case s) where
  getLoc c = getLoc (c ^. caseKw) <> getLoc (c ^. caseBranches . to last)

--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@ -13,6 +13,8 @@ import Data.Map qualified as Map
 import Juvix.Compiler.Concrete.Data.Scope.Base
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Extra qualified as Concrete
+import Juvix.Compiler.Concrete.Gen qualified as Gen
+import Juvix.Compiler.Concrete.Keywords
 import Juvix.Compiler.Concrete.Keywords qualified as Kw
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Pretty.Options
@ -538,11 +540,52 @@ ppLet isTop Let {..} = do
      letExpression' = ppMaybeTopExpression isTop _letExpression
  align $ ppCode _letKw <> letFunDefs' <> ppCode _letInKw <+> letExpression'

+instance (SingI s, SingI k) => PrettyPrint (SideIfBranch s k) where
+  ppCode SideIfBranch {..} = do
+    let kwPipe' = ppCode <$> _sideIfBranchPipe ^. unIrrelevant
+        kwIfElse' = ppCode _sideIfBranchKw
+        kwAssign' = ppCode _sideIfBranchAssignKw
+        condition' = case sing :: SIfBranchKind k of
+          SBranchIfBool -> Just (ppExpressionType _sideIfBranchCondition)
+          SBranchIfElse -> Nothing
+        body' = ppExpressionType _sideIfBranchBody
+    kwPipe'
+      <?+> ( kwIfElse'
+               <+?> condition'
+               <+> kwAssign'
+                 <> oneLineOrNext body'
+           )
+
+instance (SingI s) => PrettyPrint (SideIfs s) where
+  ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => SideIfs s -> Sem r ()
+  ppCode SideIfs {..} =
+    case (_sideIfBranches, _sideIfElse) of
+      (b :| [], Nothing) -> ppCode (set sideIfBranchPipe (Irrelevant Nothing) b)
+      (b :| bs, _) -> do
+        let putPipe :: Maybe KeywordRef -> Maybe KeywordRef
+            putPipe = \case
+              Nothing -> Just (run (runReader (getLoc b) (Gen.kw kwPipe)))
+              Just p -> Just p
+            firstBr = over (sideIfBranchPipe . unIrrelevant) putPipe b
+            ifbranches = map ppCode (toList (firstBr : bs))
+            allBranches :: [Sem r ()] = snocMaybe ifbranches (ppCode <$> _sideIfElse)
+        line <> indent (vsepHard allBranches)
+
+ppCaseBranchRhs :: forall r s. (Members '[ExactPrint, Reader Options] r, SingI s) => IsTop -> CaseBranchRhs s -> Sem r ()
+ppCaseBranchRhs isTop = \case
+  CaseBranchRhsExpression e -> ppExpressionRhs isTop e
+  CaseBranchRhsIf ifCond -> ppCode ifCond
+
+ppExpressionRhs :: (Member (Reader Options) r, Member ExactPrint r, SingI s) => IsTop -> RhsExpression s -> Sem r ()
+ppExpressionRhs isTop RhsExpression {..} = do
+  let expr' = ppMaybeTopExpression isTop _rhsExpression
+  ppCode _rhsExpressionAssignKw <> oneLineOrNext expr'
+
 ppCaseBranch :: forall r s. (Members '[ExactPrint, Reader Options] r, SingI s) => IsTop -> CaseBranch s -> Sem r ()
 ppCaseBranch isTop CaseBranch {..} = do
  let pat' = ppPatternParensType _caseBranchPattern
-      e' = ppMaybeTopExpression isTop _caseBranchExpression
-  pat' <+> ppCode _caseBranchAssignKw <> oneLineOrNext e'
+      rhs' = ppCaseBranchRhs isTop _caseBranchRhs
+  pat' <+> rhs'

 ppCase :: forall r s. (Members '[ExactPrint, Reader Options] r, SingI s) => IsTop -> Case s -> Sem r ()
 ppCase isTop Case {..} = do
@ -573,32 +616,37 @@ ppCase isTop Case {..} = do
              Just p -> ppCode p
              Nothing -> ppCode Kw.kwPipe

-instance (SingI s) => PrettyPrint (IfBranch s) where
+instance (SingI s) => PrettyPrint (IfBranch s 'BranchIfBool) where
  ppCode IfBranch {..} = do
-    let cond' = ppExpressionType _ifBranchCondition
+    let pipe' = ppCode _ifBranchPipe
+        cond' = ppExpressionType _ifBranchCondition
        e' = ppExpressionType _ifBranchExpression
-    cond' <+> ppCode _ifBranchAssignKw <> oneLineOrNext e'
+    pipe' <+> cond' <+> ppCode _ifBranchAssignKw <> oneLineOrNext e'

-ppIfBranchElse :: forall r s. (Members '[ExactPrint, Reader Options] r, SingI s) => IsTop -> IfBranchElse s -> Sem r ()
-ppIfBranchElse isTop IfBranchElse {..} = do
-  let e' = ppMaybeTopExpression isTop _ifBranchElseExpression
-  ppCode _ifBranchElseKw <+> ppCode _ifBranchElseAssignKw <> oneLineOrNext e'
+ppIfBranchElse ::
+  forall r s.
+  (Members '[ExactPrint, Reader Options] r, SingI s) =>
+  IsTop ->
+  IfBranch s 'BranchIfElse ->
+  Sem r ()
+ppIfBranchElse isTop IfBranch {..} = do
+  let e' = ppMaybeTopExpression isTop _ifBranchExpression
+  ppCode _ifBranchCondition <+> ppCode _ifBranchAssignKw <> oneLineOrNext e'

 ppIf :: forall r s. (Members '[ExactPrint, Reader Options] r, SingI s) => IsTop -> If s -> Sem r ()
 ppIf isTop If {..} = do
-  ppCode _ifKw <+> hardline <> indent (vsepHard (ppIfBranch <$> _ifBranches) <> hardline <> ppIfBranchElse' _ifBranchElse)
+  ppCode _ifKw
+    <+> hardline
+      <> indent
+        ( vsepHard (ppIfBranch <$> _ifBranches)
+            <> hardline
+            <> ppIfBranch _ifBranchElse
+        )
  where
-    ppIfBranch :: IfBranch s -> Sem r ()
-    ppIfBranch b = pipeHelper <+> ppCode b
-      where
-        pipeHelper :: Sem r ()
-        pipeHelper = ppCode (b ^. ifBranchPipe . unIrrelevant)
-
-    ppIfBranchElse' :: IfBranchElse s -> Sem r ()
-    ppIfBranchElse' b = pipeHelper <+> ppIfBranchElse isTop b
-      where
-        pipeHelper :: Sem r ()
-        pipeHelper = ppCode (b ^. ifBranchElsePipe . unIrrelevant)
+    ppIfBranch :: forall k. (SingI k) => IfBranch s k -> Sem r ()
+    ppIfBranch b = case sing :: SIfBranchKind k of
+      SBranchIfBool -> ppCode b
+      SBranchIfElse -> ppIfBranchElse isTop b

 instance PrettyPrint Universe where
  ppCode Universe {..} = ppCode _universeKw <+?> (noLoc . pretty <$> _universeLevel)
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@ -2189,6 +2189,98 @@ checkLet Let {..} =
          _letInKw
        }

+checkRhsExpression ::
+  forall r.
+  ( Members
+      '[ HighlightBuilder,
+         Reader ScopeParameters,
+         Error ScoperError,
+         State Scope,
+         State ScoperState,
+         InfoTableBuilder,
+         Reader InfoTable,
+         NameIdGen,
+         Reader Package
+       ]
+      r
+  ) =>
+  RhsExpression 'Parsed ->
+  Sem r (RhsExpression 'Scoped)
+checkRhsExpression RhsExpression {..} = do
+  expr' <- checkParseExpressionAtoms _rhsExpression
+  return
+    RhsExpression
+      { _rhsExpression = expr',
+        _rhsExpressionAssignKw
+      }
+
+checkSideIfBranch ::
+  forall r (k :: IfBranchKind).
+  ( SingI k,
+    Members
+      '[ HighlightBuilder,
+         Reader ScopeParameters,
+         Error ScoperError,
+         State Scope,
+         State ScoperState,
+         InfoTableBuilder,
+         Reader InfoTable,
+         NameIdGen,
+         Reader Package
+       ]
+      r
+  ) =>
+  SideIfBranch 'Parsed k ->
+  Sem r (SideIfBranch 'Scoped k)
+checkSideIfBranch SideIfBranch {..} = do
+  cond' <- case sing :: SIfBranchKind k of
+    SBranchIfBool -> checkParseExpressionAtoms _sideIfBranchCondition
+    SBranchIfElse -> return _sideIfBranchCondition
+  body' <- checkParseExpressionAtoms _sideIfBranchBody
+  return
+    SideIfBranch
+      { _sideIfBranchBody = body',
+        _sideIfBranchCondition = cond',
+        _sideIfBranchPipe,
+        _sideIfBranchKw,
+        _sideIfBranchAssignKw
+      }
+
+checkSideIfs ::
+  forall r.
+  ( Members
+      '[ HighlightBuilder,
+         Reader ScopeParameters,
+         Error ScoperError,
+         State Scope,
+         State ScoperState,
+         InfoTableBuilder,
+         Reader InfoTable,
+         NameIdGen,
+         Reader Package
+       ]
+      r
+  ) =>
+  SideIfs 'Parsed ->
+  Sem r (SideIfs 'Scoped)
+checkSideIfs SideIfs {..} = do
+  branches' <- mapM checkSideIfBranch _sideIfBranches
+  else' <- mapM checkSideIfBranch _sideIfElse
+  return
+    SideIfs
+      { _sideIfBranches = branches',
+        _sideIfElse = else'
+      }
+
+checkCaseBranchRhs ::
+  forall r.
+  (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) =>
+  CaseBranchRhs 'Parsed ->
+  Sem r (CaseBranchRhs 'Scoped)
+checkCaseBranchRhs = \case
+  CaseBranchRhsExpression r -> CaseBranchRhsExpression <$> checkRhsExpression r
+  CaseBranchRhsIf r -> CaseBranchRhsIf <$> checkSideIfs r
+
 checkCaseBranch ::
  forall r.
  (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) =>
@ -2196,11 +2288,11 @@ checkCaseBranch ::
  Sem r (CaseBranch 'Scoped)
 checkCaseBranch CaseBranch {..} = withLocalScope $ do
  pattern' <- checkParsePatternAtoms _caseBranchPattern
-  expression' <- (checkParseExpressionAtoms _caseBranchExpression)
+  rhs' <- checkCaseBranchRhs _caseBranchRhs
  return $
    CaseBranch
      { _caseBranchPattern = pattern',
-        _caseBranchExpression = expression',
+        _caseBranchRhs = rhs',
        ..
      }

@ -2220,12 +2312,14 @@ checkCase Case {..} = do
      }

 checkIfBranch ::
-  forall r.
-  (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) =>
-  IfBranch 'Parsed ->
-  Sem r (IfBranch 'Scoped)
+  forall r k.
+  (SingI k, Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) =>
+  IfBranch 'Parsed k ->
+  Sem r (IfBranch 'Scoped k)
 checkIfBranch IfBranch {..} = withLocalScope $ do
-  cond' <- checkParseExpressionAtoms _ifBranchCondition
+  cond' <- case sing :: SIfBranchKind k of
+    SBranchIfBool -> checkParseExpressionAtoms _ifBranchCondition
+    SBranchIfElse -> return _ifBranchCondition
  expression' <- checkParseExpressionAtoms _ifBranchExpression
  return $
    IfBranch
@ -2234,26 +2328,13 @@ checkIfBranch IfBranch {..} = withLocalScope $ do
        ..
      }

-checkIfBranchElse ::
-  forall r.
-  (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) =>
-  IfBranchElse 'Parsed ->
-  Sem r (IfBranchElse 'Scoped)
-checkIfBranchElse IfBranchElse {..} = withLocalScope $ do
-  expression' <- checkParseExpressionAtoms _ifBranchElseExpression
-  return $
-    IfBranchElse
-      { _ifBranchElseExpression = expression',
-        ..
-      }
-
 checkIf ::
  (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) =>
  If 'Parsed ->
  Sem r (If 'Scoped)
 checkIf If {..} = do
  ifBranches' <- mapM checkIfBranch _ifBranches
-  ifBranchElse' <- checkIfBranchElse _ifBranchElse
+  ifBranchElse' <- checkIfBranch _ifBranchElse
  return $
    If
      { _ifBranchElse = ifBranchElse',
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@ -825,7 +825,7 @@ expressionAtom =
      <|> AtomNamedApplicationNew <$> namedApplicationNew
      <|> AtomNamedApplication <$> namedApplication
      <|> AtomList <$> parseList
-      <|> either AtomIf AtomIdentifier <$> multiwayIf
+      <|> AtomIf <$> multiwayIf
      <|> AtomIdentifier <$> name
      <|> AtomUniverse <$> universe
      <|> AtomLambda <$> lambda
@ -1112,11 +1112,63 @@ letBlock = do
  _letExpression <- parseExpressionAtoms
  return Let {..}

+-- | The pipe for the first branch is optional
+sideIfBranch ::
+  forall r k.
+  (SingI k, Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  Bool ->
+  ParsecS r (SideIfBranch 'Parsed k)
+sideIfBranch isFirst = do
+  let ifElseKw =
+        Irrelevant <$> case sing :: SIfBranchKind k of
+          SBranchIfBool -> kw kwIf
+          SBranchIfElse -> kw kwElse
+  (_sideIfBranchPipe, _sideIfBranchKw) <- P.try $ do
+    let opt
+          | isFirst = optional
+          | otherwise = fmap Just
+    pipe' <- Irrelevant <$> opt (kw kwPipe)
+    condKw' <- ifElseKw
+    return (pipe', condKw')
+  _sideIfBranchCondition <- case sing :: SIfBranchKind k of
+    SBranchIfBool -> parseExpressionAtoms
+    SBranchIfElse -> return ()
+  _sideIfBranchAssignKw <- Irrelevant <$> kw kwAssign
+  _sideIfBranchBody <- parseExpressionAtoms
+  return SideIfBranch {..}
+
+sideIfs :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (SideIfs 'Parsed)
+sideIfs = do
+  fstBranch <- sideIfBranch True
+  moreBranches <- many (sideIfBranch False)
+  let _sideIfBranches = fstBranch :| moreBranches
+  _sideIfElse <- optional (sideIfBranch False)
+  return
+    SideIfs
+      { ..
+      }
+
+prhsExpression :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (RhsExpression 'Parsed)
+prhsExpression = do
+  _rhsExpressionAssignKw <- Irrelevant <$> kw kwAssign
+  _rhsExpression <- parseExpressionAtoms
+  return RhsExpression {..}
+
+pcaseBranchRhs :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (CaseBranchRhs 'Parsed)
+pcaseBranchRhs =
+  CaseBranchRhsExpression <$> pcaseBranchRhsExpression
+    <|> CaseBranchRhsIf <$> sideIfs
+
+pcaseBranchRhsExpression :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (RhsExpression 'Parsed)
+pcaseBranchRhsExpression = do
+  _rhsExpressionAssignKw <- Irrelevant <$> kw kwAssign
+  _rhsExpression <- parseExpressionAtoms
+  return RhsExpression {..}
+
 caseBranch :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => Irrelevant (Maybe KeywordRef) -> ParsecS r (CaseBranch 'Parsed)
 caseBranch _caseBranchPipe = do
  _caseBranchPattern <- parsePatternAtoms
-  _caseBranchAssignKw <- Irrelevant <$> kw kwAssign
-  _caseBranchExpression <- parseExpressionAtoms
+  _caseBranchRhs <- pcaseBranchRhs
  return CaseBranch {..}

 case_ :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (Case 'Parsed)
@ -1127,43 +1179,30 @@ case_ = P.label "case" $ do
  _caseBranches <- braces (pipeSep1 caseBranch) <|> pipeSep1 caseBranch
  return Case {..}

-ifBranch' :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => Irrelevant KeywordRef -> ParsecS r (IfBranch 'Parsed)
-ifBranch' _ifBranchPipe = do
-  _ifBranchCondition <- parseExpressionAtoms
+ifBranch ::
+  forall r k.
+  (SingI k, Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  ParsecS r (IfBranch 'Parsed k)
+ifBranch = do
+  _ifBranchPipe <- Irrelevant <$> pipeHelper
+  _ifBranchCondition <- case sing :: SIfBranchKind k of
+    SBranchIfBool -> parseExpressionAtoms
+    SBranchIfElse -> Irrelevant <$> kw kwElse
  _ifBranchAssignKw <- Irrelevant <$> kw kwAssign
  _ifBranchExpression <- parseExpressionAtoms
  return IfBranch {..}
+  where
+    pipeHelper :: ParsecS r KeywordRef
+    pipeHelper = case sing :: SIfBranchKind k of
+      SBranchIfBool -> P.try (kw kwPipe <* P.notFollowedBy (kw kwElse))
+      SBranchIfElse -> kw kwPipe

-parseIfBranchElse' :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => Irrelevant KeywordRef -> ParsecS r (IfBranchElse 'Parsed)
-parseIfBranchElse' _ifBranchElsePipe = do
-  _ifBranchElseKw <- Irrelevant <$> kw kwElse
-  _ifBranchElseAssignKw <- Irrelevant <$> kw kwAssign
-  _ifBranchElseExpression <- parseExpressionAtoms
-  return IfBranchElse {..}
-
-multiwayIf' :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => KeywordRef -> [IfBranch 'Parsed] -> ParsecS r (If 'Parsed)
-multiwayIf' _ifKw brs = do
-  pipeKw <- Irrelevant <$> kw kwPipe
-  multiwayIfBranchElse' _ifKw pipeKw brs <|> multiwayIfBranch' _ifKw pipeKw brs
-
-multiwayIfBranch' :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => KeywordRef -> Irrelevant KeywordRef -> [IfBranch 'Parsed] -> ParsecS r (If 'Parsed)
-multiwayIfBranch' _ifKw pipeKw brs = do
-  br <- ifBranch' pipeKw
-  multiwayIf' _ifKw (br : brs)
-
-multiwayIfBranchElse' :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => KeywordRef -> Irrelevant KeywordRef -> [IfBranch 'Parsed] -> ParsecS r (If 'Parsed)
-multiwayIfBranchElse' _ifKw pipeKw brs = do
-  off <- P.getOffset
-  _ifBranchElse <- parseIfBranchElse' pipeKw
-  case nonEmpty (reverse brs) of
-    Nothing -> parseFailure off "A multiway if must have at least one condition branch"
-    Just _ifBranches -> return If {..}
-
-multiwayIf :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (Either (If 'Parsed) Name)
+multiwayIf :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (If 'Parsed)
 multiwayIf = do
  _ifKw <- kw kwIf
-  (Left <$> multiwayIf' _ifKw [])
-    <|> return (Right $ NameUnqualified $ WithLoc (getLoc _ifKw) (_ifKw ^. keywordRefKeyword . keywordAscii))
+  _ifBranches <- many ifBranch
+  _ifBranchElse <- ifBranch
+  return If {..}

 --------------------------------------------------------------------------------
 -- Universe expression
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@ -777,9 +777,6 @@ kwMatch = keyword Str.match_
 kwWith :: Doc Ann
 kwWith = keyword Str.with_

-kwIf :: Doc Ann
-kwIf = keyword Str.if_
-
 kwThen :: Doc Ann
 kwThen = keyword Str.then_

--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@ -467,7 +467,7 @@ mkBody ppLam ty loc clauses
            <> (ppLam ^. withLocParam)

    goClause :: Level -> [Internal.PatternArg] -> Internal.Expression -> Sem r MatchBranch
-    goClause lvl pats body = goPatternArgs lvl body pats ptys
+    goClause lvl pats body = goPatternArgs lvl (Internal.CaseBranchRhsExpression body) pats ptys
      where
        ptys :: [Type]
        ptys = take (length pats) (typeArgs ty)
@ -498,13 +498,31 @@ goCase c = do
              body <-
                local
                  (set indexTableVars vars')
-                  (underBinders 1 (goExpression _caseBranchExpression))
+                  (underBinders 1 (goCaseBranchRhs _caseBranchRhs))
              return $ mkLet i (Binder (name ^. nameText) (Just $ name ^. nameLoc) ty) expr body
            _ ->
              impossible
  where
    goCaseBranch :: Type -> Internal.CaseBranch -> Sem r MatchBranch
-    goCaseBranch ty b = goPatternArgs 0 (b ^. Internal.caseBranchExpression) [b ^. Internal.caseBranchPattern] [ty]
+    goCaseBranch ty b = goPatternArgs 0 (b ^. Internal.caseBranchRhs) [b ^. Internal.caseBranchPattern] [ty]
+
+-- | FIXME Fix this as soon as side if conditions are implemented in Core. This
+-- is needed so that we can test typechecking without a crash.
+todoSideIfs ::
+  forall r.
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen, Error BadScope] r) =>
+  Internal.SideIfs ->
+  Sem r Node
+todoSideIfs s = goExpression (s ^. Internal.sideIfBranches . _head1 . Internal.sideIfBranchBody)
+
+goCaseBranchRhs ::
+  forall r.
+  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen, Error BadScope] r) =>
+  Internal.CaseBranchRhs ->
+  Sem r Node
+goCaseBranchRhs = \case
+  Internal.CaseBranchRhsExpression e -> goExpression e
+  Internal.CaseBranchRhsIf i -> todoSideIfs i

 goLambda ::
  forall r.
@ -932,7 +950,7 @@ goPatternArgs ::
  forall r.
  (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen, Error BadScope] r) =>
  Level -> -- the level of the first binder for the matched value
-  Internal.Expression ->
+  Internal.CaseBranchRhs ->
  [Internal.PatternArg] ->
  [Type] -> -- types of the patterns
  Sem r MatchBranch
@ -960,7 +978,7 @@ goPatternArgs lvl0 body = go lvl0 []
          _ ->
            impossible
      ([], []) -> do
-        body' <- goExpression body
+        body' <- goCaseBranchRhs body
        return $ MatchBranch Info.empty (nonEmpty' (reverse pats)) body'
      _ ->
        impossible
--- a/src/Juvix/Compiler/Internal/Extra/Base.hs
+++ b/src/Juvix/Compiler/Internal/Extra/Base.hs
@ -90,10 +90,27 @@ instance HasExpressions Pattern where
    PatternConstructorApp a -> PatternConstructorApp <$> leafExpressions f a
    PatternWildcardConstructor {} -> pure p

+instance HasExpressions SideIfBranch where
+  leafExpressions f b = do
+    _sideIfBranchCondition <- leafExpressions f (b ^. sideIfBranchCondition)
+    _sideIfBranchBody <- leafExpressions f (b ^. sideIfBranchBody)
+    pure SideIfBranch {..}
+
+instance HasExpressions SideIfs where
+  leafExpressions f b = do
+    _sideIfBranches <- traverse (leafExpressions f) (b ^. sideIfBranches)
+    _sideIfElse <- traverse (leafExpressions f) (b ^. sideIfElse)
+    pure SideIfs {..}
+
+instance HasExpressions CaseBranchRhs where
+  leafExpressions f = \case
+    CaseBranchRhsExpression e -> CaseBranchRhsExpression <$> leafExpressions f e
+    CaseBranchRhsIf e -> CaseBranchRhsIf <$> leafExpressions f e
+
 instance HasExpressions CaseBranch where
  leafExpressions f b = do
    _caseBranchPattern <- leafExpressions f (b ^. caseBranchPattern)
-    _caseBranchExpression <- leafExpressions f (b ^. caseBranchExpression)
+    _caseBranchRhs <- leafExpressions f (b ^. caseBranchRhs)
    pure CaseBranch {..}

 instance HasExpressions Case where
--- a/src/Juvix/Compiler/Internal/Extra/Clonable.hs
+++ b/src/Juvix/Compiler/Internal/Extra/Clonable.hs
@ -107,14 +107,39 @@ underBinders ps f = do
          modify' @FreshBindersContext (set (at (v ^. nameId)) (Just uid'))
          return (set nameId uid' v)

+instance Clonable SideIfBranch where
+  freshNameIds SideIfBranch {..} = do
+    cond' <- freshNameIds _sideIfBranchCondition
+    body' <- freshNameIds _sideIfBranchBody
+    return
+      SideIfBranch
+        { _sideIfBranchCondition = cond',
+          _sideIfBranchBody = body'
+        }
+
+instance Clonable SideIfs where
+  freshNameIds SideIfs {..} = do
+    branches' <- mapM freshNameIds _sideIfBranches
+    else' <- mapM freshNameIds _sideIfElse
+    return
+      SideIfs
+        { _sideIfBranches = branches',
+          _sideIfElse = else'
+        }
+
+instance Clonable CaseBranchRhs where
+  freshNameIds = \case
+    CaseBranchRhsExpression e -> CaseBranchRhsExpression <$> freshNameIds e
+    CaseBranchRhsIf e -> CaseBranchRhsIf <$> freshNameIds e
+
 instance Clonable CaseBranch where
  freshNameIds CaseBranch {..} =
    underBinder _caseBranchPattern $ \pat' -> do
-      body' <- freshNameIds _caseBranchExpression
+      body' <- freshNameIds _caseBranchRhs
      return
        CaseBranch
          { _caseBranchPattern = pat',
-            _caseBranchExpression = body'
+            _caseBranchRhs = body'
          }

 instance Clonable Case where
--- a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
+++ b/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
@ -259,10 +259,10 @@ goExpression p e = case e of
  ExpressionUniverse {} -> return ()
  ExpressionFunction f -> do
    goFunctionParameter p (f ^. functionLeft)
-    goExpression p (f ^. functionRight)
+    goExpression_ (f ^. functionRight)
  ExpressionApplication (Application l r _) -> do
-    goExpression p l
-    goExpression p r
+    goExpression_ l
+    goExpression_ r
  ExpressionLiteral {} -> return ()
  ExpressionCase c -> goCase c
  ExpressionHole {} -> return ()
@ -271,6 +271,9 @@ goExpression p e = case e of
  ExpressionLet l -> goLet l
  ExpressionSimpleLambda l -> goSimpleLambda l
  where
+    goExpression_ :: Expression -> Sem r ()
+    goExpression_ = goExpression p
+
    goSimpleLambda :: SimpleLambda -> Sem r ()
    goSimpleLambda l = do
      addEdgeMay p (l ^. slambdaBinder . sbinderVar)
@ -280,21 +283,36 @@ goExpression p e = case e of
      where
        goClause :: LambdaClause -> Sem r ()
        goClause (LambdaClause {..}) = do
-          goExpression p _lambdaBody
+          goExpression_ _lambdaBody
          mapM_ (goPattern p) _lambdaPatterns

    goCase :: Case -> Sem r ()
    goCase c = do
-      goExpression p (c ^. caseExpression)
+      goExpression_ (c ^. caseExpression)
      mapM_ goBranch (c ^. caseBranches)

    goBranch :: CaseBranch -> Sem r ()
-    goBranch = goExpression p . (^. caseBranchExpression)
+    goBranch = goCaseBranchRhs . (^. caseBranchRhs)
+
+    goSideIfBranch :: SideIfBranch -> Sem r ()
+    goSideIfBranch SideIfBranch {..} = do
+      goExpression_ _sideIfBranchCondition
+      goExpression_ _sideIfBranchBody
+
+    goSideIfs :: SideIfs -> Sem r ()
+    goSideIfs SideIfs {..} = do
+      mapM_ goSideIfBranch _sideIfBranches
+      mapM_ goExpression_ _sideIfElse
+
+    goCaseBranchRhs :: CaseBranchRhs -> Sem r ()
+    goCaseBranchRhs = \case
+      CaseBranchRhsExpression expr -> goExpression_ expr
+      CaseBranchRhsIf s -> goSideIfs s

    goLet :: Let -> Sem r ()
    goLet l = do
      mapM_ goLetClause (l ^. letClauses)
-      goExpression p (l ^. letExpression)
+      goExpression_ (l ^. letExpression)

    goLetClause :: LetClause -> Sem r ()
    goLetClause = \case
--- a/src/Juvix/Compiler/Internal/Extra/HasLetDefs.hs
+++ b/src/Juvix/Compiler/Internal/Extra/HasLetDefs.hs
@ -5,8 +5,9 @@ import Juvix.Prelude

 class HasLetDefs a where
  letDefs' :: [Let] -> a -> [Let]
-  letDefs :: a -> [Let]
-  letDefs = letDefs' []
+
+letDefs :: (HasLetDefs a) => a -> [Let]
+letDefs = letDefs' []

 instance (HasLetDefs a, Foldable f) => HasLetDefs (f a) where
  letDefs' = foldl' letDefs'
@ -69,8 +70,19 @@ instance HasLetDefs ConstructorApp where
 instance HasLetDefs Case where
  letDefs' acc Case {..} = letDefs' (letDefs' acc _caseExpression) _caseBranches

+instance HasLetDefs SideIfs where
+  letDefs' acc SideIfs {..} = letDefs' (letDefs' acc _sideIfBranches) _sideIfElse
+
+instance HasLetDefs CaseBranchRhs where
+  letDefs' acc = \case
+    CaseBranchRhsExpression e -> letDefs' acc e
+    CaseBranchRhsIf e -> letDefs' acc e
+
+instance HasLetDefs SideIfBranch where
+  letDefs' acc SideIfBranch {..} = letDefs' (letDefs' acc _sideIfBranchCondition) _sideIfBranchBody
+
 instance HasLetDefs CaseBranch where
-  letDefs' acc CaseBranch {..} = letDefs' acc _caseBranchExpression
+  letDefs' acc CaseBranch {..} = letDefs' acc _caseBranchRhs

 instance HasLetDefs MutualBlockLet where
  letDefs' acc MutualBlockLet {..} = letDefs' acc _mutualLet
--- a/src/Juvix/Compiler/Internal/Language.hs
+++ b/src/Juvix/Compiler/Internal/Language.hs
@ -219,9 +219,44 @@ instance Serialize SimpleLambda

 instance NFData SimpleLambda

+data SideIfBranch = SideIfBranch
+  { _sideIfBranchCondition :: Expression,
+    _sideIfBranchBody :: Expression
+  }
+  deriving stock (Eq, Generic, Data)
+
+instance Serialize SideIfBranch
+
+instance NFData SideIfBranch
+
+instance Hashable SideIfBranch
+
+data SideIfs = SideIfs
+  { _sideIfBranches :: NonEmpty SideIfBranch,
+    _sideIfElse :: Maybe Expression
+  }
+  deriving stock (Eq, Generic, Data)
+
+instance Serialize SideIfs
+
+instance NFData SideIfs
+
+instance Hashable SideIfs
+
+data CaseBranchRhs
+  = CaseBranchRhsExpression Expression
+  | CaseBranchRhsIf SideIfs
+  deriving stock (Eq, Generic, Data)
+
+instance Serialize CaseBranchRhs
+
+instance NFData CaseBranchRhs
+
+instance Hashable CaseBranchRhs
+
 data CaseBranch = CaseBranch
  { _caseBranchPattern :: PatternArg,
-    _caseBranchExpression :: Expression
+    _caseBranchRhs :: CaseBranchRhs
  }
  deriving stock (Eq, Generic, Data)

@ -434,6 +469,9 @@ data NormalizedExpression = NormalizedExpression
    _normalizedExpressionOriginal :: Expression
  }

+makeLenses ''SideIfBranch
+makeLenses ''SideIfs
+makeLenses ''CaseBranchRhs
 makeLenses ''ModuleIndex
 makeLenses ''ArgInfo
 makeLenses ''WildcardConstructor
@ -580,8 +618,23 @@ instance HasLoc LetClause where
 instance HasLoc Let where
  getLoc l = getLocSpan (l ^. letClauses) <> getLoc (l ^. letExpression)

+instance HasLoc SideIfBranch where
+  getLoc SideIfBranch {..} =
+    getLoc _sideIfBranchCondition
+      <> getLoc _sideIfBranchBody
+
+instance HasLoc SideIfs where
+  getLoc SideIfs {..} =
+    getLocSpan _sideIfBranches
+      <>? (getLoc <$> _sideIfElse)
+
+instance HasLoc CaseBranchRhs where
+  getLoc = \case
+    CaseBranchRhsExpression e -> getLoc e
+    CaseBranchRhsIf e -> getLoc e
+
 instance HasLoc CaseBranch where
-  getLoc c = getLoc (c ^. caseBranchPattern) <> getLoc (c ^. caseBranchExpression)
+  getLoc c = getLoc (c ^. caseBranchPattern) <> getLoc (c ^. caseBranchRhs)

 instance HasLoc Case where
  getLoc c = getLocSpan (c ^. caseBranches)
--- a/src/Juvix/Compiler/Internal/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs
@ -83,10 +83,37 @@ instance PrettyCode Expression where
    ExpressionLet l -> ppCode l
    ExpressionCase c -> ppCode c

+instance PrettyCode SideIfBranch where
+  ppCode SideIfBranch {..} = do
+    condition' <- ppCode _sideIfBranchCondition
+    body' <- ppCode _sideIfBranchBody
+    return $
+      kwPipe
+        <+> kwIf
+        <+> condition'
+        <+> kwAssign
+        <+> oneLineOrNext body'
+
+instance PrettyCode SideIfs where
+  ppCode SideIfs {..} =
+    case (_sideIfBranches, _sideIfElse) of
+      (b :| [], Nothing) -> ppCode b
+      _ -> do
+        ifbranches <- mapM ppCode (toList _sideIfBranches)
+        elseBr <- mapM ppCode _sideIfElse
+        let allBranches = snocMaybe ifbranches elseBr
+        return $
+          line <> indent' (vsep allBranches)
+
+instance PrettyCode CaseBranchRhs where
+  ppCode = \case
+    CaseBranchRhsExpression e -> ppCode e
+    CaseBranchRhsIf ifCond -> ppCode ifCond
+
 instance PrettyCode CaseBranch where
  ppCode CaseBranch {..} = do
    pat <- ppCode _caseBranchPattern
-    e <- ppCode _caseBranchExpression
+    e <- ppCode _caseBranchRhs
    return $ kwPipe <+> pat <+> kwAssign <+> e

 instance PrettyCode Case where
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@ -942,12 +942,12 @@ goExpression = \case
    goIf :: Concrete.If 'Scoped -> Sem r Internal.Expression
    goIf e@Concrete.If {..} = do
      if_ <- getBuiltinName (getLoc e) BuiltinBoolIf
-      go if_ (toList _ifBranches)
+      go if_ _ifBranches
      where
-        go :: Internal.Name -> [Concrete.IfBranch 'Scoped] -> Sem r Internal.Expression
+        go :: Internal.Name -> [Concrete.IfBranch 'Scoped 'BranchIfBool] -> Sem r Internal.Expression
        go if_ = \case
          [] ->
-            goExpression (_ifBranchElse ^. Concrete.ifBranchElseExpression)
+            goExpression (_ifBranchElse ^. Concrete.ifBranchExpression)
          Concrete.IfBranch {..} : brs -> do
            c <- goExpression _ifBranchCondition
            b1 <- goExpression _ifBranchExpression
@ -1070,9 +1070,60 @@ goCase c = do
    goBranch :: CaseBranch 'Scoped -> Sem r Internal.CaseBranch
    goBranch b = do
      _caseBranchPattern <- goPatternArg (b ^. caseBranchPattern)
-      _caseBranchExpression <- goExpression (b ^. caseBranchExpression)
+      _caseBranchRhs <- goCaseBranchRhs (b ^. caseBranchRhs)
      return Internal.CaseBranch {..}

+gRhsExpression ::
+  forall r.
+  (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) =>
+  RhsExpression 'Scoped ->
+  Sem r Internal.Expression
+gRhsExpression RhsExpression {..} = goExpression _rhsExpression
+
+goSideIfBranch ::
+  forall r.
+  (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) =>
+  SideIfBranch 'Scoped 'BranchIfBool ->
+  Sem r Internal.SideIfBranch
+goSideIfBranch s = do
+  cond' <- goExpression (s ^. sideIfBranchCondition)
+  body' <- goExpression (s ^. sideIfBranchBody)
+  return
+    Internal.SideIfBranch
+      { _sideIfBranchCondition = cond',
+        _sideIfBranchBody = body'
+      }
+
+goSideIfBranchElse ::
+  forall r.
+  (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) =>
+  SideIfBranch 'Scoped 'BranchIfElse ->
+  Sem r Internal.Expression
+goSideIfBranchElse s = goExpression (s ^. sideIfBranchBody)
+
+goSideIfs ::
+  forall r.
+  (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) =>
+  SideIfs 'Scoped ->
+  Sem r Internal.SideIfs
+goSideIfs s = do
+  branches' <- mapM goSideIfBranch (s ^. sideIfBranches)
+  else' <- mapM goSideIfBranchElse (s ^. sideIfElse)
+  return
+    Internal.SideIfs
+      { _sideIfBranches = branches',
+        _sideIfElse = else'
+      }
+
+goCaseBranchRhs ::
+  forall r.
+  (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) =>
+  CaseBranchRhs 'Scoped ->
+  Sem r Internal.CaseBranchRhs
+goCaseBranchRhs = \case
+  CaseBranchRhsExpression e -> Internal.CaseBranchRhsExpression <$> gRhsExpression e
+  CaseBranchRhsIf s -> Internal.CaseBranchRhsIf <$> goSideIfs s
+
 goLambda :: forall r. (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => Lambda 'Scoped -> Sem r Internal.Lambda
 goLambda l = do
  clauses' <- mapM goClause (l ^. lambdaClauses)
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs
@ -65,7 +65,7 @@ checkStrictlyPositiveOccurrences ::
  Sem r ()
 checkStrictlyPositiveOccurrences p = do
  typeOfConstr <- strongNormalize_ (p ^. checkPositivityArgsTypeOfConstructor)
-  go False typeOfConstr
+  goExpression False typeOfConstr
  where
    indInfo = p ^. checkPositivityArgsInductive
    ctorName = p ^. checkPositivityArgsConstructorName
@ -81,11 +81,11 @@ checkStrictlyPositiveOccurrences p = do
     used below indicates whether the current search is performed on the left of
     an inner arrow or not.
    -}
-    go :: Bool -> Expression -> Sem r ()
-    go inside expr = case expr of
+    goExpression :: Bool -> Expression -> Sem r ()
+    goExpression inside expr = case expr of
      ExpressionApplication tyApp -> goApp tyApp
      ExpressionCase l -> goCase l
-      ExpressionFunction (Function l r) -> go True (l ^. paramType) >> go inside r
+      ExpressionFunction (Function l r) -> goLeft (l ^. paramType) >> go r
      ExpressionHole {} -> return ()
      ExpressionInstanceHole {} -> return ()
      ExpressionIden i -> goIden i
@ -95,17 +95,38 @@ checkStrictlyPositiveOccurrences p = do
      ExpressionSimpleLambda l -> goSimpleLambda l
      ExpressionUniverse {} -> return ()
      where
+        go :: Expression -> Sem r ()
+        go = goExpression inside
+
+        goLeft :: Expression -> Sem r ()
+        goLeft = goExpression True
+
        goCase :: Case -> Sem r ()
        goCase l = do
-          go inside (l ^. caseExpression)
+          go (l ^. caseExpression)
          mapM_ goCaseBranch (l ^. caseBranches)

+        goSideIfBranch :: SideIfBranch -> Sem r ()
+        goSideIfBranch b = do
+          go (b ^. sideIfBranchCondition)
+          go (b ^. sideIfBranchBody)
+
+        goSideIfs :: SideIfs -> Sem r ()
+        goSideIfs s = do
+          mapM_ goSideIfBranch (s ^. sideIfBranches)
+          mapM_ go (s ^. sideIfElse)
+
+        goCaseBranchRhs :: CaseBranchRhs -> Sem r ()
+        goCaseBranchRhs = \case
+          CaseBranchRhsExpression e -> go e
+          CaseBranchRhsIf s -> goSideIfs s
+
        goCaseBranch :: CaseBranch -> Sem r ()
-        goCaseBranch b = go inside (b ^. caseBranchExpression)
+        goCaseBranch b = goCaseBranchRhs (b ^. caseBranchRhs)

        goLet :: Let -> Sem r ()
        goLet l = do
-          go inside (l ^. letExpression)
+          go (l ^. letExpression)
          mapM_ goLetClause (l ^. letClauses)

        goLetClause :: LetClause -> Sem r ()
@ -118,19 +139,19 @@ checkStrictlyPositiveOccurrences p = do

        goFunctionDef :: FunctionDef -> Sem r ()
        goFunctionDef d = do
-          go inside (d ^. funDefType)
-          go inside (d ^. funDefBody)
+          go (d ^. funDefType)
+          go (d ^. funDefBody)

        goSimpleLambda :: SimpleLambda -> Sem r ()
        goSimpleLambda (SimpleLambda (SimpleBinder _ lamVarTy) lamBody) = do
-          go inside lamVarTy
-          go inside lamBody
+          go lamVarTy
+          go lamBody

        goLambda :: Lambda -> Sem r ()
        goLambda l = mapM_ goClause (l ^. lambdaClauses)
          where
            goClause :: LambdaClause -> Sem r ()
-            goClause (LambdaClause _ b) = go inside b
+            goClause (LambdaClause _ b) = go b

        goIden :: Iden -> Sem r ()
        goIden = \case
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs
@ -177,11 +177,35 @@ scanCase c = do
  mapM_ scanCaseBranch (c ^. caseBranches)
  scanExpression (c ^. caseExpression)

+scanSideIfBranch ::
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
+  SideIfBranch ->
+  Sem r ()
+scanSideIfBranch SideIfBranch {..} = do
+  scanExpression _sideIfBranchCondition
+  scanExpression _sideIfBranchBody
+
+scanSideIfs ::
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
+  SideIfs ->
+  Sem r ()
+scanSideIfs SideIfs {..} = do
+  mapM_ scanSideIfBranch _sideIfBranches
+  mapM_ scanExpression _sideIfElse
+
+scanCaseBranchRhs ::
+  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
+  CaseBranchRhs ->
+  Sem r ()
+scanCaseBranchRhs = \case
+  CaseBranchRhsExpression e -> scanExpression e
+  CaseBranchRhsIf e -> scanSideIfs e
+
 scanCaseBranch ::
  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
  CaseBranch ->
  Sem r ()
-scanCaseBranch = scanExpression . (^. caseBranchExpression)
+scanCaseBranch = scanCaseBranchRhs . (^. caseBranchRhs)

 scanLet ::
  (Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
@ -444,6 +444,63 @@ checkCoercionType FunctionDef {..} = do
      Explicit -> throw (ErrWrongCoercionArgument (WrongCoercionArgument fp))
      ImplicitInstance -> throw (ErrWrongCoercionArgument (WrongCoercionArgument fp))

+checkCaseBranchRhs ::
+  forall r.
+  (Members '[Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) =>
+  Expression ->
+  CaseBranchRhs ->
+  Sem r CaseBranchRhs
+checkCaseBranchRhs expectedTy = \case
+  CaseBranchRhsExpression e -> CaseBranchRhsExpression <$> checkExpression expectedTy e
+  CaseBranchRhsIf s -> CaseBranchRhsIf <$> checkSideIfs expectedTy s
+
+checkSideIfs ::
+  forall r.
+  ( Members
+      '[ Reader InfoTable,
+         ResultBuilder,
+         Error TypeCheckerError,
+         NameIdGen,
+         Reader LocalVars,
+         Inference,
+         Output TypedHole,
+         Termination,
+         Output CastHole,
+         Reader InsertedArgsStack
+       ]
+      r
+  ) =>
+  Expression ->
+  SideIfs ->
+  Sem r SideIfs
+checkSideIfs expectedTy SideIfs {..} = do
+  branches' <- mapM (checkSideIfBranch expectedTy) _sideIfBranches
+  else' <- mapM (checkExpression expectedTy) _sideIfElse
+  return
+    SideIfs
+      { _sideIfBranches = branches',
+        _sideIfElse = else'
+      }
+
+checkSideIfBranch ::
+  forall r.
+  (Members '[Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) =>
+  Expression ->
+  SideIfBranch ->
+  Sem r SideIfBranch
+checkSideIfBranch expectedTy SideIfBranch {..} = do
+  boolTy <- getBoolType (getLoc _sideIfBranchCondition)
+  cond' <- checkExpression boolTy _sideIfBranchCondition
+  body' <- checkExpression expectedTy _sideIfBranchBody
+  return
+    SideIfBranch
+      { _sideIfBranchCondition = cond',
+        _sideIfBranchBody = body'
+      }
+
+getBoolType :: (Members '[Reader InfoTable, Error TypeCheckerError] r) => Interval -> Sem r Expression
+getBoolType loc = toExpression <$> getBuiltinName loc BuiltinBool
+
 checkExpression ::
  forall r.
  (Members '[Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) =>
@ -536,7 +593,7 @@ checkFunctionBody expectedTy body =
  case body of
    ExpressionLambda {} -> checkExpression expectedTy body
    _ -> do
-      (patterns', typedBody) <- checkClause (getLoc body) expectedTy [] body
+      (patterns', typedBody) <- checkClauseExpression (getLoc body) expectedTy [] body
      return $ case nonEmpty patterns' of
        Nothing -> typedBody
        Just lambdaPatterns' ->
@ -551,8 +608,7 @@ checkFunctionBody expectedTy body =
                      }
              }

-- | helper function for lambda functions and case branches
-checkClause ::
+checkClauseExpression ::
  forall r.
  (Members '[Reader InfoTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) =>
  Interval ->
@ -563,12 +619,30 @@ checkClause ::
  -- | Body
  Expression ->
  Sem r ([PatternArg], Expression) -- (Checked patterns, Checked body)
+checkClauseExpression clauseLoc clauseType clausePats body = do
+  (pats', rhs') <- checkClause clauseLoc clauseType clausePats (CaseBranchRhsExpression body)
+  case rhs' of
+    CaseBranchRhsExpression body' -> return (pats', body')
+    CaseBranchRhsIf {} -> impossible
+
+-- | helper function for lambda functions and case branches
+checkClause ::
+  forall r.
+  (Members '[Reader InfoTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) =>
+  Interval ->
+  -- | Type
+  Expression ->
+  -- | Arguments
+  [PatternArg] ->
+  -- | Body
+  CaseBranchRhs ->
+  Sem r ([PatternArg], CaseBranchRhs) -- (Checked patterns, Checked body)
 checkClause clauseLoc clauseType clausePats body = do
  locals0 <- ask
  (localsPats, (checkedPatterns, bodyType)) <- helper clausePats clauseType
  let locals' = locals0 <> localsPats
  bodyTy' <- substitutionE (localsToSubsE locals') bodyType
-  checkedBody <- local (const locals') (checkExpression bodyTy' body)
+  checkedBody <- local (const locals') (checkCaseBranchRhs bodyTy' body)
  return (checkedPatterns, checkedBody)
  where
    helper :: [PatternArg] -> Expression -> Sem r (LocalVars, ([PatternArg], Expression))
@ -591,7 +665,7 @@ checkClause clauseLoc clauseType clausePats body = do
      [] -> do
        (bodyParams, bodyRest) <- unfoldFunType' bodyTy
        locals <- get
-        guessedBodyParams <- withLocalVars locals (unfoldArity <$> guessArity body)
+        guessedBodyParams <- withLocalVars locals (unfoldArity <$> arityCaseRhs body)
        let pref' :: [FunctionParameter] = take pref bodyParams
            pref :: Int = aI - targetI
            preImplicits = length . takeWhile isImplicitOrInstance
@ -921,7 +995,12 @@ inferLeftAppExpression mhint e = case e of
          _caseExpressionWholeType = Just ty
          goBranch :: CaseBranch -> Sem r CaseBranch
          goBranch b = do
-            (onePat, _caseBranchExpression) <- checkClause (getLoc b) funty [b ^. caseBranchPattern] (b ^. caseBranchExpression)
+            (onePat, _caseBranchRhs) <-
+              checkClause
+                (getLoc b)
+                funty
+                [b ^. caseBranchPattern]
+                (b ^. caseBranchRhs)
            let _caseBranchPattern = case onePat of
                  [x] -> x
                  _ -> impossible
@ -957,7 +1036,7 @@ inferLeftAppExpression mhint e = case e of
      where
        goClause :: Expression -> LambdaClause -> Sem r LambdaClause
        goClause ty cl@LambdaClause {..} = do
-          (pats', body') <- checkClause (getLoc cl) ty (toList _lambdaPatterns) _lambdaBody
+          (pats', body') <- checkClauseExpression (getLoc cl) ty (toList _lambdaPatterns) _lambdaBody
          return
            LambdaClause
              { _lambdaPatterns = nonEmpty' pats',
@ -1588,16 +1667,29 @@ guessPatternArgArity p =
 arityLet :: (Members '[Reader InfoTable, Inference, Reader LocalVars] r) => Let -> Sem r Arity
 arityLet l = guessArity (l ^. letExpression)

-- | All branches should have the same arity. If they are all the same, we
-- return that, otherwise we return ArityBlocking. Probably something better can
-- be done.
+-- | If all arities are the same, we return that, otherwise we return
+-- ArityNotKnown. Probably something better can be done.
+arityBranches :: NonEmpty Arity -> Arity
+arityBranches l
+  | allSame l = head l
+  | otherwise = ArityNotKnown
+
+-- | All branches should have the same arity.
 arityCase :: (Members '[Reader InfoTable, Inference, Reader LocalVars] r) => Case -> Sem r Arity
-arityCase c = do
-  aris <- mapM (guessArity . (^. caseBranchExpression)) (c ^. caseBranches)
-  return
-    if
-        | allSame aris -> head aris
-        | otherwise -> ArityNotKnown
+arityCase c = arityBranches <$> mapM (arityCaseRhs . (^. caseBranchRhs)) (c ^. caseBranches)
+
+aritySideIf :: (Members '[Reader InfoTable, Inference, Reader LocalVars] r) => SideIfs -> Sem r Arity
+aritySideIf SideIfs {..} = do
+  let bodies :: NonEmpty Expression =
+        snocNonEmptyMaybe
+          ((^. sideIfBranchBody) <$> _sideIfBranches)
+          _sideIfElse
+  arityBranches <$> mapM guessArity bodies
+
+arityCaseRhs :: (Members '[Reader InfoTable, Inference, Reader LocalVars] r) => CaseBranchRhs -> Sem r Arity
+arityCaseRhs = \case
+  CaseBranchRhsExpression e -> guessArity e
+  CaseBranchRhsIf s -> aritySideIf s

 idenArity :: (Members '[Inference, Reader LocalVars, Reader InfoTable] r) => Iden -> Sem r Arity
 idenArity = \case
--- a/src/Juvix/Data/CodeAnn.hs
+++ b/src/Juvix/Data/CodeAnn.hs
@ -100,6 +100,9 @@ kwColon = keyword Str.colon
 kwData :: Doc Ann
 kwData = keyword Str.data_

+kwIf :: Doc Ann
+kwIf = keyword Str.if_
+
 kwAssign :: Doc Ann
 kwAssign = keyword Str.assignAscii

--- a/src/Juvix/Prelude/Base/Foundation.hs
+++ b/src/Juvix/Prelude/Base/Foundation.hs
@ -348,6 +348,14 @@ combineMaps mps =
 -- List
 --------------------------------------------------------------------------------

+snocMaybe :: [a] -> Maybe a -> [a]
+snocMaybe l = \case
+  Nothing -> l
+  Just x -> snoc l x
+
+snocNonEmptyMaybe :: NonEmpty a -> Maybe a -> NonEmpty a
+snocNonEmptyMaybe (h :| t) m = h :| snocMaybe t m
+
 revAppend :: [a] -> [a] -> [a]
 revAppend [] !ys = ys
 revAppend (x : xs) !ys = revAppend xs (x : ys)
--- a/tests/positive/Format.juvix
+++ b/tests/positive/Format.juvix
@ -427,6 +427,25 @@ fff
  {f7 : List Nat}
  : Nat := zero;

+module SideIfConditions;
+  singleCaseBr : Nat :=
+    case 12 of
+      _
+        | if 0 < 0 := 3
+        | else := 4;
+
+  multiCaseBr : Nat :=
+    case 12 of
+      | zero
+        | if 0 < 0 := 3
+        | if 0 > 0 := 6
+        | else := 4
+      | suc (suc n)
+        | if 0 < 0 := 3
+        | else := n
+      | suc n if 0 < 0 := 3;
+end;
+
 module PublicImports;

  module Inner;