content: {-# OPTIONS_GHC -Wunused-imports #-}
  
  {-# LANGUAGE NondecreasingIndentation #-}
  
  module Agda.TypeChecking.Rules.Builtin
    ( bindBuiltin
    , bindBuiltinNoDef
    , builtinKindOfName
    , bindPostulatedName
    , isUntypedBuiltin
    , bindUntypedBuiltin
    ) where
  
  import Prelude hiding (null)
  
  import Control.Monad.Except      ( catchError )
  import Control.Monad.Trans.Maybe
  
  import Data.List (find, sortBy)
  import Data.Function (on)
  
  import Agda.Interaction.Options.Base
  
  import qualified Agda.Syntax.Abstract as A
  import Agda.Syntax.Common
  import Agda.Syntax.Internal
  import Agda.Syntax.Position
  import Agda.Syntax.Scope.Base
  
  import Agda.TypeChecking.Monad
  
  import qualified Agda.TypeChecking.CompiledClause as CC
  import Agda.TypeChecking.Conversion
  import Agda.TypeChecking.Constraints ( noConstraints )
  import Agda.TypeChecking.Functions
  import Agda.TypeChecking.Names
  import Agda.TypeChecking.Pretty
  import Agda.TypeChecking.Primitive
  import Agda.TypeChecking.Positivity.Occurrence
  import Agda.TypeChecking.Reduce
  import Agda.TypeChecking.Substitute
  import Agda.TypeChecking.Telescope
  import Agda.TypeChecking.Warnings
  
  import {-# SOURCE #-} Agda.TypeChecking.Rules.Term ( checkExpr , inferExpr )
  import {-# SOURCE #-} Agda.TypeChecking.Rules.Builtin.Coinduction
  import {-# SOURCE #-} Agda.TypeChecking.Rewriting
  
  import Agda.Utils.Functor
  import Agda.Utils.List
  import Agda.Utils.List1 (pattern (:|))
  import Agda.Utils.Maybe
  import Agda.Utils.Monad
  import Agda.Utils.Null
  import Agda.Utils.Size
  
  import Agda.Utils.Impossible
  
  ---------------------------------------------------------------------------
  -- * Checking builtin pragmas
  ---------------------------------------------------------------------------
  
  builtinPostulate :: TCM Type -> BuiltinDescriptor
  builtinPostulate = BuiltinPostulate relevant
  
  builtinPostulateC :: Cubical -> TCM Type -> BuiltinDescriptor
  builtinPostulateC c m =
    builtinPostulate $ requireCubical c >> m
  
  findBuiltinInfo :: BuiltinId -> Maybe BuiltinInfo
  findBuiltinInfo b = find ((b ==) . builtinName) coreBuiltins
  
  coreBuiltins :: [BuiltinInfo]
  coreBuiltins =
    [ (builtinList                             |-> BuiltinData (tset --> tset) [builtinNil, builtinCons])
    , (builtinArg                              |-> BuiltinData (tset --> tset) [builtinArgArg])
    , (builtinAbs                              |-> BuiltinData (tset --> tset) [builtinAbsAbs])
    , (builtinArgInfo                          |-> BuiltinData tset [builtinArgArgInfo])
    , (builtinBool                             |-> BuiltinData tset [builtinTrue, builtinFalse])
    , (builtinNat                              |-> BuiltinData tset [builtinZero, builtinSuc])
    , (builtinMaybe                            |-> BuiltinData (tset --> tset) [builtinNothing, builtinJust])
    , (builtinSigma                            |-> BuiltinData (runNamesT [] $
                                                                hPi' "la" (el $ cl primLevel) $ \ a ->
                                                                hPi' "lb" (el $ cl primLevel) $ \ b ->
                                                                nPi' "A" (sort . tmSort <$> a) $ \bA ->
                                                                nPi' "B" (el' a bA --> (sort . tmSort <$> b)) $ \bB ->
                                                                ((sort . tmSort) <$> (cl primLevelMax <@> a <@> b))
                                                                )
                                                               [BuiltinSigmaCon])
    , (builtinUnit                             |-> BuiltinData tset [builtinUnitUnit])  -- actually record, but they are treated the same
    , (builtinAgdaLiteral                      |-> BuiltinData tset [builtinAgdaLitNat, builtinAgdaLitWord64, builtinAgdaLitFloat,
                                                                     builtinAgdaLitChar, builtinAgdaLitString,
                                                                     builtinAgdaLitQName, builtinAgdaLitMeta])
    , (builtinAgdaPattern                      |-> BuiltinData tset [builtinAgdaPatVar, builtinAgdaPatCon, builtinAgdaPatDot,
                                                                     builtinAgdaPatLit, builtinAgdaPatProj, builtinAgdaPatAbsurd])
    , (builtinAgdaPatVar                       |-> BuiltinDataCons (tnat --> tpat))
    , (builtinAgdaPatCon                       |-> BuiltinDataCons (tqname --> tlist (targ tpat) --> tpat))
    , (builtinAgdaPatDot                       |-> BuiltinDataCons (tterm --> tpat))
    , (builtinAgdaPatLit                       |-> BuiltinDataCons (tliteral --> tpat))
    , (builtinAgdaPatProj                      |-> BuiltinDataCons (tqname --> tpat))
    , (builtinAgdaPatAbsurd                    |-> BuiltinDataCons (tnat --> tpat))
    , (builtinLevel                            |-> builtinPostulate tLevelUniv)
    , (builtinWord64                           |-> builtinPostulate tset)
    , (builtinInteger                          |-> BuiltinData tset [builtinIntegerPos, builtinIntegerNegSuc])
    , (builtinIntegerPos                       |-> BuiltinDataCons (tnat --> tinteger))
    , (builtinIntegerNegSuc                    |-> BuiltinDataCons (tnat --> tinteger))
    , (builtinFloat                            |-> builtinPostulate tset)
    , (builtinChar                             |-> builtinPostulate tset)
    , (builtinString                           |-> builtinPostulate tset)
    , (builtinQName                            |-> builtinPostulate tset)
    , (builtinAgdaMeta                         |-> builtinPostulate tset)
    , (builtinIO                               |-> builtinPostulate (tset --> tset))
    , (builtinPath                             |-> BuiltinUnknown
                                                               (Just $ requireCubical CErased >>
                                                               hPi "a" (el primLevel) (
                                                                hPi "A" (return $ sort $ varSort 0) $
                                                                (El (varSort 1) <$> varM 0) -->
                                                                (El (varSort 1) <$> varM 0) -->
                                                                return (sort $ varSort 1)))
                                                               verifyPath)
    , (builtinPathP                            |-> builtinPostulateC CErased (hPi "a" (el primLevel) $
                                                                nPi "A" (tinterval --> return (sort $ varSort 0)) $
                                                                (El (varSort 1) <$> varM 0 <@> primIZero) -->
                                                                (El (varSort 1) <$> varM 0 <@> primIOne) -->
                                                                return (sort $ varSort 1)))
    , (builtinIntervalUniv                     |-> BuiltinSort SortIntervalUniv)
    , (builtinInterval                         |-> BuiltinData (requireCubical CErased >>
                                                                return (sort IntervalUniv)) [builtinIZero,builtinIOne])
    , (builtinSub                              |-> builtinPostulateC CErased (runNamesT [] $ hPi' "a" (el $ cl primLevel) $ \ a ->
                                                                     nPi' "A" (el' (cl primLevelSuc <@> a) (Sort . tmSort <$> a)) $ \ bA ->
                                                                     nPi' "φ" (cl tinterval) $ \ phi ->
                                                                     el's a (cl primPartial <#> a <@> phi <@> bA) --> (ssort . atomicLevel <$> a)
                                                                    ))
    , (builtinSubIn                            |-> builtinPostulateC CErased (runNamesT [] $
                                                                     hPi' "a" (el $ cl primLevel) $ \ a ->
                                                                     hPi' "A" (el' (cl primLevelSuc <@> a) (Sort . tmSort <$> a)) $ \ bA ->
                                                                     hPi' "φ" (cl tinterval) $ \ phi ->
                                                                     nPi' "x" (el' a bA) $ \ x ->
                                                                     el's a $ cl primSub <#> a <@> bA <@> phi <@> lam "o" (\ _ -> x)))
    , (builtinIZero                            |-> BuiltinDataCons tinterval)
    , (builtinIOne                             |-> BuiltinDataCons tinterval)
    , (builtinPartial                          |-> BuiltinPrim PrimPartial (const $ return ()))
    , (builtinPartialP                         |-> BuiltinPrim PrimPartialP (const $ return ()))
    , (builtinIsOne                            |-> builtinPostulateC CErased (tinterval --> return (ssort $ ClosedLevel 0)))
    , (builtinItIsOne                          |-> builtinPostulateC CErased (elSSet $ primIsOne <@> primIOne))
    , (builtinIsOne1                           |-> builtinPostulateC CErased (runNamesT [] $
                                                                     nPi' "i" (cl tinterval) $ \ i ->
                                                                     nPi' "j" (cl tinterval) $ \ j ->
                                                                     nPi' "i1" (elSSet $ cl primIsOne <@> i) $ \ i1 ->
                                                                     (elSSet $ cl primIsOne <@> (cl primIMax <@> i <@> j))))
    , (builtinIsOne2                           |-> builtinPostulateC CErased (runNamesT [] $
                                                                     nPi' "i" (cl tinterval) $ \ i ->
                                                                     nPi' "j" (cl tinterval) $ \ j ->
                                                                     nPi' "j1" (elSSet $ cl primIsOne <@> j) $ \ j1 ->
                                                                     (elSSet $ cl primIsOne <@> (cl primIMax <@> i <@> j))))
    , (builtinIsOneEmpty                       |-> builtinPostulateC CErased (runNamesT [] $
                                                                     hPi' "l" (el $ cl primLevel) $ \ l ->
                                                                     hPi' "A" (pPi' "o" (cl primIZero) $ \ _ ->
                                                                                    el' (cl primLevelSuc <@> l) (Sort . tmSort <$> l)) $ \ bA ->
                                                                     pPi' "o" (cl primIZero) (\ o ->
                                                                          el' l $ gApply' defaultIrrelevantArgInfo bA o)))
  
    , (builtinEquiv                            |-> BuiltinUnknown (Just $ requireCubical CErased >> runNamesT [] (
                                                                      hPi' "l" (el $ cl primLevel) $ \ a ->
                                                                      hPi' "l'" (el $ cl primLevel) $ \ b ->
                                                                      nPi' "A" (sort . tmSort <$> a) $ \bA ->
                                                                      nPi' "B" (sort . tmSort <$> b) $ \bB ->
                                                                      ((sort . tmSort) <$> (cl primLevelMax <@> a <@> b))
                                                                    ))
                                                                     (const $ const $ return ()))
    , (builtinEquivFun                         |-> BuiltinUnknown (Just $ requireCubical CErased >> runNamesT [] (
                                                                   hPi' "l" (el $ cl primLevel) $ \ a ->
                                                                   hPi' "l'" (el $ cl primLevel) $ \ b ->
                                                                   hPi' "A" (sort . tmSort <$> a) $ \bA ->
                                                                   hPi' "B" (sort . tmSort <$> b) $ \bB ->
                                                                   el' (cl primLevelMax <@> a <@> b) (cl primEquiv <#> a <#> b <@> bA <@> bB) -->
                                                                   (el' a bA --> el' b bB)
                                                                 ))
                                                                  (const $ const $ return ()))
    , (builtinEquivProof                       |-> BuiltinUnknown (Just $ requireCubical CErased >> runNamesT [] (
                                                                 hPi' "l" (el $ cl primLevel) $ \ la ->
                                                                 hPi' "l'" (el $ cl primLevel) $ \ lb ->
                                                                 nPi' "A" (sort . tmSort <$> la) $ \ bA ->
                                                                 nPi' "B" (sort . tmSort <$> lb) $ \ bB ->
                                                                 nPi' "e" (el' (cl primLevelMax <@> la <@> lb)
                                                                               (cl primEquiv <#> la <#> lb <@> bA <@> bB)) $ \ e -> do
                                                                 nPi' "b" (el' lb bB) $ \ b -> do
                                                                  let f = cl primEquivFun <#> la <#> lb <#> bA <#> bB <@> e
                                                                      lub = cl primLevelMax <@> la <@> lb
                                                                      fiber = el' lub
                                                                                  (cl primSigma <#> la <#> lb
                                                                                    <@> bA
                                                                                    <@> lam "a" (\ a ->
                                                                                           cl primPath <#> lb <#> bB <@> (f <@> a) <@> b))
                                                                  nPi' "φ" (cl tinterval) $ \ phi ->
                                                                    nPi' "f" (pPi' "o" phi (\ o -> fiber)) $ \ pfib ->
                                                                      el' lub (cl primSub <#> lub <#> fmap unEl fiber <@> phi <@> pfib)
                                                               ))
                                                                (const $ const $ return ()))
    , (builtinTranspProof                       |-> BuiltinUnknown (Just $ requireCubical CErased >> runNamesT [] (
                                                                 hPi' "l" (el $ cl primLevel) $ \ la -> do
                                                                 nPi' "e" (cl tinterval --> (sort . tmSort <$> la)) $ \ e -> do
                                                                 let lb = la; bA = e <@> cl primIZero; bB = e <@> cl primIOne
                                                                 nPi' "φ" (cl tinterval) $ \ phi -> do
                                                                 nPi' "a" (pPi' "o" phi (\ _ -> el' la bA)) $ \ a -> do
                                                                 let f = cl primTrans <#> lam "i" (\ _ -> la) <@> e <@> cl primIZero
                                                                     z = ilam "o" $ \ o -> f <@> (a <@> o)
                                                                 nPi' "b" (el's lb (cl primSub <#> lb <@> bB <@> phi <@> z)) $ \ b' -> do
                                                                 let b = cl primSubOut <#> lb <#> bB <#> phi <#> z <@> b'
                                                                     fiber = el' la
                                                                                 (cl primSigma <#> la <#> lb
                                                                                    <@> bA
                                                                                    <@> lam "a" (\ a ->
                                                                                           cl primPath <#> lb <#> bB <@> (f <@> a) <@> b))
                                                                 fiber
                                                               ))
                                                                (const $ const $ return ()))
    , (builtinAgdaSort                         |-> BuiltinData tset
                                                     [ builtinAgdaSortSet, builtinAgdaSortLit
                                                     , builtinAgdaSortProp, builtinAgdaSortPropLit
                                                     , builtinAgdaSortInf, builtinAgdaSortUnsupported])
    , (builtinAgdaTerm                         |-> BuiltinData tset
                                                     [ builtinAgdaTermVar, builtinAgdaTermLam, builtinAgdaTermExtLam
                                                     , builtinAgdaTermDef, builtinAgdaTermCon
                                                     , builtinAgdaTermPi, builtinAgdaTermSort
                                                     , builtinAgdaTermLit, builtinAgdaTermMeta
                                                     , builtinAgdaTermUnsupported])
    , builtinAgdaErrorPart                     |-> BuiltinData tset [ builtinAgdaErrorPartString, builtinAgdaErrorPartTerm, builtinAgdaErrorPartPatt, builtinAgdaErrorPartName ]
    , builtinAgdaErrorPartString               |-> BuiltinDataCons (tstring --> terrorpart)
    , builtinAgdaErrorPartTerm                 |-> BuiltinDataCons (tterm --> terrorpart)
    , builtinAgdaErrorPartPatt                 |-> BuiltinDataCons (tpat --> terrorpart)
    , builtinAgdaErrorPartName                 |-> BuiltinDataCons (tqname --> terrorpart)
    , builtinAgdaBlocker                       |-> BuiltinData tset [ builtinAgdaBlockerAll, builtinAgdaBlockerAny, builtinAgdaBlockerMeta ]
    , builtinAgdaBlockerAny                    |-> BuiltinDataCons (tlist tblocker --> tblocker)
    , builtinAgdaBlockerAll                    |-> BuiltinDataCons (tlist tblocker --> tblocker)
    , builtinAgdaBlockerMeta                   |-> BuiltinDataCons (tmeta --> tblocker)
    -- Andreas, 2017-01-12, issue #2386: special handling of builtinEquality
    -- , (builtinEquality                         |-> BuiltinData (hPi "a" (el primLevel) $
    --                                                             hPi "A" (return $ sort $ varSort 0) $
    --                                                             (El (varSort 1) <$> varM 0) -->
    --                                                             (El (varSort 1) <$> varM 0) -->
    --                                                             return (sort $ varSort 1))
    --                                                            [builtinRefl])
    , (builtinHiding                           |-> BuiltinData tset [builtinHidden, builtinInstance, builtinVisible])
      -- Relevance
    , (builtinRelevance                        |-> BuiltinData tset [builtinRelevant, builtinIrrelevant])
    , (builtinRelevant                         |-> BuiltinDataCons trelevance)
    , (builtinIrrelevant                       |-> BuiltinDataCons trelevance)
      -- Quantity
    , (builtinQuantity                         |-> BuiltinData tset [builtinQuantity0, builtinQuantityω])
    , (builtinQuantity0                        |-> BuiltinDataCons tquantity)
    , (builtinQuantityω                        |-> BuiltinDataCons tquantity)
      -- Modality
    , (builtinModality                         |-> BuiltinData tset [builtinModalityConstructor])
    , (builtinModalityConstructor              |-> BuiltinDataCons (trelevance --> tquantity --> tmodality))
      -- Associativity
    , builtinAssoc                             |-> BuiltinData tset [builtinAssocLeft, builtinAssocRight, builtinAssocNon]
    , builtinAssocLeft                         |-> BuiltinDataCons tassoc
    , builtinAssocRight                        |-> BuiltinDataCons tassoc
    , builtinAssocNon                          |-> BuiltinDataCons tassoc
      -- Precedence
    , builtinPrecedence                        |-> BuiltinData tset [builtinPrecRelated, builtinPrecUnrelated]
    , builtinPrecRelated                       |-> BuiltinDataCons (tfloat --> tprec)
    , builtinPrecUnrelated                     |-> BuiltinDataCons tprec
      -- Fixity
    , builtinFixity                            |-> BuiltinData tset [builtinFixityFixity]
    , builtinFixityFixity                      |-> BuiltinDataCons (tassoc --> tprec --> tfixity)
    -- Andreas, 2017-01-12, issue #2386: special handling of builtinEquality
    -- , (builtinRefl                             |-> BuiltinDataCons (hPi "a" (el primLevel) $
    --                                                                 hPi "A" (return $ sort $ varSort 0) $
    --                                                                 hPi "x" (El (varSort 1) <$> varM 0) $
    --                                                                 El (varSort 2) <$> primEquality <#> varM 2 <#> varM 1 <@> varM 0 <@> varM 0))
    , (builtinRewrite                          |-> BuiltinUnknown Nothing verifyBuiltinRewrite)
    , (builtinNil                              |-> BuiltinDataCons (hPi "A" tset (el (list v0))))
    , (builtinCons                             |-> BuiltinDataCons (hPi "A" tset (tv0 --> el (list v0) --> el (list v0))))
    , (builtinNothing                          |-> BuiltinDataCons (hPi "A" tset (el (tMaybe v0))))
    , (builtinJust                             |-> BuiltinDataCons (hPi "A" tset (tv0 --> el (tMaybe v0))))
    , (builtinZero                             |-> BuiltinDataCons tnat)
    , (builtinSuc                              |-> BuiltinDataCons (tnat --> tnat))
    , (builtinTrue                             |-> BuiltinDataCons tbool)
    , (builtinFalse                            |-> BuiltinDataCons tbool)
    , (builtinArgArg                           |-> BuiltinDataCons (hPi "A" tset (targinfo --> tv0 --> targ tv0)))
    , (builtinAbsAbs                           |-> BuiltinDataCons (hPi "A" tset (tstring  --> tv0 --> tabs tv0)))
    , (builtinArgArgInfo                       |-> BuiltinDataCons (thiding --> tmodality --> targinfo))
    , (builtinAgdaTermVar                      |-> BuiltinDataCons (tnat --> targs --> tterm))
    , (builtinAgdaTermLam                      |-> BuiltinDataCons (thiding --> tabs tterm --> tterm))
    , (builtinAgdaTermExtLam                   |-> BuiltinDataCons (tlist tclause --> targs --> tterm))
    , (builtinAgdaTermDef                      |-> BuiltinDataCons (tqname --> targs --> tterm))
    , (builtinAgdaTermCon                      |-> BuiltinDataCons (tqname --> targs --> tterm))
    , (builtinAgdaTermPi                       |-> BuiltinDataCons (targ ttype --> tabs ttype --> tterm))
    , (builtinAgdaTermSort                     |-> BuiltinDataCons (tsort --> tterm))
    , (builtinAgdaTermLit                      |-> BuiltinDataCons (tliteral --> tterm))
    , (builtinAgdaTermMeta                     |-> BuiltinDataCons (tmeta --> targs --> tterm))
    , (builtinAgdaTermUnsupported              |-> BuiltinDataCons tterm)
    , (builtinAgdaLitNat                       |-> BuiltinDataCons (tnat --> tliteral))
    , (builtinAgdaLitWord64                    |-> BuiltinDataCons (tword64 --> tliteral))
    , (builtinAgdaLitFloat                     |-> BuiltinDataCons (tfloat --> tliteral))
    , (builtinAgdaLitChar                      |-> BuiltinDataCons (tchar --> tliteral))
    , (builtinAgdaLitString                    |-> BuiltinDataCons (tstring --> tliteral))
    , (builtinAgdaLitQName                     |-> BuiltinDataCons (tqname --> tliteral))
    , (builtinAgdaLitMeta                      |-> BuiltinDataCons (tmeta --> tliteral))
    , (builtinHidden                           |-> BuiltinDataCons thiding)
    , (builtinInstance                         |-> BuiltinDataCons thiding)
    , (builtinVisible                          |-> BuiltinDataCons thiding)
    , (builtinSizeUniv                         |-> builtinPostulate tsetOmega) -- SizeUniv : Setω
    , (builtinSize                             |-> builtinPostulate tSizeUniv)
    , (builtinSizeLt                           |-> builtinPostulate (tsize ..--> tSizeUniv))
    , (builtinSizeSuc                          |-> builtinPostulate (tsize --> tsize))
    , (builtinSizeInf                          |-> builtinPostulate tsize)
    -- postulate max : {i : Size} -> Size< i -> Size< i -> Size< i
    , (builtinSizeMax                          |-> builtinPostulate (tsize --> tsize --> tsize))
       -- (hPi "i" tsize $ let a = el $ primSizeLt <@> v0 in (a --> a --> a)))
    , (builtinAgdaSortSet                      |-> BuiltinDataCons (tterm --> tsort))
    , (builtinAgdaSortLit                      |-> BuiltinDataCons (tnat --> tsort))
    , (builtinAgdaSortProp                     |-> BuiltinDataCons (tterm --> tsort))
    , (builtinAgdaSortPropLit                  |-> BuiltinDataCons (tnat --> tsort))
    , (builtinAgdaSortInf                      |-> BuiltinDataCons (tnat --> tsort))
    , (builtinAgdaSortUnsupported              |-> BuiltinDataCons tsort)
    , (builtinNatPlus                          |-> BuiltinPrim PrimNatPlus verifyPlus)
    , (builtinNatMinus                         |-> BuiltinPrim PrimNatMinus verifyMinus)
    , (builtinNatTimes                         |-> BuiltinPrim PrimNatTimes verifyTimes)
    , (builtinNatDivSucAux                     |-> BuiltinPrim PrimNatDivSucAux verifyDivSucAux)
    , (builtinNatModSucAux                     |-> BuiltinPrim PrimNatModSucAux verifyModSucAux)
    , (builtinNatEquals                        |-> BuiltinPrim PrimNatEquality verifyEquals)
    , (builtinNatLess                          |-> BuiltinPrim PrimNatLess verifyLess)
    , (builtinLevelUniv                        |-> BuiltinSort SortLevelUniv)
    , (builtinLevelZero                        |-> BuiltinPrim PrimLevelZero (const $ return ()))
    , (builtinLevelSuc                         |-> BuiltinPrim PrimLevelSuc (const $ return ()))
    , (builtinLevelMax                         |-> BuiltinPrim PrimLevelMax verifyMax)
    , (builtinProp                             |-> BuiltinSort SortProp)
    , (builtinSet                              |-> BuiltinSort SortSet)
    , (builtinStrictSet                        |-> BuiltinSort SortStrictSet)
    , (builtinPropOmega                        |-> BuiltinSort SortPropOmega)
    , (builtinSetOmega                         |-> BuiltinSort SortSetOmega)
    , (builtinSSetOmega                        |-> BuiltinSort SortStrictSetOmega)
    , (builtinAgdaClause                       |-> BuiltinData tset [builtinAgdaClauseClause, builtinAgdaClauseAbsurd])
    , (builtinAgdaClauseClause                 |-> BuiltinDataCons (ttelescope --> tlist (targ tpat) --> tterm --> tclause))
    , (builtinAgdaClauseAbsurd                 |-> BuiltinDataCons (ttelescope --> tlist (targ tpat) --> tclause))
    , (builtinAgdaDefinition                   |-> BuiltinData tset [builtinAgdaDefinitionFunDef
                                                                    ,builtinAgdaDefinitionDataDef
                                                                    ,builtinAgdaDefinitionDataConstructor
                                                                    ,builtinAgdaDefinitionRecordDef
                                                                    ,builtinAgdaDefinitionPostulate
                                                                    ,builtinAgdaDefinitionPrimitive])
    , (builtinAgdaDefinitionFunDef             |-> BuiltinDataCons (tlist tclause --> tdefn))
    , (builtinAgdaDefinitionDataDef            |-> BuiltinDataCons (tnat --> tlist tqname --> tdefn))
    , (builtinAgdaDefinitionDataConstructor    |-> BuiltinDataCons (tqname --> tquantity --> tdefn))
    , (builtinAgdaDefinitionRecordDef          |-> BuiltinDataCons (tqname --> tlist (targ tqname) --> tdefn))
    , (builtinAgdaDefinitionPostulate          |-> BuiltinDataCons tdefn)
    , (builtinAgdaDefinitionPrimitive          |-> BuiltinDataCons tdefn)
    , builtinAgdaTCM                           |-> builtinPostulate (hPi "a" tlevel $ tsetL 0 --> tsetL 0)
    , builtinAgdaTCMReturn                     |-> builtinPostulate (hPi "a" tlevel  $
                                                                     hPi "A" (tsetL 0) $
                                                                     elV 1 (varM 0) --> tTCM 1 (varM 0))
    , builtinAgdaTCMBind                       |-> builtinPostulate (hPi "a" tlevel  $ hPi "b" tlevel $
                                                                     hPi "A" (tsetL 1) $ hPi "B" (tsetL 1) $
                                                                     tTCM 3 (varM 1) --> (elV 3 (varM 1) --> tTCM 2 (varM 0)) --> tTCM 2 (varM 0))
    , builtinAgdaTCMUnify                      |-> builtinPostulate (tterm --> tterm --> tTCM_ primUnit)
    , builtinAgdaTCMTypeError                  |-> builtinPostulate (hPi "a" tlevel $ hPi "A" (tsetL 0) $ tlist terrorpart --> tTCM 1 (varM 0))
    , builtinAgdaTCMInferType                  |-> builtinPostulate (tterm --> tTCM_ primAgdaTerm)
    , builtinAgdaTCMCheckType                  |-> builtinPostulate (tterm --> ttype --> tTCM_ primAgdaTerm)
    , builtinAgdaTCMNormalise                  |-> builtinPostulate (tterm --> tTCM_ primAgdaTerm)
    , builtinAgdaTCMReduce                     |-> builtinPostulate (tterm --> tTCM_ primAgdaTerm)
    , builtinAgdaTCMCatchError                 |-> builtinPostulate (hPi "a" tlevel $ hPi "A" (tsetL 0) $
                                                                     tTCM 1 (varM 0) --> tTCM 1 (varM 0) --> tTCM 1 (varM 0))
    , builtinAgdaTCMGetContext                 |-> builtinPostulate (tTCM_ (unEl <$> ttelescope))
    , builtinAgdaTCMExtendContext              |-> builtinPostulate (hPi "a" tlevel $ hPi "A" (tsetL 0) $
                                                                     tstring --> targ ttype --> tTCM 1 (varM 0) --> tTCM 1 (varM 0))
    , builtinAgdaTCMInContext                  |-> builtinPostulate (hPi "a" tlevel $ hPi "A" (tsetL 0) $
                                                                     ttelescope --> tTCM 1 (varM 0) --> tTCM 1 (varM 0))
    , builtinAgdaTCMFreshName                  |-> builtinPostulate (tstring --> tTCM_ primQName)
    , builtinAgdaTCMDeclareDef                 |-> builtinPostulate (targ tqname --> ttype --> tTCM_ primUnit)
    , builtinAgdaTCMDeclarePostulate           |-> builtinPostulate (targ tqname --> ttype --> tTCM_ primUnit)
    , builtinAgdaTCMDeclareData                |-> builtinPostulate (tqname --> tnat --> ttype --> tTCM_ primUnit)
    , builtinAgdaTCMDefineData                 |-> builtinPostulate (tqname --> tlist (tpair primLevelZero primLevelZero tqname (tpair primLevelZero primLevelZero tquantity ttype)) --> tTCM_ primUnit)
    , builtinAgdaTCMDefineFun                  |-> builtinPostulate (tqname --> tlist tclause --> tTCM_ primUnit)
    , builtinAgdaTCMGetType                    |-> builtinPostulate (tqname --> tTCM_ primAgdaTerm)
    , builtinAgdaTCMGetDefinition              |-> builtinPostulate (tqname --> tTCM_ primAgdaDefinition)
    , builtinAgdaTCMQuoteTerm                  |-> builtinPostulate (hPi "a" tlevel $ hPi "A" (tsetL 0) $ elV 1 (varM 0) --> tTCM_ primAgdaTerm)
    , builtinAgdaTCMUnquoteTerm                |-> builtinPostulate (hPi "a" tlevel $ hPi "A" (tsetL 0) $ tterm --> tTCM 1 (varM 0))
    , builtinAgdaTCMQuoteOmegaTerm             |-> builtinPostulate (hPi "A" tsetOmega $ elInf (varM 0) --> tTCM_ primAgdaTerm)
    , builtinAgdaTCMBlock                      |-> builtinPostulate (hPi "a" tlevel $ hPi "A" (tsetL 0) $ tblocker --> tTCM 1 (varM 0))
    , builtinAgdaTCMCommit                     |-> builtinPostulate (tTCM_ primUnit)
    , builtinAgdaTCMIsMacro                    |-> builtinPostulate (tqname --> tTCM_ primBool)
    , builtinAgdaTCMWithNormalisation          |-> builtinPostulate (hPi "a" tlevel $ hPi "A" (tsetL 0) $ tbool --> tTCM 1 (varM 0) --> tTCM 1 (varM 0))
    , builtinAgdaTCMWithReconstructed          |-> builtinPostulate (hPi "a" tlevel $ hPi "A" (tsetL 0) $ tbool --> tTCM 1 (varM 0) --> tTCM 1 (varM 0))
    , builtinAgdaTCMWithExpandLast             |-> builtinPostulate (hPi "a" tlevel $ hPi "A" (tsetL 0) $ tbool --> tTCM 1 (varM 0) --> tTCM 1 (varM 0))
    , builtinAgdaTCMWithReduceDefs             |-> builtinPostulate (hPi "a" tlevel $ hPi "A" (tsetL 0) $ (tpair primLevelZero primLevelZero tbool (tlist tqname)) --> tTCM 1 (varM 0) --> tTCM 1 (varM 0))
    , builtinAgdaTCMAskNormalisation           |-> builtinPostulate (tTCM_ (unEl <$> tbool))
    , builtinAgdaTCMAskReconstructed           |-> builtinPostulate (tTCM_ (unEl <$> tbool))
    , builtinAgdaTCMAskExpandLast              |-> builtinPostulate (tTCM_ (unEl <$> tbool))
    , builtinAgdaTCMAskReduceDefs              |-> builtinPostulate (tTCM_ (unEl <$> (tpair primLevelZero primLevelZero tbool (tlist tqname))))
    , builtinAgdaTCMFormatErrorParts           |-> builtinPostulate (tlist terrorpart --> tTCM_ primString)
    , builtinAgdaTCMDebugPrint                 |-> builtinPostulate (tstring --> tnat --> tlist terrorpart --> tTCM_ primUnit)
  
    , builtinAgdaTCMNoConstraints              |-> builtinPostulate (hPi "a" tlevel $ hPi "A" (tsetL 0) $ tTCM 1 (varM 0) --> tTCM 1 (varM 0))
    , builtinAgdaTCMWorkOnTypes                |-> builtinPostulate (hPi "a" tlevel $ hPi "A" (tsetL 0) $ tTCM 1 (varM 0) --> tTCM 1 (varM 0))
    , builtinAgdaTCMRunSpeculative             |-> builtinPostulate (hPi "a" tlevel $ hPi "A" (tsetL 0) $
                                                                     tTCM 1 (primSigma <#> varM 1 <#> primLevelZero <@> varM 0 <@> (Lam defaultArgInfo . Abs "_" <$> primBool)) --> tTCM 1 (varM 0))
    , builtinAgdaTCMExec                       |-> builtinPostulate (tstring --> tlist tstring --> tstring -->
                                                                     tTCM_ (primSigma <#> primLevelZero <#> primLevelZero <@> primNat <@>
                                                                            (Lam defaultArgInfo . Abs "_" <$> (primSigma <#> primLevelZero <#> primLevelZero <@> primString <@>
                                                                             (Lam defaultArgInfo . Abs "_" <$> primString)))))
    , builtinAgdaTCMCheckFromString            |-> builtinPostulate (tstring --> ttype --> tTCM_ primAgdaTerm)
    , builtinAgdaTCMGetInstances               |-> builtinPostulate (tmeta --> tTCM_ (list primAgdaTerm))
    , builtinAgdaTCMSolveInstances             |-> builtinPostulate (tTCM_ primUnit)
    , builtinAgdaTCMPragmaForeign              |-> builtinPostulate (tstring --> tstring --> tTCM_ primUnit)
    , builtinAgdaTCMPragmaCompile              |-> builtinPostulate (tstring --> tqname --> tstring --> tTCM_ primUnit)
    ]
    where
          (|->) = BuiltinInfo
  
          v0 :: TCM Term
          v0 = varM 0
  
          tv0 :: TCM Type
          tv0 = el v0
  
          arg :: TCM Term -> TCM Term
          arg t = primArg <@> t
  
          elV x a = El (varSort x) <$> a
  
          tsetL l    = return $ sort (varSort l)
          tsetOmega  = return $ sort $ Inf UType 0
          tlevel     = el primLevel
          tlist x    = el $ list (fmap unEl x)
          tmaybe x   = el $ tMaybe (fmap unEl x)
          tpair lx ly x y = el $ primSigma
                              <#> lx
                              <#> ly
                              <@> fmap unEl x
                              <@> (Lam defaultArgInfo . NoAbs "_" <$> fmap unEl y)
          targ x     = el (arg (fmap unEl x))
          tabs x     = el (primAbs <@> fmap unEl x)
          targs      = el (list (arg primAgdaTerm))
          tterm      = el primAgdaTerm
          terrorpart = el primAgdaErrorPart
          tnat       = el primNat
          tword64    = el primWord64
          tinteger   = el primInteger
          tfloat     = el primFloat
          tchar      = el primChar
          tstring    = el primString
          tqname     = el primQName
          tmeta      = el primAgdaMeta
          tblocker   = el primAgdaBlocker
          tsize      = El sSizeUniv <$> primSize
          tbool      = el primBool
          thiding    = el primHiding
          trelevance = el primRelevance
          tquantity  = el primQuantity
          tmodality  = el primModality
          tassoc     = el primAssoc
          tprec      = el primPrecedence
          tfixity    = el primFixity
  --        tcolors    = el (list primAgdaTerm) -- TODO guilhem
          targinfo   = el primArgInfo
          ttype      = el primAgdaTerm
          tsort      = el primAgdaSort
          tdefn      = el primAgdaDefinition
          tliteral   = el primAgdaLiteral
          tpat       = el primAgdaPattern
          tclause    = el primAgdaClause
          ttelescope = tlist (tpair primLevelZero primLevelZero tstring (targ ttype))
          tTCM l a   = elV l (primAgdaTCM <#> varM l <@> a)
          tTCM_ a    = el (primAgdaTCM <#> primLevelZero <@> a)
          tinterval  = El IntervalUniv <$> primInterval
  
          verifyPlus plus =
              verify ["n","m"] $ \(@@) zero suc (==) (===) choice -> do
                  let m = var 0
                      n = var 1
                      x + y = plus @@ x @@ y
  
                  -- We allow recursion on any argument
                  choice
                      [ do n + zero  == n
                           n + suc m == suc (n + m)
                      , do suc n + m == suc (n + m)
                           zero  + m == m
                      ]
  
          verifyMinus minus =
              verify ["n","m"] $ \(@@) zero suc (==) (===) choice -> do
                  let m = var 0
                      n = var 1
                      x - y = minus @@ x @@ y
  
                  -- We allow recursion on any argument
                  zero  - zero  == zero
                  zero  - suc m == zero
                  suc n - zero  == suc n
                  suc n - suc m == (n - m)
  
          verifyTimes times = do
              plus <- primNatPlus
              verify ["n","m"] $ \(@@) zero suc (==) (===) choice -> do
                  let m = var 0
                      n = var 1
                      x + y = plus  @@ x @@ y
                      x * y = times @@ x @@ y
  
                  choice
                      [ do n * zero == zero
                           choice [ (n * suc m) == (n + (n * m))
                                  , (n * suc m) == ((n * m) + n)
                                  ]
                      , do zero * n == zero
                           choice [ (suc n * m) == (m + (n * m))
                                  , (suc n * m) == ((n * m) + m)
                                  ]
                      ]
  
          verifyDivSucAux dsAux =
              verify ["k","m","n","j"] $ \(@@) zero suc (==) (===) choice -> do
                  let aux k m n j = dsAux @@ k @@ m @@ n @@ j
                      k           = var 0
                      m           = var 1
                      n           = var 2
                      j           = var 3
  
                  aux k m zero    j       == k
                  aux k m (suc n) zero    == aux (suc k) m n m
                  aux k m (suc n) (suc j) == aux k m n j
  
          verifyModSucAux dsAux =
              verify ["k","m","n","j"] $ \(@@) zero suc (==) (===) choice -> do
                  let aux k m n j = dsAux @@ k @@ m @@ n @@ j
                      k           = var 0
                      m           = var 1
                      n           = var 2
                      j           = var 3
  
                  aux k m zero    j       == k
                  aux k m (suc n) zero    == aux zero m n m
                  aux k m (suc n) (suc j) == aux (suc k) m n j
  
          verifyEquals eq =
              verify ["n","m"] $ \(@@) zero suc (==) (===) choice -> do
              true  <- primTrue
              false <- primFalse
              let x == y = eq @@ x @@ y
                  m      = var 0
                  n      = var 1
              (zero  == zero ) === true
              (suc n == suc m) === (n == m)
              (suc n == zero ) === false
              (zero  == suc n) === false
  
          verifyLess leq =
              verify ["n","m"] $ \(@@) zero suc (==) (===) choice -> do
              true  <- primTrue
              false <- primFalse
              let x < y = leq @@ x @@ y
                  m     = var 0
                  n     = var 1
              (n     < zero)  === false
              (suc n < suc m) === (n < m)
              (zero  < suc m) === true
  
          verifyMax maxV = return ()  -- TODO: make max a postulate
  
          verify xs = verify' primNat primZero primSuc xs
  
          verify' ::  TCM Term -> TCM Term -> TCM Term ->
                      [String] -> ( (Term -> Term -> Term) -> Term -> (Term -> Term) ->
                                  (Term -> Term -> TCM ()) ->
                                  (Term -> Term -> TCM ()) ->
                                  ([TCM ()] -> TCM ()) -> TCM a) -> TCM a
          verify' pNat pZero pSuc xs f = do
              nat  <- El (mkType 0) <$> pNat
              zero <- pZero
              s    <- pSuc
              let x == y  = noConstraints $ equalTerm nat x y
                  -- Andreas: 2013-10-21 I put primBool here on the inside
                  -- since some Nat-builtins do not require Bool-builtins
                  x === y = do bool <- El (mkType 0) <$> primBool
                               noConstraints $ equalTerm bool x y
                  suc n  = s `apply1` n
                  choice = foldr1 (\x y -> x `catchError` \_ -> y)
              xs <- mapM freshName_ xs
              addContext (xs, domFromArg $ defaultArg nat) $ f apply1 zero suc (==) (===) choice
  
          verifyPath :: Term -> Type -> TCM ()
          verifyPath path t = do
            let hlam n t = glam (setHiding Hidden defaultArgInfo) n t
            noConstraints $ equalTerm t path =<< runNamesT [] (
              hlam "l" $ \ l -> hlam "A" $ \ bA -> cl primPathP <#> l <@> lam "i" (\ _ -> bA))
  
  -- | Checks that builtin with name @b : String@ of type @t : Term@
  --   is a data type or inductive record with @n : Int@ constructors.
  --   Returns the name of the data/record type.
  inductiveCheck :: BuiltinId -> Int -> Term -> TCM (QName, Definition)
  inductiveCheck b n t = do
    caseMaybeM (headSymbol t) no $ \q -> do
        def <- getConstInfo q
        let yes = return (q, def)
        case theDef def of
          Datatype { dataCons = cs }
            | length cs == n -> yes
            | otherwise      -> no
          Record { recInduction = ind } | n == 1 && ind /= Just CoInductive -> yes
          _ -> no
    where
    headSymbol :: Term -> TCM (Maybe QName)
    headSymbol t = reduce t >>= \case
      Def q _ -> return $ Just q
      Lam _ b -> headSymbol $ lazyAbsApp b __DUMMY_TERM__
      _       -> return Nothing
  
    no = typeError $ BuiltinMustBeData b n
  
  -- | @bindPostulatedName builtin q m@ checks that @q@ is a postulated
  -- name, and binds the builtin @builtin@ to the term @m q def@,
  -- where @def@ is the current 'Definition' of @q@.
  
  bindPostulatedName ::
    BuiltinId -> ResolvedName -> (QName -> Definition -> TCM Term) -> TCM ()
  bindPostulatedName builtin x m = do
    q   <- getName x
    def <- getConstInfo q
    case theDef def of
      Axiom {} -> bindBuiltinName builtin =<< m q def
      _        -> err
    where
    err :: forall m a. MonadTCError m => m a
    err = typeError $ BuiltinMustBePostulate builtin
    getName = \case
      DefinedName _ d NoSuffix -> return $ anameName d
      _ -> err
  
  addHaskellPragma :: QName -> String -> TCM ()
  addHaskellPragma = addPragma ghcBackendName
  
  bindAndSetHaskellCode :: BuiltinId -> String -> Term -> TCM ()
  bindAndSetHaskellCode b hs t = do
    d <- fromMaybe __IMPOSSIBLE__ <$> getDef t
    bindBuiltinName b t
    addHaskellPragma d hs
  
  bindBuiltinBool :: Term -> TCM ()
  bindBuiltinBool = bindAndSetHaskellCode builtinBool "= type Bool"
  
  -- | Check that we're not trying to bind true and false to the same
  -- constructor.
  checkBuiltinBool :: TCM ()
  checkBuiltinBool = do
    true  <- getBuiltin' builtinTrue
    false <- getBuiltin' builtinFalse
    when (true == false) $
      typeError $ InvalidBuiltin "Cannot bind TRUE and FALSE to the same constructor"
  
  bindBuiltinInt :: Term -> TCM ()
  bindBuiltinInt = bindAndSetHaskellCode builtinInteger "= type Integer"
  
  bindBuiltinNat :: Term -> TCM ()
  bindBuiltinNat t = do
    bindBuiltinData builtinNat t
    name <- fromMaybe __IMPOSSIBLE__ <$> getDef t
    addHaskellPragma name "= type Integer"
  
  -- | Only use for datatypes with distinct arities of constructors.
  --   Binds the constructors together with the datatype.
  bindBuiltinData :: BuiltinId -> Term -> TCM ()
  bindBuiltinData s t = do
    bindBuiltinName s t
    name <- fromMaybe __IMPOSSIBLE__ <$> getDef t
    Datatype{ dataCons = cs } <- theDef <$> getConstInfo name
    let getArity c = do
          Constructor{ conArity = a } <- theDef <$> getConstInfo c
          return a
        getBuiltinArity (BuiltinDataCons t) = arity <$> t
        getBuiltinArity _ = __IMPOSSIBLE__
        sortByM f xs = map fst . sortBy (compare `on` snd) . zip xs <$> mapM f xs
    -- Order constructurs by arity
    cs <- sortByM getArity cs
    -- Do the same for the builtins
    let bcis = fromMaybe __IMPOSSIBLE__ $ do
          BuiltinData _ bcs <- builtinDesc <$> findBuiltinInfo s
          mapM findBuiltinInfo bcs
    bcis <- sortByM (getBuiltinArity . builtinDesc) bcis
    unless (length cs == length bcis) __IMPOSSIBLE__  -- we already checked this
    zipWithM_ (\ c bci -> bindBuiltinInfo bci (A.Con $ unambiguous $ setRange (getRange name) c)) cs bcis
  
  bindBuiltinUnit :: Term -> TCM ()
  bindBuiltinUnit t = do
    unit <- fromMaybe __IMPOSSIBLE__ <$> getDef t
    def <- theDef <$> getConstInfo unit
    case def of
      Record { recFields = [], recConHead = con } -> do
        bindBuiltinName builtinUnit t
        bindBuiltinName builtinUnitUnit (Con con ConOSystem [])
      _ -> typeError $ InvalidBuiltin "Builtin UNIT must be a singleton record type"
  
  bindBuiltinSigma :: Term -> TCM ()
  bindBuiltinSigma t = do
    sigma <- fromMaybe __IMPOSSIBLE__ <$> getDef t
    def <- theDef <$> getConstInfo sigma
    case def of
      Record { recFields = [fst,snd], recConHead = con } -> do
        bindBuiltinName builtinSigma t
      _ -> typeError $ InvalidBuiltin "Builtin SIGMA must be a record type with two fields"
  
  -- | Bind BUILTIN EQUALITY and BUILTIN REFL.
  bindBuiltinEquality :: ResolvedName -> TCM ()
  bindBuiltinEquality x = do
    (v, _t) <- inferExpr (A.nameToExpr x)
  
    -- Equality needs to be a data type with 1 constructor
    (eq, def) <- inductiveCheck builtinEquality 1 v
  
    -- Check that the type is the type of a polymorphic relation, i.e.,
    -- Γ → (A : Set _) → A → A → Set _
    TelV eqTel eqCore <- telView $ defType def
    let no = typeError $ InvalidBuiltin "The type of BUILTIN EQUALITY must be a polymorphic relation"
  
    -- The target is a sort since eq is a data type.
    unless (isJust $ isSort $ unEl eqCore) __IMPOSSIBLE__
  
    -- The types of the last two arguments must be the third-last argument
    unless (natSize eqTel >= 3) no
    let (a, b) = fromMaybe __IMPOSSIBLE__ $ last2 $ telToList eqTel
    [a,b] <- reduce $ map (unEl . snd . unDom) [a,b]
    unless (deBruijnView a == Just 0) no
    unless (deBruijnView b == Just 1) no
  
    -- Get the single constructor.
    case theDef def of
      Datatype { dataCons = [c] } -> do
        bindBuiltinName builtinEquality v
  
        -- Check type of REFL.  It has to be of the form
        -- pars → (x : A) → Eq ... x x
  
        -- Check the arguments
        cdef <- getConstInfo c
        TelV conTel conCore <- telView $ defType cdef
        ts <- reduce $ map (unEl . snd . unDom) $ drop (conPars $ theDef cdef) $ telToList conTel
        -- After dropping the parameters, there should be maximally one argument.
        unless (length ts <= 1) wrongRefl
        unless (all ((Just 0 ==) . deBruijnView) ts) wrongRefl
  
        -- Check the target
        case unEl conCore of
          Def _ es -> do
            let vs = map unArg $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
            (a,b) <- reduce $ fromMaybe __IMPOSSIBLE__ $ last2 vs
            unless (deBruijnView a == Just 0) wrongRefl
            unless (deBruijnView b == Just 0) wrongRefl
            bindBuiltinName builtinRefl (Con (ConHead c IsData Inductive []) ConOSystem [])
          _ -> __IMPOSSIBLE__
      _ -> typeError $ InvalidBuiltin "Builtin EQUALITY must be a data type with a single constructor"
    where
    wrongRefl = typeError $ InvalidBuiltin "Wrong type of constructor of BUILTIN EQUALITY"
  
  bindBuiltinInfo :: BuiltinInfo -> A.Expr -> TCM ()
  bindBuiltinInfo (BuiltinInfo s d) e = do
      case d of
        BuiltinData t cs -> do
          v <- checkExpr e =<< t
          unless (s == builtinUnit) $ do
            void $ inductiveCheck s (length cs) v
          if | s == builtinEquality -> __IMPOSSIBLE__ -- bindBuiltinEquality v
             | s == builtinBool     -> bindBuiltinBool     v
             | s == builtinNat      -> bindBuiltinNat      v
             | s == builtinInteger  -> bindBuiltinInt      v
             | s == builtinUnit     -> bindBuiltinUnit     v
             | s == builtinSigma    -> bindBuiltinSigma    v
             | s == builtinList     -> bindBuiltinData s   v
             | s == builtinMaybe    -> bindBuiltinData s   v
             | otherwise            -> bindBuiltinName s   v
  
        BuiltinDataCons t -> do
  
          let name (Lam h b)  = name (absBody b)
              name (Con c ci _) = Con c ci []
              name _          = __IMPOSSIBLE__
  
          v0 <- checkExpr e =<< t
  
          case e of
            A.Con{} -> return ()
            _       -> typeError $ BuiltinMustBeConstructor s e
  
          let v@(Con h _ []) = name v0
  
          bindBuiltinName s v
  
          when (s `elem` [builtinFalse, builtinTrue]) checkBuiltinBool
  
        BuiltinPrim pfname axioms -> do
          case e of
            A.Def qx -> do
  
              PrimImpl t pf <- lookupPrimitiveFunction pfname
              v <- checkExpr e t
  
              axioms v
  
              info <- getConstInfo qx
              let cls = defClauses info
                  a   = defAbstract info
                  o   = defOpaque info
                  mcc = defCompiled info
                  inv = defInverse info
              -- What happens if defArgOccurrences info does not match
              -- primFunArgOccurrences pf? Let's require the latter to
              -- be the empty list.
              unless (primFunArgOccurrences pf == []) __IMPOSSIBLE__
              bindPrimitive pfname $ pf { primFunName = qx }
              addConstant qx $ info { theDef = Primitive { primAbstr    = a
                                                         , primName     = pfname
                                                         , primClauses  = cls
                                                         , primInv      = inv
                                                         , primCompiled = mcc
                                                         , primOpaque   = o
                                                         } }
  
              -- needed? yes, for checking equations for mul
              bindBuiltinName s v
  
            _ -> typeError $ BuiltinMustBeFunction s
  
        BuiltinSort{} -> __IMPOSSIBLE__ -- always a "BuiltinNoDef"
  
        BuiltinPostulate rel t -> do
          t' <- t
          v <- applyRelevanceToContext rel $ checkExpr e t'
          let err = typeError $ BuiltinMustBePostulate s
          case e of
            A.Def q -> do
              def <- getConstInfo q
              case theDef def of
                Axiom {} -> do
                  builtinSizeHook s q t'
                  -- And compilation pragmas for base types
                  when (s == builtinLevel)  $ setConstTranspAxiom q >> addHaskellPragma q "= type ()"
                  when (s == builtinChar)   $ setConstTranspAxiom q >> addHaskellPragma q "= type Char"
                  when (s == builtinString) $ setConstTranspAxiom q >> addHaskellPragma q "= type Data.Text.Text"
                  when (s == builtinFloat)  $ setConstTranspAxiom q >> addHaskellPragma q "= type Double"
                  when (s == builtinWord64) $ setConstTranspAxiom q >> addHaskellPragma q "= type MAlonzo.RTE.Word64"
                  when (s == builtinPathP)  $ builtinPathPHook q
                  bindBuiltinName s v
                _        -> err
            _ -> err
  
        BuiltinUnknown mt f -> do
          (v, t) <- caseMaybe mt (inferExpr e) $ \ tcmt -> do
            t <- tcmt
            (,t) <$> checkExpr e t
          f v t
          if | s == builtinRewrite -> runMaybeT (getQNameFromTerm v) >>= \case
                Nothing -> typeError $ InvalidBuiltin "Invalid rewrite relation"
                Just q  -> bindBuiltinRewriteRelation q
             | otherwise           -> bindBuiltinName s v
  
  setConstTranspAxiom :: QName -> TCM ()
  setConstTranspAxiom q =
    modifySignature $ updateDefinition q $ updateTheDef (const $ constTranspAxiom)
  
  builtinPathPHook :: QName -> TCM ()
  builtinPathPHook q =
        modifySignature $ updateDefinition q
        $ updateDefPolarity       id
        . updateDefArgOccurrences (const [Unused,StrictPos,Mixed,Mixed])
  
  -- | Bind a builtin thing to an expression.
  bindBuiltin :: BuiltinId -> ResolvedName -> TCM ()
  bindBuiltin b x = do
    unlessM ((0 ==) <$> getContextSize) $ do
      -- Andreas, 2017-11-01, issue #2824
      -- Only raise an error if the name for the builtin is defined in a parametrized module.
      let
        failure :: forall m a. MonadTCError m => m a
        failure = typeError $ BuiltinInParameterisedModule b
      -- Get the non-empty list of AbstractName for x
      xs <- case x of
        VarName{}            -> failure
        DefinedName _ x NoSuffix -> return $ x :| []
        DefinedName _ x Suffix{} -> failure
        FieldName xs         -> return xs
        ConstructorName _ xs -> return xs
        PatternSynResName xs -> failure
        UnknownName          -> failure
      -- For ambiguous names, we check all of their definitions:
      unlessM (forallM xs $ null <.> lookupSection . qnameModule . anameName) $
        failure
    -- Since the name was define in a parameter-free context, we can switch to the empty context.
    -- (And we should!)
    inTopContext $ do
    if | b == builtinRefl  -> warning $ OldBuiltin b builtinEquality
       | b == builtinZero  -> now builtinNat b
       | b == builtinSuc   -> now builtinNat b
       | b == builtinNil   -> now builtinList b
       | b == builtinCons  -> now builtinList b
       | b == builtinInf   -> bindBuiltinInf x
       | b == builtinSharp -> bindBuiltinSharp x
       | b == builtinFlat  -> bindBuiltinFlat x
       | b == builtinEquality -> bindBuiltinEquality x
       | Just i <- findBuiltinInfo b -> bindBuiltinInfo i (A.nameToExpr x)
       | otherwise -> typeError $ NoSuchBuiltinName (getBuiltinId b)
    where
      now new b = warning $ OldBuiltin b new
  
  isUntypedBuiltin :: BuiltinId -> Bool
  isUntypedBuiltin = hasElem [ builtinFromNat, builtinFromNeg, builtinFromString ]
  
  bindUntypedBuiltin :: BuiltinId -> ResolvedName -> TCM ()
  bindUntypedBuiltin b = \case
    DefinedName _ x NoSuffix -> bind x
    DefinedName _ x Suffix{} -> wrong
    FieldName (x :| [])  -> bind x
    FieldName (x :| _)   -> amb x
    VarName _x _bnd      -> wrong
    UnknownName          -> wrong
    ConstructorName _ xs -> err xs
    PatternSynResName xs -> err xs
    where
    bind x = bindBuiltinName b (Def (anameName x) [])
    wrong  = typeError $ BuiltinMustBeDef b
    amb x  = genericDocError =<< do text "Name " <+> prettyTCM x <+> text " is ambiguous"
    err (x :| xs1)
      | null xs1  = wrong
      | otherwise = amb x
  
  -- | Bind a builtin thing to a new name.
  --
  -- Since their type is closed, it does not matter whether we are in a
  -- parameterized module when we declare them.
  -- We simply ignore the parameters.
  bindBuiltinNoDef :: BuiltinId -> A.QName -> TCM ()
  bindBuiltinNoDef b q = inTopContext $ do
    when (b `elem` sizeBuiltins) $
      requireOptionSizedTypes $ "to declare size BUILTIN " ++ getBuiltinId b
    case builtinDesc <$> findBuiltinInfo b of
  
      Just (BuiltinPostulate rel mt) -> do
        -- We start by adding the corresponding postulate
        t   <- mt
        fun <- emptyFunctionData
        addConstant' q (setRelevance rel defaultArgInfo) t (def fun)
        -- And we then *modify* the definition based on our needs:
        -- We add polarity information for SIZE-related definitions
        builtinSizeHook b q t
        -- Finally, bind the BUILTIN in the environment.
        bindBuiltinName b $ Def q []
        where
          -- Andreas, 2015-02-14
          -- Special treatment of SizeUniv, should maybe be a primitive.
          def fun
              | b == builtinSizeUniv = FunctionDefn $ fun
                  { _funClauses    = [ (empty :: Clause) { clauseBody = Just $ Sort sSizeUniv } ]
                  , _funCompiled   = Just (CC.Done 0 NotRecursive [] $ Sort sSizeUniv)
                  , _funMutual     = Just []
                  , _funTerminates = Just True
                  }
              | otherwise = defaultAxiom
  
      Just (BuiltinPrim name axioms) -> do
        PrimImpl t pf <- lookupPrimitiveFunction name
        bindPrimitive name $ pf { primFunName = q }
        let v   = Def q []
            def = Primitive { primAbstr    = ConcreteDef
                            , primName     = name
                            , primClauses  = []
                            , primInv      = NotInjective
                            , primCompiled = Just (CC.Done 0 NotRecursive [] $ Def q [])
                            , primOpaque   = TransparentDef
                            }
        lang <- getLanguage
        addConstant q $
          (defaultDefn defaultArgInfo q t lang def)
            { defArgOccurrences = primFunArgOccurrences pf }
        axioms v
        bindBuiltinName b v
  
      Just (BuiltinDataCons mt) -> do
        t       <- mt
        d       <- return $! getPrimName $ unEl t
        erasure <- optErasure <$> pragmaOptions
        let
          ch = ConHead q IsData Inductive []
          def = Constructor
                { conPars   = 0   -- Andrea TODO: fix zeros
                , conArity  = 0
                , conSrcCon = ch
                , conData   = d
                , conAbstr  = ConcreteDef
                , conComp   = emptyCompKit
                , conProj   = Nothing
                , conForced = []
                , conErased = Nothing
                , conErasure = erasure
                , conInline  = False
                }
        addConstant' q defaultArgInfo t def
        addDataCons d [q]
  
        bindBuiltinName b $ Con ch ConOSystem []
  
      Just (BuiltinData mt cs) -> do
        t <- mt
        addConstant' q defaultArgInfo t (def t)
        bindBuiltinName b $ Def q []
        where
          def t = Datatype
                { dataPars       = 0
                , dataIxs        = 0
                , dataClause     = Nothing
                , dataCons       = []     -- Constructors are added later
                , dataSort       = getSort t
                , dataAbstr      = ConcreteDef
                , dataMutual     = Nothing
                , dataPathCons   = []
                , dataTranspIx   = Nothing -- Id has custom transp def.
                , dataTransp     = Nothing
                }
  
      Just (BuiltinSort builtinSort) -> do
        let s = case builtinSort of
                  SortUniv u       -> Univ u $ ClosedLevel 0
                  SortOmega u      -> Inf u 0
                  SortIntervalUniv -> IntervalUniv
                  SortLevelUniv    -> LevelUniv
            def = PrimitiveSort builtinSort s
        -- Check for the cubical flag if the sort requries it
        case builtinSort of
          SortIntervalUniv -> requireCubical CErased
          _ -> return ()
        addConstant' q defaultArgInfo (sort $ univSort s) def
        bindBuiltinName b $ Def q []
  
      Just{}  -> __IMPOSSIBLE__
      Nothing -> __IMPOSSIBLE__ -- typeError $ NoSuchBuiltinName b
  
  
  builtinKindOfName :: BuiltinId -> Maybe KindOfName
  builtinKindOfName = distinguish <.> findBuiltinInfo
    where
    distinguish d = case builtinDesc d of
      BuiltinDataCons{}  -> ConName
      BuiltinData{}      -> DataName       -- Andreas, 2020-04-13: Crude.  Could be @RecName@.
      BuiltinPrim{}      -> PrimName
      BuiltinPostulate{} -> AxiomName
      BuiltinSort{}      -> PrimName
      BuiltinUnknown{}   -> OtherDefName
  