-- | Free variable check that reduces the subject to make certain variables not
--   free. Used when pruning metavariables in Agda.TypeChecking.MetaVars.Occurs.
module Agda.TypeChecking.Free.Reduce
  ( ForceNotFree
  , forceNotFree
  , reallyFree
  , IsFree(..)
  ) where

import Prelude hiding (null)

import Control.Monad.Reader
import Control.Monad.State

import qualified Data.IntMap as IntMap
import Data.IntMap (IntMap)
import qualified Data.IntSet as IntSet
import Data.IntSet (IntSet)

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Free
import Agda.TypeChecking.Free.Precompute

import Agda.Utils.Monad
import Agda.Utils.Null

-- | A variable can either not occur (`NotFree`) or it does occur
--   (`MaybeFree`).  In the latter case, the occurrence may disappear
--   depending on the instantiation of some set of metas.
data IsFree
  = MaybeFree MetaSet
  | NotFree
  deriving (IsFree -> IsFree -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IsFree -> IsFree -> Bool
$c/= :: IsFree -> IsFree -> Bool
== :: IsFree -> IsFree -> Bool
$c== :: IsFree -> IsFree -> Bool
Eq, Int -> IsFree -> ShowS
[IsFree] -> ShowS
IsFree -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IsFree] -> ShowS
$cshowList :: [IsFree] -> ShowS
show :: IsFree -> String
$cshow :: IsFree -> String
showsPrec :: Int -> IsFree -> ShowS
$cshowsPrec :: Int -> IsFree -> ShowS
Show)

-- | Try to enforce a set of variables not occurring in a given
--   type. Returns a possibly reduced version of the type and for each
--   of the given variables whether it is either not free, or
--   maybe free depending on some metavariables.
forceNotFree :: (ForceNotFree a, Reduce a, MonadReduce m)
             => IntSet -> a -> m (IntMap IsFree, a)
forceNotFree :: forall a (m :: * -> *).
(ForceNotFree a, Reduce a, MonadReduce m) =>
IntSet -> a -> m (IntMap IsFree, a)
forceNotFree IntSet
xs a
a = do
  -- Initially, all variables are marked as `NotFree`. This is changed
  -- to `MaybeFree` when we find an occurrence.
  let mxs :: IntMap IsFree
mxs = forall a. (Int -> a) -> IntSet -> IntMap a
IntMap.fromSet (forall a b. a -> b -> a
const IsFree
NotFree) IntSet
xs
  (a
a, IntMap IsFree
mxs) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFreeR forall a b. (a -> b) -> a -> b
$ forall a. PrecomputeFreeVars a => a -> a
precomputeFreeVars_ a
a) forall a. Monoid a => a
mempty) IntMap IsFree
mxs
  forall (m :: * -> *) a. Monad m => a -> m a
return (IntMap IsFree
mxs, a
a)

-- | Checks if the given term contains any free variables that are in
--   the given set of variables, possibly reducing the term in the
--   process.  Returns `Right Nothing` if there are such variables,
--   `Right (Just v')` if there are none (where v' is the possibly
--   reduced version of the given term) or `Left b` if the problem is
--   blocked on a meta.
reallyFree :: (MonadReduce m, Reduce a, ForceNotFree a)
           => IntSet -> a -> m (Either Blocked_ (Maybe a))
reallyFree :: forall (m :: * -> *) a.
(MonadReduce m, Reduce a, ForceNotFree a) =>
IntSet -> a -> m (Either Blocked_ (Maybe a))
reallyFree IntSet
xs a
v = do
  (IntMap IsFree
mxs , a
v') <- forall a (m :: * -> *).
(ForceNotFree a, Reduce a, MonadReduce m) =>
IntSet -> a -> m (IntMap IsFree, a)
forceNotFree IntSet
xs a
v
  case forall a b. (a -> b -> b) -> b -> IntMap a -> b
IntMap.foldr IsFree -> IsFree -> IsFree
pickFree IsFree
NotFree IntMap IsFree
mxs of
    MaybeFree MetaSet
ms
      | forall a. Null a => a -> Bool
null MetaSet
ms   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a. Maybe a
Nothing
      | Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
blocker ()
      where blocker :: Blocker
blocker = MetaSet -> Blocker
metaSetToBlocker MetaSet
ms
    IsFree
NotFree -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right (forall a. a -> Maybe a
Just a
v')

  where
    -- Check if any of the variables occur freely.
    -- Prefer occurrences that do not depend on any metas.
    pickFree :: IsFree -> IsFree -> IsFree
    pickFree :: IsFree -> IsFree -> IsFree
pickFree f1 :: IsFree
f1@(MaybeFree MetaSet
ms1) IsFree
f2
      | forall a. Null a => a -> Bool
null MetaSet
ms1  = IsFree
f1
    pickFree f1 :: IsFree
f1@(MaybeFree MetaSet
ms1) f2 :: IsFree
f2@(MaybeFree MetaSet
ms2)
      | forall a. Null a => a -> Bool
null MetaSet
ms2  = IsFree
f2
      | Bool
otherwise = IsFree
f1
    pickFree f1 :: IsFree
f1@(MaybeFree MetaSet
ms1) IsFree
NotFree = IsFree
f1
    pickFree IsFree
NotFree IsFree
f2 = IsFree
f2

type MonadFreeRed m =
  ( MonadReader MetaSet m
  , MonadState (IntMap IsFree) m
  , MonadReduce m
  )

class (PrecomputeFreeVars a, Subst a) => ForceNotFree a where
  -- Reduce the argument if necessary, to make as many as possible of
  -- the variables in the state not free. Updates the state, marking
  -- the variables that couldn't be make not free as `MaybeFree`. By
  -- updating the state as soon as a variable can not be reduced away,
  -- we avoid trying to get rid of it in other places.
  forceNotFree' :: (MonadFreeRed m) => a -> m a

-- Return the set of variables for which there is still hope that they
-- may not occur.
varsToForceNotFree :: (MonadFreeRed m) => m IntSet
varsToForceNotFree :: forall (m :: * -> *). MonadFreeRed m => m IntSet
varsToForceNotFree = forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall a. IntMap a -> IntSet
IntMap.keysSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. (a -> Bool) -> IntMap a -> IntMap a
IntMap.filter (forall a. Eq a => a -> a -> Bool
== IsFree
NotFree)))

-- Reduce the argument if there are offending free variables. Doesn't call the
-- continuation when no reduction is required.
reduceIfFreeVars :: (Reduce a, ForceNotFree a, MonadFreeRed m)
                 => (a -> m a) -> a -> m a
reduceIfFreeVars :: forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
(a -> m a) -> a -> m a
reduceIfFreeVars a -> m a
k a
a = do
  IntSet
xs <- forall (m :: * -> *). MonadFreeRed m => m IntSet
varsToForceNotFree
  let fvs :: IntSet
fvs     = forall a. PrecomputeFreeVars a => a -> IntSet
precomputedFreeVars a
a
      notfree :: Bool
notfree = IntSet -> IntSet -> Bool
IntSet.disjoint IntSet
xs IntSet
fvs
  if Bool
notfree
    then forall (m :: * -> *) a. Monad m => a -> m a
return a
a
    else a -> m a
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PrecomputeFreeVars a => a -> a
precomputeFreeVars_ forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce a
a

-- Careful not to define forceNotFree' = forceNotFreeR since that would loop.
forceNotFreeR :: (Reduce a, ForceNotFree a, MonadFreeRed m)
              => a -> m a
forceNotFreeR :: forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFreeR = forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
(a -> m a) -> a -> m a
reduceIfFreeVars forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree'

instance (Reduce a, ForceNotFree a) => ForceNotFree (Arg a) where
  -- Precomputed free variables are stored in the Arg so reduceIf outside the
  -- traverse.
  forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => Arg a -> m (Arg a)
forceNotFree' = forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
(a -> m a) -> a -> m a
reduceIfFreeVars (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree')

instance (Reduce a, ForceNotFree a, TermSubst a) => ForceNotFree (Dom a) where
  forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => Dom a -> m (Dom a)
forceNotFree' = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFreeR

instance (Reduce a, ForceNotFree a) => ForceNotFree (Abs a) where
  -- Reduction stops at abstractions (lambda/pi) so do reduceIf/forceNotFreeR here.
  forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => Abs a -> m (Abs a)
forceNotFree' a :: Abs a
a@NoAbs{} = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFreeR Abs a
a
  forceNotFree' a :: Abs a
a@Abs{} =
    -- Shift variables up when going under the abstraction and back down when
    -- coming out of it. Since we never add new indices to the state
    -- there's no danger of getting negative indices.
    forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
(a -> m a) -> a -> m a
reduceIfFreeVars (forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ (forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall a. (Int -> Int) -> IntMap a -> IntMap a
IntMap.mapKeys forall a. Enum a => a -> a
succ) (\ ()
_ -> forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall a. (Int -> Int) -> IntMap a -> IntMap a
IntMap.mapKeys forall a. Enum a => a -> a
pred) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                      forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree') Abs a
a

instance ForceNotFree a => ForceNotFree [a] where
  forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => [a] -> m [a]
forceNotFree' = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree'

instance (Reduce a, ForceNotFree a) => ForceNotFree (Elim' a) where
  -- There's an Arg inside Elim' which stores precomputed free vars, so let's
  -- not skip over that.
  forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => Elim' a -> m (Elim' a)
forceNotFree' (Apply Arg a
arg)    = forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Arg a
arg
  forceNotFree' e :: Elim' a
e@Proj{}       = forall (m :: * -> *) a. Monad m => a -> m a
return Elim' a
e
  forceNotFree' (IApply a
x a
y a
r) = forall a. a -> a -> a -> Elim' a
IApply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFreeR a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFreeR a
y forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFreeR a
r

instance ForceNotFree Type where
  forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => Type -> m Type
forceNotFree' (El Sort' Term
s Term
t) = forall t a. Sort' t -> a -> Type'' t a
El forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Sort' Term
s forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Term
t

instance ForceNotFree Term where
  forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => Term -> m Term
forceNotFree' = \case
    Var Int
x Elims
es   -> do
      MetaSet
metas <- forall r (m :: * -> *). MonadReader r m => m r
ask
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall a. (a -> a) -> Int -> IntMap a -> IntMap a
IntMap.adjust (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ MetaSet -> IsFree
MaybeFree MetaSet
metas) Int
x
      Int -> Elims -> Term
Var Int
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Elims
es
    Def QName
f Elims
es   -> QName -> Elims -> Term
Def QName
f    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Elims
es
    Con ConHead
c ConInfo
h Elims
es -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
h  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Elims
es
    MetaV MetaId
x Elims
es -> forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (MetaId -> MetaSet -> MetaSet
insertMetaSet MetaId
x) forall a b. (a -> b) -> a -> b
$
                  MetaId -> Elims -> Term
MetaV MetaId
x  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Elims
es
    Lam ArgInfo
h Abs Term
b    -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
h    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Abs Term
b
    Pi Dom Type
a Abs Type
b     -> Dom Type -> Abs Type -> Term
Pi       forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Dom Type
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Abs Type
b  -- Dom and Abs do reduceIf so not needed here
    Sort Sort' Term
s     -> Sort' Term -> Term
Sort     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Sort' Term
s
    Level Level
l    -> Level -> Term
Level    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Level
l
    DontCare Term
t -> Term -> Term
DontCare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(Reduce a, ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFreeR Term
t  -- Reduction stops at DontCare so reduceIf
    t :: Term
t@Lit{}    -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
    t :: Term
t@Dummy{}  -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

instance ForceNotFree Level where
  forceNotFree' :: forall (m :: * -> *). MonadFreeRed m => Level -> m Level
forceNotFree' (Max Integer
m [PlusLevel' Term]
as) = forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' [PlusLevel' Term]
as

instance ForceNotFree PlusLevel where
  forceNotFree' :: forall (m :: * -> *).
MonadFreeRed m =>
PlusLevel' Term -> m (PlusLevel' Term)
forceNotFree' (Plus Integer
k Term
a) = forall t. Integer -> t -> PlusLevel' t
Plus Integer
k forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Term
a

instance ForceNotFree Sort where
  -- Reduce for sorts already goes under all sort constructors, so we can get
  -- away without forceNotFreeR here.
  forceNotFree' :: forall (m :: * -> *).
MonadFreeRed m =>
Sort' Term -> m (Sort' Term)
forceNotFree' = \case
    Type Level
l     -> forall t. Level' t -> Sort' t
Type     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Level
l
    Prop Level
l     -> forall t. Level' t -> Sort' t
Prop     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Level
l
    SSet Level
l     -> forall t. Level' t -> Sort' t
SSet     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Level
l
    PiSort Dom' Term Term
a Sort' Term
b Abs (Sort' Term)
c -> forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Dom' Term Term
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Sort' Term
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Abs (Sort' Term)
c
    FunSort Sort' Term
a Sort' Term
b -> forall t. Sort' t -> Sort' t -> Sort' t
FunSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Sort' Term
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Sort' Term
b
    UnivSort Sort' Term
s -> forall t. Sort' t -> Sort' t
UnivSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Sort' Term
s
    MetaS MetaId
x Elims
es -> forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Elims
es
    DefS QName
d Elims
es  -> forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ForceNotFree a, MonadFreeRed m) =>
a -> m a
forceNotFree' Elims
es
    s :: Sort' Term
s@(Inf IsFibrant
_ Integer
_)-> forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
    s :: Sort' Term
s@Sort' Term
SizeUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
    s :: Sort' Term
s@Sort' Term
LockUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
    s :: Sort' Term
s@Sort' Term
IntervalUniv -> forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
    s :: Sort' Term
s@DummyS{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s