content: {-# LANGUAGE AllowAmbiguousTypes  #-}
  {-# LANGUAGE BangPatterns         #-}
  {-# LANGUAGE FlexibleContexts     #-}
  {-# LANGUAGE LambdaCase           #-}
  {-# LANGUAGE OverloadedStrings    #-}
  {-# LANGUAGE PatternSynonyms      #-}
  {-# LANGUAGE RankNTypes           #-}
  {-# LANGUAGE ScopedTypeVariables  #-}
  {-# LANGUAGE StandaloneDeriving   #-}
  {-# LANGUAGE UndecidableInstances #-}
  {-# LANGUAGE ViewPatterns         #-}
  
  {-| Eval-apply environment machine with conversion checking and quoting to
      normal forms. Fairly similar to GHCI's STG machine algorithmically, but much
      simpler, with no known call optimization or environment trimming.
  
      Potential optimizations without changing Expr:
  
      * In conversion checking, get non-shadowing variables not by linear
        Env-walking, but by keeping track of Env size, and generating names which
        are known to be illegal as source-level names (to rule out shadowing).
  
      * Use HashMap Text chunks for large let-definitions blocks. "Large" vs
        "Small" is fairly cheap to determine at evaluation time.
  
      Potential optimizations with changing Expr:
  
      * Use actual full de Bruijn indices in Var instead of Text counting indices.
        Then, we'd switch to full de Bruijn levels in Val as well, and use proper
        constant time non-shadowing name generation.
  -}
  
  module Dhall.Eval (
      judgmentallyEqual
    , normalize
    , alphaNormalize
    , eval
    , quote
    , envNames
    , countNames
    , conv
    , toVHPi
    , Closure(..)
    , Names(..)
    , Environment(..)
    , Val(..)
    , (~>)
    , textShow
    , dateShow
    , timeShow
    , timezoneShow
    ) where
  
  import Data.Bifunctor     (first)
  import Data.ByteString    (ByteString)
  import Data.Foldable      (foldr', toList)
  import Data.List.NonEmpty (NonEmpty (..))
  import Data.Sequence      (Seq, ViewL (..), ViewR (..))
  import Data.Text          (Text)
  import Data.Time          (Day, TimeOfDay (..), TimeZone)
  import Data.Void          (Void)
  import Dhall.Map          (Map)
  import Dhall.Set          (Set)
  import GHC.Natural        (Natural)
  import Prelude            hiding (succ)
  
  import Dhall.Syntax
      ( Binding (..)
      , Chunks (..)
      , Const (..)
      , DhallDouble (..)
      , Expr (..)
      , FunctionBinding (..)
      , PreferAnnotation (..)
      , RecordField (..)
      , Var (..)
      , WithComponent (..)
      )
  
  import qualified Data.Char
  import qualified Data.Sequence as Sequence
  import qualified Data.Set
  import qualified Data.Text     as Text
  import qualified Data.Time     as Time
  import qualified Dhall.Map     as Map
  import qualified Dhall.Set
  import qualified Dhall.Syntax  as Syntax
  import qualified Text.Printf   as Printf
  
  data Environment a
      = Empty
      | Skip   !(Environment a) {-# UNPACK #-} !Text
      | Extend !(Environment a) {-# UNPACK #-} !Text (Val a)
  
  deriving instance (Show a, Show (Val a -> Val a)) => Show (Environment a)
  
  errorMsg :: String
  errorMsg = unlines
    [ _ERROR <> ": Compiler bug                                                        "
    , "                                                                                "
    , "An ill-typed expression was encountered during normalization.                   "
    , "Explanation: This error message means that there is a bug in the Dhall compiler."
    , "You didn't do anything wrong, but if you would like to see this problem fixed   "
    , "then you should report the bug at:                                              "
    , "                                                                                "
    , "https://github.com/dhall-lang/dhall-haskell/issues                              "
    ]
    where
      _ERROR :: String
      _ERROR = "\ESC[1;31mError\ESC[0m"
  
  
  data Closure a = Closure !Text !(Environment a) !(Expr Void a)
  
  deriving instance (Show a, Show (Val a -> Val a)) => Show (Closure a)
  
  data VChunks a = VChunks ![(Text, Val a)] !Text
  
  deriving instance (Show a, Show (Val a -> Val a)) => Show (VChunks a)
  
  instance Semigroup (VChunks a) where
    VChunks xys z <> VChunks [] z' = VChunks xys (z <> z')
    VChunks xys z <> VChunks ((x', y'):xys') z' = VChunks (xys ++ (z <> x', y'):xys') z'
  
  instance Monoid (VChunks a) where
    mempty = VChunks [] mempty
  
  {-| Some information is lost when `eval` converts a `Lam` or a built-in function
      from the `Expr` type to a `VHLam` of the `Val` type and `quote` needs that
      information in order to reconstruct an equivalent `Expr`.  This `HLamInfo`
      type holds that extra information necessary to perform that reconstruction
  -}
  data HLamInfo a
    = Prim
    -- ^ Don't store any information
    | Typed !Text (Val a)
    -- ^ Store the original name and type of the variable bound by the `Lam`
    | NaturalSubtractZero
    -- ^ The original function was a @Natural/subtract 0@.  We need to preserve
    --   this information in case the @Natural/subtract@ ends up not being fully
    --   saturated, in which case we need to recover the unsaturated built-in
    | TextReplaceEmpty
    -- ^ The original function was a @Text/replace ""@
    | TextReplaceEmptyArgument (Val a)
    -- ^ The original function was a @Text/replace "" replacement@
  
  deriving instance (Show a, Show (Val a -> Val a)) => Show (HLamInfo a)
  
  pattern VPrim :: (Val a -> Val a) -> Val a
  pattern VPrim f = VHLam Prim f
  
  toVHPi :: Eq a => Val a -> Maybe (Text, Val a, Val a -> Val a)
  toVHPi (VPi a b@(Closure x _ _)) = Just (x, a, instantiate b)
  toVHPi (VHPi x a b             ) = Just (x, a, b)
  toVHPi  _                        = Nothing
  {-# INLINABLE toVHPi #-}
  
  data Val a
      = VConst !Const
      | VVar !Text !Int
      | VPrimVar
      | VApp !(Val a) !(Val a)
  
      | VLam (Val a) {-# UNPACK #-} !(Closure a)
      | VHLam !(HLamInfo a) !(Val a -> Val a)
  
      | VPi (Val a) {-# UNPACK #-} !(Closure a)
      | VHPi !Text (Val a) !(Val a -> Val a)
  
      | VBool
      | VBoolLit !Bool
      | VBoolAnd !(Val a) !(Val a)
      | VBoolOr !(Val a) !(Val a)
      | VBoolEQ !(Val a) !(Val a)
      | VBoolNE !(Val a) !(Val a)
      | VBoolIf !(Val a) !(Val a) !(Val a)
  
      | VBytes
      | VBytesLit ByteString
  
      | VNatural
      | VNaturalLit !Natural
      | VNaturalFold !(Val a) !(Val a) !(Val a) !(Val a)
      | VNaturalBuild !(Val a)
      | VNaturalIsZero !(Val a)
      | VNaturalEven !(Val a)
      | VNaturalOdd !(Val a)
      | VNaturalToInteger !(Val a)
      | VNaturalShow !(Val a)
      | VNaturalSubtract !(Val a) !(Val a)
      | VNaturalPlus !(Val a) !(Val a)
      | VNaturalTimes !(Val a) !(Val a)
  
      | VInteger
      | VIntegerLit !Integer
      | VIntegerClamp !(Val a)
      | VIntegerNegate !(Val a)
      | VIntegerShow !(Val a)
      | VIntegerToDouble !(Val a)
  
      | VDouble
      | VDoubleLit !DhallDouble
      | VDoubleShow !(Val a)
  
      | VText
      | VTextLit !(VChunks a)
      | VTextAppend !(Val a) !(Val a)
      | VTextShow !(Val a)
      | VTextReplace !(Val a) !(Val a) !(Val a)
  
      | VDate
      | VDateLiteral Time.Day
      | VDateShow !(Val a)
      | VTime
      | VTimeLiteral Time.TimeOfDay Word
      | VTimeShow !(Val a)
      | VTimeZone
      | VTimeZoneLiteral Time.TimeZone
      | VTimeZoneShow !(Val a)
  
      | VList !(Val a)
      | VListLit !(Maybe (Val a)) !(Seq (Val a))
      | VListAppend !(Val a) !(Val a)
      | VListBuild   (Val a) !(Val a)
      | VListFold    (Val a) !(Val a) !(Val a) !(Val a) !(Val a)
      | VListLength  (Val a) !(Val a)
      | VListHead    (Val a) !(Val a)
      | VListLast    (Val a) !(Val a)
      | VListIndexed (Val a) !(Val a)
      | VListReverse (Val a) !(Val a)
  
      | VOptional (Val a)
      | VSome (Val a)
      | VNone (Val a)
      | VRecord !(Map Text (Val a))
      | VRecordLit !(Map Text (Val a))
      | VUnion !(Map Text (Maybe (Val a)))
      | VCombine !(Maybe Text) !(Val a) !(Val a)
      | VCombineTypes !(Val a) !(Val a)
      | VPrefer !(Val a) !(Val a)
      | VMerge !(Val a) !(Val a) !(Maybe (Val a))
      | VToMap !(Val a) !(Maybe (Val a))
      | VShowConstructor !(Val a)
      | VField !(Val a) !Text
      | VInject !(Map Text (Maybe (Val a))) !Text !(Maybe (Val a))
      | VProject !(Val a) !(Either (Set Text) (Val a))
      | VAssert !(Val a)
      | VEquivalent !(Val a) !(Val a)
      | VWith !(Val a) (NonEmpty WithComponent) !(Val a)
      | VEmbed a
  
  -- | For use with "Text.Show.Functions".
  deriving instance (Show a, Show (Val a -> Val a)) => Show (Val a)
  
  (~>) :: Val a -> Val a -> Val a
  (~>) a b = VHPi "_" a (\_ -> b)
  {-# INLINE (~>) #-}
  
  infixr 5 ~>
  
  countEnvironment :: Text -> Environment a -> Int
  countEnvironment x = go (0 :: Int)
    where
      go !acc Empty             = acc
      go  acc (Skip env x'    ) = go (if x == x' then acc + 1 else acc) env
      go  acc (Extend env x' _) = go (if x == x' then acc + 1 else acc) env
  
  instantiate :: Eq a => Closure a -> Val a -> Val a
  instantiate (Closure x env t) !u = eval (Extend env x u) t
  {-# INLINE instantiate #-}
  
  -- Out-of-env variables have negative de Bruijn levels.
  vVar :: Environment a -> Var -> Val a
  vVar env0 (V x i0) = go env0 i0
    where
      go (Extend env x' v) i
          | x == x' =
              if i == 0 then v else go env (i - 1)
          | otherwise =
              go env i
      go (Skip env x') i
          | x == x' =
              if i == 0 then VVar x (countEnvironment x env) else go env (i - 1)
          | otherwise =
              go env i
      go Empty i =
          VVar x (negate i - 1)
  
  vApp :: Eq a => Val a -> Val a -> Val a
  vApp !t !u =
      case t of
          VLam _ t'  -> instantiate t' u
          VHLam _ t' -> t' u
          t'        -> VApp t' u
  {-# INLINE vApp #-}
  
  vPrefer :: Eq a => Environment a -> Val a -> Val a -> Val a
  vPrefer env t u =
      case (t, u) of
          (VRecordLit m, u') | null m ->
              u'
          (t', VRecordLit m) | null m ->
              t'
          (VRecordLit m, VRecordLit m') ->
              VRecordLit (Map.union m' m)
          (t', u') | conv env t' u' ->
              t'
          (t', u') ->
              VPrefer t' u'
  {-# INLINE vPrefer #-}
  
  vCombine :: Maybe Text -> Val a -> Val a -> Val a
  vCombine mk t u =
      case (t, u) of
          (VRecordLit m, u') | null m ->
              u'
          (t', VRecordLit m) | null m ->
              t'
          (VRecordLit m, VRecordLit m') ->
              VRecordLit (Map.unionWith (vCombine Nothing) m m')
          (t', u') ->
              VCombine mk t' u'
  
  vCombineTypes :: Val a -> Val a -> Val a
  vCombineTypes t u =
      case (t, u) of
          (VRecord m, u') | null m ->
              u'
          (t', VRecord m) | null m ->
              t'
          (VRecord m, VRecord m') ->
              VRecord (Map.unionWith vCombineTypes m m')
          (t', u') ->
              VCombineTypes t' u'
  
  vListAppend :: Val a -> Val a -> Val a
  vListAppend t u =
      case (t, u) of
          (VListLit _ xs, u') | null xs ->
              u'
          (t', VListLit _ ys) | null ys ->
              t'
          (VListLit t' xs, VListLit _ ys) ->
              VListLit t' (xs <> ys)
          (t', u') ->
              VListAppend t' u'
  {-# INLINE vListAppend #-}
  
  vNaturalPlus :: Val a -> Val a -> Val a
  vNaturalPlus t u =
      case (t, u) of
          (VNaturalLit 0, u') ->
              u'
          (t', VNaturalLit 0) ->
              t'
          (VNaturalLit m, VNaturalLit n) ->
              VNaturalLit (m + n)
          (t', u') ->
              VNaturalPlus t' u'
  {-# INLINE vNaturalPlus #-}
  
  vField :: Val a -> Text -> Val a
  vField t0 k = go t0
    where
      go = \case
          VUnion m -> case Map.lookup k m of
              Just (Just _) -> VPrim $ \ ~u -> VInject m k (Just u)
              Just Nothing  -> VInject m k Nothing
              _             -> error errorMsg
          VRecordLit m
              | Just v <- Map.lookup k m -> v
              | otherwise -> error errorMsg
          VProject t _ -> go t
          VPrefer (VRecordLit m) r -> case Map.lookup k m of
              Just v -> VField (VPrefer (singletonVRecordLit v) r) k
              Nothing -> go r
          VPrefer l (VRecordLit m) -> case Map.lookup k m of
              Just v -> v
              Nothing -> go l
          VCombine mk (VRecordLit m) r -> case Map.lookup k m of
              Just v -> VField (VCombine mk (singletonVRecordLit v) r) k
              Nothing -> go r
          VCombine mk l (VRecordLit m) -> case Map.lookup k m of
              Just v -> VField (VCombine mk l (singletonVRecordLit v)) k
              Nothing -> go l
          t -> VField t k
  
      singletonVRecordLit v = VRecordLit (Map.singleton k v)
  {-# INLINE vField #-}
  
  vTextReplace :: Text -> Val a -> Text -> VChunks a
  vTextReplace needle replacement haystack = go haystack
    where
      go t
          | Text.null suffix = VChunks [] t
          | otherwise =
              let remainder = Text.drop (Text.length needle) suffix
  
                  rest = go remainder
  
              in  case replacement of
                      VTextLit replacementChunks ->
                          VChunks [] prefix <> replacementChunks <> rest
                      _ ->
                          VChunks [(prefix, replacement)] "" <> rest
        where
          (prefix, suffix) = Text.breakOn needle t
  
  vProjectByFields :: Eq a => Environment a -> Val a -> Set Text -> Val a
  vProjectByFields env t ks =
      if null ks
          then VRecordLit mempty
          else case t of
              VRecordLit kvs ->
                  let kvs' = Map.restrictKeys kvs (Dhall.Set.toSet ks)
                  in  VRecordLit kvs'
              VProject t' _ ->
                  vProjectByFields env t' ks
              VPrefer l (VRecordLit kvs) ->
                  let ksSet = Dhall.Set.toSet ks
  
                      kvs' = Map.restrictKeys kvs ksSet
  
                      ks' =
                          Dhall.Set.fromSet
                              (Data.Set.difference ksSet (Map.keysSet kvs'))
  
                  in  vPrefer env (vProjectByFields env l ks') (VRecordLit kvs')
              t' ->
                  VProject t' (Left ks)
  
  vWith :: Val a -> NonEmpty WithComponent -> Val a -> Val a
  vWith (VRecordLit kvs) (WithLabel k  :| []     ) v = VRecordLit (Map.insert k  v  kvs)
  vWith (VRecordLit kvs) (WithLabel k₀ :| k₁ : ks) v = VRecordLit (Map.insert k₀ e₂ kvs)
    where
      e₁ =
          case Map.lookup k₀ kvs of
              Nothing  -> VRecordLit mempty
              Just e₁' -> e₁'
  
      e₂ = vWith e₁ (k₁ :| ks) v
  vWith (VNone _T) (WithQuestion :| _      ) _ = VNone _T
  vWith (VSome  _) (WithQuestion :| []     ) v = VSome v
  vWith (VSome  t) (WithQuestion :| k₁ : ks) v = VSome (vWith t (k₁ :| ks) v)
  vWith e₀ ks v₀ = VWith e₀ ks v₀
  
  eval :: forall a. Eq a => Environment a -> Expr Void a -> Val a
  eval !env t0 =
      case t0 of
          Const k ->
              VConst k
          Var v ->
              vVar env v
          Lam _ (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = a }) t ->
              VLam (eval env a) (Closure x env t)
          Pi _ x a b ->
              VPi (eval env a) (Closure x env b)
          App t u ->
              vApp (eval env t) (eval env u)
          Let (Binding _ x _ _mA _ a) b ->
              let !env' = Extend env x (eval env a)
              in  eval env' b
          Annot t _ ->
              eval env t
          Bool ->
              VBool
          BoolLit b ->
              VBoolLit b
          BoolAnd t u ->
              case (eval env t, eval env u) of
                  (VBoolLit True, u')       -> u'
                  (VBoolLit False, _)       -> VBoolLit False
                  (t', VBoolLit True)       -> t'
                  (_ , VBoolLit False)      -> VBoolLit False
                  (t', u') | conv env t' u' -> t'
                  (t', u')                  -> VBoolAnd t' u'
          BoolOr t u ->
              case (eval env t, eval env u) of
                  (VBoolLit False, u')      -> u'
                  (VBoolLit True, _)        -> VBoolLit True
                  (t', VBoolLit False)      -> t'
                  (_ , VBoolLit True)       -> VBoolLit True
                  (t', u') | conv env t' u' -> t'
                  (t', u')                  -> VBoolOr t' u'
          BoolEQ t u ->
              case (eval env t, eval env u) of
                  (VBoolLit True, u')       -> u'
                  (t', VBoolLit True)       -> t'
                  (t', u') | conv env t' u' -> VBoolLit True
                  (t', u')                  -> VBoolEQ t' u'
          BoolNE t u ->
              case (eval env t, eval env u) of
                  (VBoolLit False, u')      -> u'
                  (t', VBoolLit False)      -> t'
                  (t', u') | conv env t' u' -> VBoolLit False
                  (t', u')                  -> VBoolNE t' u'
          BoolIf b t f ->
              case (eval env b, eval env t, eval env f) of
                  (VBoolLit True,  t', _ )            -> t'
                  (VBoolLit False, _ , f')            -> f'
                  (b', VBoolLit True, VBoolLit False) -> b'
                  (_, t', f') | conv env t' f'        -> t'
                  (b', t', f')                        -> VBoolIf b' t' f'
          Bytes ->
              VBytes
          BytesLit b ->
              VBytesLit b
          Natural ->
              VNatural
          NaturalLit n ->
              VNaturalLit n
          NaturalFold ->
              VPrim $ \n ->
              VPrim $ \natural ->
              VPrim $ \succ ->
              VPrim $ \zero ->
              let inert = VNaturalFold n natural succ zero
              in  case zero of
                  VPrimVar -> inert
                  _ -> case succ of
                      VPrimVar -> inert
                      _ -> case natural of
                          VPrimVar -> inert
                          _ -> case n of
                              VNaturalLit n' ->
                                  -- Use an `Integer` for the loop, due to the
                                  -- following issue:
                                  --
                                  -- https://github.com/ghcjs/ghcjs/issues/782
                                  go zero (fromIntegral n' :: Integer) where
                                    go !acc 0 = acc
                                    go acc m =
                                    -- Detect a shortcut: if succ acc == acc then return acc immediately.
                                      let next = vApp succ acc
                                      in  if conv env next acc then acc else go next (m - 1)
                              _ -> inert
          NaturalBuild ->
              VPrim $ \case
                  VPrimVar ->
                      VNaturalBuild VPrimVar
                  t ->       t
                      `vApp` VNatural
                      `vApp` VHLam (Typed "n" VNatural) (\n -> vNaturalPlus n (VNaturalLit 1))
                      `vApp` VNaturalLit 0
  
          NaturalIsZero -> VPrim $ \case
              VNaturalLit n -> VBoolLit (n == 0)
              n             -> VNaturalIsZero n
          NaturalEven -> VPrim $ \case
              VNaturalLit n -> VBoolLit (even n)
              n             -> VNaturalEven n
          NaturalOdd -> VPrim $ \case
              VNaturalLit n -> VBoolLit (odd n)
              n             -> VNaturalOdd n
          NaturalToInteger -> VPrim $ \case
              VNaturalLit n -> VIntegerLit (fromIntegral n)
              n             -> VNaturalToInteger n
          NaturalShow -> VPrim $ \case
              VNaturalLit n -> VTextLit (VChunks [] (Text.pack (show n)))
              n             -> VNaturalShow n
          NaturalSubtract -> VPrim $ \case
              VNaturalLit 0 ->
                  VHLam NaturalSubtractZero id
              x@(VNaturalLit m) ->
                  VPrim $ \case
                      VNaturalLit n
                          | n >= m ->
                              -- Use an `Integer` for the subtraction, due to the
                              -- following issue:
                              --
                              -- https://github.com/ghcjs/ghcjs/issues/782
                              VNaturalLit (fromIntegral (subtract (fromIntegral m :: Integer) (fromIntegral n :: Integer)))
                          | otherwise -> VNaturalLit 0
                      y -> VNaturalSubtract x y
              x ->
                  VPrim $ \case
                      VNaturalLit 0    -> VNaturalLit 0
                      y | conv env x y -> VNaturalLit 0
                      y                -> VNaturalSubtract x y
          NaturalPlus t u ->
              vNaturalPlus (eval env t) (eval env u)
          NaturalTimes t u ->
              case (eval env t, eval env u) of
                  (VNaturalLit 1, u'           ) -> u'
                  (t'           , VNaturalLit 1) -> t'
                  (VNaturalLit 0, _            ) -> VNaturalLit 0
                  (_            , VNaturalLit 0) -> VNaturalLit 0
                  (VNaturalLit m, VNaturalLit n) -> VNaturalLit (m * n)
                  (t'           , u'           ) -> VNaturalTimes t' u'
          Integer ->
              VInteger
          IntegerLit n ->
              VIntegerLit n
          IntegerClamp ->
              VPrim $ \case
                  VIntegerLit n
                      | 0 <= n    -> VNaturalLit (fromInteger n)
                      | otherwise -> VNaturalLit 0
                  n -> VIntegerClamp n
          IntegerNegate ->
              VPrim $ \case
                  VIntegerLit n -> VIntegerLit (negate n)
                  n             -> VIntegerNegate n
          IntegerShow ->
              VPrim $ \case
                  VIntegerLit n
                      | 0 <= n    -> VTextLit (VChunks [] (Text.pack ('+':show n)))
                      | otherwise -> VTextLit (VChunks [] (Text.pack (show n)))
                  n -> VIntegerShow n
          IntegerToDouble ->
              VPrim $ \case
                  VIntegerLit n -> VDoubleLit (DhallDouble (read (show n)))
                  -- `(read . show)` is used instead of `fromInteger`
                  -- because `read` uses the correct rounding rule.
                  -- See https://gitlab.haskell.org/ghc/ghc/issues/17231.
                  n             -> VIntegerToDouble n
          Double ->
              VDouble
          DoubleLit n ->
              VDoubleLit n
          DoubleShow ->
              VPrim $ \case
                  VDoubleLit (DhallDouble n) -> VTextLit (VChunks [] (Text.pack (show n)))
                  n                          -> VDoubleShow n
          Text ->
              VText
          TextLit cs ->
              case evalChunks cs of
                  VChunks [("", t)] "" -> t
                  vcs                  -> VTextLit vcs
          TextAppend t u ->
              eval env (TextLit (Chunks [("", t), ("", u)] ""))
          TextShow ->
              VPrim $ \case
                  VTextLit (VChunks [] x) -> VTextLit (VChunks [] (textShow x))
                  t                       -> VTextShow t
          TextReplace ->
              VPrim $ \needle ->
              let hLamInfo0 = case needle of
                      VTextLit (VChunks [] "") -> TextReplaceEmpty
                      _                        -> Prim
  
              in  VHLam hLamInfo0 $ \replacement ->
              let hLamInfo1 = case needle of
                      VTextLit (VChunks [] "") ->
                          TextReplaceEmptyArgument replacement
                      _ ->
                          Prim
              in  VHLam hLamInfo1 $ \haystack ->
                      case needle of
                          VTextLit (VChunks [] "") ->
                              haystack
  
                          VTextLit (VChunks [] needleText) ->
                              case haystack of
                                  VTextLit (VChunks [] haystackText) ->
                                      case replacement of
                                          VTextLit (VChunks [] replacementText) ->
                                              VTextLit $ VChunks []
                                                  (Text.replace
                                                      needleText
                                                      replacementText
                                                      haystackText
                                                  )
                                          _ ->
                                              VTextLit
                                                  (vTextReplace
                                                      needleText
                                                      replacement
                                                      haystackText
                                                  )
                                  _ ->
                                      VTextReplace needle replacement haystack
                          _ ->
                              VTextReplace needle replacement haystack
          Date ->
              VDate
          DateLiteral d ->
              VDateLiteral d
          DateShow ->
              VPrim $ \case
                  VDateLiteral d -> VTextLit (VChunks [] (dateShow d))
                  t              -> VDateShow t
          Time ->
              VTime
          TimeLiteral t p ->
              VTimeLiteral t p
          TimeShow ->
              VPrim $ \case
                  VTimeLiteral d p -> VTextLit (VChunks [] (timeShow d p))
                  t                -> VTimeShow t
          TimeZone ->
              VTimeZone
          TimeZoneLiteral z ->
              VTimeZoneLiteral z
          TimeZoneShow ->
              VPrim $ \case
                  VTimeZoneLiteral d -> VTextLit (VChunks [] (timezoneShow d))
                  t                  -> VTimeZoneShow t
          List ->
              VPrim VList
          ListLit ma ts ->
              VListLit (fmap (eval env) ma) (fmap (eval env) ts)
          ListAppend t u ->
              vListAppend (eval env t) (eval env u)
          ListBuild ->
              VPrim $ \a ->
              VPrim $ \case
                  VPrimVar ->
                      VListBuild a VPrimVar
                  t ->       t
                      `vApp` VList a
                      `vApp` VHLam (Typed "a" a) (\x ->
                             VHLam (Typed "as" (VList a)) (\as ->
                             vListAppend (VListLit Nothing (pure x)) as))
                      `vApp` VListLit (Just (VList a)) mempty
  
          ListFold ->
              VPrim $ \a ->
              VPrim $ \as ->
              VPrim $ \list ->
              VPrim $ \cons ->
              VPrim $ \nil ->
              let inert = VListFold a as list cons nil
              in  case nil of
                  VPrimVar -> inert
                  _ -> case cons of
                      VPrimVar -> inert
                      _ -> case list of
                          VPrimVar -> inert
                          _ -> case a of
                              VPrimVar -> inert
                              _ -> case as of
                                  VListLit _ as' ->
                                      foldr' (\x b -> cons `vApp` x `vApp` b) nil as'
                                  _ -> inert
          ListLength ->
              VPrim $ \ a ->
              VPrim $ \case
                  VListLit _ as -> VNaturalLit (fromIntegral (Sequence.length as))
                  as            -> VListLength a as
          ListHead ->
              VPrim $ \ a ->
              VPrim $ \case
                  VListLit _ as ->
                      case Sequence.viewl as of
                          y :< _ -> VSome y
                          _      -> VNone a
                  as ->
                      VListHead a as
          ListLast ->
              VPrim $ \ a ->
              VPrim $ \case
                  VListLit _ as ->
                      case Sequence.viewr as of
                          _ :> t -> VSome t
                          _      -> VNone a
                  as -> VListLast a as
          ListIndexed ->
              VPrim $ \ a ->
              VPrim $ \case
                  VListLit _ as ->
                      let a' =
                              if null as
                              then Just (VList (VRecord (Map.unorderedFromList [("index", VNatural), ("value", a)])))
                              else Nothing
  
                          as' =
                              Sequence.mapWithIndex
                                  (\i t ->
                                      VRecordLit
                                          (Map.unorderedFromList
                                              [ ("index", VNaturalLit (fromIntegral i))
                                              , ("value", t)
                                              ]
                                          )
                                  )
                                  as
  
                          in  VListLit a' as'
                  t ->
                      VListIndexed a t
          ListReverse ->
              VPrim $ \ ~a ->
              VPrim $ \case
                  VListLit t as | null as ->
                      VListLit t as
                  VListLit _ as ->
                      VListLit Nothing (Sequence.reverse as)
                  t ->
                      VListReverse a t
          Optional ->
              VPrim VOptional
          Some t ->
              VSome (eval env t)
          None ->
              VPrim $ \ ~a -> VNone a
          Record kts ->
              VRecord (Map.sort (eval env . recordFieldValue <$> kts))
          RecordLit kts ->
              VRecordLit (Map.sort (eval env . recordFieldValue <$> kts))
          Union kts ->
              VUnion (Map.sort (fmap (fmap (eval env)) kts))
          Combine _ mk t u ->
              vCombine mk (eval env t) (eval env u)
          CombineTypes _ t u ->
              vCombineTypes (eval env t) (eval env u)
          Prefer _ _ t u ->
              vPrefer env (eval env t) (eval env u)
          RecordCompletion t u ->
              eval env (Annot (Prefer mempty PreferFromCompletion (Field t def) u) (Field t typ))
            where
              def = Syntax.makeFieldSelection "default"
              typ = Syntax.makeFieldSelection "Type"
          Merge x y ma ->
              case (eval env x, eval env y, fmap (eval env) ma) of
                  (VRecordLit m, VInject _ k mt, _)
                      | Just f <- Map.lookup k m -> maybe f (vApp f) mt
                      | otherwise                -> error errorMsg
                  (VRecordLit m, VSome t, _)
                      | Just f <- Map.lookup "Some" m -> vApp f t
                      | otherwise                     -> error errorMsg
                  (VRecordLit m, VNone _, _)
                      | Just t <- Map.lookup "None" m -> t
                      | otherwise                     -> error errorMsg
                  (x', y', ma') -> VMerge x' y' ma'
          ToMap x ma ->
              case (eval env x, fmap (eval env) ma) of
                  (VRecordLit m, ma'@(Just _)) | null m ->
                      VListLit ma' Sequence.empty
                  (VRecordLit m, _) ->
                      let entry (k, v) =
                              VRecordLit
                                  (Map.unorderedFromList
                                      [ ("mapKey", VTextLit $ VChunks [] k)
                                      , ("mapValue", v)
                                      ]
                                  )
  
                          s = (Sequence.fromList . map entry . Map.toAscList) m
  
                      in  VListLit Nothing s
                  (x', ma') ->
                      VToMap x' ma'
          ShowConstructor x ->
              case eval env x of
                  VInject m k _
                      | Just _ <- Map.lookup k m -> VTextLit (VChunks [] k)
                      | otherwise                -> error errorMsg
                  VSome _ -> VTextLit (VChunks [] "Some")
                  VNone _ -> VTextLit (VChunks [] "None")
                  x' -> VShowConstructor x'
          Field t (Syntax.fieldSelectionLabel -> k) ->
              vField (eval env t) k
          Project t (Left ks) ->
              vProjectByFields env (eval env t) (Dhall.Set.sort (Dhall.Set.fromList ks))
          Project t (Right e) ->
              case eval env e of
                  VRecord kts ->
                      vProjectByFields env (eval env t) (Dhall.Set.fromSet (Map.keysSet kts))
                  e' ->
                      VProject (eval env t) (Right e')
          Assert t ->
              VAssert (eval env t)
          Equivalent _ t u ->
              VEquivalent (eval env t) (eval env u)
          With e₀ ks v ->
              vWith (eval env e₀) ks (eval env v)
          Note _ e ->
              eval env e
          ImportAlt t _ ->
              eval env t
          Embed a ->
              VEmbed a
    where
      evalChunks :: Chunks Void a -> VChunks a
      evalChunks (Chunks xys z) = foldr' cons nil xys
        where
          cons (x, t) vcs =
              case eval env t of
                  VTextLit vcs' -> VChunks [] x <> vcs' <> vcs
                  t'            -> VChunks [(x, t')] mempty <> vcs
  
          nil = VChunks [] z
      {-# INLINE evalChunks #-}
  
  eqListBy :: (a -> a -> Bool) -> [a] -> [a] -> Bool
  eqListBy f = go
    where
      go (x:xs) (y:ys) | f x y = go xs ys
      go [] [] = True
      go _  _  = False
  {-# INLINE eqListBy #-}
  
  eqMapsBy :: Ord k => (v -> v -> Bool) -> Map k v -> Map k v -> Bool
  eqMapsBy f mL mR =
      Map.size mL == Map.size mR
      && eqListBy eq (Map.toAscList mL) (Map.toAscList mR)
    where
      eq (kL, vL) (kR, vR) = kL == kR && f vL vR
  {-# INLINE eqMapsBy #-}
  
  eqMaybeBy :: (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
  eqMaybeBy f = go
    where
      go (Just x) (Just y) = f x y
      go Nothing  Nothing  = True
      go _        _        = False
  {-# INLINE eqMaybeBy #-}
  
  -- | Utility that powers the @Text/show@ built-in
  textShow :: Text -> Text
  textShow text = "\"" <> Text.concatMap f text <> "\""
    where
      f '"'  = "\\\""
      f '$'  = "\\u0024"
      f '\\' = "\\\\"
      f '\b' = "\\b"
      f '\n' = "\\n"
      f '\r' = "\\r"
      f '\t' = "\\t"
      f '\f' = "\\f"
      f c | c <= '\x1F' = Text.pack (Printf.printf "\\u%04x" (Data.Char.ord c))
          | otherwise   = Text.singleton c
  
  -- | Utility that powers the @Date/show@ built-in
  dateShow :: Day -> Text
  dateShow = Text.pack . Time.formatTime Time.defaultTimeLocale "%0Y-%m-%d"
  
  -- | Utility that powers the @Time/show@ built-in
  timeShow :: TimeOfDay -> Word -> Text
  timeShow (TimeOfDay hh mm seconds) precision =
      Text.pack (Printf.printf "%02d:%02d:%02d" hh mm ss <> suffix)
    where
      magnitude :: Integer
      magnitude = 10 ^ precision
  
      (ss, fraction) =
          truncate (seconds * fromInteger magnitude) `divMod` magnitude
  
      suffix
          | precision == 0 = ""
          | otherwise      = Printf.printf ".%0*d" precision fraction
  
  -- | Utility that powers the @TimeZone/show@ built-in
  timezoneShow :: TimeZone -> Text
  timezoneShow = Text.pack . Time.formatTime Time.defaultTimeLocale "%Ez"
  
  conv :: forall a. Eq a => Environment a -> Val a -> Val a -> Bool
  conv !env t0 t0' =
      case (t0, t0') of
          (VConst k, VConst k') ->
              k == k'
          (VVar x i, VVar x' i') ->
              x == x' && i == i'
          (VLam _ (freshClosure -> (x, v, t)), VLam _ t' ) ->
              convSkip x (instantiate t v) (instantiate t' v)
          (VLam _ (freshClosure -> (x, v, t)), VHLam _ t') ->
              convSkip x (instantiate t v) (t' v)
          (VLam _ (freshClosure -> (x, v, t)), t'        ) ->
              convSkip x (instantiate t v) (vApp t' v)
          (VHLam _ t, VLam _ (freshClosure -> (x, v, t'))) ->
              convSkip x (t v) (instantiate t' v)
          (VHLam _ t, VHLam _ t'                    ) ->
              let (x, v) = fresh "x" in convSkip x (t v) (t' v)
          (VHLam _ t, t'                            ) ->
              let (x, v) = fresh "x" in convSkip x (t v) (vApp t' v)
          (t, VLam _ (freshClosure -> (x, v, t'))) ->
              convSkip x (vApp t v) (instantiate t' v)
          (t, VHLam _ t'  ) ->
              let (x, v) = fresh "x" in convSkip x (vApp t v) (t' v)
          (VApp t u, VApp t' u') ->
              conv env t t' && conv env u u'
          (VPi a b, VPi a' (freshClosure -> (x, v, b'))) ->
              conv env a a' && convSkip x (instantiate b v) (instantiate b' v)
          (VPi a b, VHPi (fresh -> (x, v)) a' b') ->
              conv env a a' && convSkip x (instantiate b v) (b' v)
          (VHPi _ a b, VPi a' (freshClosure -> (x, v, b'))) ->
              conv env a a' && convSkip x (b v) (instantiate b' v)
          (VHPi _ a b, VHPi (fresh -> (x, v)) a' b') ->
              conv env a a' && convSkip x (b v) (b' v)
          (VBool, VBool) ->
              True
          (VBoolLit b, VBoolLit b') ->
              b == b'
          (VBoolAnd t u, VBoolAnd t' u') ->
              conv env t t' && conv env u u'
          (VBoolOr t u, VBoolOr t' u') ->
              conv env t t' && conv env u u'
          (VBoolEQ t u, VBoolEQ t' u') ->
              conv env t t' && conv env u u'
          (VBoolNE t u, VBoolNE t' u') ->
              conv env t t' && conv env u u'
          (VBoolIf t u v, VBoolIf t' u' v') ->
              conv env t t' && conv env u u' && conv env v v'
          (VBytes, VBytes) ->
              True
          (VBytesLit l, VBytesLit r) ->
              l == r
          (VNatural, VNatural) ->
              True
          (VNaturalLit n, VNaturalLit n') ->
              n == n'
          (VNaturalFold t _ u v, VNaturalFold t' _ u' v') ->
              conv env t t' && conv env u u' && conv env v v'
          (VNaturalBuild t, VNaturalBuild t') ->
              conv env t t'
          (VNaturalIsZero t, VNaturalIsZero t') ->
              conv env t t'
          (VNaturalEven t, VNaturalEven t') ->
              conv env t t'
          (VNaturalOdd t, VNaturalOdd t') ->
              conv env t t'
          (VNaturalToInteger t, VNaturalToInteger t') ->
              conv env t t'
          (VNaturalShow t, VNaturalShow t') ->
              conv env t t'
          (VNaturalSubtract x y, VNaturalSubtract x' y') ->
              conv env x x' && conv env y y'
          (VNaturalPlus t u, VNaturalPlus t' u') ->
              conv env t t' && conv env u u'
          (VNaturalTimes t u, VNaturalTimes t' u') ->
              conv env t t' && conv env u u'
          (VInteger, VInteger) ->
              True
          (VIntegerLit t, VIntegerLit t') ->
              t == t'
          (VIntegerClamp t, VIntegerClamp t') ->
              conv env t t'
          (VIntegerNegate t, VIntegerNegate t') ->
              conv env t t'
          (VIntegerShow t, VIntegerShow t') ->
              conv env t t'
          (VIntegerToDouble t, VIntegerToDouble t') ->
              conv env t t'
          (VDouble, VDouble) ->
              True
          (VDoubleLit n, VDoubleLit n') ->
              n == n'
          (VDoubleShow t, VDoubleShow t') ->
              conv env t t'
          (VText, VText) ->
              True
          (VTextLit cs, VTextLit cs') ->
              convChunks cs cs'
          (VTextAppend t u, VTextAppend t' u') ->
              conv env t t' && conv env u u'
          (VTextShow t, VTextShow t') ->
              conv env t t'
          (VTextReplace a b c, VTextReplace a' b' c') ->
              conv env a a' && conv env b b' && conv env c c'
          (VDate, VDate) ->
              True
          (VDateLiteral l, VDateLiteral r) ->
              l == r
          (VDateShow t, VDateShow t') ->
              conv env t t'
          (VTime, VTime) ->
              True
          (VTimeLiteral tl pl, VTimeLiteral tr pr) ->
              tl == tr && pl == pr
          (VTimeShow t, VTimeShow t') ->
              conv env t t'
          (VTimeZone, VTimeZone) ->
              True
          (VTimeZoneLiteral l, VTimeZoneLiteral r) ->
              l == r
          (VTimeZoneShow t, VTimeZoneShow t') ->
              conv env t t'
          (VList a, VList a') ->
              conv env a a'
          (VListLit _ xs, VListLit _ xs') ->
              eqListBy (conv env) (toList xs) (toList xs')
          (VListAppend t u, VListAppend t' u') ->
              conv env t t' && conv env u u'
          (VListBuild _ t, VListBuild _ t') ->
              conv env t t'
          (VListLength a t, VListLength a' t') ->
              conv env a a' && conv env t t'
          (VListHead _ t, VListHead _ t') ->
              conv env t t'
          (VListLast _ t, VListLast _ t') ->
              conv env t t'
          (VListIndexed _ t, VListIndexed _ t') ->
              conv env t t'
          (VListReverse _ t, VListReverse _ t') ->
              conv env t t'
          (VListFold a l _ t u, VListFold a' l' _ t' u') ->
              conv env a a' && conv env l l' && conv env t t' && conv env u u'
          (VOptional a, VOptional a') ->
              conv env a a'
          (VSome t, VSome t') ->
              conv env t t'
          (VNone _, VNone _) ->
              True
          (VRecord m, VRecord m') ->
              eqMapsBy (conv env) m m'
          (VRecordLit m, VRecordLit m') ->
              eqMapsBy (conv env) m m'
          (VUnion m, VUnion m') ->
              eqMapsBy (eqMaybeBy (conv env)) m m'
          (VCombine _ t u, VCombine _ t' u') ->
              conv env t t' && conv env u u'
          (VCombineTypes t u, VCombineTypes t' u') ->
              conv env t t' && conv env u u'
          (VPrefer t u, VPrefer t' u') ->
              conv env t t' && conv env u u'
          (VMerge t u _, VMerge t' u' _) ->
              conv env t t' && conv env u u'
          (VToMap t _, VToMap t' _) ->
              conv env t t'
          (VShowConstructor t, VShowConstructor t') ->
              conv env t t'
          (VField t k, VField t' k') ->
              conv env t t' && k == k'
          (VProject t (Left ks), VProject t' (Left ks')) ->
              conv env t t' && ks == ks'
          (VProject t (Right e), VProject t' (Right e')) ->
              conv env t t' && conv env e e'
          (VAssert t, VAssert t') ->
              conv env t t'
          (VEquivalent t u, VEquivalent t' u') ->
              conv env t t' && conv env u u'
          (VInject m k mt, VInject m' k' mt') ->
              eqMapsBy (eqMaybeBy (conv env)) m m' && k == k' && eqMaybeBy (conv env) mt mt'
          (VEmbed a, VEmbed a') ->
              a == a'
          (_, _) ->
              False
    where
      fresh :: Text -> (Text, Val a)
      fresh x = (x, VVar x (countEnvironment x env))
      {-# INLINE fresh #-}
  
      freshClosure :: Closure a -> (Text, Val a, Closure a)
      freshClosure closure@(Closure x _ _) = (x, snd (fresh x), closure)
      {-# INLINE freshClosure #-}
  
      convChunks :: VChunks a -> VChunks a -> Bool
      convChunks (VChunks xys z) (VChunks xys' z') =
        eqListBy (\(x, y) (x', y') -> x == x' && conv env y y') xys xys' && z == z'
      {-# INLINE convChunks #-}
  
      convSkip :: Text -> Val a -> Val a -> Bool
      convSkip x = conv (Skip env x)
      {-# INLINE convSkip #-}
  
  judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool
  judgmentallyEqual (Syntax.denote -> t) (Syntax.denote -> u) =
      conv Empty (eval Empty t) (eval Empty u)
  {-# INLINABLE judgmentallyEqual #-}
  
  data Names
    = EmptyNames
    | Bind !Names {-# UNPACK #-} !Text
    deriving Show
  
  envNames :: Environment a -> Names
  envNames Empty = EmptyNames
  envNames (Skip   env x  ) = Bind (envNames env) x
  envNames (Extend env x _) = Bind (envNames env) x
  
  countNames :: Text -> Names -> Int
  countNames x = go 0
    where
      go !acc EmptyNames         = acc
      go  acc (Bind env x') = go (if x == x' then acc + 1 else acc) env
  
  -- | Quote a value into beta-normal form.
  quote :: forall a. Eq a => Names -> Val a -> Expr Void a
  quote !env !t0 =
      case t0 of
          VConst k ->
              Const k
          VVar !x !i ->
              Var (V x (countNames x env - i - 1))
          VApp t u ->
              quote env t `qApp` u
          VLam a (freshClosure -> (x, v, t)) ->
              Lam
                  mempty
                  (Syntax.makeFunctionBinding x (quote env a))
                  (quoteBind x (instantiate t v))
          VHLam i t ->
              case i of
                  Typed (fresh -> (x, v)) a ->
                      Lam mempty
                          (Syntax.makeFunctionBinding x (quote env a))
                          (quoteBind x (t v))
                  Prim ->
                      quote env (t VPrimVar)
                  NaturalSubtractZero ->
                      App NaturalSubtract (NaturalLit 0)
                  TextReplaceEmpty ->
                      App TextReplace (TextLit (Chunks [] ""))
                  TextReplaceEmptyArgument replacement ->
                      App (App TextReplace (TextLit (Chunks [] "")))
                          (quote env replacement)
  
          VPi a (freshClosure -> (x, v, b)) ->
              Pi mempty x (quote env a) (quoteBind x (instantiate b v))
          VHPi (fresh -> (x, v)) a b ->
              Pi mempty x (quote env a) (quoteBind x (b v))
          VBool ->
              Bool
          VBoolLit b ->
              BoolLit b
          VBoolAnd t u ->
              BoolAnd (quote env t) (quote env u)
          VBoolOr t u ->
              BoolOr (quote env t) (quote env u)
          VBoolEQ t u ->
              BoolEQ (quote env t) (quote env u)
          VBoolNE t u ->
              BoolNE (quote env t) (quote env u)
          VBoolIf t u v ->
              BoolIf (quote env t) (quote env u) (quote env v)
          VBytes ->
              Bytes
          VBytesLit b ->
              BytesLit b
          VNatural ->
              Natural
          VNaturalLit n ->
              NaturalLit n
          VNaturalFold a t u v ->
              NaturalFold `qApp` a `qApp` t `qApp` u `qApp` v
          VNaturalBuild t ->
              NaturalBuild `qApp` t
          VNaturalIsZero t ->
              NaturalIsZero `qApp` t
          VNaturalEven t ->
              NaturalEven `qApp` t
          VNaturalOdd t ->
              NaturalOdd `qApp` t
          VNaturalToInteger t ->
              NaturalToInteger `qApp` t
          VNaturalShow t ->
              NaturalShow `qApp` t
          VNaturalPlus t u ->
              NaturalPlus (quote env t) (quote env u)
          VNaturalTimes t u ->
              NaturalTimes (quote env t) (quote env u)
          VNaturalSubtract x y ->
              NaturalSubtract `qApp` x `qApp` y
          VInteger ->
              Integer
          VIntegerLit n ->
              IntegerLit n
          VIntegerClamp t ->
              IntegerClamp `qApp` t
          VIntegerNegate t ->
              IntegerNegate `qApp` t
          VIntegerShow t ->
              IntegerShow `qApp` t
          VIntegerToDouble t ->
              IntegerToDouble `qApp` t
          VDouble ->
              Double
          VDoubleLit n ->
              DoubleLit n
          VDoubleShow t ->
              DoubleShow `qApp` t
          VText ->
              Text
          VTextLit (VChunks xys z) ->
              TextLit (Chunks (fmap (fmap (quote env)) xys) z)
          VTextAppend t u ->
              TextAppend (quote env t) (quote env u)
          VTextShow t ->
              TextShow `qApp` t
          VTextReplace a b c ->
              TextReplace `qApp` a `qApp` b `qApp` c
          VDate ->
              Date
          VDateLiteral d ->
              DateLiteral d
          VDateShow t ->
              DateShow `qApp` t
          VTime ->
              Time
          VTimeLiteral t p ->
              TimeLiteral t p
          VTimeShow t ->
              TimeShow `qApp` t
          VTimeZone ->
              TimeZone
          VTimeZoneLiteral z ->
              TimeZoneLiteral z
          VTimeZoneShow t ->
              TimeZoneShow `qApp` t
          VList t ->
              List `qApp` t
          VListLit ma ts ->
              ListLit (fmap (quote env) ma) (fmap (quote env) ts)
          VListAppend t u ->
              ListAppend (quote env t) (quote env u)
          VListBuild a t ->
              ListBuild `qApp` a `qApp` t
          VListFold a l t u v ->
              ListFold `qApp` a `qApp` l `qApp` t `qApp` u `qApp` v
          VListLength a t ->
              ListLength `qApp` a `qApp` t
          VListHead a t ->
              ListHead `qApp` a `qApp` t
          VListLast a t ->
              ListLast `qApp` a `qApp` t
          VListIndexed a t ->
              ListIndexed `qApp` a `qApp` t
          VListReverse a t ->
              ListReverse `qApp` a `qApp` t
          VOptional a ->
              Optional `qApp` a
          VSome t ->
              Some (quote env t)
          VNone t ->
              None `qApp` t
          VRecord m ->
              Record (fmap quoteRecordField m)
          VRecordLit m ->
              RecordLit (fmap quoteRecordField m)
          VUnion m ->
              Union (fmap (fmap (quote env)) m)
          VCombine mk t u ->
              Combine mempty mk (quote env t) (quote env u)
          VCombineTypes t u ->
              CombineTypes mempty (quote env t) (quote env u)
          VPrefer t u ->
              Prefer mempty PreferFromSource (quote env t) (quote env u)
          VMerge t u ma ->
              Merge (quote env t) (quote env u) (fmap (quote env) ma)
          VToMap t ma ->
              ToMap (quote env t) (fmap (quote env) ma)
          VShowConstructor t ->
              ShowConstructor (quote env t)
          VField t k ->
              Field (quote env t) $ Syntax.makeFieldSelection k
          VProject t p ->
              Project (quote env t) (first Dhall.Set.toList (fmap (quote env) p))
          VAssert t ->
              Assert (quote env t)
          VEquivalent t u ->
              Equivalent mempty (quote env t) (quote env u)
          VWith e ks v ->
              With (quote env e) ks (quote env v)
          VInject m k Nothing ->
              Field (Union (fmap (fmap (quote env)) m)) $ Syntax.makeFieldSelection k
          VInject m k (Just t) ->
              Field (Union (fmap (fmap (quote env)) m)) (Syntax.makeFieldSelection k) `qApp` t
          VEmbed a ->
              Embed a
          VPrimVar ->
              error errorMsg
    where
      fresh :: Text -> (Text, Val a)
      fresh x = (x, VVar x (countNames x env))
      {-# INLINE fresh #-}
  
      freshClosure :: Closure a -> (Text, Val a, Closure a)
      freshClosure closure@(Closure x _ _) = (x, snd (fresh x), closure)
      {-# INLINE freshClosure #-}
  
      quoteBind :: Text -> Val a -> Expr Void a
      quoteBind x = quote (Bind env x)
      {-# INLINE quoteBind #-}
  
      qApp :: Expr Void a -> Val a -> Expr Void a
      qApp t VPrimVar = t
      qApp t u        = App t (quote env u)
      {-# INLINE qApp #-}
  
      quoteRecordField :: Val a -> RecordField Void a
      quoteRecordField = Syntax.makeRecordField . quote env
      {-# INLINE quoteRecordField #-}
  
  -- | Normalize an expression in an environment of values. Any variable pointing out of
  --   the environment is treated as opaque free variable.
  nf :: Eq a => Environment a -> Expr s a -> Expr t a
  nf !env = Syntax.renote . quote (envNames env) . eval env . Syntax.denote
  
  normalize :: Eq a => Expr s a -> Expr t a
  normalize = nf Empty
  {-# INLINABLE normalize #-}
  
  alphaNormalize :: Expr s a -> Expr s a
  alphaNormalize = goEnv EmptyNames
    where
      goVar :: Names -> Text -> Int -> Expr s a
      goVar e topX topI = go 0 e topI
        where
          go !acc (Bind env x) !i
            | x == topX = if i == 0 then Var (V "_" acc) else go (acc + 1) env (i - 1)
            | otherwise = go (acc + 1) env i
          go _ EmptyNames i = Var (V topX i)
  
      goEnv :: Names -> Expr s a -> Expr s a
      goEnv !e0 t0 =
          case t0 of
              Const k ->
                  Const k
              Var (V x i) ->
                  goVar e0 x i
              Lam cs (FunctionBinding src0 x src1 src2 t) u ->
                  Lam cs (FunctionBinding src0 "_" src1 src2 (go t)) (goBind x u)
              Pi cs x a b ->
                  Pi cs "_" (go a) (goBind x b)
              App t u ->
                  App (go t) (go u)
              Let (Binding src0 x src1 mA src2 a) b ->
                  Let (Binding src0 "_" src1 (fmap (fmap go) mA) src2 (go a)) (goBind x b)
              Annot t u ->
                  Annot (go t) (go u)
              Bool ->
                  Bool
              BoolLit b ->
                  BoolLit b
              BoolAnd t u ->
                  BoolAnd (go t) (go u)
              BoolOr t u ->
                  BoolOr  (go t) (go u)
              BoolEQ t u ->
                  BoolEQ  (go t) (go u)
              BoolNE t u ->
                  BoolNE  (go t) (go u)
              BoolIf b t f ->
                  BoolIf  (go b) (go t) (go f)
              Bytes ->
                  Bytes
              BytesLit b ->
                  BytesLit b
              Natural ->
                  Natural
              NaturalLit n ->
                  NaturalLit n
              NaturalFold ->
                  NaturalFold
              NaturalBuild ->
                  NaturalBuild
              NaturalIsZero ->
                  NaturalIsZero
              NaturalEven ->
                  NaturalEven
              NaturalOdd ->
                  NaturalOdd
              NaturalToInteger ->
                  NaturalToInteger
              NaturalShow ->
                  NaturalShow
              NaturalSubtract ->
                  NaturalSubtract
              NaturalPlus t u ->
                  NaturalPlus (go t) (go u)
              NaturalTimes t u ->
                  NaturalTimes (go t) (go u)
              Integer ->
                  Integer
              IntegerLit n ->
                  IntegerLit n
              IntegerClamp ->
                  IntegerClamp
              IntegerNegate ->
                  IntegerNegate
              IntegerShow ->
                  IntegerShow
              IntegerToDouble ->
                  IntegerToDouble
              Double ->
                  Double
              DoubleLit n ->
                  DoubleLit n
              DoubleShow ->
                  DoubleShow
              Text ->
                  Text
              TextLit cs ->
                  TextLit (goChunks cs)
              TextAppend t u ->
                  TextAppend (go t) (go u)
              TextShow ->
                  TextShow
              TextReplace ->
                  TextReplace
              Date ->
                  Date
              DateLiteral d ->
                  DateLiteral d
              DateShow ->
                  DateShow
              Time ->
                  Time
              TimeLiteral t p ->
                  TimeLiteral t p
              TimeShow ->
                  TimeShow
              TimeZone ->
                  TimeZone
              TimeZoneLiteral z ->
                  TimeZoneLiteral z
              TimeZoneShow ->
                  TimeZoneShow
              List ->
                  List
              ListLit ma ts ->
                  ListLit (fmap go ma) (fmap go ts)
              ListAppend t u ->
                  ListAppend (go t) (go u)
              ListBuild ->
                  ListBuild
              ListFold ->
                  ListFold
              ListLength ->
                  ListLength
              ListHead ->
                  ListHead
              ListLast ->
                  ListLast
              ListIndexed ->
                  ListIndexed
              ListReverse ->
                  ListReverse
              Optional ->
                  Optional
              Some t ->
                  Some (go t)
              None ->
                  None
              Record kts ->
                  Record (goRecordField <$> kts)
              RecordLit kts ->
                  RecordLit (goRecordField <$> kts)
              Union kts ->
                  Union (fmap (fmap go) kts)
              Combine cs m t u ->
                  Combine cs m (go t) (go u)
              CombineTypes cs t u ->
                  CombineTypes cs (go t) (go u)
              Prefer cs b t u ->
                  Prefer cs b (go t) (go u)
              RecordCompletion t u ->
                  RecordCompletion (go t) (go u)
              Merge x y ma ->
                  Merge (go x) (go y) (fmap go ma)
              ToMap x ma ->
                  ToMap (go x) (fmap go ma)
              ShowConstructor x ->
                  ShowConstructor (go x)
              Field t k ->
                  Field (go t) k
              Project t ks ->
                  Project (go t) (fmap go ks)
              Assert t ->
                  Assert (go t)
              Equivalent cs t u ->
                  Equivalent cs (go t) (go u)
              With e k v ->
                  With (go e) k (go v)
              Note s e ->
                  Note s (go e)
              ImportAlt t u ->
                  ImportAlt (go t) (go u)
              Embed a ->
                  Embed a
        where
          go                     = goEnv e0
          goBind x               = goEnv (Bind e0 x)
          goChunks (Chunks ts x) = Chunks (fmap (fmap go) ts) x
          goRecordField (RecordField s0 e s1 s2) = RecordField s0 (go e) s1 s2
  