    module Agda.TypeChecking.Rules.LHS.Problem
           ( FlexibleVars , FlexibleVarKind(..) , FlexibleVar(..) , allFlexVars
           , FlexChoice(..) , ChooseFlex(..)
           , ProblemEq(..) , Problem(..) , problemEqs
           , problemRestPats, problemCont, problemInPats
           , AsBinding(..) , DotPattern(..) , AbsurdPattern(..), AnnotationPattern(..)
           , LHSState(..) , lhsTel , lhsOutPat , lhsProblem , lhsTarget
           , LeftoverPatterns(..), getLeftoverPatterns, getUserVariableNames
           ) where

    import Prelude hiding (null)

    import Control.Arrow        ( (***) )
    import Control.Monad        ( zipWithM )
    import Control.Monad.Writer ( MonadWriter(..), Writer, runWriter )

    import Data.Functor (($>))
    import Data.IntMap (IntMap)
    import qualified Data.IntMap as IntMap
    import Data.List ( partition )
    import Data.Semigroup ( Semigroup, (<>) )
    import qualified Data.Set as Set

    import Agda.Syntax.Common
    import Agda.Syntax.Position
    import Agda.Syntax.Internal
    import Agda.Syntax.Abstract (ProblemEq(..))
    import qualified Agda.Syntax.Abstract as A

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Pretty

    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.Null
    import Agda.Utils.Singleton
    import Agda.Utils.Size
    import qualified Agda.Utils.Pretty as PP

    type FlexibleVars   = [FlexibleVar Nat]

    -- | When we encounter a flexible variable in the unifier, where did it come from?
    --   The alternatives are ordered such that we will assign the higher one first,
    --   i.e., first we try to assign a @DotFlex@, then...
    data FlexibleVarKind
      = RecordFlex [FlexibleVarKind]
          -- ^ From a record pattern ('ConP').
          --   Saves the 'FlexibleVarKind' of its subpatterns.
      | ImplicitFlex -- ^ From a hidden formal argument or underscore ('WildP').
      | DotFlex      -- ^ From a dot pattern ('DotP').
      | OtherFlex    -- ^ From a non-record constructor or literal ('ConP' or 'LitP').
      deriving (FlexibleVarKind -> FlexibleVarKind -> Bool
    (FlexibleVarKind -> FlexibleVarKind -> Bool)
    -> (FlexibleVarKind -> FlexibleVarKind -> Bool)
    -> Eq FlexibleVarKind
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: FlexibleVarKind -> FlexibleVarKind -> Bool
    $c/= :: FlexibleVarKind -> FlexibleVarKind -> Bool
    == :: FlexibleVarKind -> FlexibleVarKind -> Bool
    $c== :: FlexibleVarKind -> FlexibleVarKind -> Bool
    Eq, Int -> FlexibleVarKind -> ShowS
    [FlexibleVarKind] -> ShowS
    FlexibleVarKind -> ArgName
    (Int -> FlexibleVarKind -> ShowS)
    -> (FlexibleVarKind -> ArgName)
    -> ([FlexibleVarKind] -> ShowS)
    -> Show FlexibleVarKind
    forall a.
    (Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
    showList :: [FlexibleVarKind] -> ShowS
    $cshowList :: [FlexibleVarKind] -> ShowS
    show :: FlexibleVarKind -> ArgName
    $cshow :: FlexibleVarKind -> ArgName
    showsPrec :: Int -> FlexibleVarKind -> ShowS
    $cshowsPrec :: Int -> FlexibleVarKind -> ShowS
    Show)

    -- | Flexible variables are equipped with information where they come from,
    --   in order to make a choice which one to assign when two flexibles are unified.
    data FlexibleVar a = FlexibleVar
      { forall a. FlexibleVar a -> ArgInfo
    flexArgInfo :: ArgInfo
      , forall a. FlexibleVar a -> IsForced
    flexForced  :: IsForced
      , forall a. FlexibleVar a -> FlexibleVarKind
    flexKind    :: FlexibleVarKind
      , forall a. FlexibleVar a -> Maybe Int
    flexPos     :: Maybe Int
      , forall a. FlexibleVar a -> a
    flexVar     :: a
      } deriving (FlexibleVar a -> FlexibleVar a -> Bool
    (FlexibleVar a -> FlexibleVar a -> Bool)
    -> (FlexibleVar a -> FlexibleVar a -> Bool) -> Eq (FlexibleVar a)
    forall a. Eq a => FlexibleVar a -> FlexibleVar a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: FlexibleVar a -> FlexibleVar a -> Bool
    $c/= :: forall a. Eq a => FlexibleVar a -> FlexibleVar a -> Bool
    == :: FlexibleVar a -> FlexibleVar a -> Bool
    $c== :: forall a. Eq a => FlexibleVar a -> FlexibleVar a -> Bool
    Eq, Int -> FlexibleVar a -> ShowS
    [FlexibleVar a] -> ShowS
    FlexibleVar a -> ArgName
    (Int -> FlexibleVar a -> ShowS)
    -> (FlexibleVar a -> ArgName)
    -> ([FlexibleVar a] -> ShowS)
    -> Show (FlexibleVar a)
    forall a. Show a => Int -> FlexibleVar a -> ShowS
    forall a. Show a => [FlexibleVar a] -> ShowS
    forall a. Show a => FlexibleVar a -> ArgName
    forall a.
    (Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
    showList :: [FlexibleVar a] -> ShowS
    $cshowList :: forall a. Show a => [FlexibleVar a] -> ShowS
    show :: FlexibleVar a -> ArgName
    $cshow :: forall a. Show a => FlexibleVar a -> ArgName
    showsPrec :: Int -> FlexibleVar a -> ShowS
    $cshowsPrec :: forall a. Show a => Int -> FlexibleVar a -> ShowS
    Show, (forall a b. (a -> b) -> FlexibleVar a -> FlexibleVar b)
    -> (forall a b. a -> FlexibleVar b -> FlexibleVar a)
    -> Functor FlexibleVar
    forall a b. a -> FlexibleVar b -> FlexibleVar a
    forall a b. (a -> b) -> FlexibleVar a -> FlexibleVar 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 -> FlexibleVar b -> FlexibleVar a
    $c<$ :: forall a b. a -> FlexibleVar b -> FlexibleVar a
    fmap :: forall a b. (a -> b) -> FlexibleVar a -> FlexibleVar b
    $cfmap :: forall a b. (a -> b) -> FlexibleVar a -> FlexibleVar b
    Functor, (forall m. Monoid m => FlexibleVar m -> m)
    -> (forall m a. Monoid m => (a -> m) -> FlexibleVar a -> m)
    -> (forall m a. Monoid m => (a -> m) -> FlexibleVar a -> m)
    -> (forall a b. (a -> b -> b) -> b -> FlexibleVar a -> b)
    -> (forall a b. (a -> b -> b) -> b -> FlexibleVar a -> b)
    -> (forall b a. (b -> a -> b) -> b -> FlexibleVar a -> b)
    -> (forall b a. (b -> a -> b) -> b -> FlexibleVar a -> b)
    -> (forall a. (a -> a -> a) -> FlexibleVar a -> a)
    -> (forall a. (a -> a -> a) -> FlexibleVar a -> a)
    -> (forall a. FlexibleVar a -> [a])
    -> (forall a. FlexibleVar a -> Bool)
    -> (forall a. FlexibleVar a -> Int)
    -> (forall a. Eq a => a -> FlexibleVar a -> Bool)
    -> (forall a. Ord a => FlexibleVar a -> a)
    -> (forall a. Ord a => FlexibleVar a -> a)
    -> (forall a. Num a => FlexibleVar a -> a)
    -> (forall a. Num a => FlexibleVar a -> a)
    -> Foldable FlexibleVar
    forall a. Eq a => a -> FlexibleVar a -> Bool
    forall a. Num a => FlexibleVar a -> a
    forall a. Ord a => FlexibleVar a -> a
    forall m. Monoid m => FlexibleVar m -> m
    forall a. FlexibleVar a -> Bool
    forall a. FlexibleVar a -> Int
    forall a. FlexibleVar a -> [a]
    forall a. (a -> a -> a) -> FlexibleVar a -> a
    forall m a. Monoid m => (a -> m) -> FlexibleVar a -> m
    forall b a. (b -> a -> b) -> b -> FlexibleVar a -> b
    forall a b. (a -> b -> b) -> b -> FlexibleVar 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 => FlexibleVar a -> a
    $cproduct :: forall a. Num a => FlexibleVar a -> a
    sum :: forall a. Num a => FlexibleVar a -> a
    $csum :: forall a. Num a => FlexibleVar a -> a
    minimum :: forall a. Ord a => FlexibleVar a -> a
    $cminimum :: forall a. Ord a => FlexibleVar a -> a
    maximum :: forall a. Ord a => FlexibleVar a -> a
    $cmaximum :: forall a. Ord a => FlexibleVar a -> a
    elem :: forall a. Eq a => a -> FlexibleVar a -> Bool
    $celem :: forall a. Eq a => a -> FlexibleVar a -> Bool
    length :: forall a. FlexibleVar a -> Int
    $clength :: forall a. FlexibleVar a -> Int
    null :: forall a. FlexibleVar a -> Bool
    $cnull :: forall a. FlexibleVar a -> Bool
    toList :: forall a. FlexibleVar a -> [a]
    $ctoList :: forall a. FlexibleVar a -> [a]
    foldl1 :: forall a. (a -> a -> a) -> FlexibleVar a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> FlexibleVar a -> a
    foldr1 :: forall a. (a -> a -> a) -> FlexibleVar a -> a
    $cfoldr1 :: forall a. (a -> a -> a) -> FlexibleVar a -> a
    foldl' :: forall b a. (b -> a -> b) -> b -> FlexibleVar a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> FlexibleVar a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> FlexibleVar a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> FlexibleVar a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> FlexibleVar a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> FlexibleVar a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> FlexibleVar a -> b
    $cfoldr :: forall a b. (a -> b -> b) -> b -> FlexibleVar a -> b
    foldMap' :: forall m a. Monoid m => (a -> m) -> FlexibleVar a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> FlexibleVar a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> FlexibleVar a -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> FlexibleVar a -> m
    fold :: forall m. Monoid m => FlexibleVar m -> m
    $cfold :: forall m. Monoid m => FlexibleVar m -> m
    Foldable, Functor FlexibleVar
    Foldable FlexibleVar
    Functor FlexibleVar
    -> Foldable FlexibleVar
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> FlexibleVar a -> f (FlexibleVar b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        FlexibleVar (f a) -> f (FlexibleVar a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> FlexibleVar a -> m (FlexibleVar b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        FlexibleVar (m a) -> m (FlexibleVar a))
    -> Traversable FlexibleVar
    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 =>
    FlexibleVar (m a) -> m (FlexibleVar a)
    forall (f :: * -> *) a.
    Applicative f =>
    FlexibleVar (f a) -> f (FlexibleVar a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> FlexibleVar a -> m (FlexibleVar b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> FlexibleVar a -> f (FlexibleVar b)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    FlexibleVar (m a) -> m (FlexibleVar a)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    FlexibleVar (m a) -> m (FlexibleVar a)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> FlexibleVar a -> m (FlexibleVar b)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> FlexibleVar a -> m (FlexibleVar b)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    FlexibleVar (f a) -> f (FlexibleVar a)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    FlexibleVar (f a) -> f (FlexibleVar a)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> FlexibleVar a -> f (FlexibleVar b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> FlexibleVar a -> f (FlexibleVar b)
    Traversable)

    instance LensArgInfo (FlexibleVar a) where
      getArgInfo :: FlexibleVar a -> ArgInfo
    getArgInfo = FlexibleVar a -> ArgInfo
    forall a. FlexibleVar a -> ArgInfo
    flexArgInfo
      setArgInfo :: ArgInfo -> FlexibleVar a -> FlexibleVar a
    setArgInfo ArgInfo
    ai FlexibleVar a
    fl = FlexibleVar a
    fl { flexArgInfo :: ArgInfo
    flexArgInfo = ArgInfo
    ai }
      mapArgInfo :: (ArgInfo -> ArgInfo) -> FlexibleVar a -> FlexibleVar a
    mapArgInfo ArgInfo -> ArgInfo
    f  FlexibleVar a
    fl = FlexibleVar a
    fl { flexArgInfo :: ArgInfo
    flexArgInfo = ArgInfo -> ArgInfo
    f (FlexibleVar a -> ArgInfo
    forall a. FlexibleVar a -> ArgInfo
    flexArgInfo FlexibleVar a
    fl) }

    instance LensHiding (FlexibleVar a)
    instance LensOrigin (FlexibleVar a)
    instance LensModality (FlexibleVar a)

    -- UNUSED
    -- defaultFlexibleVar :: a -> FlexibleVar a
    -- defaultFlexibleVar a = FlexibleVar Hidden Inserted ImplicitFlex Nothing a

    -- UNUSED
    -- flexibleVarFromHiding :: Hiding -> a -> FlexibleVar a
    -- flexibleVarFromHiding h a = FlexibleVar h ImplicitFlex Nothing a

    allFlexVars :: [IsForced] -> Telescope -> FlexibleVars
    allFlexVars :: [IsForced] -> Telescope -> FlexibleVars
    allFlexVars [IsForced]
    forced Telescope
    tel = (Int -> Dom (ArgName, Type) -> IsForced -> FlexibleVar Int)
    -> [Int] -> [Dom (ArgName, Type)] -> [IsForced] -> FlexibleVars
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 Int -> Dom (ArgName, Type) -> IsForced -> FlexibleVar Int
    forall {a}.
    LensArgInfo a =>
    Int -> a -> IsForced -> FlexibleVar Int
    makeFlex (Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    n) (Telescope -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Telescope
    tel) [IsForced]
    fs
      where
        n :: Int
    n  = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel
        fs :: [IsForced]
    fs = [IsForced]
    forced [IsForced] -> [IsForced] -> [IsForced]
    forall a. [a] -> [a] -> [a]
    ++ IsForced -> [IsForced]
    forall a. a -> [a]
    repeat IsForced
    NotForced
        makeFlex :: Int -> a -> IsForced -> FlexibleVar Int
    makeFlex Int
    i a
    d IsForced
    f = ArgInfo
    -> IsForced
    -> FlexibleVarKind
    -> Maybe Int
    -> Int
    -> FlexibleVar Int
    forall a.
    ArgInfo
    -> IsForced -> FlexibleVarKind -> Maybe Int -> a -> FlexibleVar a
    FlexibleVar (a -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo a
    d) IsForced
    f FlexibleVarKind
    ImplicitFlex (Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    i) Int
    i

    data FlexChoice = ChooseLeft | ChooseRight | ChooseEither | ExpandBoth
      deriving (FlexChoice -> FlexChoice -> Bool
    (FlexChoice -> FlexChoice -> Bool)
    -> (FlexChoice -> FlexChoice -> Bool) -> Eq FlexChoice
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: FlexChoice -> FlexChoice -> Bool
    $c/= :: FlexChoice -> FlexChoice -> Bool
    == :: FlexChoice -> FlexChoice -> Bool
    $c== :: FlexChoice -> FlexChoice -> Bool
    Eq, Int -> FlexChoice -> ShowS
    [FlexChoice] -> ShowS
    FlexChoice -> ArgName
    (Int -> FlexChoice -> ShowS)
    -> (FlexChoice -> ArgName)
    -> ([FlexChoice] -> ShowS)
    -> Show FlexChoice
    forall a.
    (Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
    showList :: [FlexChoice] -> ShowS
    $cshowList :: [FlexChoice] -> ShowS
    show :: FlexChoice -> ArgName
    $cshow :: FlexChoice -> ArgName
    showsPrec :: Int -> FlexChoice -> ShowS
    $cshowsPrec :: Int -> FlexChoice -> ShowS
    Show)

    instance Semigroup FlexChoice where
      FlexChoice
    ExpandBoth   <> :: FlexChoice -> FlexChoice -> FlexChoice
    <> FlexChoice
    _            = FlexChoice
    ExpandBoth
      FlexChoice
    _            <> FlexChoice
    ExpandBoth   = FlexChoice
    ExpandBoth
      FlexChoice
    ChooseEither <> FlexChoice
    y            = FlexChoice
    y
      FlexChoice
    x            <> FlexChoice
    ChooseEither = FlexChoice
    x
      FlexChoice
    ChooseLeft   <> FlexChoice
    ChooseRight  = FlexChoice
    ExpandBoth -- If there's dot patterns on both sides,
      FlexChoice
    ChooseRight  <> FlexChoice
    ChooseLeft   = FlexChoice
    ExpandBoth -- we need to eta-expand
      FlexChoice
    ChooseLeft   <> FlexChoice
    ChooseLeft   = FlexChoice
    ChooseLeft
      FlexChoice
    ChooseRight  <> FlexChoice
    ChooseRight  = FlexChoice
    ChooseRight

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

    class ChooseFlex a where
      chooseFlex :: a -> a -> FlexChoice

    instance ChooseFlex FlexibleVarKind where
      chooseFlex :: FlexibleVarKind -> FlexibleVarKind -> FlexChoice
    chooseFlex FlexibleVarKind
    DotFlex         FlexibleVarKind
    DotFlex         = FlexChoice
    ChooseEither
      chooseFlex FlexibleVarKind
    DotFlex         FlexibleVarKind
    _               = FlexChoice
    ChooseLeft
      chooseFlex FlexibleVarKind
    _               FlexibleVarKind
    DotFlex         = FlexChoice
    ChooseRight
      chooseFlex (RecordFlex [FlexibleVarKind]
    xs) (RecordFlex [FlexibleVarKind]
    ys) = [FlexibleVarKind] -> [FlexibleVarKind] -> FlexChoice
    forall a. ChooseFlex a => a -> a -> FlexChoice
    chooseFlex [FlexibleVarKind]
    xs [FlexibleVarKind]
    ys
      chooseFlex (RecordFlex [FlexibleVarKind]
    xs) FlexibleVarKind
    y               = [FlexibleVarKind] -> [FlexibleVarKind] -> FlexChoice
    forall a. ChooseFlex a => a -> a -> FlexChoice
    chooseFlex [FlexibleVarKind]
    xs (FlexibleVarKind -> [FlexibleVarKind]
    forall a. a -> [a]
    repeat FlexibleVarKind
    y)
      chooseFlex FlexibleVarKind
    x               (RecordFlex [FlexibleVarKind]
    ys) = [FlexibleVarKind] -> [FlexibleVarKind] -> FlexChoice
    forall a. ChooseFlex a => a -> a -> FlexChoice
    chooseFlex (FlexibleVarKind -> [FlexibleVarKind]
    forall a. a -> [a]
    repeat FlexibleVarKind
    x) [FlexibleVarKind]
    ys
      chooseFlex FlexibleVarKind
    ImplicitFlex    FlexibleVarKind
    ImplicitFlex    = FlexChoice
    ChooseEither
      chooseFlex FlexibleVarKind
    ImplicitFlex    FlexibleVarKind
    _               = FlexChoice
    ChooseLeft
      chooseFlex FlexibleVarKind
    _               FlexibleVarKind
    ImplicitFlex    = FlexChoice
    ChooseRight
      chooseFlex FlexibleVarKind
    OtherFlex       FlexibleVarKind
    OtherFlex       = FlexChoice
    ChooseEither

    instance ChooseFlex a => ChooseFlex [a] where
      chooseFlex :: [a] -> [a] -> FlexChoice
    chooseFlex [a]
    xs [a]
    ys = [FlexChoice] -> FlexChoice
    forall a. Monoid a => [a] -> a
    mconcat ([FlexChoice] -> FlexChoice) -> [FlexChoice] -> FlexChoice
    forall a b. (a -> b) -> a -> b
    $ (a -> a -> FlexChoice) -> [a] -> [a] -> [FlexChoice]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith a -> a -> FlexChoice
    forall a. ChooseFlex a => a -> a -> FlexChoice
    chooseFlex [a]
    xs [a]
    ys

    instance ChooseFlex a => ChooseFlex (Maybe a) where
      chooseFlex :: Maybe a -> Maybe a -> FlexChoice
    chooseFlex Maybe a
    Nothing Maybe a
    Nothing = FlexChoice
    ChooseEither
      chooseFlex Maybe a
    Nothing (Just a
    y) = FlexChoice
    ChooseLeft
      chooseFlex (Just a
    x) Maybe a
    Nothing = FlexChoice
    ChooseRight
      chooseFlex (Just a
    x) (Just a
    y) = a -> a -> FlexChoice
    forall a. ChooseFlex a => a -> a -> FlexChoice
    chooseFlex a
    x a
    y

    instance ChooseFlex ArgInfo where
      chooseFlex :: ArgInfo -> ArgInfo -> FlexChoice
    chooseFlex ArgInfo
    ai1 ArgInfo
    ai2 = [FlexChoice] -> FlexChoice
    firstChoice [ Origin -> Origin -> FlexChoice
    forall a. ChooseFlex a => a -> a -> FlexChoice
    chooseFlex (ArgInfo -> Origin
    forall a. LensOrigin a => a -> Origin
    getOrigin ArgInfo
    ai1) (ArgInfo -> Origin
    forall a. LensOrigin a => a -> Origin
    getOrigin ArgInfo
    ai2)
                                       , Hiding -> Hiding -> FlexChoice
    forall a. ChooseFlex a => a -> a -> FlexChoice
    chooseFlex (ArgInfo -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding ArgInfo
    ai1) (ArgInfo -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding ArgInfo
    ai2) ]

    instance ChooseFlex IsForced where
      chooseFlex :: IsForced -> IsForced -> FlexChoice
    chooseFlex IsForced
    NotForced IsForced
    NotForced = FlexChoice
    ChooseEither
      chooseFlex IsForced
    NotForced IsForced
    Forced    = FlexChoice
    ChooseRight
      chooseFlex IsForced
    Forced    IsForced
    NotForced = FlexChoice
    ChooseLeft
      chooseFlex IsForced
    Forced    IsForced
    Forced    = FlexChoice
    ChooseEither

    instance ChooseFlex Hiding where
      chooseFlex :: Hiding -> Hiding -> FlexChoice
    chooseFlex Hiding
    Hidden     Hiding
    Hidden     = FlexChoice
    ChooseEither
      chooseFlex Hiding
    Hidden     Hiding
    _          = FlexChoice
    ChooseLeft
      chooseFlex Hiding
    _          Hiding
    Hidden     = FlexChoice
    ChooseRight
      chooseFlex Instance{} Instance{} = FlexChoice
    ChooseEither
      chooseFlex Instance{} Hiding
    _          = FlexChoice
    ChooseLeft
      chooseFlex Hiding
    _          Instance{} = FlexChoice
    ChooseRight
      chooseFlex Hiding
    _          Hiding
    _          = FlexChoice
    ChooseEither

    instance ChooseFlex Origin where
      chooseFlex :: Origin -> Origin -> FlexChoice
    chooseFlex Origin
    Inserted  Origin
    Inserted  = FlexChoice
    ChooseEither
      chooseFlex Origin
    Inserted  Origin
    _         = FlexChoice
    ChooseLeft
      chooseFlex Origin
    _         Origin
    Inserted  = FlexChoice
    ChooseRight
      chooseFlex Origin
    Reflected Origin
    Reflected = FlexChoice
    ChooseEither
      chooseFlex Origin
    Reflected Origin
    _         = FlexChoice
    ChooseLeft
      chooseFlex Origin
    _         Origin
    Reflected = FlexChoice
    ChooseRight
      chooseFlex Origin
    _         Origin
    _         = FlexChoice
    ChooseEither

    instance ChooseFlex Int where
      chooseFlex :: Int -> Int -> FlexChoice
    chooseFlex Int
    x Int
    y = case Int -> Int -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Int
    x Int
    y of
        Ordering
    LT -> FlexChoice
    ChooseLeft
        Ordering
    EQ -> FlexChoice
    ChooseEither
        Ordering
    GT -> FlexChoice
    ChooseRight

    instance (ChooseFlex a) => ChooseFlex (FlexibleVar a) where
      chooseFlex :: FlexibleVar a -> FlexibleVar a -> FlexChoice
    chooseFlex (FlexibleVar ArgInfo
    ai1 IsForced
    fc1 FlexibleVarKind
    f1 Maybe Int
    p1 a
    i1) (FlexibleVar ArgInfo
    ai2 IsForced
    fc2 FlexibleVarKind
    f2 Maybe Int
    p2 a
    i2) =
        [FlexChoice] -> FlexChoice
    firstChoice [ FlexibleVarKind -> FlexibleVarKind -> FlexChoice
    forall a. ChooseFlex a => a -> a -> FlexChoice
    chooseFlex FlexibleVarKind
    f1 FlexibleVarKind
    f2, IsForced -> IsForced -> FlexChoice
    forall a. ChooseFlex a => a -> a -> FlexChoice
    chooseFlex IsForced
    fc1 IsForced
    fc2, ArgInfo -> ArgInfo -> FlexChoice
    forall a. ChooseFlex a => a -> a -> FlexChoice
    chooseFlex ArgInfo
    ai1 ArgInfo
    ai2
                    , Maybe Int -> Maybe Int -> FlexChoice
    forall a. ChooseFlex a => a -> a -> FlexChoice
    chooseFlex Maybe Int
    p1 Maybe Int
    p2, a -> a -> FlexChoice
    forall a. ChooseFlex a => a -> a -> FlexChoice
    chooseFlex a
    i1 a
    i2]

    firstChoice :: [FlexChoice] -> FlexChoice
    firstChoice :: [FlexChoice] -> FlexChoice
    firstChoice []                  = FlexChoice
    ChooseEither
    firstChoice (FlexChoice
    ChooseEither : [FlexChoice]
    xs) = [FlexChoice] -> FlexChoice
    firstChoice [FlexChoice]
    xs
    firstChoice (FlexChoice
    x            : [FlexChoice]
    _ ) = FlexChoice
    x

    -- | The user patterns we still have to split on.
    data Problem a = Problem
      { forall a. Problem a -> [ProblemEq]
    _problemEqs      :: [ProblemEq]
        -- ^ User patterns which are typed
        --   (including the ones generated from implicit arguments).
      , forall a. Problem a -> [NamedArg Pattern]
    _problemRestPats :: [NamedArg A.Pattern]
        -- ^ List of user patterns which could not yet be typed.
        --   Example:
        --   @
        --      f : (b : Bool) -> if b then Nat else Nat -> Nat
        --      f true          = zero
        --      f false zero    = zero
        --      f false (suc n) = n
        --   @
        --   In this sitation, for clause 2, we construct an initial problem
        --   @
        --      problemEqs      = [false = b]
        --      problemRestPats = [zero]
        --   @
        --   As we instantiate @b@ to @false@, the 'targetType' reduces to
        --   @Nat -> Nat@ and we can move pattern @zero@ over to @problemEqs@.
      , forall a. Problem a -> LHSState a -> TCM a
    _problemCont     :: LHSState a -> TCM a
        -- ^ The code that checks the RHS.
      }
      deriving Int -> Problem a -> ShowS
    [Problem a] -> ShowS
    Problem a -> ArgName
    (Int -> Problem a -> ShowS)
    -> (Problem a -> ArgName)
    -> ([Problem a] -> ShowS)
    -> Show (Problem a)
    forall a. Int -> Problem a -> ShowS
    forall a. [Problem a] -> ShowS
    forall a. Problem a -> ArgName
    forall a.
    (Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
    showList :: [Problem a] -> ShowS
    $cshowList :: forall a. [Problem a] -> ShowS
    show :: Problem a -> ArgName
    $cshow :: forall a. Problem a -> ArgName
    showsPrec :: Int -> Problem a -> ShowS
    $cshowsPrec :: forall a. Int -> Problem a -> ShowS
    Show

    problemEqs :: Lens' [ProblemEq] (Problem a)
    problemEqs :: forall a. Lens' [ProblemEq] (Problem a)
    problemEqs [ProblemEq] -> f [ProblemEq]
    f Problem a
    p = [ProblemEq] -> f [ProblemEq]
    f (Problem a -> [ProblemEq]
    forall a. Problem a -> [ProblemEq]
    _problemEqs Problem a
    p) f [ProblemEq] -> ([ProblemEq] -> Problem a) -> f (Problem a)
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \[ProblemEq]
    x -> Problem a
    p {_problemEqs :: [ProblemEq]
    _problemEqs = [ProblemEq]
    x}

    problemRestPats :: Lens' [NamedArg A.Pattern] (Problem a)
    problemRestPats :: forall a. Lens' [NamedArg Pattern] (Problem a)
    problemRestPats [NamedArg Pattern] -> f [NamedArg Pattern]
    f Problem a
    p = [NamedArg Pattern] -> f [NamedArg Pattern]
    f (Problem a -> [NamedArg Pattern]
    forall a. Problem a -> [NamedArg Pattern]
    _problemRestPats Problem a
    p) f [NamedArg Pattern]
    -> ([NamedArg Pattern] -> Problem a) -> f (Problem a)
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \[NamedArg Pattern]
    x -> Problem a
    p {_problemRestPats :: [NamedArg Pattern]
    _problemRestPats = [NamedArg Pattern]
    x}

    problemCont :: Lens' (LHSState a -> TCM a) (Problem a)
    problemCont :: forall a. Lens' (LHSState a -> TCM a) (Problem a)
    problemCont (LHSState a -> TCM a) -> f (LHSState a -> TCM a)
    f Problem a
    p = (LHSState a -> TCM a) -> f (LHSState a -> TCM a)
    f (Problem a -> LHSState a -> TCM a
    forall a. Problem a -> LHSState a -> TCM a
    _problemCont Problem a
    p) f (LHSState a -> TCM a)
    -> ((LHSState a -> TCM a) -> Problem a) -> f (Problem a)
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \LHSState a -> TCM a
    x -> Problem a
    p {_problemCont :: LHSState a -> TCM a
    _problemCont = LHSState a -> TCM a
    x}

    problemInPats :: Problem a -> [A.Pattern]
    problemInPats :: forall a. Problem a -> [Pattern]
    problemInPats = (ProblemEq -> Pattern) -> [ProblemEq] -> [Pattern]
    forall a b. (a -> b) -> [a] -> [b]
    map ProblemEq -> Pattern
    problemInPat ([ProblemEq] -> [Pattern])
    -> (Problem a -> [ProblemEq]) -> Problem a -> [Pattern]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Problem a -> Lens' [ProblemEq] (Problem a) -> [ProblemEq]
    forall o i. o -> Lens' i o -> i
    ^. forall a. Lens' [ProblemEq] (Problem a)
    Lens' [ProblemEq] (Problem a)
    problemEqs)

    data AsBinding = AsB Name Term Type Modality
    data DotPattern = Dot A.Expr Term (Dom Type)
    data AbsurdPattern = Absurd Range Type
    data AnnotationPattern = Ann A.Expr Type

    -- | State worked on during the main loop of checking a lhs.
    --   [Ulf Norell's PhD, page. 35]
    data LHSState a = LHSState
      { forall a. LHSState a -> Telescope
    _lhsTel     :: Telescope
        -- ^ The types of the pattern variables.
      , forall a. LHSState a -> [NamedArg DeBruijnPattern]
    _lhsOutPat  :: [NamedArg DeBruijnPattern]
        -- ^ Patterns after splitting.
        --   The de Bruijn indices refer to positions in the list of abstract syntax
        --   patterns in the problem, counted from the back (right-to-left).
      , forall a. LHSState a -> Problem a
    _lhsProblem :: Problem a
        -- ^ User patterns of supposed type @delta@.
      , forall a. LHSState a -> Arg Type
    _lhsTarget  :: Arg Type
        -- ^ Type eliminated by 'problemRestPats' in the problem.
        --   Can be 'Irrelevant' to indicate that we came by
        --   an irrelevant projection and, hence, the rhs must
        --   be type-checked in irrelevant mode.
      , forall a. LHSState a -> [Maybe Int]
    _lhsPartialSplit :: ![Maybe Int]
        -- ^ have we splitted with a PartialFocus?
      }

    lhsTel :: Lens' Telescope (LHSState a)
    lhsTel :: forall a. Lens' Telescope (LHSState a)
    lhsTel Telescope -> f Telescope
    f LHSState a
    p = Telescope -> f Telescope
    f (LHSState a -> Telescope
    forall a. LHSState a -> Telescope
    _lhsTel LHSState a
    p) f Telescope -> (Telescope -> LHSState a) -> f (LHSState a)
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \Telescope
    x -> LHSState a
    p {_lhsTel :: Telescope
    _lhsTel = Telescope
    x}

    lhsOutPat :: Lens' [NamedArg DeBruijnPattern] (LHSState a)
    lhsOutPat :: forall a. Lens' [NamedArg DeBruijnPattern] (LHSState a)
    lhsOutPat [NamedArg DeBruijnPattern] -> f [NamedArg DeBruijnPattern]
    f LHSState a
    p = [NamedArg DeBruijnPattern] -> f [NamedArg DeBruijnPattern]
    f (LHSState a -> [NamedArg DeBruijnPattern]
    forall a. LHSState a -> [NamedArg DeBruijnPattern]
    _lhsOutPat LHSState a
    p) f [NamedArg DeBruijnPattern]
    -> ([NamedArg DeBruijnPattern] -> LHSState a) -> f (LHSState a)
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \[NamedArg DeBruijnPattern]
    x -> LHSState a
    p {_lhsOutPat :: [NamedArg DeBruijnPattern]
    _lhsOutPat = [NamedArg DeBruijnPattern]
    x}

    lhsProblem :: Lens' (Problem a) (LHSState a)
    lhsProblem :: forall a. Lens' (Problem a) (LHSState a)
    lhsProblem Problem a -> f (Problem a)
    f LHSState a
    p = Problem a -> f (Problem a)
    f (LHSState a -> Problem a
    forall a. LHSState a -> Problem a
    _lhsProblem LHSState a
    p) f (Problem a) -> (Problem a -> LHSState a) -> f (LHSState a)
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \Problem a
    x -> LHSState a
    p {_lhsProblem :: Problem a
    _lhsProblem = Problem a
    x}

    lhsTarget :: Lens' (Arg Type) (LHSState a)
    lhsTarget :: forall a. Lens' (Arg Type) (LHSState a)
    lhsTarget Arg Type -> f (Arg Type)
    f LHSState a
    p = Arg Type -> f (Arg Type)
    f (LHSState a -> Arg Type
    forall a. LHSState a -> Arg Type
    _lhsTarget LHSState a
    p) f (Arg Type) -> (Arg Type -> LHSState a) -> f (LHSState a)
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \Arg Type
    x -> LHSState a
    p {_lhsTarget :: Arg Type
    _lhsTarget = Arg Type
    x}

    -- UNUSED Liang-Ting Chen 2019-07-16
    --lhsPartialSplit :: Lens' [Maybe Int] (LHSState a)
    --lhsPartialSplit f p = f (_lhsPartialSplit p) <&> \x -> p {_lhsPartialSplit = x}

    data PatVarPosition = PVLocal | PVParam
      deriving (Int -> PatVarPosition -> ShowS
    [PatVarPosition] -> ShowS
    PatVarPosition -> ArgName
    (Int -> PatVarPosition -> ShowS)
    -> (PatVarPosition -> ArgName)
    -> ([PatVarPosition] -> ShowS)
    -> Show PatVarPosition
    forall a.
    (Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
    showList :: [PatVarPosition] -> ShowS
    $cshowList :: [PatVarPosition] -> ShowS
    show :: PatVarPosition -> ArgName
    $cshow :: PatVarPosition -> ArgName
    showsPrec :: Int -> PatVarPosition -> ShowS
    $cshowsPrec :: Int -> PatVarPosition -> ShowS
    Show, PatVarPosition -> PatVarPosition -> Bool
    (PatVarPosition -> PatVarPosition -> Bool)
    -> (PatVarPosition -> PatVarPosition -> Bool) -> Eq PatVarPosition
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: PatVarPosition -> PatVarPosition -> Bool
    $c/= :: PatVarPosition -> PatVarPosition -> Bool
    == :: PatVarPosition -> PatVarPosition -> Bool
    $c== :: PatVarPosition -> PatVarPosition -> Bool
    Eq)

    data LeftoverPatterns = LeftoverPatterns
      { LeftoverPatterns -> IntMap [(Name, PatVarPosition)]
    patternVariables :: IntMap [(A.Name,PatVarPosition)]
      , LeftoverPatterns -> [AsBinding]
    asPatterns       :: [AsBinding]
      , LeftoverPatterns -> [DotPattern]
    dotPatterns      :: [DotPattern]
      , LeftoverPatterns -> [AbsurdPattern]
    absurdPatterns   :: [AbsurdPattern]
      , LeftoverPatterns -> [AnnotationPattern]
    typeAnnotations  :: [AnnotationPattern]
      , LeftoverPatterns -> [Pattern]
    otherPatterns    :: [A.Pattern]
      }

    instance Semigroup LeftoverPatterns where
      LeftoverPatterns
    x <> :: LeftoverPatterns -> LeftoverPatterns -> LeftoverPatterns
    <> LeftoverPatterns
    y = LeftoverPatterns :: IntMap [(Name, PatVarPosition)]
    -> [AsBinding]
    -> [DotPattern]
    -> [AbsurdPattern]
    -> [AnnotationPattern]
    -> [Pattern]
    -> LeftoverPatterns
    LeftoverPatterns
        { patternVariables :: IntMap [(Name, PatVarPosition)]
    patternVariables = ([(Name, PatVarPosition)]
     -> [(Name, PatVarPosition)] -> [(Name, PatVarPosition)])
    -> IntMap [(Name, PatVarPosition)]
    -> IntMap [(Name, PatVarPosition)]
    -> IntMap [(Name, PatVarPosition)]
    forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
    IntMap.unionWith [(Name, PatVarPosition)]
    -> [(Name, PatVarPosition)] -> [(Name, PatVarPosition)]
    forall a. [a] -> [a] -> [a]
    (++) (LeftoverPatterns -> IntMap [(Name, PatVarPosition)]
    patternVariables LeftoverPatterns
    x) (LeftoverPatterns -> IntMap [(Name, PatVarPosition)]
    patternVariables LeftoverPatterns
    y)
        , asPatterns :: [AsBinding]
    asPatterns       = LeftoverPatterns -> [AsBinding]
    asPatterns LeftoverPatterns
    x [AsBinding] -> [AsBinding] -> [AsBinding]
    forall a. [a] -> [a] -> [a]
    ++ LeftoverPatterns -> [AsBinding]
    asPatterns LeftoverPatterns
    y
        , dotPatterns :: [DotPattern]
    dotPatterns      = LeftoverPatterns -> [DotPattern]
    dotPatterns LeftoverPatterns
    x [DotPattern] -> [DotPattern] -> [DotPattern]
    forall a. [a] -> [a] -> [a]
    ++ LeftoverPatterns -> [DotPattern]
    dotPatterns LeftoverPatterns
    y
        , absurdPatterns :: [AbsurdPattern]
    absurdPatterns   = LeftoverPatterns -> [AbsurdPattern]
    absurdPatterns LeftoverPatterns
    x [AbsurdPattern] -> [AbsurdPattern] -> [AbsurdPattern]
    forall a. [a] -> [a] -> [a]
    ++ LeftoverPatterns -> [AbsurdPattern]
    absurdPatterns LeftoverPatterns
    y
        , typeAnnotations :: [AnnotationPattern]
    typeAnnotations  = LeftoverPatterns -> [AnnotationPattern]
    typeAnnotations LeftoverPatterns
    x [AnnotationPattern] -> [AnnotationPattern] -> [AnnotationPattern]
    forall a. [a] -> [a] -> [a]
    ++ LeftoverPatterns -> [AnnotationPattern]
    typeAnnotations LeftoverPatterns
    y
        , otherPatterns :: [Pattern]
    otherPatterns    = LeftoverPatterns -> [Pattern]
    otherPatterns LeftoverPatterns
    x [Pattern] -> [Pattern] -> [Pattern]
    forall a. [a] -> [a] -> [a]
    ++ LeftoverPatterns -> [Pattern]
    otherPatterns LeftoverPatterns
    y
        }

    instance Null LeftoverPatterns where
      empty :: LeftoverPatterns
    empty = IntMap [(Name, PatVarPosition)]
    -> [AsBinding]
    -> [DotPattern]
    -> [AbsurdPattern]
    -> [AnnotationPattern]
    -> [Pattern]
    -> LeftoverPatterns
    LeftoverPatterns IntMap [(Name, PatVarPosition)]
    forall a. Null a => a
    empty [] [] [] [] []
      null :: LeftoverPatterns -> Bool
    null (LeftoverPatterns IntMap [(Name, PatVarPosition)]
    as [AsBinding]
    bs [DotPattern]
    cs [AbsurdPattern]
    ds [AnnotationPattern]
    es [Pattern]
    fs) = IntMap [(Name, PatVarPosition)] -> Bool
    forall a. Null a => a -> Bool
    null IntMap [(Name, PatVarPosition)]
    as Bool -> Bool -> Bool
    && [AsBinding] -> Bool
    forall a. Null a => a -> Bool
    null [AsBinding]
    bs Bool -> Bool -> Bool
    && [DotPattern] -> Bool
    forall a. Null a => a -> Bool
    null [DotPattern]
    cs Bool -> Bool -> Bool
    && [AbsurdPattern] -> Bool
    forall a. Null a => a -> Bool
    null [AbsurdPattern]
    ds Bool -> Bool -> Bool
    && [AnnotationPattern] -> Bool
    forall a. Null a => a -> Bool
    null [AnnotationPattern]
    es Bool -> Bool -> Bool
    && [Pattern] -> Bool
    forall a. Null a => a -> Bool
    null [Pattern]
    fs

    instance Monoid LeftoverPatterns where
      mempty :: LeftoverPatterns
    mempty  = LeftoverPatterns
    forall a. Null a => a
    empty
      mappend :: LeftoverPatterns -> LeftoverPatterns -> LeftoverPatterns
    mappend = LeftoverPatterns -> LeftoverPatterns -> LeftoverPatterns
    forall a. Semigroup a => a -> a -> a
    (<>)

    instance PP.Pretty PatVarPosition where
      pretty :: PatVarPosition -> Doc
    pretty = ArgName -> Doc
    PP.text (ArgName -> Doc)
    -> (PatVarPosition -> ArgName) -> PatVarPosition -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PatVarPosition -> ArgName
    forall a. Show a => a -> ArgName
    show

    instance PrettyTCM LeftoverPatterns where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => LeftoverPatterns -> m Doc
    prettyTCM (LeftoverPatterns IntMap [(Name, PatVarPosition)]
    varp [AsBinding]
    asb [DotPattern]
    dotp [AbsurdPattern]
    absurdp [AnnotationPattern]
    annp [Pattern]
    otherp) = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ m Doc
    "pattern variables: " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [(Int, [(Name, PatVarPosition)])] -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (IntMap [(Name, PatVarPosition)]
    -> [(Int, [(Name, PatVarPosition)])]
    forall a. IntMap a -> [(Int, a)]
    IntMap.toList IntMap [(Name, PatVarPosition)]
    varp)
        , m Doc
    "as bindings:       " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((AsBinding -> m Doc) -> [AsBinding] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map AsBinding -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [AsBinding]
    asb)
        , m Doc
    "dot patterns:      " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((DotPattern -> m Doc) -> [DotPattern] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map DotPattern -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [DotPattern]
    dotp)
        , m Doc
    "absurd patterns:   " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((AbsurdPattern -> m Doc) -> [AbsurdPattern] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map AbsurdPattern -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [AbsurdPattern]
    absurdp)
        , m Doc
    "type annotations:  " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((AnnotationPattern -> m Doc) -> [AnnotationPattern] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map AnnotationPattern -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [AnnotationPattern]
    annp)
        , m Doc
    "other patterns:    " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((Pattern -> m Doc) -> [Pattern] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Pattern -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [Pattern]
    otherp)
        ]

    -- | Classify remaining patterns after splitting is complete into pattern
    --   variables, as patterns, dot patterns, and absurd patterns.
    --   Precondition: there are no more constructor patterns.
    getLeftoverPatterns
      :: forall m. PureTCM m
      => [ProblemEq] -> m LeftoverPatterns
    getLeftoverPatterns :: forall (m :: * -> *).
    PureTCM m =>
    [ProblemEq] -> m LeftoverPatterns
    getLeftoverPatterns [ProblemEq]
    eqs = do
      ArgName -> Int -> TCM Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCM Doc -> m ()
    reportSDoc ArgName
    "tc.lhs.top" Int
    30 (TCM Doc -> m ()) -> TCM Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCM Doc
    "classifying leftover patterns"
      Set ArgName
    params <- [ArgName] -> Set ArgName
    forall a. Ord a => [a] -> Set a
    Set.fromList ([ArgName] -> Set ArgName)
    -> (Telescope -> [ArgName]) -> Telescope -> Set ArgName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> [ArgName]
    teleNames (Telescope -> Set ArgName) -> m Telescope -> m (Set ArgName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (ModuleName -> m Telescope
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m Telescope
    lookupSection (ModuleName -> m Telescope) -> m ModuleName -> m Telescope
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule)
      let isParamName :: Name -> Bool
    isParamName = (ArgName -> Set ArgName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set ArgName
    params) (ArgName -> Bool) -> (Name -> ArgName) -> Name -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> ArgName
    nameToArgName
      [LeftoverPatterns] -> LeftoverPatterns
    forall a. Monoid a => [a] -> a
    mconcat ([LeftoverPatterns] -> LeftoverPatterns)
    -> m [LeftoverPatterns] -> m LeftoverPatterns
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (ProblemEq -> m LeftoverPatterns)
    -> [ProblemEq] -> m [LeftoverPatterns]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((Name -> Bool) -> ProblemEq -> m LeftoverPatterns
    getLeftoverPattern Name -> Bool
    isParamName) [ProblemEq]
    eqs
      where
        patternVariable :: Name -> Int -> LeftoverPatterns
    patternVariable Name
    x Int
    i  = LeftoverPatterns
    forall a. Null a => a
    empty { patternVariables :: IntMap [(Name, PatVarPosition)]
    patternVariables = (Int, [(Name, PatVarPosition)]) -> IntMap [(Name, PatVarPosition)]
    forall el coll. Singleton el coll => el -> coll
    singleton (Int
    i,[(Name
    x,PatVarPosition
    PVLocal)]) }
        moduleParameter :: Name -> Int -> LeftoverPatterns
    moduleParameter Name
    x Int
    i  = LeftoverPatterns
    forall a. Null a => a
    empty { patternVariables :: IntMap [(Name, PatVarPosition)]
    patternVariables = (Int, [(Name, PatVarPosition)]) -> IntMap [(Name, PatVarPosition)]
    forall el coll. Singleton el coll => el -> coll
    singleton (Int
    i,[(Name
    x,PatVarPosition
    PVParam)]) }
        asPattern :: Name -> Term -> Dom' t Type -> LeftoverPatterns
    asPattern Name
    x Term
    v Dom' t Type
    a      = LeftoverPatterns
    forall a. Null a => a
    empty { asPatterns :: [AsBinding]
    asPatterns       = AsBinding -> [AsBinding]
    forall el coll. Singleton el coll => el -> coll
    singleton (Name -> Term -> Type -> Modality -> AsBinding
    AsB Name
    x Term
    v (Dom' t Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom' t Type
    a) (Dom' t Type -> Modality
    forall a. LensModality a => a -> Modality
    getModality Dom' t Type
    a)) }
        dotPattern :: Expr -> Term -> Dom Type -> LeftoverPatterns
    dotPattern Expr
    e Term
    v Dom Type
    a     = LeftoverPatterns
    forall a. Null a => a
    empty { dotPatterns :: [DotPattern]
    dotPatterns      = DotPattern -> [DotPattern]
    forall el coll. Singleton el coll => el -> coll
    singleton (Expr -> Term -> Dom Type -> DotPattern
    Dot Expr
    e Term
    v Dom Type
    a) }
        absurdPattern :: Range -> Type -> LeftoverPatterns
    absurdPattern Range
    info Type
    a = LeftoverPatterns
    forall a. Null a => a
    empty { absurdPatterns :: [AbsurdPattern]
    absurdPatterns   = AbsurdPattern -> [AbsurdPattern]
    forall el coll. Singleton el coll => el -> coll
    singleton (Range -> Type -> AbsurdPattern
    Absurd Range
    info Type
    a) }
        annPattern :: Expr -> Type -> LeftoverPatterns
    annPattern Expr
    t Type
    a       = LeftoverPatterns
    forall a. Null a => a
    empty { typeAnnotations :: [AnnotationPattern]
    typeAnnotations  = AnnotationPattern -> [AnnotationPattern]
    forall el coll. Singleton el coll => el -> coll
    singleton (Expr -> Type -> AnnotationPattern
    Ann Expr
    t Type
    a) }
        otherPattern :: Pattern -> LeftoverPatterns
    otherPattern Pattern
    p       = LeftoverPatterns
    forall a. Null a => a
    empty { otherPatterns :: [Pattern]
    otherPatterns    = Pattern -> [Pattern]
    forall el coll. Singleton el coll => el -> coll
    singleton Pattern
    p }

        getLeftoverPattern :: (A.Name -> Bool) -> ProblemEq -> m LeftoverPatterns
        getLeftoverPattern :: (Name -> Bool) -> ProblemEq -> m LeftoverPatterns
    getLeftoverPattern Name -> Bool
    isParamName (ProblemEq Pattern
    p Term
    v Dom Type
    a) = case Pattern
    p of
          (A.VarP A.BindName{unBind :: BindName -> Name
    unBind = Name
    x}) -> Term -> Type -> m (Maybe Int)
    forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Int)
    isEtaVar Term
    v (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a) m (Maybe Int)
    -> (Maybe Int -> m LeftoverPatterns) -> m LeftoverPatterns
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Just Int
    i  | Name -> Bool
    isParamName Name
    x -> LeftoverPatterns -> m LeftoverPatterns
    forall (m :: * -> *) a. Monad m => a -> m a
    return (LeftoverPatterns -> m LeftoverPatterns)
    -> LeftoverPatterns -> m LeftoverPatterns
    forall a b. (a -> b) -> a -> b
    $ Name -> Int -> LeftoverPatterns
    moduleParameter Name
    x Int
    i
                    | Bool
    otherwise     -> LeftoverPatterns -> m LeftoverPatterns
    forall (m :: * -> *) a. Monad m => a -> m a
    return (LeftoverPatterns -> m LeftoverPatterns)
    -> LeftoverPatterns -> m LeftoverPatterns
    forall a b. (a -> b) -> a -> b
    $ Name -> Int -> LeftoverPatterns
    patternVariable Name
    x Int
    i
            Maybe Int
    Nothing -> LeftoverPatterns -> m LeftoverPatterns
    forall (m :: * -> *) a. Monad m => a -> m a
    return (LeftoverPatterns -> m LeftoverPatterns)
    -> LeftoverPatterns -> m LeftoverPatterns
    forall a b. (a -> b) -> a -> b
    $ Name -> Term -> Dom Type -> LeftoverPatterns
    forall {t}. Name -> Term -> Dom' t Type -> LeftoverPatterns
    asPattern Name
    x Term
    v Dom Type
    a
          (A.WildP PatInfo
    _)       -> LeftoverPatterns -> m LeftoverPatterns
    forall (m :: * -> *) a. Monad m => a -> m a
    return LeftoverPatterns
    forall a. Monoid a => a
    mempty
          (A.AsP PatInfo
    info A.BindName{unBind :: BindName -> Name
    unBind = Name
    x} Pattern
    p)  -> (Name -> Term -> Dom Type -> LeftoverPatterns
    forall {t}. Name -> Term -> Dom' t Type -> LeftoverPatterns
    asPattern Name
    x Term
    v Dom Type
    a LeftoverPatterns -> LeftoverPatterns -> LeftoverPatterns
    forall a. Monoid a => a -> a -> a
    `mappend`) (LeftoverPatterns -> LeftoverPatterns)
    -> m LeftoverPatterns -> m LeftoverPatterns
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
            (Name -> Bool) -> ProblemEq -> m LeftoverPatterns
    getLeftoverPattern Name -> Bool
    isParamName (ProblemEq -> m LeftoverPatterns)
    -> ProblemEq -> m LeftoverPatterns
    forall a b. (a -> b) -> a -> b
    $ Pattern -> Term -> Dom Type -> ProblemEq
    ProblemEq Pattern
    p Term
    v Dom Type
    a
          (A.DotP PatInfo
    info Expr
    e)   -> LeftoverPatterns -> m LeftoverPatterns
    forall (m :: * -> *) a. Monad m => a -> m a
    return (LeftoverPatterns -> m LeftoverPatterns)
    -> LeftoverPatterns -> m LeftoverPatterns
    forall a b. (a -> b) -> a -> b
    $ Expr -> Term -> Dom Type -> LeftoverPatterns
    dotPattern Expr
    e Term
    v Dom Type
    a
          (A.AbsurdP PatInfo
    info)  -> LeftoverPatterns -> m LeftoverPatterns
    forall (m :: * -> *) a. Monad m => a -> m a
    return (LeftoverPatterns -> m LeftoverPatterns)
    -> LeftoverPatterns -> m LeftoverPatterns
    forall a b. (a -> b) -> a -> b
    $ Range -> Type -> LeftoverPatterns
    absurdPattern (PatInfo -> Range
    forall a. HasRange a => a -> Range
    getRange PatInfo
    info) (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a)
          (A.AnnP PatInfo
    info Expr
    t Pattern
    p) -> (Expr -> Type -> LeftoverPatterns
    annPattern Expr
    t (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a) LeftoverPatterns -> LeftoverPatterns -> LeftoverPatterns
    forall a. Monoid a => a -> a -> a
    `mappend`) (LeftoverPatterns -> LeftoverPatterns)
    -> m LeftoverPatterns -> m LeftoverPatterns
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
            (Name -> Bool) -> ProblemEq -> m LeftoverPatterns
    getLeftoverPattern Name -> Bool
    isParamName (ProblemEq -> m LeftoverPatterns)
    -> ProblemEq -> m LeftoverPatterns
    forall a b. (a -> b) -> a -> b
    $ Pattern -> Term -> Dom Type -> ProblemEq
    ProblemEq Pattern
    p Term
    v Dom Type
    a
          Pattern
    _                 -> LeftoverPatterns -> m LeftoverPatterns
    forall (m :: * -> *) a. Monad m => a -> m a
    return (LeftoverPatterns -> m LeftoverPatterns)
    -> LeftoverPatterns -> m LeftoverPatterns
    forall a b. (a -> b) -> a -> b
    $ Pattern -> LeftoverPatterns
    otherPattern Pattern
    p

    -- | Build a renaming for the internal patterns using variable names from
    --   the user patterns. If there are multiple user names for the same internal
    --   variable, the unused ones are returned as as-bindings.
    --   Names that are not also module parameters are preferred over
    --   those that are.
    getUserVariableNames
      :: Telescope                         -- ^ The telescope of pattern variables
      -> IntMap [(A.Name,PatVarPosition)]  -- ^ The list of user names for each pattern variable
      -> ([Maybe A.Name], [AsBinding])
    getUserVariableNames :: Telescope
    -> IntMap [(Name, PatVarPosition)] -> ([Maybe Name], [AsBinding])
    getUserVariableNames Telescope
    tel IntMap [(Name, PatVarPosition)]
    names = Writer [AsBinding] [Maybe Name] -> ([Maybe Name], [AsBinding])
    forall w a. Writer w a -> (a, w)
    runWriter (Writer [AsBinding] [Maybe Name] -> ([Maybe Name], [AsBinding]))
    -> Writer [AsBinding] [Maybe Name] -> ([Maybe Name], [AsBinding])
    forall a b. (a -> b) -> a -> b
    $
      (Dom Type -> Int -> WriterT [AsBinding] Identity (Maybe Name))
    -> [Dom Type] -> [Int] -> Writer [AsBinding] [Maybe Name]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM Dom Type -> Int -> WriterT [AsBinding] Identity (Maybe Name)
    makeVar (Telescope -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Telescope
    tel) (Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom (Int -> [Int]) -> Int -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel)

      where
        makeVar :: Dom Type -> Int -> Writer [AsBinding] (Maybe A.Name)
        makeVar :: Dom Type -> Int -> WriterT [AsBinding] Identity (Maybe Name)
    makeVar Dom Type
    a Int
    i = case [(Name, PatVarPosition)] -> ([Name], [Name])
    partitionIsParam ([(Name, PatVarPosition)]
    -> Int
    -> IntMap [(Name, PatVarPosition)]
    -> [(Name, PatVarPosition)]
    forall a. a -> Int -> IntMap a -> a
    IntMap.findWithDefault [] Int
    i IntMap [(Name, PatVarPosition)]
    names) of
          ([]     , [])   -> Maybe Name -> WriterT [AsBinding] Identity (Maybe Name)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Name
    forall a. Maybe a
    Nothing
          ((Name
    x:[Name]
    xs) , [])   -> [Name] -> WriterT [AsBinding] Identity ()
    tellAsBindings [Name]
    xs WriterT [AsBinding] Identity ()
    -> Maybe Name -> WriterT [AsBinding] Identity (Maybe Name)
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> (Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x)
          ([Name]
    xs     , Name
    y:[Name]
    ys) -> [Name] -> WriterT [AsBinding] Identity ()
    tellAsBindings ([Name]
    xs [Name] -> [Name] -> [Name]
    forall a. [a] -> [a] -> [a]
    ++ [Name]
    ys) WriterT [AsBinding] Identity ()
    -> Maybe Name -> WriterT [AsBinding] Identity (Maybe Name)
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> (Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    y)
          where
            tellAsBindings :: [Name] -> WriterT [AsBinding] Identity ()
    tellAsBindings = [AsBinding] -> WriterT [AsBinding] Identity ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell ([AsBinding] -> WriterT [AsBinding] Identity ())
    -> ([Name] -> [AsBinding])
    -> [Name]
    -> WriterT [AsBinding] Identity ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name -> AsBinding) -> [Name] -> [AsBinding]
    forall a b. (a -> b) -> [a] -> [b]
    map (\Name
    y -> Name -> Term -> Type -> Modality -> AsBinding
    AsB Name
    y (Int -> Term
    var Int
    i) (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a) (Dom Type -> Modality
    forall a. LensModality a => a -> Modality
    getModality Dom Type
    a))

        partitionIsParam :: [(A.Name,PatVarPosition)] -> ([A.Name],[A.Name])
        partitionIsParam :: [(Name, PatVarPosition)] -> ([Name], [Name])
    partitionIsParam = (((Name, PatVarPosition) -> Name)
    -> [(Name, PatVarPosition)] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, PatVarPosition) -> Name
    forall a b. (a, b) -> a
    fst ([(Name, PatVarPosition)] -> [Name])
    -> ([(Name, PatVarPosition)] -> [Name])
    -> ([(Name, PatVarPosition)], [(Name, PatVarPosition)])
    -> ([Name], [Name])
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** ((Name, PatVarPosition) -> Name)
    -> [(Name, PatVarPosition)] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, PatVarPosition) -> Name
    forall a b. (a, b) -> a
    fst) (([(Name, PatVarPosition)], [(Name, PatVarPosition)])
     -> ([Name], [Name]))
    -> ([(Name, PatVarPosition)]
        -> ([(Name, PatVarPosition)], [(Name, PatVarPosition)]))
    -> [(Name, PatVarPosition)]
    -> ([Name], [Name])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Name, PatVarPosition) -> Bool)
    -> [(Name, PatVarPosition)]
    -> ([(Name, PatVarPosition)], [(Name, PatVarPosition)])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition ((PatVarPosition -> PatVarPosition -> Bool
    forall a. Eq a => a -> a -> Bool
    == PatVarPosition
    PVParam) (PatVarPosition -> Bool)
    -> ((Name, PatVarPosition) -> PatVarPosition)
    -> (Name, PatVarPosition)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, PatVarPosition) -> PatVarPosition
    forall a b. (a, b) -> b
    snd)

    instance Subst (Problem a) where
      type SubstArg (Problem a) = Term
      applySubst :: Substitution' (SubstArg (Problem a)) -> Problem a -> Problem a
    applySubst Substitution' (SubstArg (Problem a))
    rho (Problem [ProblemEq]
    eqs [NamedArg Pattern]
    rps LHSState a -> TCM a
    cont) = [ProblemEq]
    -> [NamedArg Pattern] -> (LHSState a -> TCM a) -> Problem a
    forall a.
    [ProblemEq]
    -> [NamedArg Pattern] -> (LHSState a -> TCM a) -> Problem a
    Problem (Substitution' (SubstArg [ProblemEq]) -> [ProblemEq] -> [ProblemEq]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg [ProblemEq])
    Substitution' (SubstArg (Problem a))
    rho [ProblemEq]
    eqs) [NamedArg Pattern]
    rps LHSState a -> TCM a
    cont

    instance Subst AsBinding where
      type SubstArg AsBinding = Term
      applySubst :: Substitution' (SubstArg AsBinding) -> AsBinding -> AsBinding
    applySubst Substitution' (SubstArg AsBinding)
    rho (AsB Name
    x Term
    v Type
    a Modality
    m) = (\(Term
    v,Type
    a) -> Name -> Term -> Type -> Modality -> AsBinding
    AsB Name
    x Term
    v Type
    a Modality
    m) ((Term, Type) -> AsBinding) -> (Term, Type) -> AsBinding
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg (Term, Type))
    -> (Term, Type) -> (Term, Type)
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg (Term, Type))
    Substitution' (SubstArg AsBinding)
    rho (Term
    v, Type
    a)

    instance Subst DotPattern where
      type SubstArg DotPattern = Term
      applySubst :: Substitution' (SubstArg DotPattern) -> DotPattern -> DotPattern
    applySubst Substitution' (SubstArg DotPattern)
    rho (Dot Expr
    e Term
    v Dom Type
    a) = (Term -> Dom Type -> DotPattern) -> (Term, Dom Type) -> DotPattern
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (Expr -> Term -> Dom Type -> DotPattern
    Dot Expr
    e) ((Term, Dom Type) -> DotPattern) -> (Term, Dom Type) -> DotPattern
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg (Term, Dom Type))
    -> (Term, Dom Type) -> (Term, Dom Type)
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg (Term, Dom Type))
    Substitution' (SubstArg DotPattern)
    rho (Term
    v, Dom Type
    a)

    instance Subst AbsurdPattern where
      type SubstArg AbsurdPattern = Term
      applySubst :: Substitution' (SubstArg AbsurdPattern)
    -> AbsurdPattern -> AbsurdPattern
    applySubst Substitution' (SubstArg AbsurdPattern)
    rho (Absurd Range
    r Type
    a) = Range -> Type -> AbsurdPattern
    Absurd Range
    r (Type -> AbsurdPattern) -> Type -> AbsurdPattern
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg Type)
    Substitution' (SubstArg AbsurdPattern)
    rho Type
    a

    instance PrettyTCM ProblemEq where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => ProblemEq -> m Doc
    prettyTCM (ProblemEq Pattern
    p Term
    v Dom Type
    a) = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
        [ Pattern -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Pattern
    p m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    "="
        , Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    ":"
        , Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Dom Type
    a
        ]

    instance PrettyTCM AsBinding where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => AsBinding -> m Doc
    prettyTCM (AsB Name
    x Term
    v Type
    a Modality
    m) =
        [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ Name -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Name
    x m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    "@" m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v)
            , Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ m Doc
    ":" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a
            ]

    instance PrettyTCM DotPattern where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => DotPattern -> m Doc
    prettyTCM (Dot Expr
    e Term
    v Dom Type
    a) = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
        [ Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Expr
    e m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    "="
        , Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    ":"
        , Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Dom Type
    a
        ]

    instance PrettyTCM AbsurdPattern where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => AbsurdPattern -> m Doc
    prettyTCM (Absurd Range
    r Type
    a) = m Doc
    "() :" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a

    instance PrettyTCM AnnotationPattern where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => AnnotationPattern -> m Doc
    prettyTCM (Ann Expr
    a Type
    p) = Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    p m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    ":" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Expr
    a

    instance PP.Pretty AsBinding where
      pretty :: AsBinding -> Doc
    pretty (AsB Name
    x Term
    v Type
    a Modality
    m) =
        Name -> Doc
    forall a. Pretty a => a -> Doc
    PP.pretty Name
    x Doc -> Doc -> Doc
    PP.<+> Doc
    "=" Doc -> Doc -> Doc
    PP.<+>
          Doc -> Int -> Doc -> Doc
    PP.hang (Term -> Doc
    forall a. Pretty a => a -> Doc
    PP.pretty Term
    v Doc -> Doc -> Doc
    PP.<+> Doc
    ":") Int
    2 (Type -> Doc
    forall a. Pretty a => a -> Doc
    PP.pretty Type
    a)

    instance InstantiateFull AsBinding where
      instantiateFull' :: AsBinding -> ReduceM AsBinding
    instantiateFull' (AsB Name
    x Term
    v Type
    a Modality
    m) = Name -> Term -> Type -> Modality -> AsBinding
    AsB Name
    x (Term -> Type -> Modality -> AsBinding)
    -> ReduceM Term -> ReduceM (Type -> Modality -> AsBinding)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> ReduceM Term
    forall t. InstantiateFull t => t -> ReduceM t
    instantiateFull' Term
    v ReduceM (Type -> Modality -> AsBinding)
    -> ReduceM Type -> ReduceM (Modality -> AsBinding)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Type -> ReduceM Type
    forall t. InstantiateFull t => t -> ReduceM t
    instantiateFull' Type
    a ReduceM (Modality -> AsBinding)
    -> ReduceM Modality -> ReduceM AsBinding
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Modality -> ReduceM Modality
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Modality
    m

    instance PrettyTCM (LHSState a) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => LHSState a -> m Doc
    prettyTCM (LHSState Telescope
    tel [NamedArg DeBruijnPattern]
    outPat (Problem [ProblemEq]
    eqs [NamedArg Pattern]
    rps LHSState a -> TCM a
    _) Arg Type
    target [Maybe Int]
    _) = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ m Doc
    "tel             = " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    tel
        , m Doc
    "outPat          = " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> m Doc -> m Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel ([NamedArg DeBruijnPattern] -> m Doc
    forall (m :: * -> *).
    MonadPretty m =>
    [NamedArg DeBruijnPattern] -> m Doc
    prettyTCMPatternList [NamedArg DeBruijnPattern]
    outPat)
        , m Doc
    "problemEqs      = " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> m Doc -> m Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ (ProblemEq -> m Doc) -> [ProblemEq] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ProblemEq -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [ProblemEq]
    eqs)
        , m Doc
    "problemRestPats = " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((NamedArg Pattern -> m Doc) -> [NamedArg Pattern] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg Pattern -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [NamedArg Pattern]
    rps)
        , m Doc
    "target          = " m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> m Doc -> m Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (Arg Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Arg Type
    target)
        ]