    module Agda.Syntax.Internal.Blockers where

    import Control.DeepSeq

    import Data.Data (Data)
    import Data.Set (Set)
    import qualified Data.Set as Set
    import Data.Semigroup

    import GHC.Generics (Generic)

    import Agda.Syntax.Common
    import Agda.Syntax.Internal.Elim

    import Agda.Utils.Pretty hiding ((<>))
    import Agda.Utils.Functor

    ---------------------------------------------------------------------------
    -- * Blocked Terms
    ---------------------------------------------------------------------------

    -- | Even if we are not stuck on a meta during reduction
    --   we can fail to reduce a definition by pattern matching
    --   for another reason.
    data NotBlocked' t
      = StuckOn (Elim' t)
        -- ^ The 'Elim' is neutral and blocks a pattern match.
      | Underapplied
        -- ^ Not enough arguments were supplied to complete the matching.
      | AbsurdMatch
        -- ^ We matched an absurd clause, results in a neutral 'Def'.
      | MissingClauses
        -- ^ We ran out of clauses, all considered clauses
        --   produced an actual mismatch.
        --   This can happen when try to reduce a function application
        --   but we are still missing some function clauses.
        --   See "Agda.TypeChecking.Patterns.Match".
      | ReallyNotBlocked
        -- ^ Reduction was not blocked, we reached a whnf
        --   which can be anything but a stuck @'Def'@.
      deriving (Int -> NotBlocked' t -> ShowS
    [NotBlocked' t] -> ShowS
    NotBlocked' t -> String
    (Int -> NotBlocked' t -> ShowS)
    -> (NotBlocked' t -> String)
    -> ([NotBlocked' t] -> ShowS)
    -> Show (NotBlocked' t)
    forall t. Show t => Int -> NotBlocked' t -> ShowS
    forall t. Show t => [NotBlocked' t] -> ShowS
    forall t. Show t => NotBlocked' t -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [NotBlocked' t] -> ShowS
    $cshowList :: forall t. Show t => [NotBlocked' t] -> ShowS
    show :: NotBlocked' t -> String
    $cshow :: forall t. Show t => NotBlocked' t -> String
    showsPrec :: Int -> NotBlocked' t -> ShowS
    $cshowsPrec :: forall t. Show t => Int -> NotBlocked' t -> ShowS
    Show, Typeable (NotBlocked' t)
    Typeable (NotBlocked' t)
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> NotBlocked' t -> c (NotBlocked' t))
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c (NotBlocked' t))
    -> (NotBlocked' t -> Constr)
    -> (NotBlocked' t -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c (NotBlocked' t)))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c (NotBlocked' t)))
    -> ((forall b. Data b => b -> b) -> NotBlocked' t -> NotBlocked' t)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r)
    -> (forall u. (forall d. Data d => d -> u) -> NotBlocked' t -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> NotBlocked' t -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d)
        -> NotBlocked' t -> m (NotBlocked' t))
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d)
        -> NotBlocked' t -> m (NotBlocked' t))
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d)
        -> NotBlocked' t -> m (NotBlocked' t))
    -> Data (NotBlocked' t)
    NotBlocked' t -> DataType
    NotBlocked' t -> Constr
    (forall b. Data b => b -> b) -> NotBlocked' t -> NotBlocked' t
    forall {t}. Data t => Typeable (NotBlocked' t)
    forall t. Data t => NotBlocked' t -> DataType
    forall t. Data t => NotBlocked' t -> Constr
    forall t.
    Data t =>
    (forall b. Data b => b -> b) -> NotBlocked' t -> NotBlocked' t
    forall t u.
    Data t =>
    Int -> (forall d. Data d => d -> u) -> NotBlocked' t -> u
    forall t u.
    Data t =>
    (forall d. Data d => d -> u) -> NotBlocked' t -> [u]
    forall t r r'.
    Data t =>
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r
    forall t r r'.
    Data t =>
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r
    forall t (m :: * -> *).
    (Data t, Monad m) =>
    (forall d. Data d => d -> m d)
    -> NotBlocked' t -> m (NotBlocked' t)
    forall t (m :: * -> *).
    (Data t, MonadPlus m) =>
    (forall d. Data d => d -> m d)
    -> NotBlocked' t -> m (NotBlocked' t)
    forall t (c :: * -> *).
    Data t =>
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (NotBlocked' t)
    forall t (c :: * -> *).
    Data t =>
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> NotBlocked' t -> c (NotBlocked' t)
    forall t (t :: * -> *) (c :: * -> *).
    (Data t, Typeable t) =>
    (forall d. Data d => c (t d)) -> Maybe (c (NotBlocked' t))
    forall t (t :: * -> * -> *) (c :: * -> *).
    (Data t, Typeable t) =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (NotBlocked' t))
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> NotBlocked' t -> u
    forall u. (forall d. Data d => d -> u) -> NotBlocked' t -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> NotBlocked' t -> m (NotBlocked' t)
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> NotBlocked' t -> m (NotBlocked' t)
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (NotBlocked' t)
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> NotBlocked' t -> c (NotBlocked' t)
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (NotBlocked' t))
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (NotBlocked' t))
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> NotBlocked' t -> m (NotBlocked' t)
    $cgmapMo :: forall t (m :: * -> *).
    (Data t, MonadPlus m) =>
    (forall d. Data d => d -> m d)
    -> NotBlocked' t -> m (NotBlocked' t)
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> NotBlocked' t -> m (NotBlocked' t)
    $cgmapMp :: forall t (m :: * -> *).
    (Data t, MonadPlus m) =>
    (forall d. Data d => d -> m d)
    -> NotBlocked' t -> m (NotBlocked' t)
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> NotBlocked' t -> m (NotBlocked' t)
    $cgmapM :: forall t (m :: * -> *).
    (Data t, Monad m) =>
    (forall d. Data d => d -> m d)
    -> NotBlocked' t -> m (NotBlocked' t)
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> NotBlocked' t -> u
    $cgmapQi :: forall t u.
    Data t =>
    Int -> (forall d. Data d => d -> u) -> NotBlocked' t -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> NotBlocked' t -> [u]
    $cgmapQ :: forall t u.
    Data t =>
    (forall d. Data d => d -> u) -> NotBlocked' t -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r
    $cgmapQr :: forall t r r'.
    Data t =>
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r
    $cgmapQl :: forall t r r'.
    Data t =>
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> NotBlocked' t -> r
    gmapT :: (forall b. Data b => b -> b) -> NotBlocked' t -> NotBlocked' t
    $cgmapT :: forall t.
    Data t =>
    (forall b. Data b => b -> b) -> NotBlocked' t -> NotBlocked' t
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (NotBlocked' t))
    $cdataCast2 :: forall t (t :: * -> * -> *) (c :: * -> *).
    (Data t, Typeable t) =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (NotBlocked' t))
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (NotBlocked' t))
    $cdataCast1 :: forall t (t :: * -> *) (c :: * -> *).
    (Data t, Typeable t) =>
    (forall d. Data d => c (t d)) -> Maybe (c (NotBlocked' t))
    dataTypeOf :: NotBlocked' t -> DataType
    $cdataTypeOf :: forall t. Data t => NotBlocked' t -> DataType
    toConstr :: NotBlocked' t -> Constr
    $ctoConstr :: forall t. Data t => NotBlocked' t -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (NotBlocked' t)
    $cgunfold :: forall t (c :: * -> *).
    Data t =>
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (NotBlocked' t)
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> NotBlocked' t -> c (NotBlocked' t)
    $cgfoldl :: forall t (c :: * -> *).
    Data t =>
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> NotBlocked' t -> c (NotBlocked' t)
    Data, (forall x. NotBlocked' t -> Rep (NotBlocked' t) x)
    -> (forall x. Rep (NotBlocked' t) x -> NotBlocked' t)
    -> Generic (NotBlocked' t)
    forall x. Rep (NotBlocked' t) x -> NotBlocked' t
    forall x. NotBlocked' t -> Rep (NotBlocked' t) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall t x. Rep (NotBlocked' t) x -> NotBlocked' t
    forall t x. NotBlocked' t -> Rep (NotBlocked' t) x
    $cto :: forall t x. Rep (NotBlocked' t) x -> NotBlocked' t
    $cfrom :: forall t x. NotBlocked' t -> Rep (NotBlocked' t) x
    Generic)

    -- | 'ReallyNotBlocked' is the unit.
    --   'MissingClauses' is dominant.
    --   @'StuckOn'{}@ should be propagated, if tied, we take the left.
    instance Semigroup (NotBlocked' t) where
      NotBlocked' t
    ReallyNotBlocked <> :: NotBlocked' t -> NotBlocked' t -> NotBlocked' t
    <> NotBlocked' t
    b = NotBlocked' t
    b
      -- MissingClauses is dominant (absorptive)
      b :: NotBlocked' t
    b@NotBlocked' t
    MissingClauses <> NotBlocked' t
    _ = NotBlocked' t
    b
      NotBlocked' t
    _ <> b :: NotBlocked' t
    b@NotBlocked' t
    MissingClauses = NotBlocked' t
    b
      -- StuckOn is second strongest
      b :: NotBlocked' t
    b@StuckOn{}      <> NotBlocked' t
    _ = NotBlocked' t
    b
      NotBlocked' t
    _ <> b :: NotBlocked' t
    b@StuckOn{}      = NotBlocked' t
    b
      NotBlocked' t
    b <> NotBlocked' t
    _                = NotBlocked' t
    b

    instance Monoid (NotBlocked' t) where
      -- ReallyNotBlocked is neutral
      mempty :: NotBlocked' t
    mempty  = NotBlocked' t
    forall t. NotBlocked' t
    ReallyNotBlocked
      mappend :: NotBlocked' t -> NotBlocked' t -> NotBlocked' t
    mappend = NotBlocked' t -> NotBlocked' t -> NotBlocked' t
    forall a. Semigroup a => a -> a -> a
    (<>)

    instance NFData t => NFData (NotBlocked' t)

    -- | What is causing the blocking? Or in other words which metas or problems need to be solved to
    --   unblock the blocked computation/constraint.
    data Blocker = UnblockOnAll (Set Blocker)
                 | UnblockOnAny (Set Blocker)
                 | UnblockOnMeta MetaId     -- ^ Unblock if meta is instantiated
                 | UnblockOnProblem ProblemId
      deriving (Typeable Blocker
    Typeable Blocker
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> Blocker -> c Blocker)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Blocker)
    -> (Blocker -> Constr)
    -> (Blocker -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Blocker))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Blocker))
    -> ((forall b. Data b => b -> b) -> Blocker -> Blocker)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> Blocker -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> Blocker -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Blocker -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> Blocker -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Blocker -> m Blocker)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Blocker -> m Blocker)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Blocker -> m Blocker)
    -> Data Blocker
    Blocker -> DataType
    Blocker -> Constr
    (forall b. Data b => b -> b) -> Blocker -> Blocker
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Blocker -> u
    forall u. (forall d. Data d => d -> u) -> Blocker -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Blocker -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Blocker -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Blocker -> m Blocker
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Blocker -> m Blocker
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Blocker
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Blocker -> c Blocker
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Blocker)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Blocker)
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Blocker -> m Blocker
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Blocker -> m Blocker
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Blocker -> m Blocker
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Blocker -> m Blocker
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Blocker -> m Blocker
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Blocker -> m Blocker
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Blocker -> u
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Blocker -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> Blocker -> [u]
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Blocker -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Blocker -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Blocker -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Blocker -> r
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Blocker -> r
    gmapT :: (forall b. Data b => b -> b) -> Blocker -> Blocker
    $cgmapT :: (forall b. Data b => b -> b) -> Blocker -> Blocker
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Blocker)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Blocker)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Blocker)
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Blocker)
    dataTypeOf :: Blocker -> DataType
    $cdataTypeOf :: Blocker -> DataType
    toConstr :: Blocker -> Constr
    $ctoConstr :: Blocker -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Blocker
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Blocker
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Blocker -> c Blocker
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Blocker -> c Blocker
    Data, Int -> Blocker -> ShowS
    [Blocker] -> ShowS
    Blocker -> String
    (Int -> Blocker -> ShowS)
    -> (Blocker -> String) -> ([Blocker] -> ShowS) -> Show Blocker
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Blocker] -> ShowS
    $cshowList :: [Blocker] -> ShowS
    show :: Blocker -> String
    $cshow :: Blocker -> String
    showsPrec :: Int -> Blocker -> ShowS
    $cshowsPrec :: Int -> Blocker -> ShowS
    Show, Blocker -> Blocker -> Bool
    (Blocker -> Blocker -> Bool)
    -> (Blocker -> Blocker -> Bool) -> Eq Blocker
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Blocker -> Blocker -> Bool
    $c/= :: Blocker -> Blocker -> Bool
    == :: Blocker -> Blocker -> Bool
    $c== :: Blocker -> Blocker -> Bool
    Eq, Eq Blocker
    Eq Blocker
    -> (Blocker -> Blocker -> Ordering)
    -> (Blocker -> Blocker -> Bool)
    -> (Blocker -> Blocker -> Bool)
    -> (Blocker -> Blocker -> Bool)
    -> (Blocker -> Blocker -> Bool)
    -> (Blocker -> Blocker -> Blocker)
    -> (Blocker -> Blocker -> Blocker)
    -> Ord Blocker
    Blocker -> Blocker -> Bool
    Blocker -> Blocker -> Ordering
    Blocker -> Blocker -> Blocker
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Blocker -> Blocker -> Blocker
    $cmin :: Blocker -> Blocker -> Blocker
    max :: Blocker -> Blocker -> Blocker
    $cmax :: Blocker -> Blocker -> Blocker
    >= :: Blocker -> Blocker -> Bool
    $c>= :: Blocker -> Blocker -> Bool
    > :: Blocker -> Blocker -> Bool
    $c> :: Blocker -> Blocker -> Bool
    <= :: Blocker -> Blocker -> Bool
    $c<= :: Blocker -> Blocker -> Bool
    < :: Blocker -> Blocker -> Bool
    $c< :: Blocker -> Blocker -> Bool
    compare :: Blocker -> Blocker -> Ordering
    $ccompare :: Blocker -> Blocker -> Ordering
    Ord, (forall x. Blocker -> Rep Blocker x)
    -> (forall x. Rep Blocker x -> Blocker) -> Generic Blocker
    forall x. Rep Blocker x -> Blocker
    forall x. Blocker -> Rep Blocker x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep Blocker x -> Blocker
    $cfrom :: forall x. Blocker -> Rep Blocker x
    Generic)

    instance NFData Blocker

    alwaysUnblock :: Blocker
    alwaysUnblock :: Blocker
    alwaysUnblock = Set Blocker -> Blocker
    UnblockOnAll Set Blocker
    forall a. Set a
    Set.empty

    neverUnblock :: Blocker
    neverUnblock :: Blocker
    neverUnblock = Set Blocker -> Blocker
    UnblockOnAny Set Blocker
    forall a. Set a
    Set.empty

    unblockOnAll :: Set Blocker -> Blocker
    unblockOnAll :: Set Blocker -> Blocker
    unblockOnAll Set Blocker
    us =
      case Set Blocker -> Set Blocker
    allViewS Set Blocker
    us of
        Set Blocker
    us | [Blocker
    u] <- Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList Set Blocker
    us -> Blocker
    u
        Set Blocker
    us                        -> Set Blocker -> Blocker
    UnblockOnAll Set Blocker
    us
      where
        allViewS :: Set Blocker -> Set Blocker
    allViewS = [Set Blocker] -> Set Blocker
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set Blocker] -> Set Blocker)
    -> (Set Blocker -> [Set Blocker]) -> Set Blocker -> Set Blocker
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Blocker -> Set Blocker) -> [Blocker] -> [Set Blocker]
    forall a b. (a -> b) -> [a] -> [b]
    map Blocker -> Set Blocker
    allView ([Blocker] -> [Set Blocker])
    -> (Set Blocker -> [Blocker]) -> Set Blocker -> [Set Blocker]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList
        allView :: Blocker -> Set Blocker
    allView (UnblockOnAll Set Blocker
    us) = Set Blocker -> Set Blocker
    allViewS Set Blocker
    us
        allView Blocker
    u                 = Blocker -> Set Blocker
    forall a. a -> Set a
    Set.singleton Blocker
    u

    unblockOnAny :: Set Blocker -> Blocker
    unblockOnAny :: Set Blocker -> Blocker
    unblockOnAny Set Blocker
    us =
      case Set Blocker -> Set Blocker
    anyViewS Set Blocker
    us of
        Set Blocker
    us | [Blocker
    u] <- Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList Set Blocker
    us        -> Blocker
    u
        Set Blocker
    us | Blocker -> Set Blocker -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member Blocker
    alwaysUnblock Set Blocker
    us -> Blocker
    alwaysUnblock
           | Bool
    otherwise                   -> Set Blocker -> Blocker
    UnblockOnAny Set Blocker
    us
      where
        anyViewS :: Set Blocker -> Set Blocker
    anyViewS = [Set Blocker] -> Set Blocker
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set Blocker] -> Set Blocker)
    -> (Set Blocker -> [Set Blocker]) -> Set Blocker -> Set Blocker
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Blocker -> Set Blocker) -> [Blocker] -> [Set Blocker]
    forall a b. (a -> b) -> [a] -> [b]
    map Blocker -> Set Blocker
    anyView ([Blocker] -> [Set Blocker])
    -> (Set Blocker -> [Blocker]) -> Set Blocker -> [Set Blocker]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList
        anyView :: Blocker -> Set Blocker
    anyView (UnblockOnAny Set Blocker
    us) = Set Blocker -> Set Blocker
    anyViewS Set Blocker
    us
        anyView Blocker
    u                 = Blocker -> Set Blocker
    forall a. a -> Set a
    Set.singleton Blocker
    u

    unblockOnEither :: Blocker -> Blocker -> Blocker
    unblockOnEither :: Blocker -> Blocker -> Blocker
    unblockOnEither Blocker
    a Blocker
    b = Set Blocker -> Blocker
    unblockOnAny (Set Blocker -> Blocker) -> Set Blocker -> Blocker
    forall a b. (a -> b) -> a -> b
    $ [Blocker] -> Set Blocker
    forall a. Ord a => [a] -> Set a
    Set.fromList [Blocker
    a, Blocker
    b]

    unblockOnMeta :: MetaId -> Blocker
    unblockOnMeta :: MetaId -> Blocker
    unblockOnMeta = MetaId -> Blocker
    UnblockOnMeta

    unblockOnProblem :: ProblemId -> Blocker
    unblockOnProblem :: ProblemId -> Blocker
    unblockOnProblem = ProblemId -> Blocker
    UnblockOnProblem

    unblockOnAllMetas :: Set MetaId -> Blocker
    unblockOnAllMetas :: Set MetaId -> Blocker
    unblockOnAllMetas = Set Blocker -> Blocker
    unblockOnAll (Set Blocker -> Blocker)
    -> (Set MetaId -> Set Blocker) -> Set MetaId -> Blocker
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (MetaId -> Blocker) -> Set MetaId -> Set Blocker
    forall a b. (a -> b) -> Set a -> Set b
    Set.mapMonotonic MetaId -> Blocker
    unblockOnMeta

    unblockOnAnyMeta :: Set MetaId -> Blocker
    unblockOnAnyMeta :: Set MetaId -> Blocker
    unblockOnAnyMeta = Set Blocker -> Blocker
    unblockOnAny (Set Blocker -> Blocker)
    -> (Set MetaId -> Set Blocker) -> Set MetaId -> Blocker
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (MetaId -> Blocker) -> Set MetaId -> Set Blocker
    forall a b. (a -> b) -> Set a -> Set b
    Set.mapMonotonic MetaId -> Blocker
    unblockOnMeta

    onBlockingMetasM :: Monad m => (MetaId -> m Blocker) -> Blocker -> m Blocker
    onBlockingMetasM :: forall (m :: * -> *).
    Monad m =>
    (MetaId -> m Blocker) -> Blocker -> m Blocker
    onBlockingMetasM MetaId -> m Blocker
    f (UnblockOnAll Set Blocker
    bs)    = Set Blocker -> Blocker
    unblockOnAll (Set Blocker -> Blocker)
    -> ([Blocker] -> Set Blocker) -> [Blocker] -> Blocker
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Blocker] -> Set Blocker
    forall a. Ord a => [a] -> Set a
    Set.fromList ([Blocker] -> Blocker) -> m [Blocker] -> m Blocker
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Blocker -> m Blocker) -> [Blocker] -> m [Blocker]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((MetaId -> m Blocker) -> Blocker -> m Blocker
    forall (m :: * -> *).
    Monad m =>
    (MetaId -> m Blocker) -> Blocker -> m Blocker
    onBlockingMetasM MetaId -> m Blocker
    f) (Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList Set Blocker
    bs)
    onBlockingMetasM MetaId -> m Blocker
    f (UnblockOnAny Set Blocker
    bs)    = Set Blocker -> Blocker
    unblockOnAny (Set Blocker -> Blocker)
    -> ([Blocker] -> Set Blocker) -> [Blocker] -> Blocker
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Blocker] -> Set Blocker
    forall a. Ord a => [a] -> Set a
    Set.fromList ([Blocker] -> Blocker) -> m [Blocker] -> m Blocker
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Blocker -> m Blocker) -> [Blocker] -> m [Blocker]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((MetaId -> m Blocker) -> Blocker -> m Blocker
    forall (m :: * -> *).
    Monad m =>
    (MetaId -> m Blocker) -> Blocker -> m Blocker
    onBlockingMetasM MetaId -> m Blocker
    f) (Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList Set Blocker
    bs)
    onBlockingMetasM MetaId -> m Blocker
    f (UnblockOnMeta MetaId
    x)    = MetaId -> m Blocker
    f MetaId
    x
    onBlockingMetasM MetaId -> m Blocker
    f b :: Blocker
    b@UnblockOnProblem{} = Blocker -> m Blocker
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Blocker
    b

    allBlockingMetas :: Blocker -> Set MetaId
    allBlockingMetas :: Blocker -> Set MetaId
    allBlockingMetas (UnblockOnAll Set Blocker
    us)  = [Set MetaId] -> Set MetaId
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set MetaId] -> Set MetaId) -> [Set MetaId] -> Set MetaId
    forall a b. (a -> b) -> a -> b
    $ (Blocker -> Set MetaId) -> [Blocker] -> [Set MetaId]
    forall a b. (a -> b) -> [a] -> [b]
    map Blocker -> Set MetaId
    allBlockingMetas ([Blocker] -> [Set MetaId]) -> [Blocker] -> [Set MetaId]
    forall a b. (a -> b) -> a -> b
    $ Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList Set Blocker
    us
    allBlockingMetas (UnblockOnAny Set Blocker
    us)  = [Set MetaId] -> Set MetaId
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set MetaId] -> Set MetaId) -> [Set MetaId] -> Set MetaId
    forall a b. (a -> b) -> a -> b
    $ (Blocker -> Set MetaId) -> [Blocker] -> [Set MetaId]
    forall a b. (a -> b) -> [a] -> [b]
    map Blocker -> Set MetaId
    allBlockingMetas ([Blocker] -> [Set MetaId]) -> [Blocker] -> [Set MetaId]
    forall a b. (a -> b) -> a -> b
    $ Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList Set Blocker
    us
    allBlockingMetas (UnblockOnMeta MetaId
    x)  = MetaId -> Set MetaId
    forall a. a -> Set a
    Set.singleton MetaId
    x
    allBlockingMetas UnblockOnProblem{} = Set MetaId
    forall a. Set a
    Set.empty

    allBlockingProblems :: Blocker -> Set ProblemId
    allBlockingProblems :: Blocker -> Set ProblemId
    allBlockingProblems (UnblockOnAll Set Blocker
    us)    = [Set ProblemId] -> Set ProblemId
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set ProblemId] -> Set ProblemId)
    -> [Set ProblemId] -> Set ProblemId
    forall a b. (a -> b) -> a -> b
    $ (Blocker -> Set ProblemId) -> [Blocker] -> [Set ProblemId]
    forall a b. (a -> b) -> [a] -> [b]
    map Blocker -> Set ProblemId
    allBlockingProblems ([Blocker] -> [Set ProblemId]) -> [Blocker] -> [Set ProblemId]
    forall a b. (a -> b) -> a -> b
    $ Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList Set Blocker
    us
    allBlockingProblems (UnblockOnAny Set Blocker
    us)    = [Set ProblemId] -> Set ProblemId
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set ProblemId] -> Set ProblemId)
    -> [Set ProblemId] -> Set ProblemId
    forall a b. (a -> b) -> a -> b
    $ (Blocker -> Set ProblemId) -> [Blocker] -> [Set ProblemId]
    forall a b. (a -> b) -> [a] -> [b]
    map Blocker -> Set ProblemId
    allBlockingProblems ([Blocker] -> [Set ProblemId]) -> [Blocker] -> [Set ProblemId]
    forall a b. (a -> b) -> a -> b
    $ Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList Set Blocker
    us
    allBlockingProblems UnblockOnMeta{}      = Set ProblemId
    forall a. Set a
    Set.empty
    allBlockingProblems (UnblockOnProblem ProblemId
    p) = ProblemId -> Set ProblemId
    forall a. a -> Set a
    Set.singleton ProblemId
    p

    -- Note: We pick the All rather than the Any as the semigroup instance.
    instance Semigroup Blocker where
      Blocker
    x <> :: Blocker -> Blocker -> Blocker
    <> Blocker
    y = Set Blocker -> Blocker
    unblockOnAll (Set Blocker -> Blocker) -> Set Blocker -> Blocker
    forall a b. (a -> b) -> a -> b
    $ [Blocker] -> Set Blocker
    forall a. Ord a => [a] -> Set a
    Set.fromList [Blocker
    x, Blocker
    y]

    instance Monoid Blocker where
      mempty :: Blocker
    mempty = Blocker
    alwaysUnblock
      mappend :: Blocker -> Blocker -> Blocker
    mappend = Blocker -> Blocker -> Blocker
    forall a. Semigroup a => a -> a -> a
    (<>)

    instance Pretty Blocker where
      pretty :: Blocker -> Doc
    pretty (UnblockOnAll Set Blocker
    us)      = Doc
    "all" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc -> Doc
    parens ([Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> [Doc] -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    "," ([Doc] -> [Doc]) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ (Blocker -> Doc) -> [Blocker] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Blocker -> Doc
    forall a. Pretty a => a -> Doc
    pretty ([Blocker] -> [Doc]) -> [Blocker] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList Set Blocker
    us)
      pretty (UnblockOnAny Set Blocker
    us)      = Doc
    "any" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc -> Doc
    parens ([Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> [Doc] -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    punctuate Doc
    "," ([Doc] -> [Doc]) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ (Blocker -> Doc) -> [Blocker] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Blocker -> Doc
    forall a. Pretty a => a -> Doc
    pretty ([Blocker] -> [Doc]) -> [Blocker] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ Set Blocker -> [Blocker]
    forall a. Set a -> [a]
    Set.toList Set Blocker
    us)
      pretty (UnblockOnMeta MetaId
    m)      = MetaId -> Doc
    forall a. Pretty a => a -> Doc
    pretty MetaId
    m
      pretty (UnblockOnProblem ProblemId
    pid) = Doc
    "problem" Doc -> Doc -> Doc
    <+> ProblemId -> Doc
    forall a. Pretty a => a -> Doc
    pretty ProblemId
    pid

    -- | Something where a meta variable may block reduction. Notably a top-level meta is considered
    --   blocking. This did not use to be the case (pre Aug 2020).
    data Blocked' t a
      = Blocked    { forall t a. Blocked' t a -> Blocker
    theBlocker      :: Blocker,       forall t a. Blocked' t a -> a
    ignoreBlocking :: a }
      | NotBlocked { forall t a. Blocked' t a -> NotBlocked' t
    blockingStatus  :: NotBlocked' t, ignoreBlocking :: a }
      deriving (Typeable (Blocked' t a)
    Typeable (Blocked' t a)
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> Blocked' t a -> c (Blocked' t a))
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c (Blocked' t a))
    -> (Blocked' t a -> Constr)
    -> (Blocked' t a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c (Blocked' t a)))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c (Blocked' t a)))
    -> ((forall b. Data b => b -> b) -> Blocked' t a -> Blocked' t a)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Blocked' t a -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> Blocked' t a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a))
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a))
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a))
    -> Data (Blocked' t a)
    Blocked' t a -> DataType
    Blocked' t a -> Constr
    (forall b. Data b => b -> b) -> Blocked' t a -> Blocked' t a
    forall a.
    Typeable a
    -> (forall (c :: * -> *).
        (forall d b. Data d => c (d -> b) -> d -> c b)
        -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Blocked' t a -> u
    forall u. (forall d. Data d => d -> u) -> Blocked' t a -> [u]
    forall {t} {a}. (Data t, Data a) => Typeable (Blocked' t a)
    forall t a. (Data t, Data a) => Blocked' t a -> DataType
    forall t a. (Data t, Data a) => Blocked' t a -> Constr
    forall t a.
    (Data t, Data a) =>
    (forall b. Data b => b -> b) -> Blocked' t a -> Blocked' t a
    forall t a u.
    (Data t, Data a) =>
    Int -> (forall d. Data d => d -> u) -> Blocked' t a -> u
    forall t a u.
    (Data t, Data a) =>
    (forall d. Data d => d -> u) -> Blocked' t a -> [u]
    forall t a r r'.
    (Data t, Data a) =>
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r
    forall t a r r'.
    (Data t, Data a) =>
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r
    forall t a (m :: * -> *).
    (Data t, Data a, Monad m) =>
    (forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
    forall t a (m :: * -> *).
    (Data t, Data a, MonadPlus m) =>
    (forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
    forall t a (c :: * -> *).
    (Data t, Data a) =>
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Blocked' t a)
    forall t a (c :: * -> *).
    (Data t, Data a) =>
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Blocked' t a -> c (Blocked' t a)
    forall t a (t :: * -> *) (c :: * -> *).
    (Data t, Data a, Typeable t) =>
    (forall d. Data d => c (t d)) -> Maybe (c (Blocked' t a))
    forall t a (t :: * -> * -> *) (c :: * -> *).
    (Data t, Data a, Typeable t) =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Blocked' t a))
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Blocked' t a)
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Blocked' t a -> c (Blocked' t a)
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Blocked' t a))
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Blocked' t a))
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
    $cgmapMo :: forall t a (m :: * -> *).
    (Data t, Data a, MonadPlus m) =>
    (forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
    $cgmapMp :: forall t a (m :: * -> *).
    (Data t, Data a, MonadPlus m) =>
    (forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
    $cgmapM :: forall t a (m :: * -> *).
    (Data t, Data a, Monad m) =>
    (forall d. Data d => d -> m d) -> Blocked' t a -> m (Blocked' t a)
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Blocked' t a -> u
    $cgmapQi :: forall t a u.
    (Data t, Data a) =>
    Int -> (forall d. Data d => d -> u) -> Blocked' t a -> u
    gmapQ :: forall u. (forall d. Data d => d -> u) -> Blocked' t a -> [u]
    $cgmapQ :: forall t a u.
    (Data t, Data a) =>
    (forall d. Data d => d -> u) -> Blocked' t a -> [u]
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r
    $cgmapQr :: forall t a r r'.
    (Data t, Data a) =>
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r
    $cgmapQl :: forall t a r r'.
    (Data t, Data a) =>
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Blocked' t a -> r
    gmapT :: (forall b. Data b => b -> b) -> Blocked' t a -> Blocked' t a
    $cgmapT :: forall t a.
    (Data t, Data a) =>
    (forall b. Data b => b -> b) -> Blocked' t a -> Blocked' t a
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Blocked' t a))
    $cdataCast2 :: forall t a (t :: * -> * -> *) (c :: * -> *).
    (Data t, Data a, Typeable t) =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Blocked' t a))
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Blocked' t a))
    $cdataCast1 :: forall t a (t :: * -> *) (c :: * -> *).
    (Data t, Data a, Typeable t) =>
    (forall d. Data d => c (t d)) -> Maybe (c (Blocked' t a))
    dataTypeOf :: Blocked' t a -> DataType
    $cdataTypeOf :: forall t a. (Data t, Data a) => Blocked' t a -> DataType
    toConstr :: Blocked' t a -> Constr
    $ctoConstr :: forall t a. (Data t, Data a) => Blocked' t a -> Constr
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Blocked' t a)
    $cgunfold :: forall t a (c :: * -> *).
    (Data t, Data a) =>
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Blocked' t a)
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Blocked' t a -> c (Blocked' t a)
    $cgfoldl :: forall t a (c :: * -> *).
    (Data t, Data a) =>
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Blocked' t a -> c (Blocked' t a)
    Data, Int -> Blocked' t a -> ShowS
    [Blocked' t a] -> ShowS
    Blocked' t a -> String
    (Int -> Blocked' t a -> ShowS)
    -> (Blocked' t a -> String)
    -> ([Blocked' t a] -> ShowS)
    -> Show (Blocked' t a)
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    forall t a. (Show a, Show t) => Int -> Blocked' t a -> ShowS
    forall t a. (Show a, Show t) => [Blocked' t a] -> ShowS
    forall t a. (Show a, Show t) => Blocked' t a -> String
    showList :: [Blocked' t a] -> ShowS
    $cshowList :: forall t a. (Show a, Show t) => [Blocked' t a] -> ShowS
    show :: Blocked' t a -> String
    $cshow :: forall t a. (Show a, Show t) => Blocked' t a -> String
    showsPrec :: Int -> Blocked' t a -> ShowS
    $cshowsPrec :: forall t a. (Show a, Show t) => Int -> Blocked' t a -> ShowS
    Show, (forall a b. (a -> b) -> Blocked' t a -> Blocked' t b)
    -> (forall a b. a -> Blocked' t b -> Blocked' t a)
    -> Functor (Blocked' t)
    forall a b. a -> Blocked' t b -> Blocked' t a
    forall a b. (a -> b) -> Blocked' t a -> Blocked' t b
    forall t a b. a -> Blocked' t b -> Blocked' t a
    forall t a b. (a -> b) -> Blocked' t a -> Blocked' t b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: forall a b. a -> Blocked' t b -> Blocked' t a
    $c<$ :: forall t a b. a -> Blocked' t b -> Blocked' t a
    fmap :: forall a b. (a -> b) -> Blocked' t a -> Blocked' t b
    $cfmap :: forall t a b. (a -> b) -> Blocked' t a -> Blocked' t b
    Functor, (forall m. Monoid m => Blocked' t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Blocked' t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Blocked' t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Blocked' t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Blocked' t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Blocked' t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Blocked' t a -> b)
    -> (forall a. (a -> a -> a) -> Blocked' t a -> a)
    -> (forall a. (a -> a -> a) -> Blocked' t a -> a)
    -> (forall a. Blocked' t a -> [a])
    -> (forall a. Blocked' t a -> Bool)
    -> (forall a. Blocked' t a -> Int)
    -> (forall a. Eq a => a -> Blocked' t a -> Bool)
    -> (forall a. Ord a => Blocked' t a -> a)
    -> (forall a. Ord a => Blocked' t a -> a)
    -> (forall a. Num a => Blocked' t a -> a)
    -> (forall a. Num a => Blocked' t a -> a)
    -> Foldable (Blocked' t)
    forall a. Eq a => a -> Blocked' t a -> Bool
    forall a. Num a => Blocked' t a -> a
    forall a. Ord a => Blocked' t a -> a
    forall m. Monoid m => Blocked' t m -> m
    forall a. Blocked' t a -> Bool
    forall a. Blocked' t a -> Int
    forall a. Blocked' t a -> [a]
    forall a. (a -> a -> a) -> Blocked' t a -> a
    forall t a. Eq a => a -> Blocked' t a -> Bool
    forall t a. Num a => Blocked' t a -> a
    forall t a. Ord a => Blocked' t a -> a
    forall m a. Monoid m => (a -> m) -> Blocked' t a -> m
    forall t m. Monoid m => Blocked' t m -> m
    forall t a. Blocked' t a -> Bool
    forall t a. Blocked' t a -> Int
    forall t a. Blocked' t a -> [a]
    forall b a. (b -> a -> b) -> b -> Blocked' t a -> b
    forall a b. (a -> b -> b) -> b -> Blocked' t a -> b
    forall t a. (a -> a -> a) -> Blocked' t a -> a
    forall t m a. Monoid m => (a -> m) -> Blocked' t a -> m
    forall t b a. (b -> a -> b) -> b -> Blocked' t a -> b
    forall t a b. (a -> b -> b) -> b -> Blocked' t a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    product :: forall a. Num a => Blocked' t a -> a
    $cproduct :: forall t a. Num a => Blocked' t a -> a
    sum :: forall a. Num a => Blocked' t a -> a
    $csum :: forall t a. Num a => Blocked' t a -> a
    minimum :: forall a. Ord a => Blocked' t a -> a
    $cminimum :: forall t a. Ord a => Blocked' t a -> a
    maximum :: forall a. Ord a => Blocked' t a -> a
    $cmaximum :: forall t a. Ord a => Blocked' t a -> a
    elem :: forall a. Eq a => a -> Blocked' t a -> Bool
    $celem :: forall t a. Eq a => a -> Blocked' t a -> Bool
    length :: forall a. Blocked' t a -> Int
    $clength :: forall t a. Blocked' t a -> Int
    null :: forall a. Blocked' t a -> Bool
    $cnull :: forall t a. Blocked' t a -> Bool
    toList :: forall a. Blocked' t a -> [a]
    $ctoList :: forall t a. Blocked' t a -> [a]
    foldl1 :: forall a. (a -> a -> a) -> Blocked' t a -> a
    $cfoldl1 :: forall t a. (a -> a -> a) -> Blocked' t a -> a
    foldr1 :: forall a. (a -> a -> a) -> Blocked' t a -> a
    $cfoldr1 :: forall t a. (a -> a -> a) -> Blocked' t a -> a
    foldl' :: forall b a. (b -> a -> b) -> b -> Blocked' t a -> b
    $cfoldl' :: forall t b a. (b -> a -> b) -> b -> Blocked' t a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Blocked' t a -> b
    $cfoldl :: forall t b a. (b -> a -> b) -> b -> Blocked' t a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Blocked' t a -> b
    $cfoldr' :: forall t a b. (a -> b -> b) -> b -> Blocked' t a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Blocked' t a -> b
    $cfoldr :: forall t a b. (a -> b -> b) -> b -> Blocked' t a -> b
    foldMap' :: forall m a. Monoid m => (a -> m) -> Blocked' t a -> m
    $cfoldMap' :: forall t m a. Monoid m => (a -> m) -> Blocked' t a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Blocked' t a -> m
    $cfoldMap :: forall t m a. Monoid m => (a -> m) -> Blocked' t a -> m
    fold :: forall m. Monoid m => Blocked' t m -> m
    $cfold :: forall t m. Monoid m => Blocked' t m -> m
    Foldable, Functor (Blocked' t)
    Foldable (Blocked' t)
    Functor (Blocked' t)
    -> Foldable (Blocked' t)
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> Blocked' t a -> f (Blocked' t b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        Blocked' t (f a) -> f (Blocked' t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> Blocked' t a -> m (Blocked' t b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        Blocked' t (m a) -> m (Blocked' t a))
    -> Traversable (Blocked' t)
    forall t. Functor (Blocked' t)
    forall t. Foldable (Blocked' t)
    forall t (m :: * -> *) a.
    Monad m =>
    Blocked' t (m a) -> m (Blocked' t a)
    forall t (f :: * -> *) a.
    Applicative f =>
    Blocked' t (f a) -> f (Blocked' t a)
    forall t (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Blocked' t a -> m (Blocked' t b)
    forall t (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Blocked' t a -> f (Blocked' t b)
    forall (t :: * -> *).
    Functor t
    -> Foldable t
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a.
    Monad m =>
    Blocked' t (m a) -> m (Blocked' t a)
    forall (f :: * -> *) a.
    Applicative f =>
    Blocked' t (f a) -> f (Blocked' t a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Blocked' t a -> m (Blocked' t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Blocked' t a -> f (Blocked' t b)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    Blocked' t (m a) -> m (Blocked' t a)
    $csequence :: forall t (m :: * -> *) a.
    Monad m =>
    Blocked' t (m a) -> m (Blocked' t a)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Blocked' t a -> m (Blocked' t b)
    $cmapM :: forall t (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Blocked' t a -> m (Blocked' t b)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Blocked' t (f a) -> f (Blocked' t a)
    $csequenceA :: forall t (f :: * -> *) a.
    Applicative f =>
    Blocked' t (f a) -> f (Blocked' t a)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Blocked' t a -> f (Blocked' t b)
    $ctraverse :: forall t (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Blocked' t a -> f (Blocked' t b)
    Traversable, (forall x. Blocked' t a -> Rep (Blocked' t a) x)
    -> (forall x. Rep (Blocked' t a) x -> Blocked' t a)
    -> Generic (Blocked' t a)
    forall x. Rep (Blocked' t a) x -> Blocked' t a
    forall x. Blocked' t a -> Rep (Blocked' t a) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall t a x. Rep (Blocked' t a) x -> Blocked' t a
    forall t a x. Blocked' t a -> Rep (Blocked' t a) x
    $cto :: forall t a x. Rep (Blocked' t a) x -> Blocked' t a
    $cfrom :: forall t a x. Blocked' t a -> Rep (Blocked' t a) x
    Generic)

    instance Decoration (Blocked' t) where
      traverseF :: forall (m :: * -> *) a b.
    Functor m =>
    (a -> m b) -> Blocked' t a -> m (Blocked' t b)
    traverseF a -> m b
    f (Blocked Blocker
    b a
    x)     = Blocker -> b -> Blocked' t b
    forall t a. Blocker -> a -> Blocked' t a
    Blocked Blocker
    b (b -> Blocked' t b) -> m b -> m (Blocked' t b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m b
    f a
    x
      traverseF a -> m b
    f (NotBlocked NotBlocked' t
    nb a
    x) = NotBlocked' t -> b -> Blocked' t b
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' t
    nb (b -> Blocked' t b) -> m b -> m (Blocked' t b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m b
    f a
    x

    -- | Blocking on _all_ blockers.
    instance Applicative (Blocked' t) where
      pure :: forall a. a -> Blocked' t a
    pure = a -> Blocked' t a
    forall a t. a -> Blocked' t a
    notBlocked
      Blocked' t (a -> b)
    f <*> :: forall a b. Blocked' t (a -> b) -> Blocked' t a -> Blocked' t b
    <*> Blocked' t a
    e = ((Blocked' t (a -> b)
    f Blocked' t (a -> b) -> () -> Blocked' t ()
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> ()) Blocked' t () -> Blocked' t () -> Blocked' t ()
    forall a. Monoid a => a -> a -> a
    `mappend` (Blocked' t a
    e Blocked' t a -> () -> Blocked' t ()
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> ())) Blocked' t () -> b -> Blocked' t b
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Blocked' t (a -> b) -> a -> b
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked' t (a -> b)
    f (Blocked' t a -> a
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked' t a
    e)

    instance Semigroup a => Semigroup (Blocked' t a) where
      Blocked Blocker
    x a
    a    <> :: Blocked' t a -> Blocked' t a -> Blocked' t a
    <> Blocked Blocker
    y a
    b    = Blocker -> a -> Blocked' t a
    forall t a. Blocker -> a -> Blocked' t a
    Blocked (Blocker
    x Blocker -> Blocker -> Blocker
    forall a. Semigroup a => a -> a -> a
    <> Blocker
    y) (a
    a a -> a -> a
    forall a. Semigroup a => a -> a -> a
    <> a
    b)
      b :: Blocked' t a
    b@Blocked{}    <> NotBlocked{}   = Blocked' t a
    b
      NotBlocked{}   <> b :: Blocked' t a
    b@Blocked{}    = Blocked' t a
    b
      NotBlocked NotBlocked' t
    x a
    a <> NotBlocked NotBlocked' t
    y a
    b = NotBlocked' t -> a -> Blocked' t a
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked (NotBlocked' t
    x NotBlocked' t -> NotBlocked' t -> NotBlocked' t
    forall a. Semigroup a => a -> a -> a
    <> NotBlocked' t
    y) (a
    a a -> a -> a
    forall a. Semigroup a => a -> a -> a
    <> a
    b)

    instance (Semigroup a, Monoid a) => Monoid (Blocked' t a) where
      mempty :: Blocked' t a
    mempty = a -> Blocked' t a
    forall a t. a -> Blocked' t a
    notBlocked a
    forall a. Monoid a => a
    mempty
      mappend :: Blocked' t a -> Blocked' t a -> Blocked' t a
    mappend = Blocked' t a -> Blocked' t a -> Blocked' t a
    forall a. Semigroup a => a -> a -> a
    (<>)

    instance (NFData t, NFData a) => NFData (Blocked' t a)

    -- | When trying to reduce @f es@, on match failed on one
    --   elimination @e ∈ es@ that came with info @r :: NotBlocked@.
    --   @stuckOn e r@ produces the new @NotBlocked@ info.
    --
    --   'MissingClauses' must be propagated, as this is blockage
    --   that can be lifted in the future (as more clauses are added).
    --
    --   @'StuckOn' e0@ is also propagated, since it provides more
    --   precise information as @StuckOn e@ (as @e0@ is the original
    --   reason why reduction got stuck and usually a subterm of @e@).
    --   An information like @StuckOn (Apply (Arg info (Var i [])))@
    --   (stuck on a variable) could be used by the lhs/coverage checker
    --   to trigger a split on that (pattern) variable.
    --
    --   In the remaining cases for @r@, we are terminally stuck
    --   due to @StuckOn e@.  Propagating @'AbsurdMatch'@ does not
    --   seem useful.
    --
    --   'Underapplied' must not be propagated, as this would mean
    --   that @f es@ is underapplied, which is not the case (it is stuck).
    --   Note that 'Underapplied' can only arise when projection patterns were
    --   missing to complete the original match (in @e@).
    --   (Missing ordinary pattern would mean the @e@ is of function type,
    --   but we cannot match against something of function type.)
    stuckOn :: Elim' t -> NotBlocked' t -> NotBlocked' t
    stuckOn :: forall t. Elim' t -> NotBlocked' t -> NotBlocked' t
    stuckOn Elim' t
    e NotBlocked' t
    r =
      case NotBlocked' t
    r of
        NotBlocked' t
    MissingClauses   -> NotBlocked' t
    r
        StuckOn{}        -> NotBlocked' t
    r
        NotBlocked' t
    Underapplied     -> NotBlocked' t
    r'
        NotBlocked' t
    AbsurdMatch      -> NotBlocked' t
    r'
        NotBlocked' t
    ReallyNotBlocked -> NotBlocked' t
    r'
      where r' :: NotBlocked' t
    r' = Elim' t -> NotBlocked' t
    forall t. Elim' t -> NotBlocked' t
    StuckOn Elim' t
    e

    ---------------------------------------------------------------------------
    -- * Handling blocked terms.
    ---------------------------------------------------------------------------

    blockedOn :: Blocker -> a -> Blocked' t a
    blockedOn :: forall a t. Blocker -> a -> Blocked' t a
    blockedOn Blocker
    b | Blocker
    alwaysUnblock Blocker -> Blocker -> Bool
    forall a. Eq a => a -> a -> Bool
    == Blocker
    b = a -> Blocked' t a
    forall a t. a -> Blocked' t a
    notBlocked
                | Bool
    otherwise          = Blocker -> a -> Blocked' t a
    forall t a. Blocker -> a -> Blocked' t a
    Blocked Blocker
    b

    blocked :: MetaId -> a -> Blocked' t a
    blocked :: forall a t. MetaId -> a -> Blocked' t a
    blocked = Blocker -> a -> Blocked' t a
    forall t a. Blocker -> a -> Blocked' t a
    Blocked (Blocker -> a -> Blocked' t a)
    -> (MetaId -> Blocker) -> MetaId -> a -> Blocked' t a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaId -> Blocker
    unblockOnMeta

    notBlocked :: a -> Blocked' t a
    notBlocked :: forall a t. a -> Blocked' t a
    notBlocked = NotBlocked' t -> a -> Blocked' t a
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' t
    forall t. NotBlocked' t
    ReallyNotBlocked

    blocked_ :: MetaId -> Blocked' t ()
    blocked_ :: forall t. MetaId -> Blocked' t ()
    blocked_ MetaId
    x = MetaId -> () -> Blocked' t ()
    forall a t. MetaId -> a -> Blocked' t a
    blocked MetaId
    x ()

    notBlocked_ :: Blocked' t ()
    notBlocked_ :: forall t. Blocked' t ()
    notBlocked_ = () -> Blocked' t ()
    forall a t. a -> Blocked' t a
    notBlocked ()

    -----------------------------------------------------------------------------
    -- * Waking up logic
    -----------------------------------------------------------------------------

    -- | Should a constraint wake up or not? If not, we might refine the unblocker.
    data WakeUp = WakeUp | DontWakeUp (Maybe Blocker)
      deriving (Int -> WakeUp -> ShowS
    [WakeUp] -> ShowS
    WakeUp -> String
    (Int -> WakeUp -> ShowS)
    -> (WakeUp -> String) -> ([WakeUp] -> ShowS) -> Show WakeUp
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [WakeUp] -> ShowS
    $cshowList :: [WakeUp] -> ShowS
    show :: WakeUp -> String
    $cshow :: WakeUp -> String
    showsPrec :: Int -> WakeUp -> ShowS
    $cshowsPrec :: Int -> WakeUp -> ShowS
    Show, WakeUp -> WakeUp -> Bool
    (WakeUp -> WakeUp -> Bool)
    -> (WakeUp -> WakeUp -> Bool) -> Eq WakeUp
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: WakeUp -> WakeUp -> Bool
    $c/= :: WakeUp -> WakeUp -> Bool
    == :: WakeUp -> WakeUp -> Bool
    $c== :: WakeUp -> WakeUp -> Bool
    Eq)

    wakeUpWhen :: (constr -> Bool) -> (constr -> WakeUp) -> constr -> WakeUp
    wakeUpWhen :: forall constr.
    (constr -> Bool) -> (constr -> WakeUp) -> constr -> WakeUp
    wakeUpWhen constr -> Bool
    guard constr -> WakeUp
    wake constr
    c | constr -> Bool
    guard constr
    c   = constr -> WakeUp
    wake constr
    c
                            | Bool
    otherwise = Maybe Blocker -> WakeUp
    DontWakeUp Maybe Blocker
    forall a. Maybe a
    Nothing

    wakeUpWhen_ :: (constr -> Bool) -> constr -> WakeUp
    wakeUpWhen_ :: forall constr. (constr -> Bool) -> constr -> WakeUp
    wakeUpWhen_ constr -> Bool
    p = (constr -> Bool) -> (constr -> WakeUp) -> constr -> WakeUp
    forall constr.
    (constr -> Bool) -> (constr -> WakeUp) -> constr -> WakeUp
    wakeUpWhen constr -> Bool
    p (WakeUp -> constr -> WakeUp
    forall a b. a -> b -> a
    const WakeUp
    WakeUp)

    wakeIfBlockedOnProblem :: ProblemId -> Blocker -> WakeUp
    wakeIfBlockedOnProblem :: ProblemId -> Blocker -> WakeUp
    wakeIfBlockedOnProblem ProblemId
    pid Blocker
    u
      | Blocker
    u' Blocker -> Blocker -> Bool
    forall a. Eq a => a -> a -> Bool
    == Blocker
    alwaysUnblock = WakeUp
    WakeUp
      | Bool
    otherwise           = Maybe Blocker -> WakeUp
    DontWakeUp (Blocker -> Maybe Blocker
    forall a. a -> Maybe a
    Just Blocker
    u')
      where
        u' :: Blocker
    u' = ProblemId -> Blocker -> Blocker
    unblockProblem ProblemId
    pid Blocker
    u

    wakeIfBlockedOnMeta :: MetaId -> Blocker -> WakeUp
    wakeIfBlockedOnMeta :: MetaId -> Blocker -> WakeUp
    wakeIfBlockedOnMeta MetaId
    x Blocker
    u
      | Blocker
    u' Blocker -> Blocker -> Bool
    forall a. Eq a => a -> a -> Bool
    == Blocker
    alwaysUnblock = WakeUp
    WakeUp
      | Bool
    otherwise           = Maybe Blocker -> WakeUp
    DontWakeUp (Blocker -> Maybe Blocker
    forall a. a -> Maybe a
    Just Blocker
    u')
      where
        u' :: Blocker
    u' = MetaId -> Blocker -> Blocker
    unblockMeta MetaId
    x Blocker
    u

    unblockMeta :: MetaId -> Blocker -> Blocker
    unblockMeta :: MetaId -> Blocker -> Blocker
    unblockMeta MetaId
    x u :: Blocker
    u@(UnblockOnMeta MetaId
    y) | MetaId
    x MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == MetaId
    y    = Blocker
    alwaysUnblock
                                      | Bool
    otherwise = Blocker
    u
    unblockMeta MetaId
    _ u :: Blocker
    u@UnblockOnProblem{} = Blocker
    u
    unblockMeta MetaId
    x (UnblockOnAll Set Blocker
    us)    = Set Blocker -> Blocker
    unblockOnAll (Set Blocker -> Blocker) -> Set Blocker -> Blocker
    forall a b. (a -> b) -> a -> b
    $ (Blocker -> Blocker) -> Set Blocker -> Set Blocker
    forall b a. Ord b => (a -> b) -> Set a -> Set b
    Set.map (MetaId -> Blocker -> Blocker
    unblockMeta MetaId
    x) Set Blocker
    us
    unblockMeta MetaId
    x (UnblockOnAny Set Blocker
    us)    = Set Blocker -> Blocker
    unblockOnAny (Set Blocker -> Blocker) -> Set Blocker -> Blocker
    forall a b. (a -> b) -> a -> b
    $ (Blocker -> Blocker) -> Set Blocker -> Set Blocker
    forall b a. Ord b => (a -> b) -> Set a -> Set b
    Set.map (MetaId -> Blocker -> Blocker
    unblockMeta MetaId
    x) Set Blocker
    us

    unblockProblem :: ProblemId -> Blocker -> Blocker
    unblockProblem :: ProblemId -> Blocker -> Blocker
    unblockProblem ProblemId
    p u :: Blocker
    u@(UnblockOnProblem ProblemId
    q) | ProblemId
    p ProblemId -> ProblemId -> Bool
    forall a. Eq a => a -> a -> Bool
    == ProblemId
    q    = Blocker
    alwaysUnblock
                                            | Bool
    otherwise = Blocker
    u
    unblockProblem ProblemId
    _ u :: Blocker
    u@UnblockOnMeta{} = Blocker
    u
    unblockProblem ProblemId
    p (UnblockOnAll Set Blocker
    us) = Set Blocker -> Blocker
    unblockOnAll (Set Blocker -> Blocker) -> Set Blocker -> Blocker
    forall a b. (a -> b) -> a -> b
    $ (Blocker -> Blocker) -> Set Blocker -> Set Blocker
    forall b a. Ord b => (a -> b) -> Set a -> Set b
    Set.map (ProblemId -> Blocker -> Blocker
    unblockProblem ProblemId
    p) Set Blocker
    us
    unblockProblem ProblemId
    p (UnblockOnAny Set Blocker
    us) = Set Blocker -> Blocker
    unblockOnAny (Set Blocker -> Blocker) -> Set Blocker -> Blocker
    forall a b. (a -> b) -> a -> b
    $ (Blocker -> Blocker) -> Set Blocker -> Set Blocker
    forall b a. Ord b => (a -> b) -> Set a -> Set b
    Set.map (ProblemId -> Blocker -> Blocker
    unblockProblem ProblemId
    p) Set Blocker
    us