Remove MonadFail from HasBuiltins

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

@@ -1484,7 +1484,7 @@ instance Reify Sort where
         I.Inf u 0 -> return $ A.Def' (nameOfUniv ULarge u) A.NoSuffix
         I.Inf u n -> return $ A.Def' (nameOfUniv ULarge u) (A.Suffix n)
         I.SizeUniv  -> do
-          I.Def sizeU [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSizeUniv
+          sizeU <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSizeUniv
           return $ A.Def sizeU
         I.LockUniv  -> do
           lockU <- fromMaybe __IMPOSSIBLE__ <$> getName' builtinLockUniv

src/full/Agda/Termination/Monad.hs

@@ -11,8 +11,6 @@ import Prelude hiding (null)
 
 import Control.Applicative hiding (empty)
 
-import qualified Control.Monad.Fail as Fail
-
 import Control.Monad          ( forM )
 import Control.Monad.IO.Class ( MonadIO(..) )
 import Control.Monad.Except
@@ -179,7 +177,6 @@ newtype TerM a = TerM { terM :: ReaderT TerEnv TCM a }
   deriving ( Functor
            , Applicative
            , Monad
-           , Fail.MonadFail
            , MonadError TCErr
            , MonadStatistics
            , HasOptions

src/full/Agda/TypeChecking/Coverage/Match.hs

@@ -483,13 +483,13 @@ isLitP (DotP _ u) = reduce u >>= \case
   Lit l -> return $ Just l
   _ -> return $ Nothing
 isLitP (ConP c ci []) = do
-  Con zero _ [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinZero
-  if c == zero
+  zero <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinZero
+  if conName c == zero
     then return $ Just $ LitNat 0
     else return Nothing
 isLitP (ConP c ci [a]) | visible a && isRelevant a = do
-  Con suc _ [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSuc
-  if c == suc
+  suc <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSuc
+  if conName c == suc
     then fmap inc <$> isLitP (namedArg a)
     else return Nothing
   where

src/full/Agda/TypeChecking/Level.hs

@@ -53,46 +53,46 @@ levelType' =
 isLevelType :: PureTCM m => Type -> m Bool
 isLevelType a = reduce (unEl a) >>= \case
   Def f [] -> do
-    Def lvl [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinLevel
+    lvl <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinLevel
     return $ f == lvl
   _ -> return False
 
 {-# SPECIALIZE builtinLevelKit :: TCM LevelKit #-}
 {-# SPECIALIZE builtinLevelKit :: ReduceM LevelKit #-}
 builtinLevelKit :: (HasBuiltins m) => m LevelKit
 builtinLevelKit = do
-    level@(Def l [])     <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinLevel
-    zero@(Def z [])      <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinLevelZero
-    suc@(Def s [])       <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinLevelSuc
-    max@(Def m [])       <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinLevelMax
+    level <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinLevel
+    zero  <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinLevelZero
+    suc   <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinLevelSuc
+    max   <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinLevelMax
     return $ LevelKit
-      { lvlType  = level
-      , lvlSuc   = \ a -> suc `apply1` a
-      , lvlMax   = \ a b -> max `applys` [a, b]
-      , lvlZero  = zero
-      , typeName = l
-      , sucName  = s
-      , maxName  = m
-      , zeroName = z
+      { lvlType  = Def level []
+      , lvlSuc   = \ a -> Def suc [] `apply1` a
+      , lvlMax   = \ a b -> Def max [] `applys` [a, b]
+      , lvlZero  = Def zero []
+      , typeName = level
+      , sucName  = suc
+      , maxName  = max
+      , zeroName = zero
       }
 
 {-# SPECIALIZE requireLevels :: TCM LevelKit #-}
 -- | Raises an error if no level kit is available.
 requireLevels :: (HasBuiltins m, MonadTCError m) => m LevelKit
 requireLevels = do
-    level@(Def l [])     <- getBuiltin builtinLevel
-    zero@(Def z [])      <- getBuiltin builtinLevelZero
-    suc@(Def s [])       <- getBuiltin builtinLevelSuc
-    max@(Def m [])       <- getBuiltin builtinLevelMax
+    level <- getBuiltinName_ builtinLevel
+    zero  <- getBuiltinName_ builtinLevelZero
+    suc   <- getBuiltinName_ builtinLevelSuc
+    max   <- getBuiltinName_ builtinLevelMax
     return $ LevelKit
-      { lvlType  = level
-      , lvlSuc   = \ a -> suc `apply1` a
-      , lvlMax   = \ a b -> max `applys` [a, b]
-      , lvlZero  = zero
-      , typeName = l
-      , sucName  = s
-      , maxName  = m
-      , zeroName = z
+      { lvlType  = Def level []
+      , lvlSuc   = \ a -> Def suc [] `apply1` a
+      , lvlMax   = \ a b -> Def max [] `applys` [a, b]
+      , lvlZero  = Def zero []
+      , typeName = level
+      , sucName  = suc
+      , maxName  = max
+      , zeroName = zero
       }
 
 -- | Checks whether level kit is fully available.
@@ -132,16 +132,6 @@ unConstV zer suc n = foldr ($) zer (List.genericReplicate n suc)
 unPlusV :: (Term -> Term) -> PlusLevel -> Term
 unPlusV suc (Plus n a) = foldr ($) a (List.genericReplicate n suc)
 
-maybePrimCon :: TCM Term -> TCM (Maybe ConHead)
-maybePrimCon prim = tryMaybe $ do
-    Con c ci [] <- prim
-    return c
-
-maybePrimDef :: TCM Term -> TCM (Maybe QName)
-maybePrimDef prim = tryMaybe $ do
-    Def f [] <- prim
-    return f
-
 {-# SPECIALIZE levelView :: Term -> TCM Level #-}
 levelView :: PureTCM m => Term -> m Level
 levelView a = do
@@ -153,9 +143,9 @@ levelView a = do
 {-# SPECIALIZE levelView' :: Term -> TCM Level #-}
 levelView' :: PureTCM m => Term -> m Level
 levelView' a = do
-  Def lzero [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinLevelZero
-  Def lsuc  [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinLevelSuc
-  Def lmax  [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinLevelMax
+  lzero <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinLevelZero
+  lsuc  <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinLevelSuc
+  lmax  <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinLevelMax
   let view a = do
         ba <- reduceB a
         case ignoreBlocking ba of

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

@@ -41,7 +41,7 @@ import Agda.Utils.Impossible
 
 class ( Functor m
       , Applicative m
-      , Fail.MonadFail m
+      , Monad m
       ) => HasBuiltins m where
   getBuiltinThing :: SomeBuiltin -> m (Maybe (Builtin PrimFun))
 
@@ -152,26 +152,46 @@ getBuiltinRewriteRelations' = fmap rels <$> getBuiltinThing (BuiltinName builtin
     Prim{}    -> __IMPOSSIBLE__
     Builtin{} -> __IMPOSSIBLE__
 
+{-# INLINABLE getBuiltinName_ #-}
+getBuiltinName_ :: (HasBuiltins m, MonadTCError m)
+  => BuiltinId -> m QName
+getBuiltinName_ x =
+  fromMaybeM (typeError $ NoBindingForBuiltin x) $ getBuiltinName' x
+
+-- {-# INLINABLE getBuiltinName' #-}
+-- -- | Returns 'Nothing' if built-in is not bound or bound to a 'Prim' or anything other than a 'Def'.
+-- getBuiltinName' :: HasBuiltins m => BuiltinId -> m (Maybe Term)
+-- getBuiltinName' x = (getBuiltinName =<<) <$> getBuiltin' x
+--   where
+--     getBuiltinName = \case
+--       Def f [] -> Just f
+--       _        -> Nothing
+
 {-# INLINABLE getBuiltin #-}
 getBuiltin :: (HasBuiltins m, MonadTCError m)
            => BuiltinId -> m Term
 getBuiltin x =
   fromMaybeM (typeError $ NoBindingForBuiltin x) $ getBuiltin' x
 
 {-# INLINABLE getBuiltin' #-}
+-- | Returns 'Nothing' if built-in is not bound or bound to a 'Prim'.
 getBuiltin' :: HasBuiltins m => BuiltinId -> m (Maybe Term)
-getBuiltin' x = (getBuiltin =<<) <$> getBuiltinThing (BuiltinName x) where
-  getBuiltin BuiltinRewriteRelations{} = __IMPOSSIBLE__
-  getBuiltin (Builtin t)               = Just $ killRange t
-  getBuiltin _                         = Nothing
+getBuiltin' x = (getBuiltin =<<) <$> getBuiltinThing (BuiltinName x)
+  where
+    getBuiltin = \case
+      Builtin t                 -> Just $ killRange t
+      Prim{}                    -> Nothing
+      BuiltinRewriteRelations{} -> __IMPOSSIBLE__
 
 {-# INLINABLE getPrimitive' #-}
+-- | Returns 'Nothing' if primitive is not bound or bound to a 'Builtin'.
 getPrimitive' :: HasBuiltins m => PrimitiveId -> m (Maybe PrimFun)
 getPrimitive' x = (getPrim =<<) <$> getBuiltinThing (PrimitiveName x)
   where
-    getPrim (Prim pf) = return pf
-    getPrim BuiltinRewriteRelations{} = __IMPOSSIBLE__
-    getPrim _         = Nothing
+    getPrim = \case
+      Prim pf                   -> return pf
+      Builtin{}                 -> Nothing
+      BuiltinRewriteRelations{} -> __IMPOSSIBLE__
 
 {-# INLINABLE getPrimitive #-}
 getPrimitive :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
@@ -529,9 +549,9 @@ data CoinductionKit = CoinductionKit
 
 coinductionKit' :: TCM CoinductionKit
 coinductionKit' = do
-  Def inf   _ <- primInf
-  Def sharp _ <- primSharp
-  Def flat  _ <- primFlat
+  inf   <- getBuiltinName_ builtinInf
+  sharp <- getBuiltinName_ builtinSharp
+  flat  <- getBuiltinName_ builtinFlat
   return $ CoinductionKit
     { nameOfInf   = inf
     , nameOfSharp = sharp
@@ -574,12 +594,12 @@ mkSortKit prop set sset propomega setomega ssetomega = SortKit
 -- we report a type error rather than exploding.
 sortKit :: (HasBuiltins m, MonadTCError m, HasOptions m) => m SortKit
 sortKit = do
-  Def prop     _  <- getBuiltin builtinProp
-  Def set      _  <- getBuiltin builtinSet
-  Def sset     _  <- getBuiltin builtinStrictSet
-  Def propomega _ <- getBuiltin builtinPropOmega
-  Def setomega _  <- getBuiltin builtinSetOmega
-  Def ssetomega _ <- getBuiltin builtinSSetOmega
+  prop      <- getBuiltinName_ builtinProp
+  set       <- getBuiltinName_ builtinSet
+  sset      <- getBuiltinName_ builtinStrictSet
+  propomega <- getBuiltinName_ builtinPropOmega
+  setomega  <- getBuiltinName_ builtinSetOmega
+  ssetomega <- getBuiltinName_ builtinSSetOmega
   return $ mkSortKit prop set sset propomega setomega ssetomega
 
 -- | Compute a 'SortKit' in contexts that do not support failure (e.g.
@@ -588,12 +608,12 @@ sortKit = do
 -- checking.
 infallibleSortKit :: HasBuiltins m => m SortKit
 infallibleSortKit = do
-  Def prop     _  <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinProp
-  Def set      _  <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSet
-  Def sset     _  <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinStrictSet
-  Def propomega _ <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinPropOmega
-  Def setomega _  <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSetOmega
-  Def ssetomega _ <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSSetOmega
+  prop      <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinProp
+  set       <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSet
+  sset      <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinStrictSet
+  propomega <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinPropOmega
+  setomega  <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSetOmega
+  ssetomega <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSSetOmega
   return $ mkSortKit prop set sset propomega setomega ssetomega
 
 ------------------------------------------------------------------------
@@ -753,7 +773,6 @@ conidView' = do
 
 -- | Get the name of the equality type.
 primEqualityName :: TCM QName
--- primEqualityName = getDef =<< primEquality  -- LEADS TO IMPORT CYCLE
 primEqualityName = do
   eq <- primEquality
   -- Andreas, 2014-05-17 moved this here from TC.Rules.Def

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

@@ -7,14 +7,12 @@ import Control.Monad.State          ( StateT )
 import Control.Monad.Trans.Identity ( IdentityT )
 import Control.Monad.Trans          ( MonadTrans, lift )
 
-import qualified Control.Monad.Fail as Fail
-
 import Agda.TypeChecking.Monad.Base (TCMT, Builtin, PrimFun)
 import Agda.Syntax.Builtin (SomeBuiltin)
 
 class ( Functor m
       , Applicative m
-      , Fail.MonadFail m
+      , Monad m
       ) => HasBuiltins m where
   getBuiltinThing :: SomeBuiltin -> m (Maybe (Builtin PrimFun))
   default getBuiltinThing :: (MonadTrans t, HasBuiltins n, t n ~ m) => SomeBuiltin -> m (Maybe (Builtin PrimFun))

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

@@ -71,16 +71,10 @@ isSizeTypeTest =
         testType _                                    = Nothing
     return testType
 
-getBuiltinDefName :: (HasBuiltins m) => BuiltinId -> m (Maybe QName)
-getBuiltinDefName s = fromDef <$> getBuiltin' s
-  where
-    fromDef (Just (Def d [])) = Just d
-    fromDef _                 = Nothing
-
 getBuiltinSize :: (HasBuiltins m) => m (Maybe QName, Maybe QName)
 getBuiltinSize = do
-  size   <- getBuiltinDefName builtinSize
-  sizelt <- getBuiltinDefName builtinSizeLt
+  size   <- getBuiltinName' builtinSize
+  sizelt <- getBuiltinName' builtinSizeLt
   return (size, sizelt)
 
 isSizeNameTest :: (HasOptions m, HasBuiltins m) => m (QName -> Bool)
@@ -93,19 +87,9 @@ isSizeNameTestRaw = do
   (size, sizelt) <- getBuiltinSize
   return $ (`elem` [size, sizelt]) . Just
 
--- | Test whether OPTIONS --sized-types and whether
---   the size built-ins are defined.
-haveSizedTypes :: TCM Bool
-haveSizedTypes = do
-    Def _ [] <- primSize
-    Def _ [] <- primSizeInf
-    Def _ [] <- primSizeSuc
-    sizedTypesOption
-  `catchError` \_ -> return False
-
 -- | Test whether the SIZELT builtin is defined.
 haveSizeLt :: TCM Bool
-haveSizeLt = isJust <$> getBuiltinDefName builtinSizeLt
+haveSizeLt = isJust <$> getBuiltinName' builtinSizeLt
 
 -- | Add polarity info to a SIZE builtin.
 builtinSizeHook :: BuiltinId -> QName -> Type -> TCM ()
@@ -159,7 +143,7 @@ sizeSuc :: HasBuiltins m => Nat -> Term -> m Term
 sizeSuc n v | n < 0     = __IMPOSSIBLE__
             | n == 0    = return v
             | otherwise = do
-  Def suc [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSizeSuc
+  suc <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSizeSuc
   return $ fromMaybe __IMPOSSIBLE__ (iterate (sizeSuc_ suc) v !!! n)
 
 sizeSuc_ :: QName -> Term -> Term
@@ -171,7 +155,7 @@ sizeMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
 sizeMax vs = case vs of
   v :| [] -> return v
   vs  -> do
-    Def max [] <- primSizeMax
+    max <- getBuiltinName_ builtinSizeMax
     return $ foldr1 (\ u v -> Def max $ map (Apply . defaultArg) [u,v]) vs
 
 
@@ -186,8 +170,8 @@ data SizeView = SizeInf | SizeSuc Term | OtherSize Term
 sizeView :: (HasBuiltins m, MonadTCEnv m, ReadTCState m)
          => Term -> m SizeView
 sizeView v = do
-  Def inf [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSizeInf
-  Def suc [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSizeSuc
+  inf <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSizeInf
+  suc <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSizeSuc
   case v of
     Def x []        | x == inf -> return SizeInf
     Def x [Apply u] | x == suc -> return $ SizeSuc (unArg u)

src/full/Agda/TypeChecking/Names.hs

@@ -19,9 +19,6 @@ runNames [] $ do
 -}
 module Agda.TypeChecking.Names where
 
--- Control.Monad.Fail import is redundant since GHC 8.8.1
-import Control.Monad.Fail (MonadFail)
-
 import Control.Monad          ( liftM2, unless )
 import Control.Monad.Except   ( MonadError )
 import Control.Monad.Identity ( Identity, runIdentity )
@@ -48,7 +45,6 @@ newtype NamesT m a = NamesT { unName :: ReaderT Names m a }
   deriving ( Functor
            , Applicative
            , Monad
-           , MonadFail
            , MonadTrans
            , MonadState s
            , MonadIO

src/full/Agda/TypeChecking/Patterns/Abstract.hs

@@ -35,11 +35,11 @@ expandLitPattern = \case
     | n < 0     -> typeError NegativeLiteralInPattern  -- Andreas, issue #2365, negative literals not yet supported.
     | n > 20    -> typeError LiteralTooBig
     | otherwise -> do
-      Con z _ _ <- primZero
-      Con s _ _ <- primSuc
+      z <- getBuiltinName_ builtinZero
+      s <- getBuiltinName_ builtinSuc
       let r     = getRange info
-      let zero  = A.ConP cinfo (unambiguous $ setRange r $ conName z) []
-          suc p = A.ConP cinfo (unambiguous $ setRange r $ conName s) [defaultNamedArg p]
+      let zero  = A.ConP cinfo (unambiguous $ setRange r z) []
+          suc p = A.ConP cinfo (unambiguous $ setRange r s) [defaultNamedArg p]
           cinfo = A.ConPatInfo ConOCon info ConPatEager
       return $ foldr ($) zero $ List.genericReplicate n suc
   p -> return p

src/full/Agda/TypeChecking/Positivity.hs

@@ -835,7 +835,7 @@ instance PrettyTCM (Seq OccursWhere) where
                           [prettyTCM q]
         UnderInf     -> pwords "under" ++
                         [do -- this cannot fail if an 'UnderInf' has been generated
-                            Def inf _ <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinInf
+                            inf <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinInf
                             prettyTCM inf]
         VarArg       -> pwords "in an argument of a bound variable"
         MetaArg      -> pwords "in an argument of a metavariable"