    module Agda.Syntax.Internal.Blockers where

    import Control.DeepSeq

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

    import GHC.Generics (Generic)

    import Agda.Syntax.Common
    import Agda.Syntax.Abstract.Name (QName)
    import Agda.Syntax.Internal.Elim

    import Agda.Syntax.Common.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 QName
        -- ^ We ran out of clauses for 'QName', 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
    $cshowsPrec :: forall t. Show t => Int -> NotBlocked' t -> ShowS
    showsPrec :: Int -> NotBlocked' t -> ShowS
    $cshow :: forall t. Show t => NotBlocked' t -> String
    show :: NotBlocked' t -> String
    $cshowList :: forall t. Show t => [NotBlocked' t] -> ShowS
    showList :: [NotBlocked' t] -> ShowS
    Show, (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
    $cfrom :: forall t x. NotBlocked' t -> Rep (NotBlocked' t) x
    from :: forall x. NotBlocked' t -> Rep (NotBlocked' t) x
    $cto :: forall t x. Rep (NotBlocked' t) x -> NotBlocked' t
    to :: forall x. Rep (NotBlocked' t) x -> NotBlocked' t
    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@MissingClauses{} <> NotBlocked' t
    _ = NotBlocked' t
    b
      NotBlocked' t
    _ <> b :: NotBlocked' t
    b@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)

    instance Pretty t => Pretty (NotBlocked' t) where
      pretty :: NotBlocked' t -> Doc
    pretty = \case
        StuckOn Elim' t
    e        -> Doc
    "elimination" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Elim' t -> Doc
    forall a. Pretty a => a -> Doc
    pretty Elim' t
    e
        NotBlocked' t
    Underapplied     -> Doc
    "missing elimination (underapplied)"
        NotBlocked' t
    AbsurdMatch      -> Doc
    "absurd match"
        MissingClauses QName
    x -> Doc
    "missing clause for" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    x
        NotBlocked' t
    ReallyNotBlocked -> Doc
    "(not stuck)"

    -- | 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
                 | UnblockOnDef QName       -- ^ Unblock when function is defined
      deriving (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
    $cshowsPrec :: Int -> Blocker -> ShowS
    showsPrec :: Int -> Blocker -> ShowS
    $cshow :: Blocker -> String
    show :: Blocker -> String
    $cshowList :: [Blocker] -> ShowS
    showList :: [Blocker] -> ShowS
    Show, Blocker -> Blocker -> Bool
    (Blocker -> Blocker -> Bool)
    -> (Blocker -> Blocker -> Bool) -> Eq Blocker
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Blocker -> Blocker -> Bool
    == :: Blocker -> Blocker -> Bool
    $c/= :: Blocker -> Blocker -> Bool
    /= :: 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
    $ccompare :: Blocker -> Blocker -> Ordering
    compare :: Blocker -> Blocker -> Ordering
    $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
    >= :: Blocker -> Blocker -> Bool
    $cmax :: Blocker -> Blocker -> Blocker
    max :: Blocker -> Blocker -> Blocker
    $cmin :: Blocker -> Blocker -> Blocker
    min :: Blocker -> Blocker -> Blocker
    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
    $cfrom :: forall x. Blocker -> Rep Blocker x
    from :: forall x. Blocker -> Rep Blocker x
    $cto :: forall x. Rep Blocker x -> Blocker
    to :: forall x. Rep Blocker x -> Blocker
    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]

    unblockOnBoth :: Blocker -> Blocker -> Blocker
    unblockOnBoth :: Blocker -> Blocker -> Blocker
    unblockOnBoth Blocker
    a Blocker
    b = 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
    a, Blocker
    b]

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

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

    unblockOnDef :: QName -> Blocker
    unblockOnDef :: QName -> Blocker
    unblockOnDef = QName -> Blocker
    UnblockOnDef

    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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Blocker
    b
    onBlockingMetasM MetaId -> m Blocker
    f b :: Blocker
    b@UnblockOnDef{}     = Blocker -> m Blocker
    forall a. a -> m a
    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
    allBlockingMetas UnblockOnDef{}     = 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
    allBlockingProblems UnblockOnDef{}       = Set ProblemId
    forall a. Set a
    Set.empty

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

    {- There are two possible instances of Semigroup, so we don't commit
       to either one.
    instance Semigroup Blocker where
      x <> y = unblockOnAll $ Set.fromList [x, y]

    instance Monoid Blocker where
      mempty = alwaysUnblock
      mappend = (<>)
    -}

    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
    forall a. Doc a -> Doc a -> Doc a
    <+> ProblemId -> Doc
    forall a. Pretty a => a -> Doc
    pretty ProblemId
    pid
      pretty (UnblockOnDef QName
    q)       = Doc
    "definition" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> QName -> Doc
    forall a. Pretty a => a -> Doc
    pretty QName
    q

    -- | 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 (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 t, Show a) => Int -> Blocked' t a -> ShowS
    forall t a. (Show t, Show a) => [Blocked' t a] -> ShowS
    forall t a. (Show t, Show a) => Blocked' t a -> String
    $cshowsPrec :: forall t a. (Show t, Show a) => Int -> Blocked' t a -> ShowS
    showsPrec :: Int -> Blocked' t a -> ShowS
    $cshow :: forall t a. (Show t, Show a) => Blocked' t a -> String
    show :: Blocked' t a -> String
    $cshowList :: forall t a. (Show t, Show a) => [Blocked' t a] -> ShowS
    showList :: [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
    $cfmap :: forall t a b. (a -> b) -> Blocked' t a -> Blocked' t b
    fmap :: forall a b. (a -> b) -> Blocked' t a -> Blocked' t b
    $c<$ :: forall t a b. a -> Blocked' t b -> Blocked' t a
    <$ :: forall a b. a -> Blocked' t b -> Blocked' t a
    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 t m. Monoid m => Blocked' t m -> m
    forall m a. Monoid m => (a -> m) -> Blocked' t a -> 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
    $cfold :: forall t m. Monoid m => Blocked' t m -> m
    fold :: forall m. Monoid m => Blocked' t m -> 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
    foldMap' :: forall m a. Monoid m => (a -> m) -> Blocked' t a -> m
    $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
    foldr' :: forall a b. (a -> b -> 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
    foldl' :: forall b a. (b -> a -> b) -> b -> Blocked' t a -> b
    $cfoldr1 :: forall t a. (a -> a -> a) -> Blocked' t a -> a
    foldr1 :: forall a. (a -> a -> a) -> Blocked' t a -> a
    $cfoldl1 :: forall t a. (a -> a -> a) -> Blocked' t a -> a
    foldl1 :: forall a. (a -> a -> a) -> Blocked' t a -> a
    $ctoList :: forall t a. Blocked' t a -> [a]
    toList :: forall a. Blocked' t a -> [a]
    $cnull :: forall t a. Blocked' t a -> Bool
    null :: forall a. Blocked' t a -> Bool
    $clength :: forall t a. Blocked' t a -> Int
    length :: forall a. Blocked' t a -> Int
    $celem :: forall t a. Eq a => a -> Blocked' t a -> Bool
    elem :: forall a. Eq a => a -> Blocked' t a -> Bool
    $cmaximum :: forall t a. Ord a => Blocked' t a -> a
    maximum :: forall a. Ord a => Blocked' t a -> a
    $cminimum :: forall t a. Ord a => Blocked' t a -> a
    minimum :: forall a. Ord a => Blocked' t a -> a
    $csum :: forall t a. Num a => Blocked' t a -> a
    sum :: forall a. Num a => Blocked' t a -> a
    $cproduct :: forall t a. Num a => Blocked' t a -> a
    product :: forall a. Num a => Blocked' t a -> a
    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)
    $ctraverse :: forall t (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Blocked' t a -> f (Blocked' t b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Blocked' t a -> f (Blocked' t b)
    $csequenceA :: forall t (f :: * -> *) a.
    Applicative f =>
    Blocked' t (f a) -> f (Blocked' t a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Blocked' t (f a) -> f (Blocked' t a)
    $cmapM :: forall t (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Blocked' t a -> m (Blocked' t b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Blocked' t a -> m (Blocked' t b)
    $csequence :: forall t (m :: * -> *) a.
    Monad m =>
    Blocked' t (m a) -> m (Blocked' t a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    Blocked' t (m a) -> m (Blocked' t a)
    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
    $cfrom :: forall t a x. Blocked' t a -> Rep (Blocked' t a) x
    from :: forall x. Blocked' t a -> Rep (Blocked' t a) x
    $cto :: forall t a x. Rep (Blocked' t a) x -> Blocked' t a
    to :: forall x. Rep (Blocked' t a) x -> Blocked' t a
    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 -> Blocker -> Blocker
    unblockOnBoth Blocker
    x 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 = \case
        r :: NotBlocked' t
    r@MissingClauses{} -> NotBlocked' t
    r
        r :: 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 ()

    getBlocker :: Blocked' t a -> Blocker
    getBlocker :: forall t a. Blocked' t a -> Blocker
    getBlocker (Blocked Blocker
    b a
    _) = Blocker
    b
    getBlocker NotBlocked{}  = Blocker
    neverUnblock

    -----------------------------------------------------------------------------
    -- * 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
    $cshowsPrec :: Int -> WakeUp -> ShowS
    showsPrec :: Int -> WakeUp -> ShowS
    $cshow :: WakeUp -> String
    show :: WakeUp -> String
    $cshowList :: [WakeUp] -> ShowS
    showList :: [WakeUp] -> ShowS
    Show, WakeUp -> WakeUp -> Bool
    (WakeUp -> WakeUp -> Bool)
    -> (WakeUp -> WakeUp -> Bool) -> Eq WakeUp
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: WakeUp -> WakeUp -> Bool
    == :: WakeUp -> WakeUp -> Bool
    $c/= :: WakeUp -> WakeUp -> Bool
    /= :: 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

    wakeIfBlockedOnDef :: QName -> Blocker -> WakeUp
    wakeIfBlockedOnDef :: QName -> Blocker -> WakeUp
    wakeIfBlockedOnDef QName
    q 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' = QName -> Blocker -> Blocker
    unblockDef QName
    q 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
    _ u :: Blocker
    u@UnblockOnDef{}     = 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
    _ u :: Blocker
    u@UnblockOnDef{}  = 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

    unblockDef :: QName -> Blocker -> Blocker
    unblockDef :: QName -> Blocker -> Blocker
    unblockDef QName
    q u :: Blocker
    u@(UnblockOnDef QName
    q') | QName
    q QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    q'   = Blocker
    alwaysUnblock
                                     | Bool
    otherwise = Blocker
    u
    unblockDef QName
    q u :: Blocker
    u@UnblockOnMeta{} = Blocker
    u
    unblockDef QName
    q u :: Blocker
    u@UnblockOnProblem{} = Blocker
    u
    unblockDef QName
    q (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 (QName -> Blocker -> Blocker
    unblockDef QName
    q) Set Blocker
    us
    unblockDef QName
    q (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 (QName -> Blocker -> Blocker
    unblockDef QName
    q) Set Blocker
    us