module Agda.TypeChecking.MetaVars.Occurs where
import Control.Applicative
import Control.Monad
import Control.Monad.Error
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.Utils.Monad
class Occurs t where
occurs :: (TypeError -> TCM ()) -> MetaId -> [Nat] -> t -> TCM t
occursCheck :: MonadTCM tcm => MetaId -> [Nat] -> Term -> tcm Term
occursCheck m xs v = liftTCM $ do
v <- instantiate v
case v of
MetaV m' _ | m == m' -> patternViolation
Sort (MetaS m' _) | m == m' -> patternViolation
_ ->
occurs typeError m xs v `catchError` \err -> case errError err of
TypeError _ cl -> case clValue cl of
MetaOccursInItself{} ->
typeError . GenericError . show =<<
fsep [ text ("Refuse to construct infinite term by instantiating " ++ show m ++ " to")
, prettyTCM v
]
MetaCannotDependOn _ _ i ->
ifM ((&&) <$> isSortMeta m <*> (not <$> hasUniversePolymorphism))
( typeError . GenericError . show =<<
fsep [ text ("Cannot instantiate the metavariable " ++ show m ++ " to")
, prettyTCM v
, text "since universe polymorphism is not enabled"
, text "(use the --universe-polymorphism flag to enable)"
]
)
( typeError . GenericError . show =<<
fsep [ text ("Cannot instantiate the metavariable " ++ show m ++ " to")
, prettyTCM v
, text "since it contains the variable"
, enterClosure cl $ \_ -> prettyTCM (Var i [])
, text $ "which " ++ show m ++ " cannot depend on"
]
)
_ -> throwError err
_ -> throwError err
instance Occurs Term where
occurs abort m xs v = do
v <- reduceB v
case v of
Blocked _ v -> occurs' (const patternViolation) v
NotBlocked v -> occurs' abort v
where
occurs' abort v = case v of
Var i vs -> do
unless (i `elem` xs) $ abort $ MetaCannotDependOn m xs i
Var i <$> occ vs
Lam h f -> Lam h <$> occ f
Lit l -> return v
Def c vs -> Def c <$> occ vs
Con c vs -> Con c <$> occ vs
Pi a b -> uncurry Pi <$> occ (a,b)
Fun a b -> uncurry Fun <$> occ (a,b)
Sort s -> Sort <$> occ s
MetaV m' vs -> do
when (m == m') $ abort $ MetaOccursInItself m
MetaV m' <$> occurs (const patternViolation) m xs vs
where
occ x = occurs abort m xs x
instance Occurs Type where
occurs abort m xs (El s v) = uncurry El <$> occurs abort m xs (s,v)
instance Occurs Sort where
occurs abort m xs s =
do s' <- reduce s
case s' of
MetaS m' args -> do
when (m == m') $ abort $ MetaOccursInItself m
MetaS m' <$> occurs (const patternViolation) m xs args
Lub s1 s2 -> uncurry Lub <$> occurs abort m xs (s1,s2)
DLub s1 s2 -> uncurry DLub <$> occurs abort m xs (s1, s2)
Suc s -> Suc <$> occurs abort m xs s
Type a -> Type <$> occurs abort m xs a
Prop -> return s'
Inf -> return s'
instance Occurs a => Occurs (Abs a) where
occurs abort m xs (Abs s x) = Abs s <$> occurs abort m (0 : map (1+) xs) x
instance Occurs a => Occurs (Arg a) where
occurs abort m xs (Arg h x) = Arg h <$> occurs abort m xs x
instance (Occurs a, Occurs b) => Occurs (a,b) where
occurs abort m xs (x,y) = (,) <$> occurs abort m xs x <*> occurs abort m xs y
instance Occurs a => Occurs [a] where
occurs abort m xs ys = mapM (occurs abort m xs) ys