    {-# OPTIONS_GHC -Wunused-imports #-}

    {-| Definitions for fixity, precedence levels, and declared syntax.
    -}
    module Agda.Syntax.Fixity where

    import Control.DeepSeq

    import GHC.Generics (Generic)

    import Agda.Syntax.Position
    import Agda.Syntax.Common

    import Agda.Syntax.Common.Pretty

    import Agda.Utils.Impossible

    -- The Fixity data type is now defined in Agda.Syntax.Common.
    -- Andreas, 2019-08-16, issue #1346

    -- | Decorating something with @Fixity'@.
    data ThingWithFixity x = ThingWithFixity x Fixity'
      deriving ((forall a b. (a -> b) -> ThingWithFixity a -> ThingWithFixity b)
    -> (forall a b. a -> ThingWithFixity b -> ThingWithFixity a)
    -> Functor ThingWithFixity
    forall a b. a -> ThingWithFixity b -> ThingWithFixity a
    forall a b. (a -> b) -> ThingWithFixity a -> ThingWithFixity b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> ThingWithFixity a -> ThingWithFixity b
    fmap :: forall a b. (a -> b) -> ThingWithFixity a -> ThingWithFixity b
    $c<$ :: forall a b. a -> ThingWithFixity b -> ThingWithFixity a
    <$ :: forall a b. a -> ThingWithFixity b -> ThingWithFixity a
    Functor, (forall m. Monoid m => ThingWithFixity m -> m)
    -> (forall m a. Monoid m => (a -> m) -> ThingWithFixity a -> m)
    -> (forall m a. Monoid m => (a -> m) -> ThingWithFixity a -> m)
    -> (forall a b. (a -> b -> b) -> b -> ThingWithFixity a -> b)
    -> (forall a b. (a -> b -> b) -> b -> ThingWithFixity a -> b)
    -> (forall b a. (b -> a -> b) -> b -> ThingWithFixity a -> b)
    -> (forall b a. (b -> a -> b) -> b -> ThingWithFixity a -> b)
    -> (forall a. (a -> a -> a) -> ThingWithFixity a -> a)
    -> (forall a. (a -> a -> a) -> ThingWithFixity a -> a)
    -> (forall a. ThingWithFixity a -> [a])
    -> (forall a. ThingWithFixity a -> Bool)
    -> (forall a. ThingWithFixity a -> Int)
    -> (forall a. Eq a => a -> ThingWithFixity a -> Bool)
    -> (forall a. Ord a => ThingWithFixity a -> a)
    -> (forall a. Ord a => ThingWithFixity a -> a)
    -> (forall a. Num a => ThingWithFixity a -> a)
    -> (forall a. Num a => ThingWithFixity a -> a)
    -> Foldable ThingWithFixity
    forall a. Eq a => a -> ThingWithFixity a -> Bool
    forall a. Num a => ThingWithFixity a -> a
    forall a. Ord a => ThingWithFixity a -> a
    forall m. Monoid m => ThingWithFixity m -> m
    forall a. ThingWithFixity a -> Bool
    forall a. ThingWithFixity a -> Int
    forall a. ThingWithFixity a -> [a]
    forall a. (a -> a -> a) -> ThingWithFixity a -> a
    forall m a. Monoid m => (a -> m) -> ThingWithFixity a -> m
    forall b a. (b -> a -> b) -> b -> ThingWithFixity a -> b
    forall a b. (a -> b -> b) -> b -> ThingWithFixity a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => ThingWithFixity m -> m
    fold :: forall m. Monoid m => ThingWithFixity m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> ThingWithFixity a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> ThingWithFixity a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> ThingWithFixity a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> ThingWithFixity a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> ThingWithFixity a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> ThingWithFixity a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> ThingWithFixity a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> ThingWithFixity a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> ThingWithFixity a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> ThingWithFixity a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> ThingWithFixity a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> ThingWithFixity a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> ThingWithFixity a -> a
    foldr1 :: forall a. (a -> a -> a) -> ThingWithFixity a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> ThingWithFixity a -> a
    foldl1 :: forall a. (a -> a -> a) -> ThingWithFixity a -> a
    $ctoList :: forall a. ThingWithFixity a -> [a]
    toList :: forall a. ThingWithFixity a -> [a]
    $cnull :: forall a. ThingWithFixity a -> Bool
    null :: forall a. ThingWithFixity a -> Bool
    $clength :: forall a. ThingWithFixity a -> Int
    length :: forall a. ThingWithFixity a -> Int
    $celem :: forall a. Eq a => a -> ThingWithFixity a -> Bool
    elem :: forall a. Eq a => a -> ThingWithFixity a -> Bool
    $cmaximum :: forall a. Ord a => ThingWithFixity a -> a
    maximum :: forall a. Ord a => ThingWithFixity a -> a
    $cminimum :: forall a. Ord a => ThingWithFixity a -> a
    minimum :: forall a. Ord a => ThingWithFixity a -> a
    $csum :: forall a. Num a => ThingWithFixity a -> a
    sum :: forall a. Num a => ThingWithFixity a -> a
    $cproduct :: forall a. Num a => ThingWithFixity a -> a
    product :: forall a. Num a => ThingWithFixity a -> a
    Foldable, Functor ThingWithFixity
    Foldable ThingWithFixity
    (Functor ThingWithFixity, Foldable ThingWithFixity) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        ThingWithFixity (f a) -> f (ThingWithFixity a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        ThingWithFixity (m a) -> m (ThingWithFixity a))
    -> Traversable ThingWithFixity
    forall (t :: * -> *).
    (Functor t, Foldable t) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a.
    Monad m =>
    ThingWithFixity (m a) -> m (ThingWithFixity a)
    forall (f :: * -> *) a.
    Applicative f =>
    ThingWithFixity (f a) -> f (ThingWithFixity a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    ThingWithFixity (f a) -> f (ThingWithFixity a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    ThingWithFixity (f a) -> f (ThingWithFixity a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    ThingWithFixity (m a) -> m (ThingWithFixity a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    ThingWithFixity (m a) -> m (ThingWithFixity a)
    Traversable, Int -> ThingWithFixity x -> ShowS
    [ThingWithFixity x] -> ShowS
    ThingWithFixity x -> String
    (Int -> ThingWithFixity x -> ShowS)
    -> (ThingWithFixity x -> String)
    -> ([ThingWithFixity x] -> ShowS)
    -> Show (ThingWithFixity x)
    forall x. Show x => Int -> ThingWithFixity x -> ShowS
    forall x. Show x => [ThingWithFixity x] -> ShowS
    forall x. Show x => ThingWithFixity x -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall x. Show x => Int -> ThingWithFixity x -> ShowS
    showsPrec :: Int -> ThingWithFixity x -> ShowS
    $cshow :: forall x. Show x => ThingWithFixity x -> String
    show :: ThingWithFixity x -> String
    $cshowList :: forall x. Show x => [ThingWithFixity x] -> ShowS
    showList :: [ThingWithFixity x] -> ShowS
    Show)

    instance LensFixity' (ThingWithFixity a) where
      lensFixity' :: Lens' (ThingWithFixity a) Fixity'
    lensFixity' Fixity' -> f Fixity'
    f (ThingWithFixity a
    a Fixity'
    fix') = a -> Fixity' -> ThingWithFixity a
    forall x. x -> Fixity' -> ThingWithFixity x
    ThingWithFixity a
    a (Fixity' -> ThingWithFixity a)
    -> f Fixity' -> f (ThingWithFixity a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Fixity' -> f Fixity'
    f Fixity'
    fix'

    instance LensFixity (ThingWithFixity a) where
      lensFixity :: Lens' (ThingWithFixity a) Fixity
    lensFixity = (Fixity' -> f Fixity')
    -> ThingWithFixity a -> f (ThingWithFixity a)
    forall a. LensFixity' a => Lens' a Fixity'
    Lens' (ThingWithFixity a) Fixity'
    lensFixity' ((Fixity' -> f Fixity')
     -> ThingWithFixity a -> f (ThingWithFixity a))
    -> ((Fixity -> f Fixity) -> Fixity' -> f Fixity')
    -> (Fixity -> f Fixity)
    -> ThingWithFixity a
    -> f (ThingWithFixity a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Fixity -> f Fixity) -> Fixity' -> f Fixity'
    forall a. LensFixity a => Lens' a Fixity
    Lens' Fixity' Fixity
    lensFixity

    -- | Do we prefer parens around arguments like @λ x → x@ or not?
    --   See 'lamBrackets'.
    data ParenPreference = PreferParen | PreferParenless
      deriving (ParenPreference -> ParenPreference -> Bool
    (ParenPreference -> ParenPreference -> Bool)
    -> (ParenPreference -> ParenPreference -> Bool)
    -> Eq ParenPreference
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: ParenPreference -> ParenPreference -> Bool
    == :: ParenPreference -> ParenPreference -> Bool
    $c/= :: ParenPreference -> ParenPreference -> Bool
    /= :: ParenPreference -> ParenPreference -> Bool
    Eq, Eq ParenPreference
    Eq ParenPreference =>
    (ParenPreference -> ParenPreference -> Ordering)
    -> (ParenPreference -> ParenPreference -> Bool)
    -> (ParenPreference -> ParenPreference -> Bool)
    -> (ParenPreference -> ParenPreference -> Bool)
    -> (ParenPreference -> ParenPreference -> Bool)
    -> (ParenPreference -> ParenPreference -> ParenPreference)
    -> (ParenPreference -> ParenPreference -> ParenPreference)
    -> Ord ParenPreference
    ParenPreference -> ParenPreference -> Bool
    ParenPreference -> ParenPreference -> Ordering
    ParenPreference -> ParenPreference -> ParenPreference
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: ParenPreference -> ParenPreference -> Ordering
    compare :: ParenPreference -> ParenPreference -> Ordering
    $c< :: ParenPreference -> ParenPreference -> Bool
    < :: ParenPreference -> ParenPreference -> Bool
    $c<= :: ParenPreference -> ParenPreference -> Bool
    <= :: ParenPreference -> ParenPreference -> Bool
    $c> :: ParenPreference -> ParenPreference -> Bool
    > :: ParenPreference -> ParenPreference -> Bool
    $c>= :: ParenPreference -> ParenPreference -> Bool
    >= :: ParenPreference -> ParenPreference -> Bool
    $cmax :: ParenPreference -> ParenPreference -> ParenPreference
    max :: ParenPreference -> ParenPreference -> ParenPreference
    $cmin :: ParenPreference -> ParenPreference -> ParenPreference
    min :: ParenPreference -> ParenPreference -> ParenPreference
    Ord, Int -> ParenPreference -> ShowS
    [ParenPreference] -> ShowS
    ParenPreference -> String
    (Int -> ParenPreference -> ShowS)
    -> (ParenPreference -> String)
    -> ([ParenPreference] -> ShowS)
    -> Show ParenPreference
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> ParenPreference -> ShowS
    showsPrec :: Int -> ParenPreference -> ShowS
    $cshow :: ParenPreference -> String
    show :: ParenPreference -> String
    $cshowList :: [ParenPreference] -> ShowS
    showList :: [ParenPreference] -> ShowS
    Show, (forall x. ParenPreference -> Rep ParenPreference x)
    -> (forall x. Rep ParenPreference x -> ParenPreference)
    -> Generic ParenPreference
    forall x. Rep ParenPreference x -> ParenPreference
    forall x. ParenPreference -> Rep ParenPreference x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. ParenPreference -> Rep ParenPreference x
    from :: forall x. ParenPreference -> Rep ParenPreference x
    $cto :: forall x. Rep ParenPreference x -> ParenPreference
    to :: forall x. Rep ParenPreference x -> ParenPreference
    Generic)

    instance NFData ParenPreference

    preferParen :: ParenPreference -> Bool
    preferParen :: ParenPreference -> Bool
    preferParen ParenPreference
    p = ParenPreference
    PreferParen ParenPreference -> ParenPreference -> Bool
    forall a. Eq a => a -> a -> Bool
    == ParenPreference
    p

    preferParenless :: ParenPreference -> Bool
    preferParenless :: ParenPreference -> Bool
    preferParenless ParenPreference
    p = ParenPreference
    PreferParenless ParenPreference -> ParenPreference -> Bool
    forall a. Eq a => a -> a -> Bool
    == ParenPreference
    p

    -- * Precendence

    -- | Precedence is associated with a context.
    data Precedence = TopCtx | FunctionSpaceDomainCtx
                    | LeftOperandCtx Fixity | RightOperandCtx Fixity ParenPreference
                    | FunctionCtx | ArgumentCtx ParenPreference | InsideOperandCtx
                    | WithFunCtx | WithArgCtx | DotPatternCtx
        deriving (Int -> Precedence -> ShowS
    [Precedence] -> ShowS
    Precedence -> String
    (Int -> Precedence -> ShowS)
    -> (Precedence -> String)
    -> ([Precedence] -> ShowS)
    -> Show Precedence
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Precedence -> ShowS
    showsPrec :: Int -> Precedence -> ShowS
    $cshow :: Precedence -> String
    show :: Precedence -> String
    $cshowList :: [Precedence] -> ShowS
    showList :: [Precedence] -> ShowS
    Show, Precedence -> Precedence -> Bool
    (Precedence -> Precedence -> Bool)
    -> (Precedence -> Precedence -> Bool) -> Eq Precedence
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Precedence -> Precedence -> Bool
    == :: Precedence -> Precedence -> Bool
    $c/= :: Precedence -> Precedence -> Bool
    /= :: Precedence -> Precedence -> Bool
    Eq, (forall x. Precedence -> Rep Precedence x)
    -> (forall x. Rep Precedence x -> Precedence) -> Generic Precedence
    forall x. Rep Precedence x -> Precedence
    forall x. Precedence -> Rep Precedence x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. Precedence -> Rep Precedence x
    from :: forall x. Precedence -> Rep Precedence x
    $cto :: forall x. Rep Precedence x -> Precedence
    to :: forall x. Rep Precedence x -> Precedence
    Generic)

    instance NFData Precedence

    instance Pretty Precedence where
      pretty :: Precedence -> Doc
    pretty = String -> Doc
    forall a. String -> Doc a
    text (String -> Doc) -> (Precedence -> String) -> Precedence -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Precedence -> String
    forall a. Show a => a -> String
    show

    -- | When printing we keep track of a stack of precedences in order to be able
    --   to decide whether it's safe to leave out parens around lambdas. An empty
    --   stack is equivalent to `TopCtx`. Invariant: `notElem TopCtx`.
    type PrecedenceStack = [Precedence]

    pushPrecedence :: Precedence -> PrecedenceStack -> PrecedenceStack
    pushPrecedence :: Precedence -> [Precedence] -> [Precedence]
    pushPrecedence Precedence
    TopCtx [Precedence]
    _  = []
    pushPrecedence Precedence
    p      [Precedence]
    ps = Precedence
    p Precedence -> [Precedence] -> [Precedence]
    forall a. a -> [a] -> [a]
    : [Precedence]
    ps

    headPrecedence :: PrecedenceStack -> Precedence
    headPrecedence :: [Precedence] -> Precedence
    headPrecedence []      = Precedence
    TopCtx
    headPrecedence (Precedence
    p : [Precedence]
    _) = Precedence
    p

    -- | Argument context preferring parens.
    argumentCtx_ :: Precedence
    argumentCtx_ :: Precedence
    argumentCtx_ = ParenPreference -> Precedence
    ArgumentCtx ParenPreference
    PreferParen

    -- | Do we need to bracket an operator application of the given fixity
    --   in a context with the given precedence.
    opBrackets :: Fixity -> PrecedenceStack -> Bool
    opBrackets :: Fixity -> [Precedence] -> Bool
    opBrackets = Bool -> Fixity -> [Precedence] -> Bool
    opBrackets' Bool
    False

    -- | Do we need to bracket an operator application of the given fixity
    --   in a context with the given precedence.
    opBrackets' :: Bool ->   -- Is the last argument a parenless lambda?
                   Fixity -> PrecedenceStack -> Bool
    opBrackets' :: Bool -> Fixity -> [Precedence] -> Bool
    opBrackets' Bool
    isLam Fixity
    f [Precedence]
    ps = Fixity -> Precedence -> Bool
    brack Fixity
    f ([Precedence] -> Precedence
    headPrecedence [Precedence]
    ps)
      where
        false :: Bool
    false = Bool
    isLam Bool -> Bool -> Bool
    && [Precedence] -> Bool
    lamBrackets [Precedence]
    ps -- require more parens for `e >>= λ x → e₁` than `e >>= e₁`
        brack :: Fixity -> Precedence -> Bool
    brack                        (Fixity Range
    _ (Related PrecedenceLevel
    n1) Associativity
    LeftAssoc)
                   (LeftOperandCtx   (Fixity Range
    _ (Related PrecedenceLevel
    n2) Associativity
    LeftAssoc))  | PrecedenceLevel
    n1 PrecedenceLevel -> PrecedenceLevel -> Bool
    forall a. Ord a => a -> a -> Bool
    >= PrecedenceLevel
    n2 = Bool
    false
        brack                        (Fixity Range
    _ (Related PrecedenceLevel
    n1) Associativity
    RightAssoc)
                   (RightOperandCtx  (Fixity Range
    _ (Related PrecedenceLevel
    n2) Associativity
    RightAssoc) ParenPreference
    _) | PrecedenceLevel
    n1 PrecedenceLevel -> PrecedenceLevel -> Bool
    forall a. Ord a => a -> a -> Bool
    >= PrecedenceLevel
    n2 = Bool
    false
        brack Fixity
    f1   (LeftOperandCtx  Fixity
    f2) | Related PrecedenceLevel
    f1 <- Fixity -> FixityLevel
    fixityLevel Fixity
    f1
                                        , Related PrecedenceLevel
    f2 <- Fixity -> FixityLevel
    fixityLevel Fixity
    f2
                                        , PrecedenceLevel
    f1 PrecedenceLevel -> PrecedenceLevel -> Bool
    forall a. Ord a => a -> a -> Bool
    > PrecedenceLevel
    f2 = Bool
    false
        brack Fixity
    f1   (RightOperandCtx Fixity
    f2 ParenPreference
    _) | Related PrecedenceLevel
    f1 <- Fixity -> FixityLevel
    fixityLevel Fixity
    f1
                                        , Related PrecedenceLevel
    f2 <- Fixity -> FixityLevel
    fixityLevel Fixity
    f2
                                        , PrecedenceLevel
    f1 PrecedenceLevel -> PrecedenceLevel -> Bool
    forall a. Ord a => a -> a -> Bool
    > PrecedenceLevel
    f2 = Bool
    false
        brack Fixity
    _ Precedence
    TopCtx                 = Bool
    false
        brack Fixity
    _ Precedence
    FunctionSpaceDomainCtx = Bool
    false
        brack Fixity
    _ Precedence
    InsideOperandCtx       = Bool
    false
        brack Fixity
    _ Precedence
    WithArgCtx             = Bool
    false
        brack Fixity
    _ Precedence
    WithFunCtx             = Bool
    false
        brack Fixity
    _ Precedence
    _                      = Bool
    True

    -- | Does a lambda-like thing (lambda, let or pi) need brackets in the
    -- given context? A peculiar thing with lambdas is that they don't
    -- need brackets in certain right operand contexts. To decide we need to look
    -- at the stack of precedences and not just the current precedence.
    -- Example: @m₁ >>= (λ x → x) >>= m₂@ (for @_>>=_@ left associative).
    lamBrackets :: PrecedenceStack -> Bool
    lamBrackets :: [Precedence] -> Bool
    lamBrackets []       = Bool
    False
    lamBrackets (Precedence
    p : [Precedence]
    ps) = case Precedence
    p of
      Precedence
    TopCtx                 -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      ArgumentCtx ParenPreference
    pref       -> ParenPreference -> Bool
    preferParen ParenPreference
    pref Bool -> Bool -> Bool
    || [Precedence] -> Bool
    lamBrackets [Precedence]
    ps
      RightOperandCtx Fixity
    _ ParenPreference
    pref -> ParenPreference -> Bool
    preferParen ParenPreference
    pref Bool -> Bool -> Bool
    || [Precedence] -> Bool
    lamBrackets [Precedence]
    ps
      Precedence
    FunctionSpaceDomainCtx -> Bool
    True
      LeftOperandCtx{}       -> Bool
    True
      Precedence
    FunctionCtx            -> Bool
    True
      Precedence
    InsideOperandCtx       -> Bool
    True
      Precedence
    WithFunCtx             -> Bool
    True
      Precedence
    WithArgCtx             -> Bool
    True
      Precedence
    DotPatternCtx          -> Bool
    True

    -- | Does a function application need brackets?
    appBrackets :: PrecedenceStack -> Bool
    appBrackets :: [Precedence] -> Bool
    appBrackets = Bool -> [Precedence] -> Bool
    appBrackets' Bool
    False

    -- | Does a function application need brackets?
    appBrackets' :: Bool ->   -- Is the argument of the application a parenless lambda?
                    PrecedenceStack -> Bool
    appBrackets' :: Bool -> [Precedence] -> Bool
    appBrackets' Bool
    isLam [Precedence]
    ps = Precedence -> Bool
    brack ([Precedence] -> Precedence
    headPrecedence [Precedence]
    ps)
      where
        brack :: Precedence -> Bool
    brack ArgumentCtx{} = Bool
    True
        brack Precedence
    DotPatternCtx = Bool
    True
        brack Precedence
    _             = Bool
    isLam Bool -> Bool -> Bool
    && [Precedence] -> Bool
    lamBrackets [Precedence]
    ps -- allow e + e₁ λ x → e₂

    -- | Does a with application need brackets?
    withAppBrackets :: PrecedenceStack -> Bool
    withAppBrackets :: [Precedence] -> Bool
    withAppBrackets = Precedence -> Bool
    brack (Precedence -> Bool)
    -> ([Precedence] -> Precedence) -> [Precedence] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Precedence] -> Precedence
    headPrecedence
      where
        brack :: Precedence -> Bool
    brack Precedence
    TopCtx                 = Bool
    False
        brack Precedence
    FunctionSpaceDomainCtx = Bool
    False
        brack Precedence
    WithFunCtx             = Bool
    False
        brack Precedence
    _                      = Bool
    True

    -- | Does a function space need brackets?
    piBrackets :: PrecedenceStack -> Bool
    piBrackets :: [Precedence] -> Bool
    piBrackets [] = Bool
    False
    piBrackets [Precedence]
    _  = Bool
    True

    roundFixBrackets :: PrecedenceStack -> Bool
    roundFixBrackets :: [Precedence] -> Bool
    roundFixBrackets [Precedence]
    ps = Precedence
    DotPatternCtx Precedence -> Precedence -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Precedence] -> Precedence
    headPrecedence [Precedence]
    ps

    instance KillRange x => KillRange (ThingWithFixity x) where
      killRange :: KillRangeT (ThingWithFixity x)
    killRange (ThingWithFixity x
    c Fixity'
    f) = x -> Fixity' -> ThingWithFixity x
    forall x. x -> Fixity' -> ThingWithFixity x
    ThingWithFixity (KillRangeT x
    forall a. KillRange a => KillRangeT a
    killRange x
    c) Fixity'
    f