[ new ] Fewer postulates needed for Primitive types (#3174)

Looking at our attempt to make (most of) the standard library compile with the
`--safe` flag (cf. agda/agda-stdlib/pull/414), it would be nice to be able to
drop some of the `postulate`s in `Agda.Builtin.*`.

* Made `String`, `Char`, `Float`, `Word64` and the `Coinduction` builtins which
  do not require a corresponding definition. This allows us to remove all of the
  corresponding `postulate`s in `Agda.Builtin.*`.

* Added a warning when a `BUILTIN` rebinds an existing name. This should make our
  change nicely backwards compatible: we don't need to use `postulate`s anymore
  but if we are then Agda simply warns us.

* Made sure `BUILTIN`-bound names are recognized as proper declarations in the
  nicifier and that they can be attached a fixity. This is only used for `Sharp`
  in `Agda.Builtin.Coinduction` at the moment.

And voilà!

src/data/lib/prim/Agda/Builtin/Char.agda

@@ -5,7 +5,6 @@ module Agda.Builtin.Char where
 open import Agda.Builtin.Nat
 open import Agda.Builtin.Bool
 
-postulate Char : Set
 {-# BUILTIN CHAR Char #-}
 
 primitive

src/data/lib/prim/Agda/Builtin/Coinduction.agda

@@ -4,11 +4,6 @@ module Agda.Builtin.Coinduction where
 
 infix 1000 ♯_
 
-postulate
-  ∞  : ∀ {a} (A : Set a) → Set a
-  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
-  ♭  : ∀ {a} {A : Set a} → ∞ A → A
-
 {-# BUILTIN INFINITY ∞  #-}
 {-# BUILTIN SHARP    ♯_ #-}
 {-# BUILTIN FLAT     ♭  #-}

src/data/lib/prim/Agda/Builtin/Float.agda

@@ -7,7 +7,6 @@ open import Agda.Builtin.Nat
 open import Agda.Builtin.Int
 open import Agda.Builtin.String
 
-postulate Float : Set
 {-# BUILTIN FLOAT Float #-}
 
 primitive

src/data/lib/prim/Agda/Builtin/String.agda

@@ -6,7 +6,6 @@ open import Agda.Builtin.Bool
 open import Agda.Builtin.List
 open import Agda.Builtin.Char
 
-postulate String : Set
 {-# BUILTIN STRING String #-}
 
 primitive

src/data/lib/prim/Agda/Builtin/Word.agda

@@ -4,7 +4,6 @@ module Agda.Builtin.Word where
 
 open import Agda.Builtin.Nat
 
-postulate Word64 : Set
 {-# BUILTIN WORD64 Word64 #-}
 
 primitive

src/full/Agda/Syntax/Abstract.hs

@@ -33,14 +33,18 @@ import Agda.Syntax.Concrete.Name (NumHoles(..))
 import Agda.Syntax.Concrete (FieldAssignment'(..), exprFieldA, HoleContent'(..))
 import qualified Agda.Syntax.Concrete as C
 import Agda.Syntax.Concrete.Pretty ()
-import Agda.Syntax.Info
-import Agda.Syntax.Common
-import Agda.Syntax.Position
+
 import Agda.Syntax.Abstract.Name
 import Agda.Syntax.Abstract.Name as A (QNamed)
+
+import qualified Agda.Syntax.Internal as I
+
+import Agda.Syntax.Common
+import Agda.Syntax.Info
+import Agda.Syntax.Fixity ( Fixity' )
 import Agda.Syntax.Literal
+import Agda.Syntax.Position
 import Agda.Syntax.Scope.Base
-import qualified Agda.Syntax.Internal as I
 
 import Agda.TypeChecking.Positivity.Occurrence
 

src/full/Agda/Syntax/Concrete.hs

@@ -393,7 +393,9 @@ data OpenShortHand = DoOpen | DontOpen
 
 data Pragma
   = OptionsPragma             Range [String]
-  | BuiltinPragma             Range String QName
+  | BuiltinPragma             Range String QName Fixity'
+    -- ^ BUILTIN pragmas with no associated definition can have a fixity
+    --   default value: @noFixity'@.
   | RewritePragma             Range [QName]
   | CompiledDataPragma        Range QName String [String]
   | CompiledTypePragma        Range QName String
@@ -664,7 +666,7 @@ instance HasRange DoStmt where
 
 instance HasRange Pragma where
   getRange (OptionsPragma r _)               = r
-  getRange (BuiltinPragma r _ _)             = r
+  getRange (BuiltinPragma r _ _ _)           = r
   getRange (RewritePragma r _)               = r
   getRange (CompiledDataPragma r _ _ _)      = r
   getRange (CompiledTypePragma r _ _)        = r
@@ -865,7 +867,7 @@ instance KillRange Pattern where
 
 instance KillRange Pragma where
   killRange (OptionsPragma _ s)               = OptionsPragma noRange s
-  killRange (BuiltinPragma _ s e)             = killRange1 (BuiltinPragma noRange s) e
+  killRange (BuiltinPragma _ s e f)           = killRange2 (BuiltinPragma noRange s) e f
   killRange (RewritePragma _ qs)              = killRange1 (RewritePragma noRange) qs
   killRange (CompiledDataPragma _ q s ss)     = killRange1 (\q -> CompiledDataPragma noRange q s ss) q
   killRange (CompiledTypePragma _ q s)        = killRange1 (\q -> CompiledTypePragma noRange q s) q
@@ -1008,7 +1010,7 @@ instance NFData Declaration where
 
 instance NFData Pragma where
   rnf (OptionsPragma _ a)               = rnf a
-  rnf (BuiltinPragma _ a b)             = rnf a `seq` rnf b
+  rnf (BuiltinPragma _ a b f)           = rnf a `seq` rnf b `seq` rnf f
   rnf (RewritePragma _ a)               = rnf a
   rnf (CompiledDataPragma _ a b c)      = rnf a `seq` rnf b `seq` rnf c
   rnf (CompiledTypePragma _ a b)        = rnf a `seq` rnf b

src/full/Agda/Syntax/Concrete/Definitions.hs

@@ -73,6 +73,7 @@ import Agda.Syntax.Concrete.Pretty ()
 import Agda.Interaction.Options.Warnings
 
 import Agda.TypeChecking.Positivity.Occurrence
+import {-# SOURCE #-} Agda.TypeChecking.Monad.Builtin ( builtinsNoDef )
 
 import Agda.Utils.AffineHole
 import Agda.Utils.Except ( MonadError(throwError,catchError) )
@@ -866,6 +867,10 @@ niceDeclarations ds = do
       Module{}             -> []
       UnquoteDecl _ xs _   -> xs
       UnquoteDef{}         -> []
+      -- BUILTIN pragmas which do not require an accompanying definition declare
+      -- the (unqualified) name they mention.
+      Pragma (BuiltinPragma _ b (QName x) _)
+        | b `elem` builtinsNoDef -> [x]
       Pragma{}             -> []
 
     inferMutualBlocks :: [NiceDeclaration] -> Nice [NiceDeclaration]
@@ -1113,6 +1118,10 @@ niceDeclarations ds = do
 
     nicePragma (PolarityPragma{}) ds = return ([], ds)
 
+    nicePragma (BuiltinPragma r str qn@(QName x) _) ds = do
+      fx <- getFixity x
+      return ([NicePragma r (BuiltinPragma r str qn fx)], ds)
+
     nicePragma p ds = return ([NicePragma (getRange p) p], ds)
 
     canHaveTerminationMeasure :: [Declaration] -> Bool

src/full/Agda/Syntax/Concrete/Pretty.hs

@@ -513,7 +513,7 @@ instance Pretty OpenShortHand where
 
 instance Pretty Pragma where
     pretty (OptionsPragma _ opts) = fsep $ map text $ "OPTIONS" : opts
-    pretty (BuiltinPragma _ b x)  = hsep [ text "BUILTIN", text b, pretty x ]
+    pretty (BuiltinPragma _ b x _) = hsep [ text "BUILTIN", text b, pretty x ]
     pretty (RewritePragma _ xs)    =
       hsep [ text "REWRITE", hsep $ map pretty xs ]
     pretty (CompiledPragma _ x hs) =

src/full/Agda/Syntax/Parser/Parser.y

@@ -1575,10 +1575,10 @@ OptionsPragma : '{-#' 'OPTIONS' PragmaStrings '#-}' { OptionsPragma (getRange ($
 BuiltinPragma :: { Pragma }
 BuiltinPragma
     : '{-#' 'BUILTIN' string PragmaQName '#-}'
-      { BuiltinPragma (getRange ($1,$2,fst $3,$4,$5)) (snd $3) $4 }
-    -- Extra rule to accept keword REWRITE also as built-in:
+      { BuiltinPragma (getRange ($1,$2,fst $3,$4,$5)) (snd $3) $4 __IMPOSSIBLE__ }
+    -- Extra rule to accept keyword REWRITE also as built-in:
     | '{-#' 'BUILTIN' 'REWRITE' PragmaQName '#-}'
-      { BuiltinPragma (getRange ($1,$2,$3,$4,$5)) "REWRITE" $4 }
+      { BuiltinPragma (getRange ($1,$2,$3,$4,$5)) "REWRITE" $4 __IMPOSSIBLE__ }
 
 RewritePragma :: { Pragma }
 RewritePragma

src/full/Agda/Syntax/Translation/AbstractToConcrete.hs

@@ -952,9 +952,9 @@ data RangeAndPragma = RangeAndPragma Range A.Pragma
 instance ToConcrete RangeAndPragma C.Pragma where
   toConcrete (RangeAndPragma r p) = case p of
     A.OptionsPragma xs  -> return $ C.OptionsPragma r xs
-    A.BuiltinPragma b x      -> C.BuiltinPragma r b <$> toConcrete x
-    A.BuiltinNoDefPragma b x -> C.BuiltinPragma r b <$> toConcrete x
-    A.RewritePragma x        -> C.RewritePragma r . singleton <$> toConcrete x
+    A.BuiltinPragma b x       -> C.BuiltinPragma r b <$> toConcrete x <*> pure noFixity'
+    A.BuiltinNoDefPragma b x  -> C.BuiltinPragma r b <$> toConcrete x <*> pure (nameFixity $ qnameName x)
+    A.RewritePragma x         -> C.RewritePragma r . singleton <$> toConcrete x
     A.CompiledTypePragma x hs -> do
       x <- toConcrete x
       return $ C.CompiledTypePragma r x hs

src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs

@@ -1902,20 +1902,25 @@ instance ToAbstract C.Pragma [A.Pragma] where
             sINLINE ++ " used on ambiguous name " ++ prettyShow x
           _        -> genericError $ "Target of " ++ sINLINE ++ " pragma should be a function"
       return [ A.InlinePragma b y ]
-  toAbstract (C.BuiltinPragma _ b q) | isUntypedBuiltin b = do
+  toAbstract (C.BuiltinPragma _ b q _) | isUntypedBuiltin b = do
     bindUntypedBuiltin b =<< toAbstract (ResolveQName q)
     return []
-  toAbstract (C.BuiltinPragma _ b q) = do
+  toAbstract (C.BuiltinPragma _ b q f) = do
     -- Andreas, 2015-02-14
     -- Some builtins cannot be given a valid Agda type,
     -- thus, they do not come with accompanying postulate or definition.
     if b `elem` builtinsNoDef then do
       case q of
         C.QName x -> do
-          unlessM ((UnknownName ==) <$> resolveName q) $ genericError $
-            "BUILTIN " ++ b ++ " declares an identifier " ++
-            "(no longer expects an already defined identifier)"
-          y <- freshAbstractQName noFixity' x
+          -- The name shouldn't exist yet. If it does, we raise a warning
+          -- and drop the existing definition.
+          unlessM ((UnknownName ==) <$> resolveName q) $ do
+            genericWarning $ P.text $
+               "BUILTIN " ++ b ++ " declares an identifier " ++
+               "(no longer expects an already defined identifier)"
+            modifyCurrentScope $ removeNameFromScope PublicNS x
+          -- We then happily bind the name
+          y <- freshAbstractQName f x
           kind <- fromMaybe __IMPOSSIBLE__ <$> builtinKindOfName b
           bindName PublicAccess kind x y
           return [ A.BuiltinNoDefPragma b y ]

src/full/Agda/TypeChecking/Monad/Builtin.hs

@@ -60,11 +60,11 @@ setBuiltinThings b = stLocalBuiltins .= b
 
 bindBuiltinName :: String -> Term -> TCM ()
 bindBuiltinName b x = do
-        builtin <- getBuiltinThing b
-        case builtin of
-            Just (Builtin y) -> typeError $ DuplicateBuiltinBinding b y x
-            Just (Prim _)    -> typeError $ NoSuchBuiltinName b
-            Nothing          -> stLocalBuiltins %= Map.insert b (Builtin x)
+  builtin <- getBuiltinThing b
+  case builtin of
+    Just (Builtin y) -> typeError $ DuplicateBuiltinBinding b y x
+    Just (Prim _)    -> typeError $ NoSuchBuiltinName b
+    Nothing          -> stLocalBuiltins %= Map.insert b (Builtin x)
 
 bindPrimitive :: String -> PrimFun -> TCM ()
 bindPrimitive b pf = do
@@ -612,6 +612,13 @@ builtinsNoDef =
   , builtinIZero
   , builtinIOne
   , builtinSetOmega
+  , builtinString
+  , builtinChar
+  , builtinFloat
+  , builtinWord64
+  , builtinInf
+  , builtinSharp
+  , builtinFlat
   ]
 
 -- | The coinductive primitives.

src/full/Agda/TypeChecking/Monad/Builtin.hs-boot

@@ -0,0 +1,3 @@
+module Agda.TypeChecking.Monad.Builtin where
+
+builtinsNoDef :: [String]

src/full/Agda/TypeChecking/Rules/Builtin.hs

@@ -52,8 +52,8 @@ import Agda.Utils.Maybe
 import Agda.Utils.Monad
 import Agda.Utils.NonemptyList
 import Agda.Utils.Null
-import Agda.Utils.Size
 import Agda.Utils.Permutation
+import Agda.Utils.Size
 
 #include "undefined.h"
 import Agda.Utils.Impossible
@@ -96,6 +96,9 @@ coreBuiltins =
   , (builtinFloat              |-> builtinPostulate tset)
   , (builtinChar               |-> builtinPostulate tset)
   , (builtinString             |-> builtinPostulate tset)
+  , (builtinInf                |-> builtinPostulate typeOfInf)
+  , (builtinSharp              |-> builtinPostulate typeOfSharp)
+  , (builtinFlat               |-> builtinPostulate typeOfFlat)
   , (builtinQName              |-> builtinPostulate tset)
   , (builtinAgdaMeta           |-> builtinPostulate tset)
   , (builtinIO                 |-> builtinPostulate (tset --> tset))
@@ -134,12 +137,12 @@ coreBuiltins =
                                                      nPi' "i" (cl tinterval) $ \ i ->
                                                      nPi' "j" (cl tinterval) $ \ j ->
                                                      nPi' "i1" (elInf $ cl primIsOne <@> i) $ \ i1 ->
-                                                     (elInf $ cl primIsOne <@> (cl (getPrimitiveTerm "primIMax") <@> i <@> j))))
+                                                     (elInf $ cl primIsOne <@> (cl primIMax <@> i <@> j))))
   , (builtinIsOne2             |-> builtinPostulate (runNamesT [] $
                                                      nPi' "i" (cl tinterval) $ \ i ->
                                                      nPi' "j" (cl tinterval) $ \ j ->
                                                      nPi' "j1" (elInf $ cl primIsOne <@> j) $ \ j1 ->
-                                                     (elInf $ cl primIsOne <@> (cl (getPrimitiveTerm "primIMax") <@> i <@> j))))
+                                                     (elInf $ cl primIsOne <@> (cl primIMax <@> i <@> j))))
   , (builtinIsOneEmpty         |-> builtinPostulate (runNamesT [] $
                                                      hPi' "l" (el $ cl primLevel) $ \ l ->
                                                      hPi' "A" (pPi' "o" (cl primIZero) $ \ _ ->
@@ -788,10 +791,6 @@ bindBuiltinInfo (BuiltinInfo s d) e = do
             case theDef def of
               Axiom {} -> do
                 builtinSizeHook s q t'
-                when (s == builtinChar)   $ addHaskellPragma q "= type Char"
-                when (s == builtinString) $ addHaskellPragma q "= type Data.Text.Text"
-                when (s == builtinFloat)  $ addHaskellPragma q "= type Double"
-                when (s == builtinWord64) $ addHaskellPragma q "= type MAlonzo.RTE.Word64"
                 bindBuiltinName s v
               _        -> err
           _ -> err
@@ -854,11 +853,37 @@ bindUntypedBuiltin b = \case
 -- We simply ignore the parameters.
 bindBuiltinNoDef :: String -> A.QName -> TCM ()
 bindBuiltinNoDef b q = inTopContext $ do
+  if | b == builtinInf   -> ax typeOfInf   >> bindBuiltinInf r
+     | b == builtinSharp -> ax typeOfSharp >> bindBuiltinSharp r
+     | b == builtinFlat  -> ax typeOfFlat  >> bindBuiltinFlat r
+     | otherwise         -> bindBuiltinNoDef' b q
+
+  where
+
+  r :: ResolvedName
+  r = DefinedName PublicAccess (AbsName q DefName Defined)
+
+  ax :: TCM Type -> TCM ()
+  ax mty = do
+    ty <- mty
+    addConstant q $ defaultDefn defaultArgInfo q ty Axiom
+
+bindBuiltinNoDef' :: String -> A.QName -> TCM ()
+bindBuiltinNoDef' b q = do
   case builtinDesc <$> findBuiltinInfo b of
     Just (BuiltinPostulate rel mt) -> do
+      -- We start by adding the corresponding postulate
       t <- mt
       addConstant q $ defaultDefn (setRelevance rel defaultArgInfo) q t def
+      -- And we then *modify* the definition based on our needs:
+      -- We add polarity information for SIZE-related definitions
       builtinSizeHook b q t
+      -- And compilation pragmas for base types
+      when (b == builtinChar)   $ addHaskellPragma q "= type Char"
+      when (b == builtinString) $ addHaskellPragma q "= type Data.Text.Text"
+      when (b == builtinFloat)  $ addHaskellPragma q "= type Double"
+      when (b == builtinWord64) $ addHaskellPragma q "= type MAlonzo.RTE.Word64"
+      -- Finally, bind the BUILTIN in the environment.
       bindBuiltinName b $ Def q []
       where
         -- Andreas, 2015-02-14

src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs-boot

@@ -1,8 +1,13 @@
 module Agda.TypeChecking.Rules.Builtin.Coinduction where
 
 import Agda.Syntax.Scope.Base
+import Agda.Syntax.Internal (Type)
 import Agda.TypeChecking.Monad
 
+typeOfInf   :: TCM Type
+typeOfSharp :: TCM Type
+typeOfFlat  :: TCM Type
+
 bindBuiltinInf   :: ResolvedName -> TCM ()
 bindBuiltinSharp :: ResolvedName -> TCM ()
 bindBuiltinFlat  :: ResolvedName -> TCM ()

test/Compiler/simple/Issue2821.out

@@ -1,6 +1,26 @@
 EXECUTED_PROGRAM
 
 ret > ExitSuccess
+out > /Issue2821.agda:24,1-30
+out > BUILTIN STRING declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out >   {-# BUILTIN STRING String #-}
+out > /Issue2821.agda:25,1-28
+out > BUILTIN CHAR declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out >   {-# BUILTIN CHAR Char #-}
+out >
+out > ———— All done; warnings encountered ————————————————————————
+out >
+out > /Issue2821.agda:24,1-30
+out > BUILTIN STRING declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out >   {-# BUILTIN STRING String #-}
+out >
+out > /Issue2821.agda:25,1-28
+out > BUILTIN CHAR declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out >   {-# BUILTIN CHAR Char #-}
 out > ALSE
 out > RUE
 out >

test/Compiler/simple/Issue2909-5.out

@@ -1,6 +1,35 @@
 COMPILE_FAILED
 
 ret > ExitFailure 1
+out > /Issue2909-5.agda:6,1-28
+out > BUILTIN INFINITY declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out >   {-# BUILTIN INFINITY ∞ #-}
+out > /Issue2909-5.agda:7,1-28
+out > BUILTIN SHARP declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out >   {-# BUILTIN SHARP ♯_ #-}
+out > /Issue2909-5.agda:8,1-28
+out > BUILTIN FLAT declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out >   {-# BUILTIN FLAT ♭ #-}
+out >
+out > ———— All done; warnings encountered ————————————————————————
+out >
+out > /Issue2909-5.agda:6,1-28
+out > BUILTIN INFINITY declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out >   {-# BUILTIN INFINITY ∞ #-}
+out >
+out > /Issue2909-5.agda:7,1-28
+out > BUILTIN SHARP declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out >   {-# BUILTIN SHARP ♯_ #-}
+out >
+out > /Issue2909-5.agda:8,1-28
+out > BUILTIN FLAT declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out >   {-# BUILTIN FLAT ♭ #-}
 out > /Issue2909-5.agda:8,22-23
 out > "COMPILE GHC as" pragmas are not allowed for the FLAT builtin.
 out >