    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.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 ( sortOn )
    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.Monad
    import Agda.Utils.Null
    import Agda.Utils.Singleton
    import Agda.Utils.Size
    import qualified Agda.Syntax.Common.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
    $c== :: FlexibleVarKind -> FlexibleVarKind -> Bool
    == :: FlexibleVarKind -> FlexibleVarKind -> Bool
    $c/= :: FlexibleVarKind -> FlexibleVarKind -> Bool
    /= :: 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
    $cshowsPrec :: Int -> FlexibleVarKind -> ShowS
    showsPrec :: Int -> FlexibleVarKind -> ShowS
    $cshow :: FlexibleVarKind -> ArgName
    show :: FlexibleVarKind -> ArgName
    $cshowList :: [FlexibleVarKind] -> ShowS
    showList :: [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
    $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
    /= :: 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
    $cshowsPrec :: forall a. Show a => Int -> FlexibleVar a -> ShowS
    showsPrec :: Int -> FlexibleVar a -> ShowS
    $cshow :: forall a. Show a => FlexibleVar a -> ArgName
    show :: FlexibleVar a -> ArgName
    $cshowList :: forall a. Show a => [FlexibleVar a] -> ShowS
    showList :: [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
    $cfmap :: forall a b. (a -> b) -> FlexibleVar a -> FlexibleVar b
    fmap :: forall a b. (a -> b) -> FlexibleVar a -> FlexibleVar b
    $c<$ :: forall a b. a -> FlexibleVar b -> FlexibleVar a
    <$ :: forall a b. a -> FlexibleVar b -> FlexibleVar a
    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
    $cfold :: forall m. Monoid m => FlexibleVar m -> m
    fold :: forall m. Monoid m => FlexibleVar m -> 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
    foldMap' :: forall m a. Monoid m => (a -> m) -> FlexibleVar a -> m
    $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
    foldr' :: forall a b. (a -> b -> 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
    foldl' :: forall b a. (b -> a -> b) -> b -> FlexibleVar a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> FlexibleVar a -> a
    foldr1 :: forall a. (a -> a -> a) -> FlexibleVar a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> FlexibleVar a -> a
    foldl1 :: forall a. (a -> a -> a) -> FlexibleVar a -> a
    $ctoList :: forall a. FlexibleVar a -> [a]
    toList :: forall a. FlexibleVar a -> [a]
    $cnull :: forall a. FlexibleVar a -> Bool
    null :: forall a. FlexibleVar a -> Bool
    $clength :: forall a. FlexibleVar a -> Int
    length :: forall a. FlexibleVar a -> Int
    $celem :: forall a. Eq a => a -> FlexibleVar a -> Bool
    elem :: forall a. Eq a => a -> FlexibleVar a -> Bool
    $cmaximum :: forall a. Ord a => FlexibleVar a -> a
    maximum :: forall a. Ord a => FlexibleVar a -> a
    $cminimum :: forall a. Ord a => FlexibleVar a -> a
    minimum :: forall a. Ord a => FlexibleVar a -> a
    $csum :: forall a. Num a => FlexibleVar a -> a
    sum :: forall a. Num a => FlexibleVar a -> a
    $cproduct :: forall a. Num a => FlexibleVar a -> a
    product :: forall a. Num a => FlexibleVar a -> a
    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)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> FlexibleVar a -> f (FlexibleVar b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> FlexibleVar a -> f (FlexibleVar b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    FlexibleVar (f a) -> f (FlexibleVar a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    FlexibleVar (f a) -> f (FlexibleVar a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> FlexibleVar a -> m (FlexibleVar b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> FlexibleVar a -> m (FlexibleVar b)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    FlexibleVar (m a) -> m (FlexibleVar a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    FlexibleVar (m a) -> m (FlexibleVar a)
    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 = ai }
      mapArgInfo :: (ArgInfo -> ArgInfo) -> FlexibleVar a -> FlexibleVar a
    mapArgInfo ArgInfo -> ArgInfo
    f  FlexibleVar a
    fl = FlexibleVar a
    fl { flexArgInfo = f (flexArgInfo 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
    $c== :: FlexChoice -> FlexChoice -> Bool
    == :: FlexChoice -> FlexChoice -> Bool
    $c/= :: FlexChoice -> FlexChoice -> Bool
    /= :: 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
    $cshowsPrec :: Int -> FlexChoice -> ShowS
    showsPrec :: Int -> FlexChoice -> ShowS
    $cshow :: FlexChoice -> ArgName
    show :: FlexChoice -> ArgName
    $cshowList :: [FlexChoice] -> ShowS
    showList :: [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
    $cshowsPrec :: forall a. Int -> Problem a -> ShowS
    showsPrec :: Int -> Problem a -> ShowS
    $cshow :: forall a. Problem a -> ArgName
    show :: Problem a -> ArgName
    $cshowList :: forall a. [Problem a] -> ShowS
    showList :: [Problem a] -> ShowS
    Show

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

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

    problemCont :: Lens' (Problem a) (LHSState a -> TCM a)
    problemCont :: forall a (f :: * -> *).
    Functor f =>
    ((LHSState a -> TCM a) -> f (LHSState a -> TCM a))
    -> Problem a -> f (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 (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \LHSState a -> TCM a
    x -> Problem a
    p {_problemCont = 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' (Problem a) [ProblemEq] -> [ProblemEq]
    forall o i. o -> Lens' o i -> i
    ^. ([ProblemEq] -> f [ProblemEq]) -> Problem a -> f (Problem a)
    forall a (f :: * -> *).
    Functor f =>
    ([ProblemEq] -> f [ProblemEq]) -> Problem a -> f (Problem a)
    Lens' (Problem a) [ProblemEq]
    problemEqs)

    data AsBinding = AsB Name Term (Dom Type)
    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?
      , forall a. LHSState a -> Bool
    _lhsIndexedSplit :: !Bool
        -- ^ Have we split on any indexed inductive types?
      }

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

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

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

    lhsTarget :: Lens' (LHSState a) (Arg Type)
    lhsTarget :: forall a (f :: * -> *).
    Functor f =>
    (Arg Type -> f (Arg Type)) -> LHSState a -> f (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 (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \Arg Type
    x -> LHSState a
    p {_lhsTarget = 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
    $cshowsPrec :: Int -> PatVarPosition -> ShowS
    showsPrec :: Int -> PatVarPosition -> ShowS
    $cshow :: PatVarPosition -> ArgName
    show :: PatVarPosition -> ArgName
    $cshowList :: [PatVarPosition] -> ShowS
    showList :: [PatVarPosition] -> ShowS
    Show, PatVarPosition -> PatVarPosition -> Bool
    (PatVarPosition -> PatVarPosition -> Bool)
    -> (PatVarPosition -> PatVarPosition -> Bool) -> Eq PatVarPosition
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: PatVarPosition -> PatVarPosition -> Bool
    == :: PatVarPosition -> PatVarPosition -> Bool
    $c/= :: PatVarPosition -> PatVarPosition -> Bool
    /= :: PatVarPosition -> PatVarPosition -> Bool
    Eq)

    data LeftoverPatterns = LeftoverPatterns
      { LeftoverPatterns -> IntMap [(Arg Name, PatVarPosition)]
    patternVariables :: IntMap [(Arg 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
        { patternVariables :: IntMap [(Arg Name, PatVarPosition)]
    patternVariables = ([(Arg Name, PatVarPosition)]
     -> [(Arg Name, PatVarPosition)] -> [(Arg Name, PatVarPosition)])
    -> IntMap [(Arg Name, PatVarPosition)]
    -> IntMap [(Arg Name, PatVarPosition)]
    -> IntMap [(Arg Name, PatVarPosition)]
    forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
    IntMap.unionWith [(Arg Name, PatVarPosition)]
    -> [(Arg Name, PatVarPosition)] -> [(Arg Name, PatVarPosition)]
    forall a. [a] -> [a] -> [a]
    (++) (LeftoverPatterns -> IntMap [(Arg Name, PatVarPosition)]
    patternVariables LeftoverPatterns
    x) (LeftoverPatterns -> IntMap [(Arg 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 [(Arg Name, PatVarPosition)]
    -> [AsBinding]
    -> [DotPattern]
    -> [AbsurdPattern]
    -> [AnnotationPattern]
    -> [Pattern]
    -> LeftoverPatterns
    LeftoverPatterns IntMap [(Arg Name, PatVarPosition)]
    forall a. Null a => a
    empty [] [] [] [] []
      null :: LeftoverPatterns -> Bool
    null (LeftoverPatterns IntMap [(Arg Name, PatVarPosition)]
    as [AsBinding]
    bs [DotPattern]
    cs [AbsurdPattern]
    ds [AnnotationPattern]
    es [Pattern]
    fs) = IntMap [(Arg Name, PatVarPosition)] -> Bool
    forall a. Null a => a -> Bool
    null IntMap [(Arg 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
    forall a. ArgName -> Doc a
    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 [(Arg 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, [(Arg Name, PatVarPosition)])] -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (IntMap [(Arg Name, PatVarPosition)]
    -> [(Int, [(Arg Name, PatVarPosition)])]
    forall a. IntMap a -> [(Int, a)]
    IntMap.toList IntMap [(Arg 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
    forall (m :: * -> *). MonadPretty m => AsBinding -> 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
    forall (m :: * -> *). MonadPretty m => DotPattern -> 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
    forall (m :: * -> *). MonadPretty m => AbsurdPattern -> 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
    forall (m :: * -> *). MonadPretty m => AnnotationPattern -> 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, MonadFresh NameId m)
      => [ProblemEq] -> m LeftoverPatterns
    getLeftoverPatterns :: forall (m :: * -> *).
    (PureTCM m, MonadFresh NameId 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"
      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
    x = if Name -> ArgName
    nameToArgName Name
    x ArgName -> Set ArgName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set ArgName
    params then PatVarPosition
    PVParam else PatVarPosition
    PVLocal
      mconcat <$> mapM (getLeftoverPattern isParamName) eqs
      where
        patternVariable :: Arg Name -> Int -> PatVarPosition -> LeftoverPatterns
    patternVariable Arg Name
    x Int
    i PatVarPosition
    isPar = LeftoverPatterns
    forall a. Null a => a
    empty { patternVariables = singleton (i,[(x,isPar)]) }
        asPattern :: Name -> Term -> Dom Type -> LeftoverPatterns
    asPattern Name
    x Term
    v Dom Type
    a      = LeftoverPatterns
    forall a. Null a => a
    empty { asPatterns       = singleton (AsB x v a) }
        dotPattern :: Expr -> Term -> Dom Type -> LeftoverPatterns
    dotPattern Expr
    e Term
    v Dom Type
    a     = LeftoverPatterns
    forall a. Null a => a
    empty { dotPatterns      = singleton (Dot e v a) }
        absurdPattern :: Range -> Type -> LeftoverPatterns
    absurdPattern Range
    info Type
    a = LeftoverPatterns
    forall a. Null a => a
    empty { absurdPatterns   = singleton (Absurd info a) }
        otherPattern :: Pattern -> LeftoverPatterns
    otherPattern Pattern
    p       = LeftoverPatterns
    forall a. Null a => a
    empty { otherPatterns    = singleton p }

        getLeftoverPattern :: (A.Name -> PatVarPosition) -> ProblemEq -> m LeftoverPatterns
        getLeftoverPattern :: (Name -> PatVarPosition) -> ProblemEq -> m LeftoverPatterns
    getLeftoverPattern Name -> PatVarPosition
    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 -> LeftoverPatterns) -> m LeftoverPatterns
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case
            Just Int
    i -> Arg Name -> Int -> PatVarPosition -> LeftoverPatterns
    patternVariable (Dom Type -> Arg Type
    forall t a. Dom' t a -> Arg a
    argFromDom Dom Type
    a Arg Type -> Name -> Arg Name
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Name
    x) Int
    i (Name -> PatVarPosition
    isParamName Name
    x)
            Maybe Int
    Nothing -> Name -> Term -> Dom Type -> LeftoverPatterns
    asPattern Name
    x Term
    v Dom Type
    a
          (A.WildP PatInfo
    r)
            | Dom Type -> Bool
    forall a. LensHiding a => a -> Bool
    isInstance Dom Type
    a ->
                -- Issue #7392: If the wildcard appears in an instance position
                -- and is not already bound as an instance in the context,
                -- add it as a let binding.
                m Bool
    -> m LeftoverPatterns -> m LeftoverPatterns -> m LeftoverPatterns
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Term -> Type -> m Bool
    isInstanceVar Term
    v (Type -> m Bool) -> Type -> m Bool
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a) (LeftoverPatterns -> m LeftoverPatterns
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return LeftoverPatterns
    forall a. Monoid a => a
    mempty) (m LeftoverPatterns -> m LeftoverPatterns)
    -> m LeftoverPatterns -> m LeftoverPatterns
    forall a b. (a -> b) -> a -> b
    $ do
                  -- TODO: avoid fresh name by assigning unique `NameId` to `WildP`s?
                  x <- Range -> m Name
    forall (m :: * -> *). MonadFresh NameId m => Range -> m Name
    freshNoName (PatInfo -> Range
    forall a. HasRange a => a -> Range
    getRange PatInfo
    r)
                  return $ asPattern x v a
            | Bool
    otherwise -> LeftoverPatterns -> m LeftoverPatterns
    forall a. a -> m a
    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
    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 -> PatVarPosition) -> ProblemEq -> m LeftoverPatterns
    getLeftoverPattern Name -> PatVarPosition
    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 a. a -> m a
    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 a. a -> m a
    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)
          Pattern
    _                 -> LeftoverPatterns -> m LeftoverPatterns
    forall a. a -> m a
    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

          where
            isInstanceVar :: Term -> Type -> m Bool
            isInstanceVar :: Term -> Type -> m Bool
    isInstanceVar Term
    v Type
    a = Term -> Type -> m (Maybe Int)
    forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Int)
    isEtaVar Term
    v Type
    a m (Maybe Int) -> (Maybe Int -> m Bool) -> m Bool
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                Just Int
    i -> Dom Type -> Bool
    forall a. LensHiding a => a -> Bool
    isInstance (Dom Type -> Bool) -> m (Dom Type) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> m (Dom Type)
    forall (m :: * -> *).
    (MonadDebug m, MonadTCEnv m) =>
    Int -> m (Dom Type)
    domOfBV Int
    i
                Maybe Int
    Nothing -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    -- | 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 [(Arg A.Name,PatVarPosition)]  -- ^ The list of user names for each pattern variable
      -> ([Maybe A.Name], [AsBinding])
    getUserVariableNames :: Telescope
    -> IntMap [(Arg Name, PatVarPosition)]
    -> ([Maybe Name], [AsBinding])
    getUserVariableNames Telescope
    tel IntMap [(Arg 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 ((Arg Name, PatVarPosition) -> Arg Name)
    -> [(Arg Name, PatVarPosition)] -> [Arg Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg Name, PatVarPosition) -> Arg Name
    forall a b. (a, b) -> a
    fst ([(Arg Name, PatVarPosition)] -> [Arg Name])
    -> [(Arg Name, PatVarPosition)] -> [Arg Name]
    forall a b. (a -> b) -> a -> b
    $ ((Arg Name, PatVarPosition) -> Bool)
    -> [(Arg Name, PatVarPosition)] -> [(Arg Name, PatVarPosition)]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    sortOn ((PatVarPosition -> PatVarPosition -> Bool
    forall a. Eq a => a -> a -> Bool
    == PatVarPosition
    PVParam) (PatVarPosition -> Bool)
    -> ((Arg Name, PatVarPosition) -> PatVarPosition)
    -> (Arg Name, PatVarPosition)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Name, PatVarPosition) -> PatVarPosition
    forall a b. (a, b) -> b
    snd) ([(Arg Name, PatVarPosition)]
    -> Int
    -> IntMap [(Arg Name, PatVarPosition)]
    -> [(Arg Name, PatVarPosition)]
    forall a. a -> Int -> IntMap a -> a
    IntMap.findWithDefault [] Int
    i IntMap [(Arg Name, PatVarPosition)]
    names) of
            [] -> Maybe Name -> WriterT [AsBinding] Identity (Maybe Name)
    forall a. a -> WriterT [AsBinding] Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Name
    forall a. Maybe a
    Nothing
            (Arg Name
    z:[Arg Name]
    zs) -> do
              [Arg Name] -> WriterT [AsBinding] Identity ()
    tellAsBindings ([Arg Name] -> WriterT [AsBinding] Identity ())
    -> [Arg Name] -> WriterT [AsBinding] Identity ()
    forall a b. (a -> b) -> a -> b
    $
                -- Issue #7392: if the name that we picked comes from an instance argument
                -- but we are *not* binding it in an instance position, we should
                -- preserve the instance by *also* adding it as a let-binding.
                if Arg Name -> Bool
    forall a. LensHiding a => a -> Bool
    isInstance Arg Name
    z Bool -> Bool -> Bool
    && Bool -> Bool
    not (Dom Type -> Bool
    forall a. LensHiding a => a -> Bool
    isInstance Dom Type
    a) then Arg Name
    zArg Name -> [Arg Name] -> [Arg Name]
    forall a. a -> [a] -> [a]
    :[Arg Name]
    zs else [Arg Name]
    zs
              Maybe Name -> WriterT [AsBinding] Identity (Maybe Name)
    forall a. a -> WriterT [AsBinding] Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Name -> WriterT [AsBinding] Identity (Maybe Name))
    -> Maybe Name -> WriterT [AsBinding] Identity (Maybe Name)
    forall a b. (a -> b) -> a -> b
    $ Name -> Maybe Name
    forall a. a -> Maybe a
    Just (Arg Name -> Name
    forall e. Arg e -> e
    unArg Arg Name
    z)
          where
            -- Use hiding status of the variable as written rather than from the telescope
            tellAsBindings :: [Arg Name] -> WriterT [AsBinding] Identity ()
    tellAsBindings = [AsBinding] -> WriterT [AsBinding] Identity ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell ([AsBinding] -> WriterT [AsBinding] Identity ())
    -> ([Arg Name] -> [AsBinding])
    -> [Arg Name]
    -> WriterT [AsBinding] Identity ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Name -> AsBinding) -> [Arg Name] -> [AsBinding]
    forall a b. (a -> b) -> [a] -> [b]
    map (\Arg Name
    y -> Name -> Term -> Dom Type -> AsBinding
    AsB (Arg Name -> Name
    forall e. Arg e -> e
    unArg Arg Name
    y) (Int -> Term
    var Int
    i) (Hiding -> Dom Type -> Dom Type
    forall a. LensHiding a => Hiding -> a -> a
    setHiding (Arg Name -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding Arg Name
    y) Dom Type
    a))

    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 Dom Type
    a) = (\(Term
    v,Dom Type
    a) -> Name -> Term -> Dom Type -> AsBinding
    AsB Name
    x Term
    v Dom Type
    a) ((Term, Dom Type) -> AsBinding) -> (Term, Dom Type) -> AsBinding
    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 AsBinding)
    rho (Term
    v, Dom 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
    forall (m :: * -> *). MonadPretty m => Term -> 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
    forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
    prettyTCM Dom Type
    a
        ]

    instance PrettyTCM AsBinding where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => AsBinding -> m Doc
    prettyTCM (AsB Name
    x Term
    v Dom Type
    a) =
        [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
    forall (m :: * -> *). MonadPretty m => Name -> 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
    forall (m :: * -> *). MonadPretty m => Term -> 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
    <+> Dom Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
    prettyTCM Dom 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
    forall (m :: * -> *). MonadPretty m => Term -> 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
    forall (m :: * -> *). MonadPretty m => Dom Type -> 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
    forall (m :: * -> *). MonadPretty m => Type -> 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
    forall (m :: * -> *). MonadPretty m => Type -> 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 Dom Type
    a) =
        Name -> Doc
    forall a. Pretty a => a -> Doc
    PP.pretty Name
    x Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    PP.<+> Doc
    "=" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    PP.<+>
          Doc -> Int -> Doc -> Doc
    forall a. Doc a -> Int -> Doc a -> Doc a
    PP.hang (Term -> Doc
    forall a. Pretty a => a -> Doc
    PP.pretty Term
    v Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    PP.<+> Doc
    ":") Int
    2 (Dom Type -> Doc
    forall a. Pretty a => a -> Doc
    PP.pretty Dom Type
    a)

    instance InstantiateFull AsBinding where
      instantiateFull' :: AsBinding -> ReduceM AsBinding
    instantiateFull' (AsB Name
    x Term
    v Dom Type
    a) = Name -> Term -> Dom Type -> AsBinding
    AsB Name
    x (Term -> Dom Type -> AsBinding)
    -> ReduceM Term -> ReduceM (Dom Type -> 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 (Dom Type -> AsBinding)
    -> ReduceM (Dom Type) -> ReduceM AsBinding
    forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Dom Type -> ReduceM (Dom Type)
    forall t. InstantiateFull t => t -> ReduceM t
    instantiateFull' Dom Type
    a

    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]
    _ Bool
    _) = [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
    forall (m :: * -> *). MonadPretty m => Telescope -> 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
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> 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
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> 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
    forall (m :: * -> *). MonadPretty m => ProblemEq -> 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
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    tel (Arg Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Arg Type -> m Doc
    prettyTCM Arg Type
    target)
        ]