    {-# LANGUAGE BangPatterns       #-}
    {-# LANGUAGE OverloadedStrings  #-}
    {-# LANGUAGE RankNTypes         #-}

    module Dhall.Normalize (
          alphaNormalize
        , normalize
        , normalizeWith
        , normalizeWithM
        , Normalizer
        , NormalizerM
        , ReifiedNormalizer (..)
        , judgmentallyEqual
        , subst
        , shift
        , isNormalized
        , isNormalizedWith
        , freeIn
        ) where

    import Control.Applicative (empty)
    import Data.Foldable
    import Data.Functor.Identity (Identity(..))
    import Data.Semigroup (Semigroup(..))
    import Data.Sequence (ViewL(..), ViewR(..))
    import Data.Traversable
    import Instances.TH.Lift ()
    import Prelude hiding (succ)

    import Dhall.Syntax
        ( Expr(..)
        , Var(..)
        , Binding(Binding)
        , Chunks(..)
        , DhallDouble(..)
        , Const(..)
        , PreferAnnotation(..)
        )

    import qualified Data.Sequence
    import qualified Data.Set
    import qualified Data.Text
    import qualified Dhall.Eval    as Eval
    import qualified Dhall.Map
    import qualified Dhall.Set
    import qualified Dhall.Syntax  as Syntax
    import qualified Lens.Family   as Lens

    {-| Returns `True` if two expressions are α-equivalent and β-equivalent and
        `False` otherwise

        `judgmentallyEqual` can fail with an `error` if you compare ill-typed
        expressions
    -}
    judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool
    judgmentallyEqual :: Expr s a -> Expr t a -> Bool
    judgmentallyEqual = Expr s a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual
    {-# INLINE judgmentallyEqual #-}

    {-| `shift` is used by both normalization and type-checking to avoid variable
        capture by shifting variable indices

        For example, suppose that you were to normalize the following expression:

    > λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x

        If you were to substitute @y@ with @x@ without shifting any variable
        indices, then you would get the following incorrect result:

    > λ(a : Type) → λ(x : a) → λ(x : a) → x  -- Incorrect normalized form

        In order to substitute @x@ in place of @y@ we need to `shift` @x@ by @1@ in
        order to avoid being misinterpreted as the @x@ bound by the innermost
        lambda.  If we perform that `shift` then we get the correct result:

    > λ(a : Type) → λ(x : a) → λ(x : a) → x@1

        As a more worked example, suppose that you were to normalize the following
        expression:

    >     λ(a : Type)
    > →   λ(f : a → a → a)
    > →   λ(x : a)
    > →   λ(x : a)
    > →   (λ(x : a) → f x x@1) x@1

        The correct normalized result would be:

    >     λ(a : Type)
    > →   λ(f : a → a → a)
    > →   λ(x : a)
    > →   λ(x : a)
    > →   f x@1 x

        The above example illustrates how we need to both increase and decrease
        variable indices as part of substitution:

        * We need to increase the index of the outer @x\@1@ to @x\@2@ before we
          substitute it into the body of the innermost lambda expression in order
          to avoid variable capture.  This substitution changes the body of the
          lambda expression to @(f x\@2 x\@1)@

        * We then remove the innermost lambda and therefore decrease the indices of
          both @x@s in @(f x\@2 x\@1)@ to @(f x\@1 x)@ in order to reflect that one
          less @x@ variable is now bound within that scope

        Formally, @(shift d (V x n) e)@ modifies the expression @e@ by adding @d@ to
        the indices of all variables named @x@ whose indices are greater than
        @(n + m)@, where @m@ is the number of bound variables of the same name
        within that scope

        In practice, @d@ is always @1@ or @-1@ because we either:

        * increment variables by @1@ to avoid variable capture during substitution
        * decrement variables by @1@ when deleting lambdas after substitution

        @n@ starts off at @0@ when substitution begins and increments every time we
        descend into a lambda or let expression that binds a variable of the same
        name in order to avoid shifting the bound variables by mistake.
    -}
    shift :: Int -> Var -> Expr s a -> Expr s a
    shift :: Int -> Var -> Expr s a -> Expr s a
    shift d :: Int
    d (V x :: Text
    x n :: Int
    n) (Var (V x' :: Text
    x' n' :: Int
    n')) = Var -> Expr s a
    forall s a. Var -> Expr s a
    Var (Text -> Int -> Var
    V Text
    x' Int
    n'')
      where
        n'' :: Int
    n'' = if Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    x' Bool -> Bool -> Bool
    && Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    n' then Int
    n' Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    d else Int
    n'
    shift d :: Int
    d (V x :: Text
    x n :: Int
    n) (Lam x' :: Text
    x' _A :: Expr s a
    _A b :: Expr s a
    b) = Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Lam Text
    x' Expr s a
    _A' Expr s a
    b'
      where
        _A' :: Expr s a
    _A' = Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    shift Int
    d (Text -> Int -> Var
    V Text
    x Int
    n ) Expr s a
    _A
        b' :: Expr s a
    b'  = Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    shift Int
    d (Text -> Int -> Var
    V Text
    x Int
    n') Expr s a
    b
          where
            n' :: Int
    n' = if Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    x' then Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 1 else Int
    n
    shift d :: Int
    d (V x :: Text
    x n :: Int
    n) (Pi x' :: Text
    x' _A :: Expr s a
    _A _B :: Expr s a
    _B) = Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Pi Text
    x' Expr s a
    _A' Expr s a
    _B'
      where
        _A' :: Expr s a
    _A' = Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    shift Int
    d (Text -> Int -> Var
    V Text
    x Int
    n ) Expr s a
    _A
        _B' :: Expr s a
    _B' = Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    shift Int
    d (Text -> Int -> Var
    V Text
    x Int
    n') Expr s a
    _B
          where
            n' :: Int
    n' = if Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    x' then Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 1 else Int
    n
    shift d :: Int
    d (V x :: Text
    x n :: Int
    n) (Let (Binding src0 :: Maybe s
    src0 f :: Text
    f src1 :: Maybe s
    src1 mt :: Maybe (Maybe s, Expr s a)
    mt src2 :: Maybe s
    src2 r :: Expr s a
    r) e :: Expr s a
    e) =
        Binding s a -> Expr s a -> Expr s a
    forall s a. Binding s a -> Expr s a -> Expr s a
    Let (Maybe s
    -> Text
    -> Maybe s
    -> Maybe (Maybe s, Expr s a)
    -> Maybe s
    -> Expr s a
    -> Binding s a
    forall s a.
    Maybe s
    -> Text
    -> Maybe s
    -> Maybe (Maybe s, Expr s a)
    -> Maybe s
    -> Expr s a
    -> Binding s a
    Binding Maybe s
    src0 Text
    f Maybe s
    src1 Maybe (Maybe s, Expr s a)
    mt' Maybe s
    src2 Expr s a
    r') Expr s a
    e'
      where
        e' :: Expr s a
    e' = Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    shift Int
    d (Text -> Int -> Var
    V Text
    x Int
    n') Expr s a
    e
          where
            n' :: Int
    n' = if Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    f then Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 1 else Int
    n

        mt' :: Maybe (Maybe s, Expr s a)
    mt' = ((Maybe s, Expr s a) -> (Maybe s, Expr s a))
    -> Maybe (Maybe s, Expr s a) -> Maybe (Maybe s, Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Expr s a -> Expr s a)
    -> (Maybe s, Expr s a) -> (Maybe s, Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    shift Int
    d (Text -> Int -> Var
    V Text
    x Int
    n))) Maybe (Maybe s, Expr s a)
    mt
        r' :: Expr s a
    r'  =             Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    shift Int
    d (Text -> Int -> Var
    V Text
    x Int
    n)  Expr s a
    r
    shift d :: Int
    d v :: Var
    v expression :: Expr s a
    expression = ASetter (Expr s a) (Expr s a) (Expr s a) (Expr s a)
    -> (Expr s a -> Expr s a) -> Expr s a -> Expr s a
    forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
    Lens.over ASetter (Expr s a) (Expr s a) (Expr s a) (Expr s a)
    forall (f :: * -> *) s a.
    Applicative f =>
    (Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a)
    Syntax.subExpressions (Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    shift Int
    d Var
    v) Expr s a
    expression

    {-| Substitute all occurrences of a variable with an expression

    > subst x C B  ~  B[x := C]
    -}
    subst :: Var -> Expr s a -> Expr s a -> Expr s a
    subst :: Var -> Expr s a -> Expr s a -> Expr s a
    subst _ _ (Const a :: Const
    a) = Const -> Expr s a
    forall s a. Const -> Expr s a
    Const Const
    a
    subst (V x :: Text
    x n :: Int
    n) e :: Expr s a
    e (Lam y :: Text
    y _A :: Expr s a
    _A b :: Expr s a
    b) = Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Lam Text
    y Expr s a
    _A' Expr s a
    b'
      where
        _A' :: Expr s a
    _A' = Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst (Text -> Int -> Var
    V Text
    x Int
    n )                  Expr s a
    e  Expr s a
    _A
        b' :: Expr s a
    b'  = Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst (Text -> Int -> Var
    V Text
    x Int
    n') (Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    shift 1 (Text -> Int -> Var
    V Text
    y 0) Expr s a
    e)  Expr s a
    b
        n' :: Int
    n'  = if Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    y then Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 1 else Int
    n
    subst (V x :: Text
    x n :: Int
    n) e :: Expr s a
    e (Pi y :: Text
    y _A :: Expr s a
    _A _B :: Expr s a
    _B) = Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Pi Text
    y Expr s a
    _A' Expr s a
    _B'
      where
        _A' :: Expr s a
    _A' = Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst (Text -> Int -> Var
    V Text
    x Int
    n )                  Expr s a
    e  Expr s a
    _A
        _B' :: Expr s a
    _B' = Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst (Text -> Int -> Var
    V Text
    x Int
    n') (Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    shift 1 (Text -> Int -> Var
    V Text
    y 0) Expr s a
    e) Expr s a
    _B
        n' :: Int
    n'  = if Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    y then Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 1 else Int
    n
    subst v :: Var
    v e :: Expr s a
    e (Var v' :: Var
    v') = if Var
    v Var -> Var -> Bool
    forall a. Eq a => a -> a -> Bool
    == Var
    v' then Expr s a
    e else Var -> Expr s a
    forall s a. Var -> Expr s a
    Var Var
    v'
    subst (V x :: Text
    x n :: Int
    n) e :: Expr s a
    e (Let (Binding src0 :: Maybe s
    src0 f :: Text
    f src1 :: Maybe s
    src1 mt :: Maybe (Maybe s, Expr s a)
    mt src2 :: Maybe s
    src2 r :: Expr s a
    r) b :: Expr s a
    b) =
        Binding s a -> Expr s a -> Expr s a
    forall s a. Binding s a -> Expr s a -> Expr s a
    Let (Maybe s
    -> Text
    -> Maybe s
    -> Maybe (Maybe s, Expr s a)
    -> Maybe s
    -> Expr s a
    -> Binding s a
    forall s a.
    Maybe s
    -> Text
    -> Maybe s
    -> Maybe (Maybe s, Expr s a)
    -> Maybe s
    -> Expr s a
    -> Binding s a
    Binding Maybe s
    src0 Text
    f Maybe s
    src1 Maybe (Maybe s, Expr s a)
    mt' Maybe s
    src2 Expr s a
    r') Expr s a
    b'
      where
        b' :: Expr s a
    b' = Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst (Text -> Int -> Var
    V Text
    x Int
    n') (Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    shift 1 (Text -> Int -> Var
    V Text
    f 0) Expr s a
    e) Expr s a
    b
          where
            n' :: Int
    n' = if Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    f then Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 1 else Int
    n

        mt' :: Maybe (Maybe s, Expr s a)
    mt' = ((Maybe s, Expr s a) -> (Maybe s, Expr s a))
    -> Maybe (Maybe s, Expr s a) -> Maybe (Maybe s, Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Expr s a -> Expr s a)
    -> (Maybe s, Expr s a) -> (Maybe s, Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst (Text -> Int -> Var
    V Text
    x Int
    n) Expr s a
    e)) Maybe (Maybe s, Expr s a)
    mt
        r' :: Expr s a
    r'  =             Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst (Text -> Int -> Var
    V Text
    x Int
    n) Expr s a
    e  Expr s a
    r
    subst x :: Var
    x e :: Expr s a
    e expression :: Expr s a
    expression = ASetter (Expr s a) (Expr s a) (Expr s a) (Expr s a)
    -> (Expr s a -> Expr s a) -> Expr s a -> Expr s a
    forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
    Lens.over ASetter (Expr s a) (Expr s a) (Expr s a) (Expr s a)
    forall (f :: * -> *) s a.
    Applicative f =>
    (Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a)
    Syntax.subExpressions (Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst Var
    x Expr s a
    e) Expr s a
    expression

    {-| This function is used to determine whether folds like @Natural/fold@ or
        @List/fold@ should be lazy or strict in their accumulator based on the type
        of the accumulator

        If this function returns `True`, then they will be strict in their
        accumulator since we can guarantee an upper bound on the amount of work to
        normalize the accumulator on each step of the loop.  If this function
        returns `False` then they will be lazy in their accumulator and only
        normalize the final result at the end of the fold
    -}
    boundedType :: Expr s a -> Bool
    boundedType :: Expr s a -> Bool
    boundedType Bool             = Bool
    True
    boundedType Natural          = Bool
    True
    boundedType Integer          = Bool
    True
    boundedType Double           = Bool
    True
    boundedType Text             = Bool
    True
    boundedType (App List _)     = Bool
    False
    boundedType (App Optional t :: Expr s a
    t) = Expr s a -> Bool
    forall s a. Expr s a -> Bool
    boundedType Expr s a
    t
    boundedType (Record kvs :: Map Text (Expr s a)
    kvs)     = (Expr s a -> Bool) -> Map Text (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Expr s a -> Bool
    forall s a. Expr s a -> Bool
    boundedType Map Text (Expr s a)
    kvs
    boundedType (Union kvs :: Map Text (Maybe (Expr s a))
    kvs)      = (Maybe (Expr s a) -> Bool) -> Map Text (Maybe (Expr s a)) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all ((Expr s a -> Bool) -> Maybe (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Expr s a -> Bool
    forall s a. Expr s a -> Bool
    boundedType) Map Text (Maybe (Expr s a))
    kvs
    boundedType _                = Bool
    False

    {-| α-normalize an expression by renaming all bound variables to @\"_\"@ and
        using De Bruijn indices to distinguish them

    >>> alphaNormalize (Lam "a" (Const Type) (Lam "b" (Const Type) (Lam "x" "a" (Lam "y" "b" "x"))))
    Lam "_" (Const Type) (Lam "_" (Const Type) (Lam "_" (Var (V "_" 1)) (Lam "_" (Var (V "_" 1)) (Var (V "_" 1)))))

        α-normalization does not affect free variables:

    >>> alphaNormalize "x"
    Var (V "x" 0)

    -}
    alphaNormalize :: Expr s a -> Expr s a
    alphaNormalize :: Expr s a -> Expr s a
    alphaNormalize = Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    Eval.alphaNormalize
    {-# INLINE alphaNormalize #-}

    {-| Reduce an expression to its normal form, performing beta reduction

        `normalize` does not type-check the expression.  You may want to type-check
        expressions before normalizing them since normalization can convert an
        ill-typed expression into a well-typed expression.

        `normalize` can also fail with `error` if you normalize an ill-typed
        expression
    -}
    normalize :: Eq a => Expr s a -> Expr t a
    normalize :: Expr s a -> Expr t a
    normalize = Expr s a -> Expr t a
    forall a s t. Eq a => Expr s a -> Expr t a
    Eval.normalize
    {-# INLINE normalize #-}

    {-| Reduce an expression to its normal form, performing beta reduction and applying
        any custom definitions.

        `normalizeWith` is designed to be used with function `typeWith`. The `typeWith`
        function allows typing of Dhall functions in a custom typing context whereas
        `normalizeWith` allows evaluating Dhall expressions in a custom context.

        To be more precise `normalizeWith` applies the given normalizer when it finds an
        application term that it cannot reduce by other means.

        Note that the context used in normalization will determine the properties of normalization.
        That is, if the functions in custom context are not total then the Dhall language, evaluated
        with those functions is not total either.

        `normalizeWith` can fail with an `error` if you normalize an ill-typed
        expression
    -}
    normalizeWith :: Eq a => Maybe (ReifiedNormalizer a) -> Expr s a -> Expr t a
    normalizeWith :: Maybe (ReifiedNormalizer a) -> Expr s a -> Expr t a
    normalizeWith (Just ctx :: ReifiedNormalizer a
    ctx) t :: Expr s a
    t = Identity (Expr t a) -> Expr t a
    forall a. Identity a -> a
    runIdentity (NormalizerM Identity a -> Expr s a -> Identity (Expr t a)
    forall (m :: * -> *) a s t.
    (Monad m, Eq a) =>
    NormalizerM m a -> Expr s a -> m (Expr t a)
    normalizeWithM (ReifiedNormalizer a -> NormalizerM Identity a
    forall a.
    ReifiedNormalizer a
    -> forall s. Expr s a -> Identity (Maybe (Expr s a))
    getReifiedNormalizer ReifiedNormalizer a
    ctx) Expr s a
    t)
    normalizeWith _          t :: Expr s a
    t = Expr s a -> Expr t a
    forall a s t. Eq a => Expr s a -> Expr t a
    Eval.normalize Expr s a
    t

    {-| This function generalizes `normalizeWith` by allowing the custom normalizer
        to use an arbitrary `Monad`

        `normalizeWithM` can fail with an `error` if you normalize an ill-typed
        expression
    -}
    normalizeWithM
        :: (Monad m, Eq a) => NormalizerM m a -> Expr s a -> m (Expr t a)
    normalizeWithM :: NormalizerM m a -> Expr s a -> m (Expr t a)
    normalizeWithM ctx :: NormalizerM m a
    ctx e0 :: Expr s a
    e0 = Expr t a -> m (Expr t a)
    forall s. Expr s a -> m (Expr s a)
    loop (Expr s a -> Expr t a
    forall s a t. Expr s a -> Expr t a
    Syntax.denote Expr s a
    e0)
     where
     loop :: Expr s a -> m (Expr s a)
    loop e :: Expr s a
    e =  case Expr s a
    e of
        Const k :: Const
    k -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Const -> Expr s a
    forall s a. Const -> Expr s a
    Const Const
    k)
        Var v :: Var
    v -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Var -> Expr s a
    forall s a. Var -> Expr s a
    Var Var
    v)
        Lam x :: Text
    x _A :: Expr s a
    _A b :: Expr s a
    b -> Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Lam Text
    x (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Expr s a)
    _A' m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> m (Expr s a)
    b'
          where
            _A' :: m (Expr s a)
    _A' = Expr s a -> m (Expr s a)
    loop Expr s a
    _A
            b' :: m (Expr s a)
    b'  = Expr s a -> m (Expr s a)
    loop Expr s a
    b
        Pi x :: Text
    x _A :: Expr s a
    _A _B :: Expr s a
    _B -> Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Pi Text
    x (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Expr s a)
    _A' m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> m (Expr s a)
    _B'
          where
            _A' :: m (Expr s a)
    _A' = Expr s a -> m (Expr s a)
    loop Expr s a
    _A
            _B' :: m (Expr s a)
    _B' = Expr s a -> m (Expr s a)
    loop Expr s a
    _B
        App f :: Expr s a
    f a :: Expr s a
    a -> do
          Maybe (Expr s a)
    res <- Expr s a -> m (Maybe (Expr s a))
    NormalizerM m a
    ctx (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    f Expr s a
    a)
          case Maybe (Expr s a)
    res of
              Just e1 :: Expr s a
    e1 -> Expr s a -> m (Expr s a)
    loop Expr s a
    e1
              Nothing -> do
                  Expr s a
    f' <- Expr s a -> m (Expr s a)
    loop Expr s a
    f
                  Expr s a
    a' <- Expr s a -> m (Expr s a)
    loop Expr s a
    a
                  case Expr s a
    f' of
                    Lam x :: Text
    x _A :: Expr s a
    _A b₀ :: Expr s a
    b₀ -> do

                        let a₂ :: Expr s a
    a₂ = Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    shift 1 (Text -> Int -> Var
    V Text
    x 0) Expr s a
    a'
                        let b₁ :: Expr s a
    b₁ = Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst (Text -> Int -> Var
    V Text
    x 0) Expr s a
    a₂ Expr s a
    b₀
                        let b₂ :: Expr s a
    b₂ = Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    shift (-1) (Text -> Int -> Var
    V Text
    x 0) Expr s a
    b₁

                        Expr s a -> m (Expr s a)
    loop Expr s a
    b₂
                    _ -> do
                      case Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    f' Expr s a
    a' of
                        App (App (App (App NaturalFold (NaturalLit n0 :: Natural
    n0)) t :: Expr s a
    t) succ' :: Expr s a
    succ') zero :: Expr s a
    zero -> do
                          Expr s a
    t' <- Expr s a -> m (Expr s a)
    loop Expr s a
    t
                          if Expr s a -> Bool
    forall s a. Expr s a -> Bool
    boundedType Expr s a
    t' then m (Expr s a)
    strict else m (Expr s a)
    lazy
                          where
                            -- Use an `Integer` for the loop, due to the following
                            -- issue:
                            --
                            -- https://github.com/ghcjs/ghcjs/issues/782
                            strict :: m (Expr s a)
    strict =       Integer -> m (Expr s a)
    forall t. (Eq t, Num t) => t -> m (Expr s a)
    strictLoop (Natural -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Natural
    n0 :: Integer)
                            lazy :: m (Expr s a)
    lazy   = Expr s a -> m (Expr s a)
    loop (  Integer -> Expr s a
    forall t. (Eq t, Num t) => t -> Expr s a
    lazyLoop (Natural -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Natural
    n0 :: Integer))

                            strictLoop :: t -> m (Expr s a)
    strictLoop !t
    0 = Expr s a -> m (Expr s a)
    loop Expr s a
    zero
                            strictLoop !t
    n = Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    succ' (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> t -> m (Expr s a)
    strictLoop (t
    n t -> t -> t
    forall a. Num a => a -> a -> a
    - 1) m (Expr s a) -> (Expr s a -> m (Expr s a)) -> m (Expr s a)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Expr s a -> m (Expr s a)
    loop

                            lazyLoop :: t -> Expr s a
    lazyLoop !t
    0 = Expr s a
    zero
                            lazyLoop !t
    n = Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    succ' (t -> Expr s a
    lazyLoop (t
    n t -> t -> t
    forall a. Num a => a -> a -> a
    - 1))
                        App NaturalBuild g :: Expr s a
    g -> Expr s a -> m (Expr s a)
    loop (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    g Expr s a
    forall s a. Expr s a
    Natural) Expr s a
    forall s a. Expr s a
    succ) Expr s a
    forall s a. Expr s a
    zero)
                          where
                            succ :: Expr s a
    succ = Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Lam "n" Expr s a
    forall s a. Expr s a
    Natural (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    NaturalPlus "n" (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit 1))

                            zero :: Expr s a
    zero = Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit 0
                        App NaturalIsZero (NaturalLit n :: Natural
    n) -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Expr s a
    forall s a. Bool -> Expr s a
    BoolLit (Natural
    n Natural -> Natural -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0))
                        App NaturalEven (NaturalLit n :: Natural
    n) -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Expr s a
    forall s a. Bool -> Expr s a
    BoolLit (Natural -> Bool
    forall a. Integral a => a -> Bool
    even Natural
    n))
                        App NaturalOdd (NaturalLit n :: Natural
    n) -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Expr s a
    forall s a. Bool -> Expr s a
    BoolLit (Natural -> Bool
    forall a. Integral a => a -> Bool
    odd Natural
    n))
                        App NaturalToInteger (NaturalLit n :: Natural
    n) -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Expr s a
    forall s a. Integer -> Expr s a
    IntegerLit (Natural -> Integer
    forall a. Integral a => a -> Integer
    toInteger Natural
    n))
                        App NaturalShow (NaturalLit n :: Natural
    n) ->
                            Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] (String -> Text
    Data.Text.pack (Natural -> String
    forall a. Show a => a -> String
    show Natural
    n))))
                        App (App NaturalSubtract (NaturalLit x :: Natural
    x)) (NaturalLit y :: Natural
    y)
                            -- Use an `Integer` for the subtraction, due to the
                            -- following issue:
                            --
                            -- https://github.com/ghcjs/ghcjs/issues/782
                            | Natural
    y Natural -> Natural -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Natural
    x ->
                                Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit (Integer -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    subtract (Natural -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Natural
    x :: Integer) (Natural -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Natural
    y :: Integer))))
                            | Bool
    otherwise ->
                                Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit 0)
                        App (App NaturalSubtract (NaturalLit 0)) y :: Expr s a
    y -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    y
                        App (App NaturalSubtract _) (NaturalLit 0) -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit 0)
                        App (App NaturalSubtract x :: Expr s a
    x) y :: Expr s a
    y | Expr s a -> Expr s a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    x Expr s a
    y -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit 0)
                        App IntegerClamp (IntegerLit n :: Integer
    n)
                            | 0 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    n -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit (Integer -> Natural
    forall a. Num a => Integer -> a
    fromInteger Integer
    n))
                            | Bool
    otherwise -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit 0)
                        App IntegerNegate (IntegerLit n :: Integer
    n) ->
                            Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Expr s a
    forall s a. Integer -> Expr s a
    IntegerLit (Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    n))
                        App IntegerShow (IntegerLit n :: Integer
    n)
                            | 0 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    n    -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] ("+" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> String -> Text
    Data.Text.pack (Integer -> String
    forall a. Show a => a -> String
    show Integer
    n))))
                            | Bool
    otherwise -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] (String -> Text
    Data.Text.pack (Integer -> String
    forall a. Show a => a -> String
    show Integer
    n))))
                        -- `(read . show)` is used instead of `fromInteger` because `read` uses
                        -- the correct rounding rule.
                        -- See https://gitlab.haskell.org/ghc/ghc/issues/17231.
                        App IntegerToDouble (IntegerLit n :: Integer
    n) -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DhallDouble -> Expr s a
    forall s a. DhallDouble -> Expr s a
    DoubleLit ((Double -> DhallDouble
    DhallDouble (Double -> DhallDouble)
    -> (Integer -> Double) -> Integer -> DhallDouble
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Double
    forall a. Read a => String -> a
    read (String -> Double) -> (Integer -> String) -> Integer -> Double
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> String
    forall a. Show a => a -> String
    show) Integer
    n))
                        App DoubleShow (DoubleLit (DhallDouble n :: Double
    n)) ->
                            Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] (String -> Text
    Data.Text.pack (Double -> String
    forall a. Show a => a -> String
    show Double
    n))))
                        App (App OptionalBuild _A₀ :: Expr s a
    _A₀) g :: Expr s a
    g ->
                            Expr s a -> m (Expr s a)
    loop (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    g Expr s a
    optional) Expr s a
    just) Expr s a
    nothing)
                          where
                            optional :: Expr s a
    optional = Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    Optional Expr s a
    _A₀

                            just :: Expr s a
    just = Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Lam "a" Expr s a
    _A₀ (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    Some "a")

                            nothing :: Expr s a
    nothing = Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    None Expr s a
    _A₀
                        App (App ListBuild _A₀ :: Expr s a
    _A₀) g :: Expr s a
    g -> Expr s a -> m (Expr s a)
    loop (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    g Expr s a
    list) Expr s a
    cons) Expr s a
    nil)
                          where
                            _A₁ :: Expr s a
    _A₁ = Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    shift 1 "a" Expr s a
    _A₀

                            list :: Expr s a
    list = Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    List Expr s a
    _A₀

                            cons :: Expr s a
    cons =
                                Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Lam "a" Expr s a
    _A₀
                                    (Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Lam "as"
                                        (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    List Expr s a
    _A₁)
                                        (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    ListAppend (Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit Maybe (Expr s a)
    forall a. Maybe a
    Nothing (Expr s a -> Seq (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure "a")) "as")
                                    )

                            nil :: Expr s a
    nil = Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit (Expr s a -> Maybe (Expr s a)
    forall a. a -> Maybe a
    Just (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    List Expr s a
    _A₀)) Seq (Expr s a)
    forall (f :: * -> *) a. Alternative f => f a
    empty
                        App (App (App (App (App ListFold _) (ListLit _ xs :: Seq (Expr s a)
    xs)) t :: Expr s a
    t) cons :: Expr s a
    cons) nil :: Expr s a
    nil -> do
                          Expr s a
    t' <- Expr s a -> m (Expr s a)
    loop Expr s a
    t
                          if Expr s a -> Bool
    forall s a. Expr s a -> Bool
    boundedType Expr s a
    t' then m (Expr s a)
    strict else m (Expr s a)
    lazy
                          where
                            strict :: m (Expr s a)
    strict =       (Expr s a -> m (Expr s a) -> m (Expr s a))
    -> m (Expr s a) -> Seq (Expr s a) -> m (Expr s a)
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Expr s a -> m (Expr s a) -> m (Expr s a)
    strictCons m (Expr s a)
    strictNil Seq (Expr s a)
    xs
                            lazy :: m (Expr s a)
    lazy   = Expr s a -> m (Expr s a)
    loop ((Expr s a -> Expr s a -> Expr s a)
    -> Expr s a -> Seq (Expr s a) -> Expr s a
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr   Expr s a -> Expr s a -> Expr s a
    lazyCons   Expr s a
    lazyNil Seq (Expr s a)
    xs)

                            strictNil :: m (Expr s a)
    strictNil = Expr s a -> m (Expr s a)
    loop Expr s a
    nil
                            lazyNil :: Expr s a
    lazyNil   =      Expr s a
    nil

                            strictCons :: Expr s a -> m (Expr s a) -> m (Expr s a)
    strictCons y :: Expr s a
    y ys :: m (Expr s a)
    ys = do
                              Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    cons Expr s a
    y) (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Expr s a)
    ys m (Expr s a) -> (Expr s a -> m (Expr s a)) -> m (Expr s a)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Expr s a -> m (Expr s a)
    loop
                            lazyCons :: Expr s a -> Expr s a -> Expr s a
    lazyCons   y :: Expr s a
    y ys :: Expr s a
    ys =       Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    cons Expr s a
    y) Expr s a
    ys
                        App (App ListLength _) (ListLit _ ys :: Seq (Expr s a)
    ys) ->
                            Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit (Int -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Seq (Expr s a) -> Int
    forall a. Seq a -> Int
    Data.Sequence.length Seq (Expr s a)
    ys)))
                        App (App ListHead t :: Expr s a
    t) (ListLit _ ys :: Seq (Expr s a)
    ys) -> Expr s a -> m (Expr s a)
    loop Expr s a
    o
                          where
                            o :: Expr s a
    o = case Seq (Expr s a) -> ViewL (Expr s a)
    forall a. Seq a -> ViewL a
    Data.Sequence.viewl Seq (Expr s a)
    ys of
                                    y :: Expr s a
    y :< _ -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    Some Expr s a
    y
                                    _      -> Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    None Expr s a
    t
                        App (App ListLast t :: Expr s a
    t) (ListLit _ ys :: Seq (Expr s a)
    ys) -> Expr s a -> m (Expr s a)
    loop Expr s a
    o
                          where
                            o :: Expr s a
    o = case Seq (Expr s a) -> ViewR (Expr s a)
    forall a. Seq a -> ViewR a
    Data.Sequence.viewr Seq (Expr s a)
    ys of
                                    _ :> y :: Expr s a
    y -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    Some Expr s a
    y
                                    _      -> Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    None Expr s a
    t
                        App (App ListIndexed _A₀ :: Expr s a
    _A₀) (ListLit _ as₀ :: Seq (Expr s a)
    as₀) -> Expr s a -> m (Expr s a)
    loop (Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit Maybe (Expr s a)
    t Seq (Expr s a)
    as₁)
                          where
                            as₁ :: Seq (Expr s a)
    as₁ = (Int -> Expr s a -> Expr s a) -> Seq (Expr s a) -> Seq (Expr s a)
    forall a b. (Int -> a -> b) -> Seq a -> Seq b
    Data.Sequence.mapWithIndex Int -> Expr s a -> Expr s a
    forall a s a. Integral a => a -> Expr s a -> Expr s a
    adapt Seq (Expr s a)
    as₀

                            _A₂ :: Expr s a
    _A₂ = Map Text (Expr s a) -> Expr s a
    forall s a. Map Text (Expr s a) -> Expr s a
    Record ([(Text, Expr s a)] -> Map Text (Expr s a)
    forall k v. Ord k => [(k, v)] -> Map k v
    Dhall.Map.fromList [(Text, Expr s a)]
    kts)
                              where
                                kts :: [(Text, Expr s a)]
    kts = [ ("index", Expr s a
    forall s a. Expr s a
    Natural)
                                      , ("value", Expr s a
    _A₀)
                                      ]

                            t :: Maybe (Expr s a)
    t | Seq (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Seq (Expr s a)
    as₀  = Expr s a -> Maybe (Expr s a)
    forall a. a -> Maybe a
    Just (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    List Expr s a
    _A₂)
                              | Bool
    otherwise = Maybe (Expr s a)
    forall a. Maybe a
    Nothing

                            adapt :: a -> Expr s a -> Expr s a
    adapt n :: a
    n a_ :: Expr s a
    a_ =
                                Map Text (Expr s a) -> Expr s a
    forall s a. Map Text (Expr s a) -> Expr s a
    RecordLit ([(Text, Expr s a)] -> Map Text (Expr s a)
    forall k v. Ord k => [(k, v)] -> Map k v
    Dhall.Map.fromList [(Text, Expr s a)]
    kvs)
                              where
                                kvs :: [(Text, Expr s a)]
    kvs = [ ("index", Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit (a -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral a
    n))
                                      , ("value", Expr s a
    a_)
                                      ]
                        App (App ListReverse _) (ListLit t :: Maybe (Expr s a)
    t xs :: Seq (Expr s a)
    xs) ->
                            Expr s a -> m (Expr s a)
    loop (Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit Maybe (Expr s a)
    t (Seq (Expr s a) -> Seq (Expr s a)
    forall a. Seq a -> Seq a
    Data.Sequence.reverse Seq (Expr s a)
    xs))

                        App (App OptionalFold t0 :: Expr s a
    t0) x0 :: Expr s a
    x0 -> do
                            Expr s a
    t1 <- Expr s a -> m (Expr s a)
    loop Expr s a
    t0
                            let optional :: Expr s a
    optional = Var -> Expr s a
    forall s a. Var -> Expr s a
    Var (Text -> Int -> Var
    V "optional" 0)
                            let lam :: Expr s a -> Expr s a
    lam term :: Expr s a
    term = (Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Lam "optional"
                                               (Const -> Expr s a
    forall s a. Const -> Expr s a
    Const Const
    Type)
                                               (Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Lam "some"
                                                   (Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Pi "_" Expr s a
    t1 Expr s a
    forall s a. Expr s a
    optional)
                                                   (Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Text -> Expr s a -> Expr s a -> Expr s a
    Lam "none" Expr s a
    forall s a. Expr s a
    optional Expr s a
    term)))
                            Expr s a
    x1 <- Expr s a -> m (Expr s a)
    loop Expr s a
    x0
                            Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr s a -> m (Expr s a)) -> Expr s a -> m (Expr s a)
    forall a b. (a -> b) -> a -> b
    $ case Expr s a
    x1 of
                                App None _ -> Expr s a -> Expr s a
    lam (Var -> Expr s a
    forall s a. Var -> Expr s a
    Var (Text -> Int -> Var
    V "none" 0))
                                Some x' :: Expr s a
    x'    -> Expr s a -> Expr s a
    lam (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App (Var -> Expr s a
    forall s a. Var -> Expr s a
    Var (Text -> Int -> Var
    V "some" 0)) Expr s a
    x')
                                _          -> Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    forall s a. Expr s a
    OptionalFold Expr s a
    t1) Expr s a
    x1

                        App TextShow (TextLit (Chunks [] oldText :: Text
    oldText)) ->
                            Expr s a -> m (Expr s a)
    loop (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    newText))
                          where
                            newText :: Text
    newText = Text -> Text
    Eval.textShow Text
    oldText
                        _ -> do
                            Maybe (Expr s a)
    res2 <- Expr s a -> m (Maybe (Expr s a))
    NormalizerM m a
    ctx (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    f' Expr s a
    a')
                            case Maybe (Expr s a)
    res2 of
                                Nothing -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    f' Expr s a
    a')
                                Just app' :: Expr s a
    app' -> Expr s a -> m (Expr s a)
    loop Expr s a
    app'
        Let (Binding _ f :: Text
    f _ _ _ r :: Expr s a
    r) b :: Expr s a
    b -> Expr s a -> m (Expr s a)
    loop Expr s a
    b''
          where
            r' :: Expr s a
    r'  = Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    shift   1  (Text -> Int -> Var
    V Text
    f 0) Expr s a
    r
            b' :: Expr s a
    b'  = Var -> Expr s a -> Expr s a -> Expr s a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst (Text -> Int -> Var
    V Text
    f 0) Expr s a
    r' Expr s a
    b
            b'' :: Expr s a
    b'' = Int -> Var -> Expr s a -> Expr s a
    forall s a. Int -> Var -> Expr s a -> Expr s a
    shift (-1) (Text -> Int -> Var
    V Text
    f 0) Expr s a
    b'
        Annot x :: Expr s a
    x _ -> Expr s a -> m (Expr s a)
    loop Expr s a
    x
        Bool -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    Bool
        BoolLit b :: Bool
    b -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Expr s a
    forall s a. Bool -> Expr s a
    BoolLit Bool
    b)
        BoolAnd x :: Expr s a
    x y :: Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall a s. Eq a => Expr s a -> Expr s a -> Expr s a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
          where
            decide :: Expr s a -> Expr s a -> Expr s a
    decide (BoolLit True )  r :: Expr s a
    r              = Expr s a
    r
            decide (BoolLit False)  _              = Bool -> Expr s a
    forall s a. Bool -> Expr s a
    BoolLit Bool
    False
            decide  l :: Expr s a
    l              (BoolLit True ) = Expr s a
    l
            decide  _              (BoolLit False) = Bool -> Expr s a
    forall s a. Bool -> Expr s a
    BoolLit Bool
    False
            decide  l :: Expr s a
    l               r :: Expr s a
    r
                | Expr s a -> Expr s a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    l Expr s a
    r = Expr s a
    l
                | Bool
    otherwise                  = Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolAnd Expr s a
    l Expr s a
    r
        BoolOr x :: Expr s a
    x y :: Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall a s. Eq a => Expr s a -> Expr s a -> Expr s a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
          where
            decide :: Expr s a -> Expr s a -> Expr s a
    decide (BoolLit False)  r :: Expr s a
    r              = Expr s a
    r
            decide (BoolLit True )  _              = Bool -> Expr s a
    forall s a. Bool -> Expr s a
    BoolLit Bool
    True
            decide  l :: Expr s a
    l              (BoolLit False) = Expr s a
    l
            decide  _              (BoolLit True ) = Bool -> Expr s a
    forall s a. Bool -> Expr s a
    BoolLit Bool
    True
            decide  l :: Expr s a
    l               r :: Expr s a
    r
                | Expr s a -> Expr s a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    l Expr s a
    r = Expr s a
    l
                | Bool
    otherwise                  = Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolOr Expr s a
    l Expr s a
    r
        BoolEQ x :: Expr s a
    x y :: Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall a s. Eq a => Expr s a -> Expr s a -> Expr s a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
          where
            decide :: Expr s a -> Expr s a -> Expr s a
    decide (BoolLit True )  r :: Expr s a
    r              = Expr s a
    r
            decide  l :: Expr s a
    l              (BoolLit True ) = Expr s a
    l
            decide  l :: Expr s a
    l               r :: Expr s a
    r
                | Expr s a -> Expr s a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    l Expr s a
    r = Bool -> Expr s a
    forall s a. Bool -> Expr s a
    BoolLit Bool
    True
                | Bool
    otherwise                  = Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolEQ Expr s a
    l Expr s a
    r
        BoolNE x :: Expr s a
    x y :: Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall a s. Eq a => Expr s a -> Expr s a -> Expr s a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
          where
            decide :: Expr s a -> Expr s a -> Expr s a
    decide (BoolLit False)  r :: Expr s a
    r              = Expr s a
    r
            decide  l :: Expr s a
    l              (BoolLit False) = Expr s a
    l
            decide  l :: Expr s a
    l               r :: Expr s a
    r
                | Expr s a -> Expr s a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    l Expr s a
    r = Bool -> Expr s a
    forall s a. Bool -> Expr s a
    BoolLit Bool
    False
                | Bool
    otherwise                  = Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    BoolNE Expr s a
    l Expr s a
    r
        BoolIf bool :: Expr s a
    bool true :: Expr s a
    true false :: Expr s a
    false -> Expr s a -> Expr s a -> Expr s a -> Expr s a
    forall a s. Eq a => Expr s a -> Expr s a -> Expr s a -> Expr s a
    decide (Expr s a -> Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    bool m (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    true m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    false
          where
            decide :: Expr s a -> Expr s a -> Expr s a -> Expr s a
    decide (BoolLit True )  l :: Expr s a
    l              _              = Expr s a
    l
            decide (BoolLit False)  _              r :: Expr s a
    r              = Expr s a
    r
            decide  b :: Expr s a
    b              (BoolLit True) (BoolLit False) = Expr s a
    b
            decide  b :: Expr s a
    b               l :: Expr s a
    l              r :: Expr s a
    r
                | Expr s a -> Expr s a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    l Expr s a
    r = Expr s a
    l
                | Bool
    otherwise                  = Expr s a -> Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a -> Expr s a
    BoolIf Expr s a
    b Expr s a
    l Expr s a
    r
        Natural -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    Natural
        NaturalLit n :: Natural
    n -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit Natural
    n)
        NaturalFold -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    NaturalFold
        NaturalBuild -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    NaturalBuild
        NaturalIsZero -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    NaturalIsZero
        NaturalEven -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    NaturalEven
        NaturalOdd -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    NaturalOdd
        NaturalToInteger -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    NaturalToInteger
        NaturalShow -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    NaturalShow
        NaturalSubtract -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    NaturalSubtract
        NaturalPlus x :: Expr s a
    x y :: Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
          where
            decide :: Expr s a -> Expr s a -> Expr s a
    decide (NaturalLit 0)  r :: Expr s a
    r             = Expr s a
    r
            decide  l :: Expr s a
    l             (NaturalLit 0) = Expr s a
    l
            decide (NaturalLit m :: Natural
    m) (NaturalLit n :: Natural
    n) = Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit (Natural
    m Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    + Natural
    n)
            decide  l :: Expr s a
    l              r :: Expr s a
    r             = Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    NaturalPlus Expr s a
    l Expr s a
    r
        NaturalTimes x :: Expr s a
    x y :: Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
          where
            decide :: Expr s a -> Expr s a -> Expr s a
    decide (NaturalLit 1)  r :: Expr s a
    r             = Expr s a
    r
            decide  l :: Expr s a
    l             (NaturalLit 1) = Expr s a
    l
            decide (NaturalLit 0)  _             = Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit 0
            decide  _             (NaturalLit 0) = Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit 0
            decide (NaturalLit m :: Natural
    m) (NaturalLit n :: Natural
    n) = Natural -> Expr s a
    forall s a. Natural -> Expr s a
    NaturalLit (Natural
    m Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    * Natural
    n)
            decide  l :: Expr s a
    l              r :: Expr s a
    r             = Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    NaturalTimes Expr s a
    l Expr s a
    r
        Integer -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    Integer
        IntegerLit n :: Integer
    n -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Expr s a
    forall s a. Integer -> Expr s a
    IntegerLit Integer
    n)
        IntegerClamp -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    IntegerClamp
        IntegerNegate -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    IntegerNegate
        IntegerShow -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    IntegerShow
        IntegerToDouble -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    IntegerToDouble
        Double -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    Double
        DoubleLit n :: DhallDouble
    n -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DhallDouble -> Expr s a
    forall s a. DhallDouble -> Expr s a
    DoubleLit DhallDouble
    n)
        DoubleShow -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    DoubleShow
        Text -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    Text
        TextLit (Chunks xys :: [(Text, Expr s a)]
    xys z :: Text
    z) -> do
            Chunks s a
    chunks' <- [Chunks s a] -> Chunks s a
    forall a. Monoid a => [a] -> a
    mconcat ([Chunks s a] -> Chunks s a) -> m [Chunks s a] -> m (Chunks s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m [Chunks s a]
    chunks
            case Chunks s a
    chunks' of
                Chunks [("", x :: Expr s a
    x)] "" -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    x
                c :: Chunks s a
    c                   -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit Chunks s a
    c)
          where
            chunks :: m [Chunks s a]
    chunks =
              (([Chunks s a] -> [Chunks s a] -> [Chunks s a]
    forall a. [a] -> [a] -> [a]
    ++ [[(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    z]) ([Chunks s a] -> [Chunks s a])
    -> ([[Chunks s a]] -> [Chunks s a])
    -> [[Chunks s a]]
    -> [Chunks s a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [[Chunks s a]] -> [Chunks s a]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat) ([[Chunks s a]] -> [Chunks s a])
    -> m [[Chunks s a]] -> m [Chunks s a]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Text, Expr s a) -> m [Chunks s a])
    -> [(Text, Expr s a)] -> m [[Chunks s a]]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (Text, Expr s a) -> m [Chunks s a]
    process [(Text, Expr s a)]
    xys

            process :: (Text, Expr s a) -> m [Chunks s a]
    process (x :: Text
    x, y :: Expr s a
    y) = do
              Expr s a
    y' <- Expr s a -> m (Expr s a)
    loop Expr s a
    y
              case Expr s a
    y' of
                TextLit c :: Chunks s a
    c -> [Chunks s a] -> m [Chunks s a]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [[(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    x, Chunks s a
    c]
                _         -> [Chunks s a] -> m [Chunks s a]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [[(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [(Text
    x, Expr s a
    y')] Text
    forall a. Monoid a => a
    mempty]
        TextAppend x :: Expr s a
    x y :: Expr s a
    y -> Expr s a -> m (Expr s a)
    loop (Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [("", Expr s a
    x), ("", Expr s a
    y)] ""))
        TextShow -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    TextShow
        List -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    List
        ListLit t :: Maybe (Expr s a)
    t es :: Seq (Expr s a)
    es
            | Seq (Expr s a) -> Bool
    forall a. Seq a -> Bool
    Data.Sequence.null Seq (Expr s a)
    es -> Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit (Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a)
    -> m (Maybe (Expr s a)) -> m (Seq (Expr s a) -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe (Expr s a))
    t' m (Seq (Expr s a) -> Expr s a)
    -> m (Seq (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Seq (Expr s a) -> m (Seq (Expr s a))
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Seq (Expr s a)
    forall a. Seq a
    Data.Sequence.empty
            | Bool
    otherwise             -> Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit Maybe (Expr s a)
    forall a. Maybe a
    Nothing (Seq (Expr s a) -> Expr s a) -> m (Seq (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Seq (Expr s a))
    es'
          where
            t' :: m (Maybe (Expr s a))
    t'  = (Expr s a -> m (Expr s a))
    -> Maybe (Expr s a) -> m (Maybe (Expr s a))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse Expr s a -> m (Expr s a)
    loop Maybe (Expr s a)
    t
            es' :: m (Seq (Expr s a))
    es' = (Expr s a -> m (Expr s a)) -> Seq (Expr s a) -> m (Seq (Expr s a))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse Expr s a -> m (Expr s a)
    loop Seq (Expr s a)
    es
        ListAppend x :: Expr s a
    x y :: Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
          where
            decide :: Expr s a -> Expr s a -> Expr s a
    decide (ListLit _ m :: Seq (Expr s a)
    m)  r :: Expr s a
    r            | Seq (Expr s a) -> Bool
    forall a. Seq a -> Bool
    Data.Sequence.null Seq (Expr s a)
    m = Expr s a
    r
            decide  l :: Expr s a
    l            (ListLit _ n :: Seq (Expr s a)
    n) | Seq (Expr s a) -> Bool
    forall a. Seq a -> Bool
    Data.Sequence.null Seq (Expr s a)
    n = Expr s a
    l
            decide (ListLit t :: Maybe (Expr s a)
    t m :: Seq (Expr s a)
    m) (ListLit _ n :: Seq (Expr s a)
    n)                        = Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit Maybe (Expr s a)
    t (Seq (Expr s a)
    m Seq (Expr s a) -> Seq (Expr s a) -> Seq (Expr s a)
    forall a. Semigroup a => a -> a -> a
    <> Seq (Expr s a)
    n)
            decide  l :: Expr s a
    l             r :: Expr s a
    r                                   = Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    ListAppend Expr s a
    l Expr s a
    r
        ListBuild -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    ListBuild
        ListFold -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    ListFold
        ListLength -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    ListLength
        ListHead -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    ListHead
        ListLast -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    ListLast
        ListIndexed -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    ListIndexed
        ListReverse -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    ListReverse
        Optional -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    Optional
        Some a :: Expr s a
    a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    Some (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Expr s a)
    a'
          where
            a' :: m (Expr s a)
    a' = Expr s a -> m (Expr s a)
    loop Expr s a
    a
        None -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    None
        OptionalFold -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    OptionalFold
        OptionalBuild -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    forall s a. Expr s a
    OptionalBuild
        Record kts :: Map Text (Expr s a)
    kts -> Map Text (Expr s a) -> Expr s a
    forall s a. Map Text (Expr s a) -> Expr s a
    Record (Map Text (Expr s a) -> Expr s a)
    -> (Map Text (Expr s a) -> Map Text (Expr s a))
    -> Map Text (Expr s a)
    -> Expr s a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map Text (Expr s a) -> Map Text (Expr s a)
    forall k v. Map k v -> Map k v
    Dhall.Map.sort (Map Text (Expr s a) -> Expr s a)
    -> m (Map Text (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Map Text (Expr s a))
    kts'
          where
            kts' :: m (Map Text (Expr s a))
    kts' = (Expr s a -> m (Expr s a))
    -> Map Text (Expr s a) -> m (Map Text (Expr s a))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse Expr s a -> m (Expr s a)
    loop Map Text (Expr s a)
    kts
        RecordLit kvs :: Map Text (Expr s a)
    kvs -> Map Text (Expr s a) -> Expr s a
    forall s a. Map Text (Expr s a) -> Expr s a
    RecordLit (Map Text (Expr s a) -> Expr s a)
    -> (Map Text (Expr s a) -> Map Text (Expr s a))
    -> Map Text (Expr s a)
    -> Expr s a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map Text (Expr s a) -> Map Text (Expr s a)
    forall k v. Map k v -> Map k v
    Dhall.Map.sort (Map Text (Expr s a) -> Expr s a)
    -> m (Map Text (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Map Text (Expr s a))
    kvs'
          where
            kvs' :: m (Map Text (Expr s a))
    kvs' = (Expr s a -> m (Expr s a))
    -> Map Text (Expr s a) -> m (Map Text (Expr s a))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse Expr s a -> m (Expr s a)
    loop Map Text (Expr s a)
    kvs
        Union kts :: Map Text (Maybe (Expr s a))
    kts -> Map Text (Maybe (Expr s a)) -> Expr s a
    forall s a. Map Text (Maybe (Expr s a)) -> Expr s a
    Union (Map Text (Maybe (Expr s a)) -> Expr s a)
    -> (Map Text (Maybe (Expr s a)) -> Map Text (Maybe (Expr s a)))
    -> Map Text (Maybe (Expr s a))
    -> Expr s a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map Text (Maybe (Expr s a)) -> Map Text (Maybe (Expr s a))
    forall k v. Map k v -> Map k v
    Dhall.Map.sort (Map Text (Maybe (Expr s a)) -> Expr s a)
    -> m (Map Text (Maybe (Expr s a))) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Map Text (Maybe (Expr s a)))
    kts'
          where
            kts' :: m (Map Text (Maybe (Expr s a)))
    kts' = (Maybe (Expr s a) -> m (Maybe (Expr s a)))
    -> Map Text (Maybe (Expr s a)) -> m (Map Text (Maybe (Expr s a)))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse ((Expr s a -> m (Expr s a))
    -> Maybe (Expr s a) -> m (Maybe (Expr s a))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse Expr s a -> m (Expr s a)
    loop) Map Text (Maybe (Expr s a))
    kts
        Combine mk :: Maybe Text
    mk x :: Expr s a
    x y :: Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
          where
            decide :: Expr s a -> Expr s a -> Expr s a
    decide (RecordLit m :: Map Text (Expr s a)
    m) r :: Expr s a
    r | Map Text (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (Expr s a)
    m =
                Expr s a
    r
            decide l :: Expr s a
    l (RecordLit n :: Map Text (Expr s a)
    n) | Map Text (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (Expr s a)
    n =
                Expr s a
    l
            decide (RecordLit m :: Map Text (Expr s a)
    m) (RecordLit n :: Map Text (Expr s a)
    n) =
                Map Text (Expr s a) -> Expr s a
    forall s a. Map Text (Expr s a) -> Expr s a
    RecordLit ((Expr s a -> Expr s a -> Expr s a)
    -> Map Text (Expr s a)
    -> Map Text (Expr s a)
    -> Map Text (Expr s a)
    forall k v. Ord k => (v -> v -> v) -> Map k v -> Map k v -> Map k v
    Dhall.Map.unionWith Expr s a -> Expr s a -> Expr s a
    decide Map Text (Expr s a)
    m Map Text (Expr s a)
    n)
            decide l :: Expr s a
    l r :: Expr s a
    r =
                Maybe Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Maybe Text -> Expr s a -> Expr s a -> Expr s a
    Combine Maybe Text
    mk Expr s a
    l Expr s a
    r
        CombineTypes x :: Expr s a
    x y :: Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
          where
            decide :: Expr s a -> Expr s a -> Expr s a
    decide (Record m :: Map Text (Expr s a)
    m) r :: Expr s a
    r | Map Text (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (Expr s a)
    m =
                Expr s a
    r
            decide l :: Expr s a
    l (Record n :: Map Text (Expr s a)
    n) | Map Text (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (Expr s a)
    n =
                Expr s a
    l
            decide (Record m :: Map Text (Expr s a)
    m) (Record n :: Map Text (Expr s a)
    n) =
                Map Text (Expr s a) -> Expr s a
    forall s a. Map Text (Expr s a) -> Expr s a
    Record ((Expr s a -> Expr s a -> Expr s a)
    -> Map Text (Expr s a)
    -> Map Text (Expr s a)
    -> Map Text (Expr s a)
    forall k v. Ord k => (v -> v -> v) -> Map k v -> Map k v -> Map k v
    Dhall.Map.unionWith Expr s a -> Expr s a -> Expr s a
    decide Map Text (Expr s a)
    m Map Text (Expr s a)
    n)
            decide l :: Expr s a
    l r :: Expr s a
    r =
                Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    CombineTypes Expr s a
    l Expr s a
    r
        Prefer _ x :: Expr s a
    x y :: Expr s a
    y -> Expr s a -> Expr s a -> Expr s a
    forall a s. Eq a => Expr s a -> Expr s a -> Expr s a
    decide (Expr s a -> Expr s a -> Expr s a)
    -> m (Expr s a) -> m (Expr s a -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr s a -> m (Expr s a)
    loop Expr s a
    x m (Expr s a -> Expr s a) -> m (Expr s a) -> m (Expr s a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr s a -> m (Expr s a)
    loop Expr s a
    y
          where
            decide :: Expr s a -> Expr s a -> Expr s a
    decide (RecordLit m :: Map Text (Expr s a)
    m) r :: Expr s a
    r | Map Text (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (Expr s a)
    m =
                Expr s a
    r
            decide l :: Expr s a
    l (RecordLit n :: Map Text (Expr s a)
    n) | Map Text (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (Expr s a)
    n =
                Expr s a
    l
            decide (RecordLit m :: Map Text (Expr s a)
    m) (RecordLit n :: Map Text (Expr s a)
    n) =
                Map Text (Expr s a) -> Expr s a
    forall s a. Map Text (Expr s a) -> Expr s a
    RecordLit (Map Text (Expr s a) -> Map Text (Expr s a) -> Map Text (Expr s a)
    forall k v. Ord k => Map k v -> Map k v -> Map k v
    Dhall.Map.union Map Text (Expr s a)
    n Map Text (Expr s a)
    m)
            decide l :: Expr s a
    l r :: Expr s a
    r | Expr s a -> Expr s a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    l Expr s a
    r =
                Expr s a
    l
            decide l :: Expr s a
    l r :: Expr s a
    r =
                PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
    forall s a.
    PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
    Prefer PreferAnnotation s a
    forall s a. PreferAnnotation s a
    PreferFromSource Expr s a
    l Expr s a
    r
        RecordCompletion x :: Expr s a
    x y :: Expr s a
    y -> do
            Expr s a -> m (Expr s a)
    loop (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    Annot (PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
    forall s a.
    PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
    Prefer PreferAnnotation s a
    forall s a. PreferAnnotation s a
    PreferFromCompletion (Expr s a -> Text -> Expr s a
    forall s a. Expr s a -> Text -> Expr s a
    Field Expr s a
    x "default") Expr s a
    y) (Expr s a -> Text -> Expr s a
    forall s a. Expr s a -> Text -> Expr s a
    Field Expr s a
    x "Type"))
        Merge x :: Expr s a
    x y :: Expr s a
    y t :: Maybe (Expr s a)
    t      -> do
            Expr s a
    x' <- Expr s a -> m (Expr s a)
    loop Expr s a
    x
            Expr s a
    y' <- Expr s a -> m (Expr s a)
    loop Expr s a
    y
            case Expr s a
    x' of
                RecordLit kvsX :: Map Text (Expr s a)
    kvsX ->
                    case Expr s a
    y' of
                        Field (Union ktsY :: Map Text (Maybe (Expr s a))
    ktsY) kY :: Text
    kY ->
                            case Text -> Map Text (Maybe (Expr s a)) -> Maybe (Maybe (Expr s a))
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    kY Map Text (Maybe (Expr s a))
    ktsY of
                                Just Nothing ->
                                    case Text -> Map Text (Expr s a) -> Maybe (Expr s a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    kY Map Text (Expr s a)
    kvsX of
                                        Just vX :: Expr s a
    vX -> Expr s a -> m (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    vX
                                        Nothing -> Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    Merge Expr s a
    x' Expr s a
    y' (Maybe (Expr s a) -> Expr s a)
    -> m (Maybe (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe (Expr s a))
    t'
                                _ ->
                                    Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    Merge Expr s a
    x' Expr s a
    y' (Maybe (Expr s a) -> Expr s a)
    -> m (Maybe (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe (Expr s a))
    t'
                        App (Field (Union ktsY :: Map Text (Maybe (Expr s a))
    ktsY) kY :: Text
    kY) vY :: Expr s a
    vY ->
                            case Text -> Map Text (Maybe (Expr s a)) -> Maybe (Maybe (Expr s a))
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    kY Map Text (Maybe (Expr s a))
    ktsY of
                                Just (Just _) ->
                                    case Text -> Map Text (Expr s a) -> Maybe (Expr s a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    kY Map Text (Expr s a)
    kvsX of
                                        Just vX :: Expr s a
    vX -> Expr s a -> m (Expr s a)
    loop (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    vX Expr s a
    vY)
                                        Nothing -> Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    Merge Expr s a
    x' Expr s a
    y' (Maybe (Expr s a) -> Expr s a)
    -> m (Maybe (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe (Expr s a))
    t'
                                _ ->
                                    Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    Merge Expr s a
    x' Expr s a
    y' (Maybe (Expr s a) -> Expr s a)
    -> m (Maybe (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe (Expr s a))
    t'
                        Some a :: Expr s a
    a ->
                            case Text -> Map Text (Expr s a) -> Maybe (Expr s a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup "Some" Map Text (Expr s a)
    kvsX of
                                Just vX :: Expr s a
    vX -> Expr s a -> m (Expr s a)
    loop (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr s a
    vX Expr s a
    a)
                                Nothing -> Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    Merge Expr s a
    x' Expr s a
    y' (Maybe (Expr s a) -> Expr s a)
    -> m (Maybe (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe (Expr s a))
    t'
                        App None _ ->
                            case Text -> Map Text (Expr s a) -> Maybe (Expr s a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup "None" Map Text (Expr s a)
    kvsX of
                                Just vX :: Expr s a
    vX -> Expr s a -> m (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr s a
    vX
                                Nothing -> Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    Merge Expr s a
    x' Expr s a
    y' (Maybe (Expr s a) -> Expr s a)
    -> m (Maybe (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe (Expr s a))
    t'
                        _ -> Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    Merge Expr s a
    x' Expr s a
    y' (Maybe (Expr s a) -> Expr s a)
    -> m (Maybe (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe (Expr s a))
    t'
                _ -> Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    forall s a. Expr s a -> Expr s a -> Maybe (Expr s a) -> Expr s a
    Merge Expr s a
    x' Expr s a
    y' (Maybe (Expr s a) -> Expr s a)
    -> m (Maybe (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Maybe (Expr s a))
    t'
          where
            t' :: m (Maybe (Expr s a))
    t' = (Expr s a -> m (Expr s a))
    -> Maybe (Expr s a) -> m (Maybe (Expr s a))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse Expr s a -> m (Expr s a)
    loop Maybe (Expr s a)
    t
        ToMap x :: Expr s a
    x t :: Maybe (Expr s a)
    t        -> do
            Expr s a
    x' <- Expr s a -> m (Expr s a)
    loop Expr s a
    x
            Maybe (Expr s a)
    t' <- (Expr s a -> m (Expr s a))
    -> Maybe (Expr s a) -> m (Maybe (Expr s a))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse Expr s a -> m (Expr s a)
    loop Maybe (Expr s a)
    t
            case Expr s a
    x' of
                RecordLit kvsX :: Map Text (Expr s a)
    kvsX -> do
                    let entry :: (Text, Expr s a) -> Expr s a
    entry (key :: Text
    key, value :: Expr s a
    value) =
                            Map Text (Expr s a) -> Expr s a
    forall s a. Map Text (Expr s a) -> Expr s a
    RecordLit
                                ([(Text, Expr s a)] -> Map Text (Expr s a)
    forall k v. Ord k => [(k, v)] -> Map k v
    Dhall.Map.fromList
                                    [ ("mapKey"  , Chunks s a -> Expr s a
    forall s a. Chunks s a -> Expr s a
    TextLit ([(Text, Expr s a)] -> Text -> Chunks s a
    forall s a. [(Text, Expr s a)] -> Text -> Chunks s a
    Chunks [] Text
    key))
                                    , ("mapValue", Expr s a
    value                  )
                                    ]
                                )

                    let keyValues :: Seq (Expr s a)
    keyValues = [Expr s a] -> Seq (Expr s a)
    forall a. [a] -> Seq a
    Data.Sequence.fromList (((Text, Expr s a) -> Expr s a) -> [(Text, Expr s a)] -> [Expr s a]
    forall a b. (a -> b) -> [a] -> [b]
    map (Text, Expr s a) -> Expr s a
    forall s a. (Text, Expr s a) -> Expr s a
    entry (Map Text (Expr s a) -> [(Text, Expr s a)]
    forall k v. Ord k => Map k v -> [(k, v)]
    Dhall.Map.toList Map Text (Expr s a)
    kvsX))

                    let listType :: Maybe (Expr s a)
    listType = case Maybe (Expr s a)
    t' of
                            Just _ | Seq (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Seq (Expr s a)
    keyValues ->
                                Maybe (Expr s a)
    t'
                            _ ->
                                Maybe (Expr s a)
    forall a. Maybe a
    Nothing

                    Expr s a -> m (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    forall s a. Maybe (Expr s a) -> Seq (Expr s a) -> Expr s a
    ListLit Maybe (Expr s a)
    listType Seq (Expr s a)
    keyValues)
                _ -> do
                    Expr s a -> m (Expr s a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr s a -> Maybe (Expr s a) -> Expr s a
    forall s a. Expr s a -> Maybe (Expr s a) -> Expr s a
    ToMap Expr s a
    x' Maybe (Expr s a)
    t')
        Field r :: Expr s a
    r x :: Text
    x        -> do
            let singletonRecordLit :: Expr s a -> Expr s a
    singletonRecordLit v :: Expr s a
    v = Map Text (Expr s a) -> Expr s a
    forall s a. Map Text (Expr s a) -> Expr s a
    RecordLit (Text -> Expr s a -> Map Text (Expr s a)
    forall k v. k -> v -> Map k v
    Dhall.Map.singleton Text
    x Expr s a
    v)

            Expr s a
    r' <- Expr s a -> m (Expr s a)
    loop Expr s a
    r
            case Expr s a
    r' of
                RecordLit kvs :: Map Text (Expr s a)
    kvs ->
                    case Text -> Map Text (Expr s a) -> Maybe (Expr s a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    x Map Text (Expr s a)
    kvs of
                        Just v :: Expr s a
    v  -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    v
                        Nothing -> Expr s a -> Text -> Expr s a
    forall s a. Expr s a -> Text -> Expr s a
    Field (Expr s a -> Text -> Expr s a)
    -> m (Expr s a) -> m (Text -> Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Map Text (Expr s a) -> Expr s a
    forall s a. Map Text (Expr s a) -> Expr s a
    RecordLit (Map Text (Expr s a) -> Expr s a)
    -> m (Map Text (Expr s a)) -> m (Expr s a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr s a -> m (Expr s a))
    -> Map Text (Expr s a) -> m (Map Text (Expr s a))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse Expr s a -> m (Expr s a)
    loop Map Text (Expr s a)
    kvs) m (Text -> Expr s a) -> m Text -> m (Expr s a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Text -> m Text
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Text
    x
                Project r_ :: Expr s a
    r_ _ -> Expr s a -> m (Expr s a)
    loop (Expr s a -> Text -> Expr s a
    forall s a. Expr s a -> Text -> Expr s a
    Field Expr s a
    r_ Text
    x)
                Prefer _ (RecordLit kvs :: Map Text (Expr s a)
    kvs) r_ :: Expr s a
    r_ -> case Text -> Map Text (Expr s a) -> Maybe (Expr s a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    x Map Text (Expr s a)
    kvs of
                    Just v :: Expr s a
    v -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr s a -> Text -> Expr s a
    forall s a. Expr s a -> Text -> Expr s a
    Field (PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
    forall s a.
    PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
    Prefer PreferAnnotation s a
    forall s a. PreferAnnotation s a
    PreferFromSource (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    singletonRecordLit Expr s a
    v) Expr s a
    r_) Text
    x)
                    Nothing -> Expr s a -> m (Expr s a)
    loop (Expr s a -> Text -> Expr s a
    forall s a. Expr s a -> Text -> Expr s a
    Field Expr s a
    r_ Text
    x)
                Prefer _ l :: Expr s a
    l (RecordLit kvs :: Map Text (Expr s a)
    kvs) -> case Text -> Map Text (Expr s a) -> Maybe (Expr s a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    x Map Text (Expr s a)
    kvs of
                    Just v :: Expr s a
    v -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr s a
    v
                    Nothing -> Expr s a -> m (Expr s a)
    loop (Expr s a -> Text -> Expr s a
    forall s a. Expr s a -> Text -> Expr s a
    Field Expr s a
    l Text
    x)
                Combine m :: Maybe Text
    m (RecordLit kvs :: Map Text (Expr s a)
    kvs) r_ :: Expr s a
    r_ -> case Text -> Map Text (Expr s a) -> Maybe (Expr s a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    x Map Text (Expr s a)
    kvs of
                    Just v :: Expr s a
    v -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr s a -> Text -> Expr s a
    forall s a. Expr s a -> Text -> Expr s a
    Field (Maybe Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Maybe Text -> Expr s a -> Expr s a -> Expr s a
    Combine Maybe Text
    m (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    singletonRecordLit Expr s a
    v) Expr s a
    r_) Text
    x)
                    Nothing -> Expr s a -> m (Expr s a)
    loop (Expr s a -> Text -> Expr s a
    forall s a. Expr s a -> Text -> Expr s a
    Field Expr s a
    r_ Text
    x)
                Combine m :: Maybe Text
    m l :: Expr s a
    l (RecordLit kvs :: Map Text (Expr s a)
    kvs) -> case Text -> Map Text (Expr s a) -> Maybe (Expr s a)
    forall k v. Ord k => k -> Map k v -> Maybe v
    Dhall.Map.lookup Text
    x Map Text (Expr s a)
    kvs of
                    Just v :: Expr s a
    v -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr s a -> Text -> Expr s a
    forall s a. Expr s a -> Text -> Expr s a
    Field (Maybe Text -> Expr s a -> Expr s a -> Expr s a
    forall s a. Maybe Text -> Expr s a -> Expr s a -> Expr s a
    Combine Maybe Text
    m Expr s a
    l (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    singletonRecordLit Expr s a
    v)) Text
    x)
                    Nothing -> Expr s a -> m (Expr s a)
    loop (Expr s a -> Text -> Expr s a
    forall s a. Expr s a -> Text -> Expr s a
    Field Expr s a
    l Text
    x)
                _ -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr s a -> Text -> Expr s a
    forall s a. Expr s a -> Text -> Expr s a
    Field Expr s a
    r' Text
    x)
        Project x :: Expr s a
    x (Left fields :: Set Text
    fields)-> do
            Expr s a
    x' <- Expr s a -> m (Expr s a)
    loop Expr s a
    x
            let fieldsSet :: Set Text
    fieldsSet = Set Text -> Set Text
    forall a. Set a -> Set a
    Dhall.Set.toSet Set Text
    fields
            case Expr s a
    x' of
                RecordLit kvs :: Map Text (Expr s a)
    kvs ->
                    Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Map Text (Expr s a) -> Expr s a
    forall s a. Map Text (Expr s a) -> Expr s a
    RecordLit (Map Text (Expr s a) -> Set Text -> Map Text (Expr s a)
    forall k a. Ord k => Map k a -> Set k -> Map k a
    Dhall.Map.restrictKeys Map Text (Expr s a)
    kvs Set Text
    fieldsSet))
                Project y :: Expr s a
    y _ ->
                    Expr s a -> m (Expr s a)
    loop (Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
    forall s a. Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
    Project Expr s a
    y (Set Text -> Either (Set Text) (Expr s a)
    forall a b. a -> Either a b
    Left Set Text
    fields))
                Prefer _ l :: Expr s a
    l (RecordLit rKvs :: Map Text (Expr s a)
    rKvs) -> do
                    let rKs :: Set Text
    rKs = Map Text (Expr s a) -> Set Text
    forall k v. Map k v -> Set k
    Dhall.Map.keysSet Map Text (Expr s a)
    rKvs
                    let l' :: Expr s a
    l' = Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
    forall s a. Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
    Project Expr s a
    l (Set Text -> Either (Set Text) (Expr s a)
    forall a b. a -> Either a b
    Left (Set Text -> Set Text
    forall a. Set a -> Set a
    Dhall.Set.fromSet (Set Text -> Set Text -> Set Text
    forall a. Ord a => Set a -> Set a -> Set a
    Data.Set.difference Set Text
    fieldsSet Set Text
    rKs)))
                    let r' :: Expr s a
    r' = Map Text (Expr s a) -> Expr s a
    forall s a. Map Text (Expr s a) -> Expr s a
    RecordLit (Map Text (Expr s a) -> Set Text -> Map Text (Expr s a)
    forall k a. Ord k => Map k a -> Set k -> Map k a
    Dhall.Map.restrictKeys Map Text (Expr s a)
    rKvs Set Text
    fieldsSet)
                    Expr s a -> m (Expr s a)
    loop (PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
    forall s a.
    PreferAnnotation s a -> Expr s a -> Expr s a -> Expr s a
    Prefer PreferAnnotation s a
    forall s a. PreferAnnotation s a
    PreferFromSource Expr s a
    l' Expr s a
    r')
                _ | Set Text -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Set Text
    fields -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Map Text (Expr s a) -> Expr s a
    forall s a. Map Text (Expr s a) -> Expr s a
    RecordLit Map Text (Expr s a)
    forall a. Monoid a => a
    mempty)
                  | Bool
    otherwise   -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
    forall s a. Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
    Project Expr s a
    x' (Set Text -> Either (Set Text) (Expr s a)
    forall a b. a -> Either a b
    Left (Set Text -> Set Text
    forall a. Ord a => Set a -> Set a
    Dhall.Set.sort Set Text
    fields)))
        Project r :: Expr s a
    r (Right e1 :: Expr s a
    e1) -> do
            Expr s a
    e2 <- Expr s a -> m (Expr s a)
    loop Expr s a
    e1

            case Expr s a
    e2 of
                Record kts :: Map Text (Expr s a)
    kts -> do
                    Expr s a -> m (Expr s a)
    loop (Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
    forall s a. Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
    Project Expr s a
    r (Set Text -> Either (Set Text) (Expr s a)
    forall a b. a -> Either a b
    Left (Set Text -> Set Text
    forall a. Set a -> Set a
    Dhall.Set.fromSet (Map Text (Expr s a) -> Set Text
    forall k v. Map k v -> Set k
    Dhall.Map.keysSet Map Text (Expr s a)
    kts))))
                _ -> do
                    Expr s a
    r' <- Expr s a -> m (Expr s a)
    loop Expr s a
    r
                    Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
    forall s a. Expr s a -> Either (Set Text) (Expr s a) -> Expr s a
    Project Expr s a
    r' (Expr s a -> Either (Set Text) (Expr s a)
    forall a b. b -> Either a b
    Right Expr s a
    e2))
        Assert t :: Expr s a
    t -> do
            Expr s a
    t' <- Expr s a -> m (Expr s a)
    loop Expr s a
    t

            Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    Assert Expr s a
    t')
        Equivalent l :: Expr s a
    l r :: Expr s a
    r -> do
            Expr s a
    l' <- Expr s a -> m (Expr s a)
    loop Expr s a
    l
            Expr s a
    r' <- Expr s a -> m (Expr s a)
    loop Expr s a
    r

            Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr s a -> Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a -> Expr s a
    Equivalent Expr s a
    l' Expr s a
    r')
        With e' :: Expr s a
    e' k :: NonEmpty Text
    k v :: Expr s a
    v -> do
            Expr s a -> m (Expr s a)
    loop (Expr s a -> Expr s a
    forall s a. Expr s a -> Expr s a
    Syntax.desugarWith (Expr s a -> NonEmpty Text -> Expr s a -> Expr s a
    forall s a. Expr s a -> NonEmpty Text -> Expr s a -> Expr s a
    With Expr s a
    e' NonEmpty Text
    k Expr s a
    v))
        Note _ e' :: Expr s a
    e' -> Expr s a -> m (Expr s a)
    loop Expr s a
    e'
        ImportAlt l :: Expr s a
    l _r :: Expr s a
    _r -> Expr s a -> m (Expr s a)
    loop Expr s a
    l
        Embed a :: a
    a -> Expr s a -> m (Expr s a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (a -> Expr s a
    forall s a. a -> Expr s a
    Embed a
    a)

    -- | Use this to wrap you embedded functions (see `normalizeWith`) to make them
    --   polymorphic enough to be used.
    type NormalizerM m a = forall s. Expr s a -> m (Maybe (Expr s a))

    -- | An variation on `NormalizerM` for pure normalizers
    type Normalizer a = NormalizerM Identity a

    -- | A reified 'Normalizer', which can be stored in structures without
    -- running into impredicative polymorphism.
    newtype ReifiedNormalizer a = ReifiedNormalizer
      { ReifiedNormalizer a
    -> forall s. Expr s a -> Identity (Maybe (Expr s a))
    getReifiedNormalizer :: Normalizer a }

    -- | Check if an expression is in a normal form given a context of evaluation.
    --   Unlike `isNormalized`, this will fully normalize and traverse through the expression.
    --
    --   It is much more efficient to use `isNormalized`.
    --
    --  `isNormalizedWith` can fail with an `error` if you check an ill-typed
    --  expression
    isNormalizedWith :: (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool
    isNormalizedWith :: Normalizer a -> Expr s a -> Bool
    isNormalizedWith ctx :: Normalizer a
    ctx e :: Expr s a
    e = Expr s a
    e Expr s a -> Expr s a -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe (ReifiedNormalizer a) -> Expr s a -> Expr s a
    forall a s t.
    Eq a =>
    Maybe (ReifiedNormalizer a) -> Expr s a -> Expr t a
    normalizeWith (ReifiedNormalizer a -> Maybe (ReifiedNormalizer a)
    forall a. a -> Maybe a
    Just (Normalizer a -> ReifiedNormalizer a
    forall a.
    (forall s. Expr s a -> Identity (Maybe (Expr s a)))
    -> ReifiedNormalizer a
    ReifiedNormalizer Normalizer a
    ctx)) Expr s a
    e

    -- | Quickly check if an expression is in normal form
    --
    -- Given a well-typed expression @e@, @'isNormalized' e@ is equivalent to
    -- @e == 'normalize' e@.
    --
    -- Given an ill-typed expression, 'isNormalized' may fail with an error, or
    -- evaluate to either False or True!
    isNormalized :: Eq a => Expr s a -> Bool
    isNormalized :: Expr s a -> Bool
    isNormalized e0 :: Expr s a
    e0 = Expr Any a -> Bool
    forall a t. Eq a => Expr t a -> Bool
    loop (Expr s a -> Expr Any a
    forall s a t. Expr s a -> Expr t a
    Syntax.denote Expr s a
    e0)
      where
        loop :: Expr t a -> Bool
    loop e :: Expr t a
    e = case Expr t a
    e of
          Const _ -> Bool
    True
          Var _ -> Bool
    True
          Lam _ a :: Expr t a
    a b :: Expr t a
    b -> Expr t a -> Bool
    loop Expr t a
    a Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    b
          Pi _ a :: Expr t a
    a b :: Expr t a
    b -> Expr t a -> Bool
    loop Expr t a
    a Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    b
          App f :: Expr t a
    f a :: Expr t a
    a -> Expr t a -> Bool
    loop Expr t a
    f Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    a Bool -> Bool -> Bool
    && case Expr t a -> Expr t a -> Expr t a
    forall s a. Expr s a -> Expr s a -> Expr s a
    App Expr t a
    f Expr t a
    a of
              App (Lam _ _ _) _ -> Bool
    False
              App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> Bool
    False
              App NaturalBuild _ -> Bool
    False
              App NaturalIsZero (NaturalLit _) -> Bool
    False
              App NaturalEven (NaturalLit _) -> Bool
    False
              App NaturalOdd (NaturalLit _) -> Bool
    False
              App NaturalShow (NaturalLit _) -> Bool
    False
              App (App NaturalSubtract (NaturalLit _)) (NaturalLit _) -> Bool
    False
              App (App NaturalSubtract (NaturalLit 0)) _ -> Bool
    False
              App (App NaturalSubtract _) (NaturalLit 0) -> Bool
    False
              App (App NaturalSubtract x :: Expr t a
    x) y :: Expr t a
    y -> Bool -> Bool
    not (Expr t a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr t a
    x Expr t a
    y)
              App NaturalToInteger (NaturalLit _) -> Bool
    False
              App IntegerNegate (IntegerLit _) -> Bool
    False
              App IntegerClamp (IntegerLit _) -> Bool
    False
              App IntegerShow (IntegerLit _) -> Bool
    False
              App IntegerToDouble (IntegerLit _) -> Bool
    False
              App DoubleShow (DoubleLit _) -> Bool
    False
              App (App OptionalBuild _) _ -> Bool
    False
              App (App ListBuild _) _ -> Bool
    False
              App (App (App (App (App (App ListFold _) (ListLit _ _)) _) _) _) _ -> Bool
    False
              App (App ListLength _) (ListLit _ _) -> Bool
    False
              App (App ListHead _) (ListLit _ _) -> Bool
    False
              App (App ListLast _) (ListLit _ _) -> Bool
    False
              App (App ListIndexed _) (ListLit _ _) -> Bool
    False
              App (App ListReverse _) (ListLit _ _) -> Bool
    False
              App (App OptionalFold _) (Some _) -> Bool
    False
              App (App OptionalFold _) (App None _) -> Bool
    False
              App TextShow (TextLit (Chunks [] _)) ->
                  Bool
    False
              _ -> Bool
    True
          Let _ _ -> Bool
    False
          Annot _ _ -> Bool
    False
          Bool -> Bool
    True
          BoolLit _ -> Bool
    True
          BoolAnd x :: Expr t a
    x y :: Expr t a
    y -> Expr t a -> Bool
    loop Expr t a
    x Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    y Bool -> Bool -> Bool
    && Expr t a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    decide Expr t a
    x Expr t a
    y
            where
              decide :: Expr s a -> Expr t a -> Bool
    decide (BoolLit _)  _          = Bool
    False
              decide  _          (BoolLit _) = Bool
    False
              decide  l :: Expr s a
    l           r :: Expr t a
    r          = Bool -> Bool
    not (Expr s a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    l Expr t a
    r)
          BoolOr x :: Expr t a
    x y :: Expr t a
    y -> Expr t a -> Bool
    loop Expr t a
    x Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    y Bool -> Bool -> Bool
    && Expr t a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    decide Expr t a
    x Expr t a
    y
            where
              decide :: Expr s a -> Expr t a -> Bool
    decide (BoolLit _)  _          = Bool
    False
              decide  _          (BoolLit _) = Bool
    False
              decide  l :: Expr s a
    l           r :: Expr t a
    r          = Bool -> Bool
    not (Expr s a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    l Expr t a
    r)
          BoolEQ x :: Expr t a
    x y :: Expr t a
    y -> Expr t a -> Bool
    loop Expr t a
    x Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    y Bool -> Bool -> Bool
    && Expr t a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    decide Expr t a
    x Expr t a
    y
            where
              decide :: Expr s a -> Expr t a -> Bool
    decide (BoolLit True)  _             = Bool
    False
              decide  _             (BoolLit True) = Bool
    False
              decide  l :: Expr s a
    l              r :: Expr t a
    r             = Bool -> Bool
    not (Expr s a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    l Expr t a
    r)
          BoolNE x :: Expr t a
    x y :: Expr t a
    y -> Expr t a -> Bool
    loop Expr t a
    x Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    y Bool -> Bool -> Bool
    && Expr t a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    decide Expr t a
    x Expr t a
    y
            where
              decide :: Expr s a -> Expr t a -> Bool
    decide (BoolLit False)  _               = Bool
    False
              decide  _              (BoolLit False ) = Bool
    False
              decide  l :: Expr s a
    l               r :: Expr t a
    r               = Bool -> Bool
    not (Expr s a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    l Expr t a
    r)
          BoolIf x :: Expr t a
    x y :: Expr t a
    y z :: Expr t a
    z ->
              Expr t a -> Bool
    loop Expr t a
    x Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    y Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    z Bool -> Bool -> Bool
    && Expr t a -> Expr t a -> Expr t a -> Bool
    forall a s a s t. Eq a => Expr s a -> Expr s a -> Expr t a -> Bool
    decide Expr t a
    x Expr t a
    y Expr t a
    z
            where
              decide :: Expr s a -> Expr s a -> Expr t a -> Bool
    decide (BoolLit _)  _              _              = Bool
    False
              decide  _          (BoolLit True) (BoolLit False) = Bool
    False
              decide  _           l :: Expr s a
    l              r :: Expr t a
    r              = Bool -> Bool
    not (Expr s a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    l Expr t a
    r)
          Natural -> Bool
    True
          NaturalLit _ -> Bool
    True
          NaturalFold -> Bool
    True
          NaturalBuild -> Bool
    True
          NaturalIsZero -> Bool
    True
          NaturalEven -> Bool
    True
          NaturalOdd -> Bool
    True
          NaturalShow -> Bool
    True
          NaturalSubtract -> Bool
    True
          NaturalToInteger -> Bool
    True
          NaturalPlus x :: Expr t a
    x y :: Expr t a
    y -> Expr t a -> Bool
    loop Expr t a
    x Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    y Bool -> Bool -> Bool
    && Expr t a -> Expr t a -> Bool
    forall s a s a. Expr s a -> Expr s a -> Bool
    decide Expr t a
    x Expr t a
    y
            where
              decide :: Expr s a -> Expr s a -> Bool
    decide (NaturalLit 0)  _             = Bool
    False
              decide  _             (NaturalLit 0) = Bool
    False
              decide (NaturalLit _) (NaturalLit _) = Bool
    False
              decide  _              _             = Bool
    True
          NaturalTimes x :: Expr t a
    x y :: Expr t a
    y -> Expr t a -> Bool
    loop Expr t a
    x Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    y Bool -> Bool -> Bool
    && Expr t a -> Expr t a -> Bool
    forall s a s a. Expr s a -> Expr s a -> Bool
    decide Expr t a
    x Expr t a
    y
            where
              decide :: Expr s a -> Expr s a -> Bool
    decide (NaturalLit 0)  _             = Bool
    False
              decide  _             (NaturalLit 0) = Bool
    False
              decide (NaturalLit 1)  _             = Bool
    False
              decide  _             (NaturalLit 1) = Bool
    False
              decide (NaturalLit _) (NaturalLit _) = Bool
    False
              decide  _              _             = Bool
    True
          Integer -> Bool
    True
          IntegerLit _ -> Bool
    True
          IntegerClamp -> Bool
    True
          IntegerNegate -> Bool
    True
          IntegerShow -> Bool
    True
          IntegerToDouble -> Bool
    True
          Double -> Bool
    True
          DoubleLit _ -> Bool
    True
          DoubleShow -> Bool
    True
          Text -> Bool
    True
          TextLit (Chunks [("", _)] "") -> Bool
    False
          TextLit (Chunks xys :: [(Text, Expr t a)]
    xys _) -> ((Text, Expr t a) -> Bool) -> [(Text, Expr t a)] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all ((Expr t a -> Bool) -> (Text, Expr t a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Expr t a -> Bool
    check) [(Text, Expr t a)]
    xys
            where
              check :: Expr t a -> Bool
    check y :: Expr t a
    y = Expr t a -> Bool
    loop Expr t a
    y Bool -> Bool -> Bool
    && case Expr t a
    y of
                  TextLit _ -> Bool
    False
                  _         -> Bool
    True
          TextAppend _ _ -> Bool
    False
          TextShow -> Bool
    True
          List -> Bool
    True
          ListLit t :: Maybe (Expr t a)
    t es :: Seq (Expr t a)
    es -> (Expr t a -> Bool) -> Maybe (Expr t a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Expr t a -> Bool
    loop Maybe (Expr t a)
    t Bool -> Bool -> Bool
    && (Expr t a -> Bool) -> Seq (Expr t a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Expr t a -> Bool
    loop Seq (Expr t a)
    es
          ListAppend x :: Expr t a
    x y :: Expr t a
    y -> Expr t a -> Bool
    loop Expr t a
    x Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    y Bool -> Bool -> Bool
    && Expr t a -> Expr t a -> Bool
    forall s a s a. Expr s a -> Expr s a -> Bool
    decide Expr t a
    x Expr t a
    y
            where
              decide :: Expr s a -> Expr s a -> Bool
    decide (ListLit _ m :: Seq (Expr s a)
    m)  _            | Seq (Expr s a) -> Bool
    forall a. Seq a -> Bool
    Data.Sequence.null Seq (Expr s a)
    m = Bool
    False
              decide  _            (ListLit _ n :: Seq (Expr s a)
    n) | Seq (Expr s a) -> Bool
    forall a. Seq a -> Bool
    Data.Sequence.null Seq (Expr s a)
    n = Bool
    False
              decide (ListLit _ _) (ListLit _ _)                        = Bool
    False
              decide  _             _                                   = Bool
    True
          ListBuild -> Bool
    True
          ListFold -> Bool
    True
          ListLength -> Bool
    True
          ListHead -> Bool
    True
          ListLast -> Bool
    True
          ListIndexed -> Bool
    True
          ListReverse -> Bool
    True
          Optional -> Bool
    True
          Some a :: Expr t a
    a -> Expr t a -> Bool
    loop Expr t a
    a
          None -> Bool
    True
          OptionalFold -> Bool
    True
          OptionalBuild -> Bool
    True
          Record kts :: Map Text (Expr t a)
    kts -> Map Text (Expr t a) -> Bool
    forall k v. Eq k => Map k v -> Bool
    Dhall.Map.isSorted Map Text (Expr t a)
    kts Bool -> Bool -> Bool
    && (Expr t a -> Bool) -> Map Text (Expr t a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Expr t a -> Bool
    loop Map Text (Expr t a)
    kts
          RecordLit kvs :: Map Text (Expr t a)
    kvs -> Map Text (Expr t a) -> Bool
    forall k v. Eq k => Map k v -> Bool
    Dhall.Map.isSorted Map Text (Expr t a)
    kvs Bool -> Bool -> Bool
    && (Expr t a -> Bool) -> Map Text (Expr t a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Expr t a -> Bool
    loop Map Text (Expr t a)
    kvs
          Union kts :: Map Text (Maybe (Expr t a))
    kts -> Map Text (Maybe (Expr t a)) -> Bool
    forall k v. Eq k => Map k v -> Bool
    Dhall.Map.isSorted Map Text (Maybe (Expr t a))
    kts Bool -> Bool -> Bool
    && (Maybe (Expr t a) -> Bool) -> Map Text (Maybe (Expr t a)) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all ((Expr t a -> Bool) -> Maybe (Expr t a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Expr t a -> Bool
    loop) Map Text (Maybe (Expr t a))
    kts
          Combine _ x :: Expr t a
    x y :: Expr t a
    y -> Expr t a -> Bool
    loop Expr t a
    x Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    y Bool -> Bool -> Bool
    && Expr t a -> Expr t a -> Bool
    forall s a s a. Expr s a -> Expr s a -> Bool
    decide Expr t a
    x Expr t a
    y
            where
              decide :: Expr s a -> Expr s a -> Bool
    decide (RecordLit m :: Map Text (Expr s a)
    m) _ | Map Text (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (Expr s a)
    m = Bool
    False
              decide _ (RecordLit n :: Map Text (Expr s a)
    n) | Map Text (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (Expr s a)
    n = Bool
    False
              decide (RecordLit _) (RecordLit _) = Bool
    False
              decide  _ _ = Bool
    True
          CombineTypes x :: Expr t a
    x y :: Expr t a
    y -> Expr t a -> Bool
    loop Expr t a
    x Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    y Bool -> Bool -> Bool
    && Expr t a -> Expr t a -> Bool
    forall s a s a. Expr s a -> Expr s a -> Bool
    decide Expr t a
    x Expr t a
    y
            where
              decide :: Expr s a -> Expr s a -> Bool
    decide (Record m :: Map Text (Expr s a)
    m) _ | Map Text (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (Expr s a)
    m = Bool
    False
              decide _ (Record n :: Map Text (Expr s a)
    n) | Map Text (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (Expr s a)
    n = Bool
    False
              decide (Record _) (Record _) = Bool
    False
              decide  _ _ = Bool
    True
          Prefer _ x :: Expr t a
    x y :: Expr t a
    y -> Expr t a -> Bool
    loop Expr t a
    x Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    y Bool -> Bool -> Bool
    && Expr t a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    decide Expr t a
    x Expr t a
    y
            where
              decide :: Expr s a -> Expr t a -> Bool
    decide (RecordLit m :: Map Text (Expr s a)
    m) _ | Map Text (Expr s a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (Expr s a)
    m = Bool
    False
              decide _ (RecordLit n :: Map Text (Expr t a)
    n) | Map Text (Expr t a) -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    Data.Foldable.null Map Text (Expr t a)
    n = Bool
    False
              decide (RecordLit _) (RecordLit _) = Bool
    False
              decide l :: Expr s a
    l r :: Expr t a
    r = Bool -> Bool
    not (Expr s a -> Expr t a -> Bool
    forall a s t. Eq a => Expr s a -> Expr t a -> Bool
    Eval.judgmentallyEqual Expr s a
    l Expr t a
    r)
          RecordCompletion _ _ -> Bool
    False
          Merge x :: Expr t a
    x y :: Expr t a
    y t :: Maybe (Expr t a)
    t -> Expr t a -> Bool
    loop Expr t a
    x Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    y Bool -> Bool -> Bool
    && (Expr t a -> Bool) -> Maybe (Expr t a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Expr t a -> Bool
    loop Maybe (Expr t a)
    t Bool -> Bool -> Bool
    && case Expr t a
    x of
              RecordLit _ -> case Expr t a
    y of
                  Field (Union _) _ -> Bool
    False
                  App (Field (Union _) _) _ -> Bool
    False
                  Some _ -> Bool
    False
                  App None _ -> Bool
    False
                  _ -> Bool
    True
              _ -> Bool
    True
          ToMap x :: Expr t a
    x t :: Maybe (Expr t a)
    t -> case Expr t a
    x of
              RecordLit _ -> Bool
    False
              _ -> Expr t a -> Bool
    loop Expr t a
    x Bool -> Bool -> Bool
    && (Expr t a -> Bool) -> Maybe (Expr t a) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Expr t a -> Bool
    loop Maybe (Expr t a)
    t
          Field r :: Expr t a
    r k :: Text
    k -> case Expr t a
    r of
              RecordLit _ -> Bool
    False
              Project _ _ -> Bool
    False
              Prefer _ (RecordLit m :: Map Text (Expr t a)
    m) _ -> Map Text (Expr t a) -> [Text]
    forall k v. Map k v -> [k]
    Dhall.Map.keys Map Text (Expr t a)
    m [Text] -> [Text] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Text
    k] Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    r
              Prefer _ _ (RecordLit _) -> Bool
    False
              Combine _ (RecordLit m :: Map Text (Expr t a)
    m) _ -> Map Text (Expr t a) -> [Text]
    forall k v. Map k v -> [k]
    Dhall.Map.keys Map Text (Expr t a)
    m [Text] -> [Text] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Text
    k] Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    r
              Combine _ _ (RecordLit m :: Map Text (Expr t a)
    m) -> Map Text (Expr t a) -> [Text]
    forall k v. Map k v -> [k]
    Dhall.Map.keys Map Text (Expr t a)
    m [Text] -> [Text] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Text
    k] Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    r
              _ -> Expr t a -> Bool
    loop Expr t a
    r
          Project r :: Expr t a
    r p :: Either (Set Text) (Expr t a)
    p -> Expr t a -> Bool
    loop Expr t a
    r Bool -> Bool -> Bool
    &&
              case Either (Set Text) (Expr t a)
    p of
                  Left s :: Set Text
    s -> case Expr t a
    r of
                      RecordLit _ -> Bool
    False
                      Project _ _ -> Bool
    False
                      Prefer _ _ (RecordLit _) -> Bool
    False
                      _ -> Bool -> Bool
    not (Set Text -> Bool
    forall a. Set a -> Bool
    Dhall.Set.null Set Text
    s) Bool -> Bool -> Bool
    && Set Text -> Bool
    forall a. Ord a => Set a -> Bool
    Dhall.Set.isSorted Set Text
    s
                  Right e' :: Expr t a
    e' -> case Expr t a
    e' of
                      Record _ -> Bool
    False
                      _ -> Expr t a -> Bool
    loop Expr t a
    e'
          Assert t :: Expr t a
    t -> Expr t a -> Bool
    loop Expr t a
    t
          Equivalent l :: Expr t a
    l r :: Expr t a
    r -> Expr t a -> Bool
    loop Expr t a
    l Bool -> Bool -> Bool
    && Expr t a -> Bool
    loop Expr t a
    r
          With{} -> Bool
    False
          Note _ e' :: Expr t a
    e' -> Expr t a -> Bool
    loop Expr t a
    e'
          ImportAlt _ _ -> Bool
    False
          Embed _ -> Bool
    True

    {-| Detect if the given variable is free within the given expression

    >>> "x" `freeIn` "x"
    True
    >>> "x" `freeIn` "y"
    False
    >>> "x" `freeIn` Lam "x" (Const Type) "x"
    False
    -}
    freeIn :: Eq a => Var -> Expr s a -> Bool
    variable :: Var
    variable@(V var :: Text
    var i :: Int
    i) freeIn :: Var -> Expr s a -> Bool
    `freeIn` expression :: Expr s a
    expression =
        Var -> Expr () a -> Expr () a -> Expr () a
    forall s a. Var -> Expr s a -> Expr s a -> Expr s a
    subst Var
    variable (Var -> Expr () a
    forall s a. Var -> Expr s a
    Var (Text -> Int -> Var
    V Text
    var (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 1))) Expr () a
    strippedExpression
          Expr () a -> Expr () a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Expr () a
    strippedExpression
      where
        denote' :: Expr t b -> Expr () b
        denote' :: Expr t b -> Expr () b
    denote' = Expr t b -> Expr () b
    forall s a t. Expr s a -> Expr t a
    Syntax.denote

        strippedExpression :: Expr () a
    strippedExpression = Expr s a -> Expr () a
    forall t b. Expr t b -> Expr () b
    denote' Expr s a
    expression