{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

-- | Unification algorithm for specializing datatype indices, as described in
--     \"Unifiers as Equivalences: Proof-Relevant Unification of Dependently
--     Typed Data\" by Jesper Cockx, Dominique Devriese, and Frank Piessens
--     (ICFP 2016).
--
--   This is the unification algorithm used for checking the left-hand side
--   of clauses (see @Agda.TypeChecking.Rules.LHS@), coverage checking (see
--   @Agda.TypeChecking.Coverage@) and indirectly also for interactive case
--   splitting (see @Agda.Interaction.MakeCase@).
--
--   A unification problem (of type @UnifyState@) consists of:
--
--   1. A telescope @varTel@ of free variables, some or all of which are
--      flexible (as indicated by @flexVars@).
--
--   2. A telescope @eqTel@ containing the types of the equations.
--
--   3. Left- and right-hand sides for each equation:
--      @varTel ⊢ eqLHS : eqTel@ and @varTel ⊢ eqRHS : eqTel@.
--
--   The unification algorithm can end in three different ways:
--   (type @UnificationResult@):
--
--   - A *positive success* @Unifies (tel, sigma, ps)@ with @tel ⊢ sigma : varTel@,
--     @tel ⊢ eqLHS [ varTel ↦ sigma ] ≡ eqRHS [ varTel ↦ sigma ] : eqTel@,
--     and @tel ⊢ ps : eqTel@. In this case, @sigma;ps@ is an *equivalence*
--     between the telescopes @tel@ and @varTel(eqLHS ≡ eqRHS)@.
--
--   - A *negative success* @NoUnify err@ means that a conflicting equation
--     was found (e.g an equation between two distinct constructors or a cycle).
--
--   - A *failure* @UnifyStuck err@ means that the unifier got stuck.
--
--   The unification algorithm itself consists of two parts:
--
--   1. A *unification strategy* takes a unification problem and produces a
--      list of suggested unification rules (of type @UnifyStep@). Strategies
--      can be constructed by composing simpler strategies (see for example the
--      definition of @completeStrategyAt@).
--
--   2. The *unification engine* @unifyStep@ takes a unification rule and tries
--      to apply it to the given state, writing the result to the UnifyOutput
--      on a success.
--
--   The unification steps (of type @UnifyStep@) are the following:
--
--   - *Deletion* removes a reflexive equation @u =?= v : a@ if the left- and
--     right-hand side @u@ and @v@ are (definitionally) equal. This rule results
--     in a failure if --without-K is enabled (see \"Pattern Matching Without K\"
--     by Jesper Cockx, Dominique Devriese, and Frank Piessens (ICFP 2014).
--
--   - *Solution* solves an equation if one side is (eta-equivalent to) a
--     flexible variable. In case both sides are flexible variables, the
--     unification strategy makes a choice according to the @chooseFlex@
--     function in @Agda.TypeChecking.Rules.LHS.Problem@.
--
--   - *Injectivity* decomposes an equation of the form
--     @c us =?= c vs : D pars is@ where @c : Δc → D pars js@ is a constructor
--     of the inductive datatype @D@ into a sequence of equations
--     @us =?= vs : delta@. In case @D@ is an indexed datatype,
--     *higher-dimensional unification* is applied (see below).
--
--   - *Conflict* detects absurd equations of the form
--     @c₁ us =?= c₂ vs : D pars is@ where @c₁@ and @c₂@ are two distinct
--     constructors of the datatype @D@.
--
--   - *Cycle* detects absurd equations of the form @x =?= v : D pars is@ where
--     @x@ is a variable of the datatype @D@ that occurs strongly rigid in @v@.
--
--   - *EtaExpandVar* eta-expands a single flexible variable @x : R@ where @R@
--     is a (eta-expandable) record type, replacing it by one variable for each
--     field of @R@.
--
--   - *EtaExpandEquation* eta-expands an equation @u =?= v : R@ where @R@ is a
--     (eta-expandable) record type, replacing it by one equation for each field
--     of @R@. The left- and right-hand sides of these equations are the
--     projections of @u@ and @v@.
--
--   - *LitConflict* detects absurd equations of the form @l₁ =?= l₂ : A@ where
--     @l₁@ and @l₂@ are distinct literal terms.
--
--   - *StripSizeSuc* simplifies an equation of the form
--     @sizeSuc x =?= sizeSuc y : Size@ to @x =?= y : Size@.
--
--   - *SkipIrrelevantEquation@ removes an equation between irrelevant terms.
--
--   - *TypeConInjectivity* decomposes an equation of the form
--     @D us =?= D vs : Type i@ where @D@ is a datatype. This rule is only used
--     if an @INJECTIVE@ pragma is used on @D@.
--
--   Higher-dimensional unification (new, does not yet appear in any paper):
--   If an equation of the form @c us =?= c vs : D pars is@ is encountered where
--   @c : Δc → D pars js@ is a constructor of an indexed datatype
--   @D pars : Φ → Type ℓ@, it is in general unsound to just simplify this
--   equation to @us =?= vs : Δc@. For this reason, the injectivity rule in the
--   paper restricts the indices @is@ to be distinct variables that are bound in
--   the telescope @eqTel@. But we can be more general by introducing new
--   variables @ks@ to the telescope @eqTel@ and equating these to @is@:
--   @
--       Δ₁(x : D pars is)Δ₂
--        ≃
--       Δ₁(ks : Φ)(x : D pars ks)(ps : is ≡Φ ks)Δ₂
--   @
--   Since @ks@ are distinct variables, it's now possible to apply injectivity
--   to the equation @x@, resulting in the following new equation telescope:
--   @
--     Δ₁(ys : Δc)(ps : is ≡Φ js[Δc ↦ ys])Δ₂
--   @
--   Now we can solve the equations @ps@ by recursively calling the unification
--   algorithm with flexible variables @Δ₁(ys : Δc)@. This is called
--   *higher-dimensional unification* since we are unifying equality proofs
--   rather than terms. If the higher-dimensional unification succeeds, the
--   resulting telescope serves as the new equation telescope for the original
--   unification problem.

module Mikan.TypeChecking.Rules.LHS.Unify
  ( UnificationResult
  , UnificationResult'(..)
  , NoLeftInv(..)
  , unifyIndices'
  , unifyIndices ) where

import Prelude hiding (null)

-- import Data.Semigroup ( All(..) )
import Data.List qualified as List
import Data.IntSet qualified as IntSet
import Data.IntSet (IntSet)

import Mikan.Benchmarking qualified as Bench

import Mikan.Syntax.Common
import Mikan.Syntax.Internal

import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Monad.Benchmark qualified as Bench
import Mikan.TypeChecking.Conversion.Pure (pureBlockOrEqualTerm, pureBlockOrEqualType)
import Mikan.TypeChecking.Constraints ()
import Mikan.TypeChecking.Coverage.Errors
import Mikan.TypeChecking.Datatypes
import Mikan.TypeChecking.Irrelevance
import Mikan.TypeChecking.Reduce
import Mikan.TypeChecking.Patterns.Match qualified as Match
import Mikan.TypeChecking.Pretty
import Mikan.TypeChecking.Substitute
import Mikan.TypeChecking.Telescope
import Mikan.TypeChecking.Free
import Mikan.TypeChecking.Free.Precompute
import Mikan.TypeChecking.Free.Reduce
import Mikan.TypeChecking.Records

import Mikan.TypeChecking.Rules.LHS.Problem
import Mikan.TypeChecking.Rules.LHS.Unify.Types
import Mikan.TypeChecking.Rules.LHS.Unify.LeftInverse

import Mikan.Utils.List
import Mikan.Utils.ListT
import Mikan.Utils.Maybe
import Mikan.Utils.Monad
import Mikan.Utils.Null
import Mikan.Utils.Size
import Mikan.Utils.Singleton
import Mikan.Utils.VarSet qualified as VarSet
import Mikan.Utils.StrictWriter
import Mikan.Utils.StrictState

import Mikan.Utils.Impossible


-- | Result of 'unifyIndices'.
type UnificationResult = UnificationResult'
  ( Telescope                  -- @tel@
  , PatternSubstitution        -- @sigma@ s.t. @tel ⊢ sigma : varTel@
  , [NamedArg DeBruijnPattern] -- @ps@    s.t. @tel ⊢ ps    : eqTel @
  )

type FullUnificationResult = UnificationResult'
  ( Telescope                  -- @tel@
  , PatternSubstitution        -- @sigma@ s.t. @tel ⊢ sigma : varTel@
  , [NamedArg DeBruijnPattern] -- @ps@    s.t. @tel ⊢ ps    : eqTel @
  , TCM (Either NoLeftInv (Substitution, Substitution)) -- (τ,leftInv)
  )

-- | Indicates whether the step should be retried after normalising the
-- types of variables in the unification state.
data RetryNormalised
  = RetryNormalised
    -- ^ Retrying can happen.
  | DontRetryNormalised UnifyState
    -- ^ We've already tried once, and this was the resulting 'UnifyState'.
  deriving (Key -> RetryNormalised -> ShowS
[RetryNormalised] -> ShowS
RetryNormalised -> String
(Key -> RetryNormalised -> ShowS)
-> (RetryNormalised -> String)
-> ([RetryNormalised] -> ShowS)
-> Show RetryNormalised
forall a.
(Key -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Key -> RetryNormalised -> ShowS
showsPrec :: Key -> RetryNormalised -> ShowS
$cshow :: RetryNormalised -> String
show :: RetryNormalised -> String
$cshowList :: [RetryNormalised] -> ShowS
showList :: [RetryNormalised] -> ShowS
Show)

data UnificationResult' a
  = Unifies RetryNormalised a         -- ^ Unification succeeded, possibly without performing normalisation.
  | NoUnify NegativeUnification       -- ^ Terms are not unifiable.
  | UnifyBlocked Blocker              -- ^ Unification got blocked on a metavariable
  | UnifyStuck   [UnificationFailure] -- ^ Some other error happened, unification got stuck.
  deriving (Key -> UnificationResult' a -> ShowS
[UnificationResult' a] -> ShowS
UnificationResult' a -> String
(Key -> UnificationResult' a -> ShowS)
-> (UnificationResult' a -> String)
-> ([UnificationResult' a] -> ShowS)
-> Show (UnificationResult' a)
forall a. Show a => Key -> UnificationResult' a -> ShowS
forall a. Show a => [UnificationResult' a] -> ShowS
forall a. Show a => UnificationResult' a -> String
forall a.
(Key -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Key -> UnificationResult' a -> ShowS
showsPrec :: Key -> UnificationResult' a -> ShowS
$cshow :: forall a. Show a => UnificationResult' a -> String
show :: UnificationResult' a -> String
$cshowList :: forall a. Show a => [UnificationResult' a] -> ShowS
showList :: [UnificationResult' a] -> ShowS
Show, (forall a b.
 (a -> b) -> UnificationResult' a -> UnificationResult' b)
-> (forall a b. a -> UnificationResult' b -> UnificationResult' a)
-> Functor UnificationResult'
forall a b. a -> UnificationResult' b -> UnificationResult' a
forall a b.
(a -> b) -> UnificationResult' a -> UnificationResult' 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) -> UnificationResult' a -> UnificationResult' b
fmap :: forall a b.
(a -> b) -> UnificationResult' a -> UnificationResult' b
$c<$ :: forall a b. a -> UnificationResult' b -> UnificationResult' a
<$ :: forall a b. a -> UnificationResult' b -> UnificationResult' a
Functor, (forall m. Monoid m => UnificationResult' m -> m)
-> (forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m)
-> (forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m)
-> (forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b)
-> (forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b)
-> (forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b)
-> (forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b)
-> (forall a. (a -> a -> a) -> UnificationResult' a -> a)
-> (forall a. (a -> a -> a) -> UnificationResult' a -> a)
-> (forall a. UnificationResult' a -> [a])
-> (forall a. UnificationResult' a -> Bool)
-> (forall a. UnificationResult' a -> Key)
-> (forall a. Eq a => a -> UnificationResult' a -> Bool)
-> (forall a. Ord a => UnificationResult' a -> a)
-> (forall a. Ord a => UnificationResult' a -> a)
-> (forall a. Num a => UnificationResult' a -> a)
-> (forall a. Num a => UnificationResult' a -> a)
-> Foldable UnificationResult'
forall a. Eq a => a -> UnificationResult' a -> Bool
forall a. Num a => UnificationResult' a -> a
forall a. Ord a => UnificationResult' a -> a
forall m. Monoid m => UnificationResult' m -> m
forall a. UnificationResult' a -> Bool
forall a. UnificationResult' a -> Key
forall a. UnificationResult' a -> [a]
forall a. (a -> a -> a) -> UnificationResult' a -> a
forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
forall a b. (a -> b -> b) -> b -> UnificationResult' 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 -> Key)
-> (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 => UnificationResult' m -> m
fold :: forall m. Monoid m => UnificationResult' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
foldr1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
foldl1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
$ctoList :: forall a. UnificationResult' a -> [a]
toList :: forall a. UnificationResult' a -> [a]
$cnull :: forall a. UnificationResult' a -> Bool
null :: forall a. UnificationResult' a -> Bool
$clength :: forall a. UnificationResult' a -> Key
length :: forall a. UnificationResult' a -> Key
$celem :: forall a. Eq a => a -> UnificationResult' a -> Bool
elem :: forall a. Eq a => a -> UnificationResult' a -> Bool
$cmaximum :: forall a. Ord a => UnificationResult' a -> a
maximum :: forall a. Ord a => UnificationResult' a -> a
$cminimum :: forall a. Ord a => UnificationResult' a -> a
minimum :: forall a. Ord a => UnificationResult' a -> a
$csum :: forall a. Num a => UnificationResult' a -> a
sum :: forall a. Num a => UnificationResult' a -> a
$cproduct :: forall a. Num a => UnificationResult' a -> a
product :: forall a. Num a => UnificationResult' a -> a
Foldable, Functor UnificationResult'
Foldable UnificationResult'
(Functor UnificationResult', Foldable UnificationResult') =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> UnificationResult' a -> f (UnificationResult' b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    UnificationResult' (f a) -> f (UnificationResult' a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> UnificationResult' a -> m (UnificationResult' b))
-> (forall (m :: * -> *) a.
    Monad m =>
    UnificationResult' (m a) -> m (UnificationResult' a))
-> Traversable UnificationResult'
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 =>
UnificationResult' (m a) -> m (UnificationResult' a)
forall (f :: * -> *) a.
Applicative f =>
UnificationResult' (f a) -> f (UnificationResult' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> UnificationResult' a -> m (UnificationResult' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> UnificationResult' a -> f (UnificationResult' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> UnificationResult' a -> f (UnificationResult' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> UnificationResult' a -> f (UnificationResult' b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
UnificationResult' (f a) -> f (UnificationResult' a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
UnificationResult' (f a) -> f (UnificationResult' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> UnificationResult' a -> m (UnificationResult' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> UnificationResult' a -> m (UnificationResult' b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
UnificationResult' (m a) -> m (UnificationResult' a)
sequence :: forall (m :: * -> *) a.
Monad m =>
UnificationResult' (m a) -> m (UnificationResult' a)
Traversable)

-- | Unify indices.
--
--   In @unifyIndices gamma flex a us vs@,
--
--   * @us@ and @vs@ are the argument lists to unify, eliminating type @a@.
--
--   * @gamma@ is the telescope of free variables in @us@ and @vs@.
--
--   * @flex@ is the set of flexible (instantiable) variables in @us@ and @vs@.
--
--   The result is the most general unifier of @us@ and @vs@.
unifyIndices
  :: Maybe NoLeftInv -- ^ Do we have a reason for not computing a left inverse?
  -> Telescope       -- ^ @gamma@
  -> FlexibleVars    -- ^ @flex@
  -> Type            -- ^ @a@
  -> Args            -- ^ @us@
  -> Args            -- ^ @vs@
  -> TCM UnificationResult
unifyIndices :: Maybe NoLeftInv
-> Telescope
-> FlexibleVars
-> Type
-> [Arg Term]
-> [Arg Term]
-> TCM UnificationResult
unifyIndices Maybe NoLeftInv
linv Telescope
tel FlexibleVars
flex Type
a [Arg Term]
us [Arg Term]
vs =
    ((Telescope, Substitution' (Pattern' DBPatVar),
  [NamedArg (Pattern' DBPatVar)],
  TCM (Either NoLeftInv (Substitution, Substitution)))
 -> (Telescope, Substitution' (Pattern' DBPatVar),
     [NamedArg (Pattern' DBPatVar)]))
-> UnificationResult'
     (Telescope, Substitution' (Pattern' DBPatVar),
      [NamedArg (Pattern' DBPatVar)],
      TCM (Either NoLeftInv (Substitution, Substitution)))
-> UnificationResult
forall a b.
(a -> b) -> UnificationResult' a -> UnificationResult' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Telescope
a,Substitution' (Pattern' DBPatVar)
b,[NamedArg (Pattern' DBPatVar)]
c,TCM (Either NoLeftInv (Substitution, Substitution))
_) -> (Telescope
a,Substitution' (Pattern' DBPatVar)
b,[NamedArg (Pattern' DBPatVar)]
c)) (UnificationResult'
   (Telescope, Substitution' (Pattern' DBPatVar),
    [NamedArg (Pattern' DBPatVar)],
    TCM (Either NoLeftInv (Substitution, Substitution)))
 -> UnificationResult)
-> TCMT
     IO
     (UnificationResult'
        (Telescope, Substitution' (Pattern' DBPatVar),
         [NamedArg (Pattern' DBPatVar)],
         TCM (Either NoLeftInv (Substitution, Substitution))))
-> TCM UnificationResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe NoLeftInv
-> Telescope
-> FlexibleVars
-> Type
-> [Arg Term]
-> [Arg Term]
-> TCMT
     IO
     (UnificationResult'
        (Telescope, Substitution' (Pattern' DBPatVar),
         [NamedArg (Pattern' DBPatVar)],
         TCM (Either NoLeftInv (Substitution, Substitution))))
unifyIndices' Maybe NoLeftInv
linv Telescope
tel FlexibleVars
flex Type
a [Arg Term]
us [Arg Term]
vs

unifyIndices'
  :: Maybe NoLeftInv -- ^ Do we have a reason for not computing a left inverse?
  -> Telescope     -- ^ @gamma@
  -> FlexibleVars  -- ^ @flex@
  -> Type          -- ^ @a@
  -> Args          -- ^ @us@
  -> Args          -- ^ @vs@
  -> TCM FullUnificationResult
unifyIndices' :: Maybe NoLeftInv
-> Telescope
-> FlexibleVars
-> Type
-> [Arg Term]
-> [Arg Term]
-> TCMT
     IO
     (UnificationResult'
        (Telescope, Substitution' (Pattern' DBPatVar),
         [NamedArg (Pattern' DBPatVar)],
         TCM (Either NoLeftInv (Substitution, Substitution))))
unifyIndices' Maybe NoLeftInv
linv Telescope
tel FlexibleVars
flex Type
a [Arg Term]
us [Arg Term]
vs = Account (BenchPhase (TCMT IO))
-> TCMT
     IO
     (UnificationResult'
        (Telescope, Substitution' (Pattern' DBPatVar),
         [NamedArg (Pattern' DBPatVar)],
         TCM (Either NoLeftInv (Substitution, Substitution))))
-> TCMT
     IO
     (UnificationResult'
        (Telescope, Substitution' (Pattern' DBPatVar),
         [NamedArg (Pattern' DBPatVar)],
         TCM (Either NoLeftInv (Substitution, Substitution))))
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.UnifyIndices] (TCMT
   IO
   (UnificationResult'
      (Telescope, Substitution' (Pattern' DBPatVar),
       [NamedArg (Pattern' DBPatVar)],
       TCM (Either NoLeftInv (Substitution, Substitution))))
 -> TCMT
      IO
      (UnificationResult'
         (Telescope, Substitution' (Pattern' DBPatVar),
          [NamedArg (Pattern' DBPatVar)],
          TCM (Either NoLeftInv (Substitution, Substitution)))))
-> TCMT
     IO
     (UnificationResult'
        (Telescope, Substitution' (Pattern' DBPatVar),
         [NamedArg (Pattern' DBPatVar)],
         TCM (Either NoLeftInv (Substitution, Substitution))))
-> TCMT
     IO
     (UnificationResult'
        (Telescope, Substitution' (Pattern' DBPatVar),
         [NamedArg (Pattern' DBPatVar)],
         TCM (Either NoLeftInv (Substitution, Substitution))))
forall a b. (a -> b) -> a -> b
$ case ([Arg Term]
us, [Arg Term]
vs) of
  ([], []) -> UnificationResult'
  (Telescope, Substitution' (Pattern' DBPatVar),
   [NamedArg (Pattern' DBPatVar)],
   TCM (Either NoLeftInv (Substitution, Substitution)))
-> TCMT
     IO
     (UnificationResult'
        (Telescope, Substitution' (Pattern' DBPatVar),
         [NamedArg (Pattern' DBPatVar)],
         TCM (Either NoLeftInv (Substitution, Substitution))))
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UnificationResult'
   (Telescope, Substitution' (Pattern' DBPatVar),
    [NamedArg (Pattern' DBPatVar)],
    TCM (Either NoLeftInv (Substitution, Substitution)))
 -> TCMT
      IO
      (UnificationResult'
         (Telescope, Substitution' (Pattern' DBPatVar),
          [NamedArg (Pattern' DBPatVar)],
          TCM (Either NoLeftInv (Substitution, Substitution)))))
-> UnificationResult'
     (Telescope, Substitution' (Pattern' DBPatVar),
      [NamedArg (Pattern' DBPatVar)],
      TCM (Either NoLeftInv (Substitution, Substitution)))
-> TCMT
     IO
     (UnificationResult'
        (Telescope, Substitution' (Pattern' DBPatVar),
         [NamedArg (Pattern' DBPatVar)],
         TCM (Either NoLeftInv (Substitution, Substitution))))
forall a b. (a -> b) -> a -> b
$ RetryNormalised
-> (Telescope, Substitution' (Pattern' DBPatVar),
    [NamedArg (Pattern' DBPatVar)],
    TCM (Either NoLeftInv (Substitution, Substitution)))
-> UnificationResult'
     (Telescope, Substitution' (Pattern' DBPatVar),
      [NamedArg (Pattern' DBPatVar)],
      TCM (Either NoLeftInv (Substitution, Substitution)))
forall a. RetryNormalised -> a -> UnificationResult' a
Unifies RetryNormalised
RetryNormalised (Telescope
tel, Substitution' (Pattern' DBPatVar)
forall a. Substitution' a
idS, [], Either NoLeftInv (Substitution, Substitution)
-> TCM (Either NoLeftInv (Substitution, Substitution))
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either NoLeftInv (Substitution, Substitution)
 -> TCM (Either NoLeftInv (Substitution, Substitution)))
-> Either NoLeftInv (Substitution, Substitution)
-> TCM (Either NoLeftInv (Substitution, Substitution))
forall a b. (a -> b) -> a -> b
$ (Substitution, Substitution)
-> Either NoLeftInv (Substitution, Substitution)
forall a b. b -> Either a b
Right (Substitution
forall a. Substitution' a
idS, Key -> Substitution
forall a. Key -> Substitution' a
raiseS Key
1))
  ([Arg Term], [Arg Term])
_        -> do
    String -> Key -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Key
10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"unifyIndices"
          , (TCMT IO Doc
"tel  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Key -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Key -> m Doc -> m Doc
nest Key
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
tel
          , (TCMT IO Doc
"flex =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Key -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Key -> m Doc -> m Doc
nest Key
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO 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 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Key] -> String
forall a. Show a => a -> String
show ([Key] -> String) -> [Key] -> String
forall a b. (a -> b) -> a -> b
$ (FlexibleVar Key -> Key) -> FlexibleVars -> [Key]
forall a b. (a -> b) -> [a] -> [b]
map' FlexibleVar Key -> Key
forall a. FlexibleVar a -> a
flexVar FlexibleVars
flex
          , (TCMT IO Doc
"a    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Key -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Key -> m Doc -> m Doc
nest Key
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO 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 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a)
          , (TCMT IO Doc
"us   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Key -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Key -> m Doc -> m Doc
nest Key
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO 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 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM [Arg Term]
us
          , (TCMT IO Doc
"vs   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Key -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Key -> m Doc -> m Doc
nest Key
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO 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 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM [Arg Term]
vs
          ]
    initialState    <- Telescope
-> FlexibleVars
-> Type
-> [Arg Term]
-> [Arg Term]
-> TCMT IO UnifyState
forall (m :: * -> *).
PureTCM m =>
Telescope
-> FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> m UnifyState
initUnifyState Telescope
tel FlexibleVars
flex Type
a [Arg Term]
us [Arg Term]
vs
    reportSDoc "tc.lhs.unify" 20 $ "initial unifyState:" <+> prettyTCM initialState
    (result,log) <- runUnifyLogT $ unify initialState rightToLeftStrategy
    reportSDoc "tc.lhs.unify" 20 $ "unification done"
    forM result $ \ UnifyState
s -> do -- Unifies case
        let output :: UnifyOutput
output = [UnifyOutput] -> UnifyOutput
forall a. Monoid a => [a] -> a
mconcat [UnifyOutput
output | (UnificationStep UnifyState
_ UnifyStep
_ UnifyOutput
output,UnifyState
_) <- UnifyLog
log ]
        let ps :: [NamedArg (Pattern' DBPatVar)]
ps = Substitution' (SubstArg [NamedArg (Pattern' DBPatVar)])
-> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (UnifyOutput -> Substitution' (Pattern' DBPatVar)
unifyProof UnifyOutput
output) ([NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)])
-> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
forall a b. (a -> b) -> a -> b
$ Telescope -> [NamedArg (Pattern' DBPatVar)]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs (UnifyState -> Telescope
eqTel UnifyState
initialState)
        let getTauInv :: TCM (Either NoLeftInv (Substitution, Substitution))
getTauInv = do
              strict     <- Lens' TCEnv Bool -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eSplitOnStrict
              case linv of
                Just NoLeftInv
reason -> Either NoLeftInv (Substitution, Substitution)
-> TCM (Either NoLeftInv (Substitution, Substitution))
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NoLeftInv -> Either NoLeftInv (Substitution, Substitution)
forall a b. a -> Either a b
Left NoLeftInv
reason)
                Maybe NoLeftInv
Nothing
                  | Bool
strict    -> Either NoLeftInv (Substitution, Substitution)
-> TCM (Either NoLeftInv (Substitution, Substitution))
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NoLeftInv -> Either NoLeftInv (Substitution, Substitution)
forall a b. a -> Either a b
Left NoLeftInv
SplitOnStrict)
                  | Bool
otherwise -> UnifyState
-> UnifyLog -> TCM (Either NoLeftInv (Substitution, Substitution))
buildLeftInverse UnifyState
initialState UnifyLog
log
        String -> Key -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Key
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [NamedArg (Pattern' DBPatVar)] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [NamedArg (Pattern' DBPatVar)]
ps
        (Telescope, Substitution' (Pattern' DBPatVar),
 [NamedArg (Pattern' DBPatVar)],
 TCM (Either NoLeftInv (Substitution, Substitution)))
-> TCMT
     IO
     (Telescope, Substitution' (Pattern' DBPatVar),
      [NamedArg (Pattern' DBPatVar)],
      TCM (Either NoLeftInv (Substitution, Substitution)))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyState -> Telescope
varTel UnifyState
s, UnifyOutput -> Substitution' (Pattern' DBPatVar)
unifySubst UnifyOutput
output, [NamedArg (Pattern' DBPatVar)]
ps, TCM (Either NoLeftInv (Substitution, Substitution))
getTauInv)


type UnifyStrategy = UnifyState -> ListT TCM UnifyStep

--UNUSED Liang-Ting Chen 2019-07-16
--leftToRightStrategy :: UnifyStrategy
--leftToRightStrategy s =
--    msum (for [0..n-1] $ \k -> completeStrategyAt k s)
--  where n = size $ eqTel s

rightToLeftStrategy :: UnifyStrategy
rightToLeftStrategy :: UnifyStrategy
rightToLeftStrategy UnifyState
s =
    [ListT (TCMT IO) UnifyStep] -> ListT (TCMT IO) UnifyStep
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum (Key -> [Key]
forall a. Integral a => a -> [a]
downFrom Key
n [Key]
-> (Key -> ListT (TCMT IO) UnifyStep)
-> [ListT (TCMT IO) UnifyStep]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Key
k -> Key -> UnifyStrategy
completeStrategyAt Key
k UnifyState
s)
  where n :: Key
n = Telescope -> Key
forall a. Sized a => a -> Key
size (Telescope -> Key) -> Telescope -> Key
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s

completeStrategyAt :: Int -> UnifyStrategy
completeStrategyAt :: Key -> UnifyStrategy
completeStrategyAt Key
k UnifyState
s = [ListT (TCMT IO) UnifyStep] -> ListT (TCMT IO) UnifyStep
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([ListT (TCMT IO) UnifyStep] -> ListT (TCMT IO) UnifyStep)
-> [ListT (TCMT IO) UnifyStep] -> ListT (TCMT IO) UnifyStep
forall a b. (a -> b) -> a -> b
$ ((Key -> UnifyStrategy) -> ListT (TCMT IO) UnifyStep)
-> [Key -> UnifyStrategy] -> [ListT (TCMT IO) UnifyStep]
forall a b. (a -> b) -> [a] -> [b]
map' (\Key -> UnifyStrategy
strat -> Key -> UnifyStrategy
strat Key
k UnifyState
s) ([Key -> UnifyStrategy] -> [ListT (TCMT IO) UnifyStep])
-> [Key -> UnifyStrategy] -> [ListT (TCMT IO) UnifyStep]
forall a b. (a -> b) -> a -> b
$
-- ASR (2021-02-07). The below eta-expansions are required by GHC >=
-- 9.0.1 (see Issue #4955).
    [ (\Key
n -> Key -> UnifyStrategy
skipIrrelevantStrategy Key
n)
    , (\Key
n -> Key -> UnifyStrategy
basicUnifyStrategy Key
n)
    , (\Key
n -> Key -> UnifyStrategy
literalStrategy Key
n)
    , (\Key
n -> Key -> UnifyStrategy
dataStrategy Key
n)
    , (\Key
n -> Key -> UnifyStrategy
etaExpandVarStrategy  Key
n)
    , (\Key
n -> Key -> UnifyStrategy
etaExpandEquationStrategy Key
n)
    , (\Key
n -> Key -> UnifyStrategy
injectivePragmaStrategy Key
n)
    , (\Key
n -> Key -> UnifyStrategy
checkEqualityStrategy Key
n)
    ]

-- | @isHom n x@ returns x lowered by n if the variables 0..n-1 don't occur in x.
--
-- This is naturally sensitive to normalization.
isHom :: (Free a, Subst a) => Int -> a -> Maybe a
isHom :: forall a. (Free a, Subst a) => Key -> a -> Maybe a
isHom Key
n a
x = do
  Bool -> Maybe ()
forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ (Key -> Bool) -> a -> Bool
forall t. Free t => (Key -> Bool) -> t -> Bool
allFreeVar (Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
>= Key
n) a
x
  a -> Maybe a
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ Key -> a -> a
forall a. Subst a => Key -> a -> a
raise (-Key
n) a
x

findFlexible :: Int -> FlexibleVars -> Maybe (FlexibleVar Nat)
findFlexible :: Key -> FlexibleVars -> Maybe (FlexibleVar Key)
findFlexible Key
i FlexibleVars
flex = (FlexibleVar Key -> Bool)
-> FlexibleVars -> Maybe (FlexibleVar Key)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((Key
i Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
==) (Key -> Bool)
-> (FlexibleVar Key -> Key) -> FlexibleVar Key -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FlexibleVar Key -> Key
forall a. FlexibleVar a -> a
flexVar) FlexibleVars
flex

basicUnifyStrategy :: Int -> UnifyStrategy
basicUnifyStrategy :: Key -> UnifyStrategy
basicUnifyStrategy Key
k UnifyState
s = do
  String -> Key -> TCMT IO Doc -> ListT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Key
40 (TCMT IO Doc -> ListT (TCMT IO) ())
-> TCMT IO Doc -> ListT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"trying basicUnifyStrategy"
  Equal dom@(unDom -> a) u v <- Equality -> ListT (TCMT IO) Equality
forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqUnLevel (Key -> UnifyState -> Equality
getEquality Key
k UnifyState
s)
    -- Andreas, 2019-02-23: reduce equality for the sake of isHom?
  ha <- fromMaybeMP $ isHom n a
  (mi, mj) <- addContext (varTel s) $ (,) <$> isEtaVar u ha <*> isEtaVar v ha
  reportSDoc "tc.lhs.unify" 30 $ "isEtaVar results: " <+> text (show [mi,mj])
  case (mi, mj) of
    (Just Key
i, Just Key
j)
     | Key
i Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
j -> ListT (TCMT IO) UnifyStep
forall a. ListT (TCMT IO) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero -- Taken care of by checkEqualityStrategy
    (Just Key
i, Just Key
j)
     | Just FlexibleVar Key
fi <- Key -> FlexibleVars -> Maybe (FlexibleVar Key)
findFlexible Key
i FlexibleVars
flex
     , Just FlexibleVar Key
fj <- Key -> FlexibleVars -> Maybe (FlexibleVar Key)
findFlexible Key
j FlexibleVars
flex -> do
       let choice :: FlexChoice
choice = FlexibleVar Key -> FlexibleVar Key -> FlexChoice
forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex FlexibleVar Key
fi FlexibleVar Key
fj
           firstTryLeft :: ListT (TCMT IO) UnifyStep
firstTryLeft  = [ListT (TCMT IO) UnifyStep] -> ListT (TCMT IO) UnifyStep
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ UnifyStep -> ListT (TCMT IO) UnifyStep
forall a. a -> ListT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Key
-> Dom Type -> FlexibleVar Key -> Term -> Either () () -> UnifyStep
Solution Key
k Dom Type
dom{unDom = ha} FlexibleVar Key
fi Term
v Either () ()
forall {b}. Either () b
left)
                                , UnifyStep -> ListT (TCMT IO) UnifyStep
forall a. a -> ListT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Key
-> Dom Type -> FlexibleVar Key -> Term -> Either () () -> UnifyStep
Solution Key
k Dom Type
dom{unDom = ha} FlexibleVar Key
fj Term
u Either () ()
forall {a}. Either a ()
right)]
           firstTryRight :: ListT (TCMT IO) UnifyStep
firstTryRight = [ListT (TCMT IO) UnifyStep] -> ListT (TCMT IO) UnifyStep
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ UnifyStep -> ListT (TCMT IO) UnifyStep
forall a. a -> ListT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Key
-> Dom Type -> FlexibleVar Key -> Term -> Either () () -> UnifyStep
Solution Key
k Dom Type
dom{unDom = ha} FlexibleVar Key
fj Term
u Either () ()
forall {a}. Either a ()
right)
                                , UnifyStep -> ListT (TCMT IO) UnifyStep
forall a. a -> ListT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Key
-> Dom Type -> FlexibleVar Key -> Term -> Either () () -> UnifyStep
Solution Key
k Dom Type
dom{unDom = ha} FlexibleVar Key
fi Term
v Either () ()
forall {b}. Either () b
left)]
       String -> Key -> TCMT IO Doc -> ListT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Key
40 (TCMT IO Doc -> ListT (TCMT IO) ())
-> TCMT IO Doc -> ListT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"fi = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (FlexibleVar Key -> String
forall a. Show a => a -> String
show FlexibleVar Key
fi)
       String -> Key -> TCMT IO Doc -> ListT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Key
40 (TCMT IO Doc -> ListT (TCMT IO) ())
-> TCMT IO Doc -> ListT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"fj = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (FlexibleVar Key -> String
forall a. Show a => a -> String
show FlexibleVar Key
fj)
       String -> Key -> TCMT IO Doc -> ListT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Key
40 (TCMT IO Doc -> ListT (TCMT IO) ())
-> TCMT IO Doc -> ListT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"chooseFlex: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (FlexChoice -> String
forall a. Show a => a -> String
show FlexChoice
choice)
       case FlexChoice
choice of
         FlexChoice
ChooseLeft   -> ListT (TCMT IO) UnifyStep
firstTryLeft
         FlexChoice
ChooseRight  -> ListT (TCMT IO) UnifyStep
firstTryRight
         FlexChoice
ExpandBoth   -> ListT (TCMT IO) UnifyStep
forall a. ListT (TCMT IO) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero -- This should be taken care of by etaExpandEquationStrategy
         FlexChoice
ChooseEither -> ListT (TCMT IO) UnifyStep
firstTryRight
    (Just Key
i, Maybe Key
_)
     | Just FlexibleVar Key
fi <- Key -> FlexibleVars -> Maybe (FlexibleVar Key)
findFlexible Key
i FlexibleVars
flex -> UnifyStep -> ListT (TCMT IO) UnifyStep
forall a. a -> ListT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT (TCMT IO) UnifyStep)
-> UnifyStep -> ListT (TCMT IO) UnifyStep
forall a b. (a -> b) -> a -> b
$ Key
-> Dom Type -> FlexibleVar Key -> Term -> Either () () -> UnifyStep
Solution Key
k Dom Type
dom{unDom = ha} FlexibleVar Key
fi Term
v Either () ()
forall {b}. Either () b
left
    (Maybe Key
_, Just Key
j)
     | Just FlexibleVar Key
fj <- Key -> FlexibleVars -> Maybe (FlexibleVar Key)
findFlexible Key
j FlexibleVars
flex -> UnifyStep -> ListT (TCMT IO) UnifyStep
forall a. a -> ListT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT (TCMT IO) UnifyStep)
-> UnifyStep -> ListT (TCMT IO) UnifyStep
forall a b. (a -> b) -> a -> b
$ Key
-> Dom Type -> FlexibleVar Key -> Term -> Either () () -> UnifyStep
Solution Key
k Dom Type
dom{unDom = ha} FlexibleVar Key
fj Term
u Either () ()
forall {a}. Either a ()
right
    (Maybe Key, Maybe Key)
_ -> ListT (TCMT IO) UnifyStep
forall a. ListT (TCMT IO) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  where
    flex :: FlexibleVars
flex = UnifyState -> FlexibleVars
flexVars UnifyState
s
    n :: Key
n = UnifyState -> Key
eqCount UnifyState
s
    left :: Either () b
left = () -> Either () b
forall a b. a -> Either a b
Left (); right :: Either a ()
right = () -> Either a ()
forall a b. b -> Either a b
Right ()

dataStrategy :: Int -> UnifyStrategy
dataStrategy :: Key -> UnifyStrategy
dataStrategy Key
k UnifyState
s = do
  String -> Key -> TCMT IO Doc -> ListT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Key
40 (TCMT IO Doc -> ListT (TCMT IO) ())
-> TCMT IO Doc -> ListT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"trying dataStrategy"
  Equal (unDom -> a) u v <- Equality -> ListT (TCMT IO) Equality
forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqConstructorForm (Equality -> ListT (TCMT IO) Equality)
-> ListT (TCMT IO) Equality -> ListT (TCMT IO) Equality
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Equality -> ListT (TCMT IO) Equality
forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqUnLevel (Equality -> ListT (TCMT IO) Equality)
-> ListT (TCMT IO) Equality -> ListT (TCMT IO) Equality
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Key -> UnifyState -> ListT (TCMT IO) Equality
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Key -> UnifyState -> m Equality
getReducedEqualityUnraised Key
k UnifyState
s
  sortOk <- reduce (getSort a) <&> \case
    Type{} -> Bool
True
    Inf{}  -> Bool
True
    SSet{} -> Bool
True
    Sort
_      -> Bool
False
  case unEl a of
    Def QName
d Elims
es | Bool
sortOk -> do
      npars <- ListT (TCMT IO) (Maybe Key) -> ListT (TCMT IO) Key
forall (m :: * -> *) a. MonadPlus m => m (Maybe a) -> m a
catMaybesMP (ListT (TCMT IO) (Maybe Key) -> ListT (TCMT IO) Key)
-> ListT (TCMT IO) (Maybe Key) -> ListT (TCMT IO) Key
forall a b. (a -> b) -> a -> b
$ QName -> ListT (TCMT IO) (Maybe Key)
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe Key)
getNumberOfParameters QName
d
      let (!pars, !ixs) = splitAt' npars $ mustAllApplyElims es
      reportSDoc "tc.lhs.unify" 40 $ addContext (varTel s `abstract` eqTel s) $
        "Found equation at datatype " <+> prettyTCM d
         <+> " with parameters " <+> prettyTCM (raise (size (eqTel s) - k) pars)
      case (u, v) of
        (Con ConHead
c ConInfo
_ Elims
_   , Con ConHead
c' ConInfo
_ Elims
_  ) | ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
c' -> UnifyStep -> ListT (TCMT IO) UnifyStep
forall a. a -> ListT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT (TCMT IO) UnifyStep)
-> UnifyStep -> ListT (TCMT IO) UnifyStep
forall a b. (a -> b) -> a -> b
$ Key
-> Type
-> QName
-> [Arg Term]
-> [Arg Term]
-> ConHead
-> UnifyStep
Injectivity Key
k Type
a QName
d [Arg Term]
pars [Arg Term]
ixs ConHead
c
        (Con ConHead
c ConInfo
_ Elims
_   , Con ConHead
c' ConInfo
_ Elims
_  ) -> UnifyStep -> ListT (TCMT IO) UnifyStep
forall a. a -> ListT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT (TCMT IO) UnifyStep)
-> UnifyStep -> ListT (TCMT IO) UnifyStep
forall a b. (a -> b) -> a -> b
$ Key -> Type -> QName -> [Arg Term] -> Term -> Term -> UnifyStep
Conflict Key
k Type
a QName
d [Arg Term]
pars Term
u Term
v
        (Term, Term)
_ -> ListT (TCMT IO) UnifyStep
forall a. ListT (TCMT IO) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    Term
_ -> ListT (TCMT IO) UnifyStep
forall a. ListT (TCMT IO) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  where
    ifOccursStronglyRigid :: Key -> a -> m b -> m b
ifOccursStronglyRigid Key
i a
u m b
ret = do
        -- Call forceNotFree to reduce u as far as possible
        -- around any occurrences of i
        (_ , u) <- ReduceM (IntMap IsFree, a) -> m (IntMap IsFree, a)
forall a. ReduceM a -> m a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM (IntMap IsFree, a) -> m (IntMap IsFree, a))
-> ReduceM (IntMap IsFree, a) -> m (IntMap IsFree, a)
forall a b. (a -> b) -> a -> b
$ VarSet -> a -> ReduceM (IntMap IsFree, a)
forall a.
(ForceNotFree a, Reduce a) =>
VarSet -> a -> ReduceM (IntMap IsFree, a)
forceNotFree (Key -> VarSet
forall el coll. Singleton el coll => el -> coll
singleton Key
i) a
u
        case flexRigOccurrenceIn i u of
          Just FlexRig
StronglyRigid -> m b
ret
          Maybe FlexRig
_ -> m b
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

checkEqualityStrategy :: Int -> UnifyStrategy
checkEqualityStrategy :: Key -> UnifyStrategy
checkEqualityStrategy Key
k UnifyState
s = do
  String -> Key -> TCMT IO Doc -> ListT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Key
40 (TCMT IO Doc -> ListT (TCMT IO) ())
-> TCMT IO Doc -> ListT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"trying checkEqualityStrategy"
  let Equal (Dom Type -> Type
forall t e. Dom' t e -> e
unDom -> Type
a) Term
u Term
v = Key -> UnifyState -> Equality
getEquality Key
k UnifyState
s
      n :: Key
n = UnifyState -> Key
eqCount UnifyState
s
  ha <- Maybe Type -> ListT (TCMT IO) Type
forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP (Maybe Type -> ListT (TCMT IO) Type)
-> Maybe Type -> ListT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ Key -> Type -> Maybe Type
forall a. (Free a, Subst a) => Key -> a -> Maybe a
isHom Key
n Type
a
  return $ Deletion k ha u v

literalStrategy :: Int -> UnifyStrategy
literalStrategy :: Key -> UnifyStrategy
literalStrategy Key
k UnifyState
s = do
  String -> Key -> TCMT IO Doc -> ListT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Key
40 (TCMT IO Doc -> ListT (TCMT IO) ())
-> TCMT IO Doc -> ListT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"trying literalStrategy"
  let n :: Key
n = UnifyState -> Key
eqCount UnifyState
s
  Equal (unDom -> a) u v <- Equality -> ListT (TCMT IO) Equality
forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqUnLevel (Equality -> ListT (TCMT IO) Equality)
-> Equality -> ListT (TCMT IO) Equality
forall a b. (a -> b) -> a -> b
$ Key -> UnifyState -> Equality
getEquality Key
k UnifyState
s
  ha <- fromMaybeMP $ isHom n a
  (u, v) <- addContext (varTel s) $ reduce (u, v)
  case (u , v) of
    (Lit Literal
l1 , Lit Literal
l2)
     | Literal
l1 Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l2  -> UnifyStep -> ListT (TCMT IO) UnifyStep
forall a. a -> ListT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT (TCMT IO) UnifyStep)
-> UnifyStep -> ListT (TCMT IO) UnifyStep
forall a b. (a -> b) -> a -> b
$ Key -> Type -> Term -> Term -> UnifyStep
Deletion Key
k Type
ha Term
u Term
v
     | Bool
otherwise -> UnifyStep -> ListT (TCMT IO) UnifyStep
forall a. a -> ListT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT (TCMT IO) UnifyStep)
-> UnifyStep -> ListT (TCMT IO) UnifyStep
forall a b. (a -> b) -> a -> b
$ Key -> Type -> Literal -> Literal -> UnifyStep
LitConflict Key
k Type
ha Literal
l1 Literal
l2
    (Term, Term)
_ -> ListT (TCMT IO) UnifyStep
forall a. ListT (TCMT IO) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

etaExpandVarStrategy :: Int -> UnifyStrategy
etaExpandVarStrategy :: Key -> UnifyStrategy
etaExpandVarStrategy Key
k UnifyState
s = do
  String -> Key -> TCMT IO Doc -> ListT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Key
40 (TCMT IO Doc -> ListT (TCMT IO) ())
-> TCMT IO Doc -> ListT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"trying etaExpandVarStrategy"
  Equal (unDom -> a) u v <- Equality -> ListT (TCMT IO) Equality
forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqUnLevel (Equality -> ListT (TCMT IO) Equality)
-> ListT (TCMT IO) Equality -> ListT (TCMT IO) Equality
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Key -> UnifyState -> ListT (TCMT IO) Equality
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Key -> UnifyState -> m Equality
getReducedEquality Key
k UnifyState
s
  shouldEtaExpand u v a s `mplus` shouldEtaExpand v u a s
  where
    -- TODO: use IsEtaVar to check if the term is a variable
    shouldEtaExpand :: Term -> Term -> Type -> UnifyStrategy
    shouldEtaExpand :: Term -> Term -> Type -> UnifyStrategy
shouldEtaExpand (Var Key
i Elims
es) Term
v Type
a UnifyState
s = do
      fi       <- Maybe (FlexibleVar Key) -> ListT (TCMT IO) (FlexibleVar Key)
forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP (Maybe (FlexibleVar Key) -> ListT (TCMT IO) (FlexibleVar Key))
-> Maybe (FlexibleVar Key) -> ListT (TCMT IO) (FlexibleVar Key)
forall a b. (a -> b) -> a -> b
$ Key -> FlexibleVars -> Maybe (FlexibleVar Key)
findFlexible Key
i (UnifyState -> FlexibleVars
flexVars UnifyState
s)
      reportSDoc "tc.lhs.unify" 50 $
        "Found flexible variable " <+> text (show i)
      -- Issue 2888: Do this if there are only projections or if it's a singleton
      -- record or if it's unified against a record constructor term. Basically
      -- we need to avoid EtaExpandEquation if EtaExpandVar is possible, or the
      -- forcing translation is unhappy.
      let k  = UnifyState -> Key
varCount UnifyState
s Key -> Key -> Key
forall a. Num a => a -> a -> a
- Key
1 Key -> Key -> Key
forall a. Num a => a -> a -> a
- Key
i -- position of var i in telescope
          b0 = Dom Type -> Type
forall t e. Dom' t e -> e
unDom (Dom Type -> Type) -> Dom Type -> Type
forall a b. (a -> b) -> a -> b
$ Key -> UnifyState -> Dom Type
getVarTypeUnraised Key
k UnifyState
s
      b         <- addContext (telFromList $ take' k $ telToList $ varTel s) $ reduce b0
      (d, pars) <- catMaybesMP $ isEtaRecordType b
      ps        <- fromMaybeMP $ allProjElims es
      guard =<< orM
        [ pure $ not $ null ps
        , isRecCon v  -- is the other term a record constructor?
        , (Right True ==) <$> runBlocked (isSingletonRecord d pars)
        ]
      reportSDoc "tc.lhs.unify" 50 $
        "with projections " <+> prettyTCM (map' snd ps)
      reportSDoc "tc.lhs.unify" 50 $
        "at record type " <+> prettyTCM d
      return $ EtaExpandVar fi d pars
    shouldEtaExpand Term
_ Term
_ Type
_ UnifyState
_ = ListT (TCMT IO) UnifyStep
forall a. ListT (TCMT IO) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

    isRecCon :: Term -> f Bool
isRecCon (Con ConHead
c ConInfo
_ Elims
_) = Maybe (QName, RecordData) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (QName, RecordData) -> Bool)
-> f (Maybe (QName, RecordData)) -> f Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> f (Maybe (QName, RecordData))
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe (QName, RecordData))
isRecordConstructor (ConHead -> QName
conName ConHead
c)
    isRecCon Term
_           = Bool -> f Bool
forall a. a -> f a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

etaExpandEquationStrategy :: Int -> UnifyStrategy
etaExpandEquationStrategy :: Key -> UnifyStrategy
etaExpandEquationStrategy Key
k UnifyState
s = do
  String -> Key -> TCMT IO Doc -> ListT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Key
40 (TCMT IO Doc -> ListT (TCMT IO) ())
-> TCMT IO Doc -> ListT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"trying etaExpandEquationStrategy"
  -- Andreas, 2019-02-23, re #3578, is the following reduce redundant?
  Equal (unDom -> a) u v <- Key -> UnifyState -> ListT (TCMT IO) Equality
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Key -> UnifyState -> m Equality
getReducedEqualityUnraised Key
k UnifyState
s
  (d, pars) <- catMaybesMP $ addContext tel $ isEtaRecordType a
  guard =<< orM
    [ (Right True ==) <$> runBlocked (isSingletonRecord d pars)
    , shouldProject u
    , shouldProject v
    ]
  return $ EtaExpandEquation k d pars
  where
    shouldProject :: PureTCM m => Term -> m Bool
    shouldProject :: forall (m :: * -> *). PureTCM m => Term -> m Bool
shouldProject = \case
      Def QName
f Elims
es   -> QName -> m Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
usesCopatterns QName
f
      Con ConHead
c ConInfo
_ Elims
_  -> Maybe (QName, RecordData) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (QName, RecordData) -> Bool)
-> m (Maybe (QName, RecordData)) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe (QName, RecordData))
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe (QName, RecordData))
isRecordConstructor (ConHead -> QName
conName ConHead
c)

      Var Key
_ Elims
_    -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      Lam ArgInfo
_ Abs Term
_    -> m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      Lit Literal
_      -> m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      Pi Dom Type
_ Abs Type
_     -> m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      Sort Sort
_     -> m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      Level Level
_    -> m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      MetaV MetaId
_ Elims
_  -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      DontCare Term
_ -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      Dummy DummyTermKind
s Elims
_  -> String -> m Bool
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ (DummyTermKind -> String
forall a. Show a => a -> String
show DummyTermKind
s)

    tel :: Telescope
tel = UnifyState -> Telescope
varTel UnifyState
s Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` ListTel -> Telescope
telFromList (Key -> ListTel -> ListTel
forall a. Key -> [a] -> [a]
take' Key
k (ListTel -> ListTel) -> ListTel -> ListTel
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList (Telescope -> ListTel) -> Telescope -> ListTel
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s)

injectivePragmaStrategy :: Int -> UnifyStrategy
injectivePragmaStrategy :: Key -> UnifyStrategy
injectivePragmaStrategy Key
k UnifyState
s = do
  String -> Key -> TCMT IO Doc -> ListT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Key
40 (TCMT IO Doc -> ListT (TCMT IO) ())
-> TCMT IO Doc -> ListT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"trying injectivePragmaStrategy"
  eq <- Equality -> ListT (TCMT IO) Equality
forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqUnLevel (Equality -> ListT (TCMT IO) Equality)
-> ListT (TCMT IO) Equality -> ListT (TCMT IO) Equality
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Key -> UnifyState -> ListT (TCMT IO) Equality
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Key -> UnifyState -> m Equality
getReducedEquality Key
k UnifyState
s
  case eq of
    Equal Dom Type
a u :: Term
u@(Def QName
d Elims
es) v :: Term
v@(Def QName
d' Elims
es') | QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
d' -> do
      -- d must have an injective pragma
      def <- QName -> ListT (TCMT IO) Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
d
      guard $ defInjective def
      let us = Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
          vs = Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es'
      return $ TypeConInjectivity k d us vs
    Equality
_ -> ListT (TCMT IO) UnifyStep
forall a. ListT (TCMT IO) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

skipIrrelevantStrategy :: Int -> UnifyStrategy
skipIrrelevantStrategy :: Key -> UnifyStrategy
skipIrrelevantStrategy Key
k UnifyState
s = do
  String -> Key -> TCMT IO Doc -> ListT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Key
40 (TCMT IO Doc -> ListT (TCMT IO) ())
-> TCMT IO Doc -> ListT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"trying skipIrrelevantStrategy"
  let Equal Dom Type
a Term
_ Term
_ = Key -> UnifyState -> Equality
getEquality Key
k UnifyState
s                                 -- reduce not necessary
  Telescope -> ListT (TCMT IO) () -> ListT (TCMT IO) ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` UnifyState -> Telescope
eqTel UnifyState
s) (ListT (TCMT IO) () -> ListT (TCMT IO) ())
-> ListT (TCMT IO) () -> ListT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
    Bool -> ListT (TCMT IO) ()
forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
guard (Bool -> ListT (TCMT IO) ())
-> (Either Blocker Bool -> Bool)
-> Either Blocker Bool
-> ListT (TCMT IO) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either Blocker Bool -> Either Blocker Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Either Blocker Bool
forall a b. b -> Either a b
Right Bool
True) (Either Blocker Bool -> ListT (TCMT IO) ())
-> ListT (TCMT IO) (Either Blocker Bool) -> ListT (TCMT IO) ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< BlockT (ListT (TCMT IO)) Bool
-> ListT (TCMT IO) (Either Blocker Bool)
forall (m :: * -> *) a. BlockT m a -> m (Either Blocker a)
runBlocked (Dom Type -> BlockT (ListT (TCMT IO)) Bool
forall a (m :: * -> *).
(LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
a -> m Bool
isPropM Dom Type
a)  -- reduction takes place here
  -- TODO: do something in case the above is blocked (i.e. `Left b`)
  UnifyStep -> ListT (TCMT IO) UnifyStep
forall a. a -> ListT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT (TCMT IO) UnifyStep)
-> UnifyStep -> ListT (TCMT IO) UnifyStep
forall a b. (a -> b) -> a -> b
$ Key -> UnifyStep
SkipIrrelevantEquation Key
k


----------------------------------------------------
-- Actually doing the unification
----------------------------------------------------

unifyStep :: UnifyState -> UnifyStep -> UnifyStepT TCM (UnificationResult' UnifyState)
unifyStep :: UnifyState
-> UnifyStep
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
unifyStep UnifyState
s Deletion{ deleteAt :: UnifyStep -> Key
deleteAt = Key
k , deleteType :: UnifyStep -> Type
deleteType = Type
a , deleteLeft :: UnifyStep -> Term
deleteLeft = Term
u , deleteRight :: UnifyStep -> Term
deleteRight = Term
v } = do
  -- Check definitional equality of u and v
  isReflexive <- Telescope
-> WriterT UnifyOutput (TCMT IO) (Either Blocker Bool)
-> WriterT UnifyOutput (TCMT IO) (Either Blocker Bool)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) (WriterT UnifyOutput (TCMT IO) (Either Blocker Bool)
 -> WriterT UnifyOutput (TCMT IO) (Either Blocker Bool))
-> WriterT UnifyOutput (TCMT IO) (Either Blocker Bool)
-> WriterT UnifyOutput (TCMT IO) (Either Blocker Bool)
forall a b. (a -> b) -> a -> b
$ TCMT IO (Either Blocker Bool)
-> WriterT UnifyOutput (TCMT IO) (Either Blocker Bool)
forall (m :: * -> *) a. Monad m => m a -> WriterT UnifyOutput m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO (Either Blocker Bool)
 -> WriterT UnifyOutput (TCMT IO) (Either Blocker Bool))
-> TCMT IO (Either Blocker Bool)
-> WriterT UnifyOutput (TCMT IO) (Either Blocker Bool)
forall a b. (a -> b) -> a -> b
$ Type -> Term -> Term -> TCMT IO (Either Blocker Bool)
pureBlockOrEqualTerm Type
a Term
u Term
v
  splitOnStrict <- viewTC eSplitOnStrict
  case isReflexive of
    Left Blocker
block   -> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ Blocker -> UnificationResult' UnifyState
forall a. Blocker -> UnificationResult' a
UnifyBlocked Blocker
block
    Right Bool
False  -> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []
    Right Bool
True | Bool -> Bool
not Bool
splitOnStrict -> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [Telescope -> Type -> Term -> UnificationFailure
UnifyReflexiveEq (UnifyState -> Telescope
varTel UnifyState
s) Type
a Term
u]
    Right Bool
True   -> do
      let (UnifyState
s', Substitution' (Pattern' DBPatVar)
sigma) = Key
-> Term
-> UnifyState
-> (UnifyState, Substitution' (Pattern' DBPatVar))
solveEq Key
k Term
u UnifyState
s
      Substitution' (Pattern' DBPatVar)
-> WriterT UnifyOutput (TCMT IO) ()
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
Substitution' (Pattern' DBPatVar) -> m ()
tellUnifyProof Substitution' (Pattern' DBPatVar)
sigma
      RetryNormalised -> UnifyState -> UnificationResult' UnifyState
forall a. RetryNormalised -> a -> UnificationResult' a
Unifies RetryNormalised
RetryNormalised (UnifyState -> UnificationResult' UnifyState)
-> WriterT UnifyOutput (TCMT IO) UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Telescope -> WriterT UnifyOutput (TCMT IO) Telescope)
-> UnifyState -> WriterT UnifyOutput (TCMT IO) UnifyState
Lens' UnifyState Telescope
lensEqTel Telescope -> WriterT UnifyOutput (TCMT IO) Telescope
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce UnifyState
s'

unifyStep UnifyState
s step :: UnifyStep
step@Solution{} = RetryNormalised
-> UnifyState
-> UnifyStep
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
solutionStep RetryNormalised
RetryNormalised UnifyState
s UnifyStep
step

unifyStep UnifyState
s (Injectivity Key
k Type
a QName
d [Arg Term]
pars [Arg Term]
ixs ConHead
c) = do
  WriterT UnifyOutput (TCMT IO) Bool
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> WriterT UnifyOutput (TCMT IO) Bool
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m Bool
consOfHIT (QName -> WriterT UnifyOutput (TCMT IO) Bool)
-> QName -> WriterT UnifyOutput (TCMT IO) Bool
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c) (UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []) (UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
 -> UnifyStepT (TCMT IO) (UnificationResult' UnifyState))
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ do

  -- Split equation telescope into parts before and after current equation
  let (ListTel
eqListTel1, Dom (ArgName, Type)
_ : ListTel
eqListTel2) = Key -> ListTel -> (ListTel, ListTel)
forall a. Key -> [a] -> ([a], [a])
splitAt' Key
k (ListTel -> (ListTel, ListTel)) -> ListTel -> (ListTel, ListTel)
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList (Telescope -> ListTel) -> Telescope -> ListTel
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
      (Telescope
eqTel1, Telescope
eqTel2) = (ListTel -> Telescope
telFromList ListTel
eqListTel1, ListTel -> Telescope
telFromList ListTel
eqListTel2)

  -- Get constructor telescope and target indices
  cdef  <- ConHead -> WriterT UnifyOutput (TCMT IO) Definition
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
ConHead -> m Definition
getConInfo ConHead
c
  let ctype  = Definition -> Type
defType Definition
cdef Type -> [Arg Term] -> Type
`piApply` [Arg Term]
pars
  addContext (varTel s `abstract` eqTel1) $ reportSDoc "tc.lhs.unify" 40 $
    "Constructor type: " <+> prettyTCM ctype
  TelV ctel ctarget <- addContext (varTel s `abstract` eqTel1) $ telView ctype
  let cixs = case Type -> Term
forall t a. Type'' t a -> a
unEl Type
ctarget of
               Def QName
d' Elims
es | QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
d' ->
                 let args :: [Arg Term]
args = Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
                 in  Key -> [Arg Term] -> [Arg Term]
forall a. Key -> [a] -> [a]
drop ([Arg Term] -> Key
forall a. [a] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [Arg Term]
pars) [Arg Term]
args
               Term
_ -> [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__

  -- Get index telescope of the datatype
  dtype    <- (`piApply` pars) . defType <$> getConstInfo d
  addContext (varTel s `abstract` eqTel1) $ reportSDoc "tc.lhs.unify" 40 $
    "Datatype type: " <+> prettyTCM dtype

  -- This is where the magic of higher-dimensional unification happens
  -- We need to generalize the indices `ixs` to the target indices of the
  -- constructor `cixs`. This is done by calling the unification algorithm
  -- recursively (this doesn't get stuck in a loop because a type should
  -- never be indexed over itself). Note the similarity with the
  -- computeNeighbourhood function in Agda.TypeChecking.Coverage.
  let hduTel = Telescope
eqTel1 Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
ctel
      notforced = Key -> IsForced -> [IsForced]
forall a. Key -> a -> [a]
replicate (Telescope -> Key
forall a. Sized a => a -> Key
size Telescope
hduTel) IsForced
NotForced

  -- The left inverse computed here is not actually used when computing
  -- a left inverse for the overall match, so as a slight optimisation
  -- we just don't bother computing it. __IMPOSSIBLE__ because that
  -- field in the result is never evaluated.
  res <- lift $ addContext (varTel s) $ unifyIndices' (Just __IMPOSSIBLE__)
           hduTel
           (allFlexVars notforced hduTel)
           (raise (size ctel) dtype)
           (raise (size ctel) ixs)
           cixs
  case res of
    -- Higher-dimensional unification can never end in a conflict,
    -- because `cong c1 ...` and `cong c2 ...` don't even have the
    -- same type for distinct constructors c1 and c2.
    NoUnify NegativeUnification
_ -> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Higher-dimensional unification is blocked: propagate
    UnifyBlocked Blocker
block -> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ Blocker -> UnificationResult' UnifyState
forall a. Blocker -> UnificationResult' a
UnifyBlocked Blocker
block

    UnifyStuck [UnificationFailure]
_ -> let n :: Key
n           = UnifyState -> Key
eqCount UnifyState
s
                        Equal (Dom Type -> Type
forall t e. Dom' t e -> e
unDom -> Type
a) Term
u Term
v = Key -> UnifyState -> Equality
getEquality Key
k UnifyState
s
                    in UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [Telescope
-> Type -> Term -> Term -> [Arg Term] -> UnificationFailure
UnifyIndicesNotVars
                         (UnifyState -> Telescope
varTel UnifyState
s Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` UnifyState -> Telescope
eqTel UnifyState
s) Type
a
                         (Key -> Term -> Term
forall a. Subst a => Key -> a -> a
raise Key
n Term
u) (Key -> Term -> Term
forall a. Subst a => Key -> a -> a
raise Key
n Term
v) (Key -> [Arg Term] -> [Arg Term]
forall a. Subst a => Key -> a -> a
raise (Key
nKey -> Key -> Key
forall a. Num a => a -> a -> a
-Key
k) [Arg Term]
ixs)]

    Unifies RetryNormalised
_ (Telescope
eqTel1', Substitution' (Pattern' DBPatVar)
rho0, [NamedArg (Pattern' DBPatVar)]
_, TCM (Either NoLeftInv (Substitution, Substitution))
_) -> do
      -- Split ps0 into parts for eqTel1 and ctel
      let (Substitution' (Pattern' DBPatVar)
rho1, Substitution' (Pattern' DBPatVar)
rho2) = Key
-> Substitution' (Pattern' DBPatVar)
-> (Substitution' (Pattern' DBPatVar),
    Substitution' (Pattern' DBPatVar))
forall a.
Key -> Substitution' a -> (Substitution' a, Substitution' a)
splitS (Telescope -> Key
forall a. Sized a => a -> Key
size Telescope
ctel) Substitution' (Pattern' DBPatVar)
rho0

      -- Compute new equation telescope context and substitution
      let ceq :: Pattern' DBPatVar
ceq     = ConHead
-> ConPatternInfo
-> [NamedArg (Pattern' DBPatVar)]
-> Pattern' DBPatVar
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
noConPatternInfo ([NamedArg (Pattern' DBPatVar)] -> Pattern' DBPatVar)
-> [NamedArg (Pattern' DBPatVar)] -> Pattern' DBPatVar
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg [NamedArg (Pattern' DBPatVar)])
-> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (Pattern' DBPatVar)
Substitution' (SubstArg [NamedArg (Pattern' DBPatVar)])
rho2 ([NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)])
-> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
forall a b. (a -> b) -> a -> b
$ Telescope -> [NamedArg (Pattern' DBPatVar)]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
ctel
          rho3 :: Substitution' (Pattern' DBPatVar)
rho3    = Pattern' DBPatVar
-> Substitution' (Pattern' DBPatVar)
-> Substitution' (Pattern' DBPatVar)
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Pattern' DBPatVar
ceq Substitution' (Pattern' DBPatVar)
rho1
          eqTel2' :: Telescope
eqTel2' = Substitution' (Pattern' DBPatVar) -> Telescope -> Telescope
forall a.
TermSubst a =>
Substitution' (Pattern' DBPatVar) -> a -> a
applyPatSubst Substitution' (Pattern' DBPatVar)
rho3 Telescope
eqTel2
          eqTel' :: Telescope
eqTel'  = Telescope
eqTel1' Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
eqTel2'
          rho :: Substitution' (Pattern' DBPatVar)
rho     = Key
-> Substitution' (Pattern' DBPatVar)
-> Substitution' (Pattern' DBPatVar)
forall a. Key -> Substitution' a -> Substitution' a
liftS (Telescope -> Key
forall a. Sized a => a -> Key
size Telescope
eqTel2) Substitution' (Pattern' DBPatVar)
rho3

      Substitution' (Pattern' DBPatVar)
-> WriterT UnifyOutput (TCMT IO) ()
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
Substitution' (Pattern' DBPatVar) -> m ()
tellUnifyProof Substitution' (Pattern' DBPatVar)
rho

      eqTel' <- Telescope
-> WriterT UnifyOutput (TCMT IO) Telescope
-> WriterT UnifyOutput (TCMT IO) Telescope
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) (WriterT UnifyOutput (TCMT IO) Telescope
 -> WriterT UnifyOutput (TCMT IO) Telescope)
-> WriterT UnifyOutput (TCMT IO) Telescope
-> WriterT UnifyOutput (TCMT IO) Telescope
forall a b. (a -> b) -> a -> b
$ Telescope -> WriterT UnifyOutput (TCMT IO) Telescope
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Telescope
eqTel'

      -- Compute new lhs and rhs by matching the old ones against rho
      (lhs', rhs') <- addContext (varTel s) $ do
        let ps = Substitution' (SubstArg [NamedArg (Pattern' DBPatVar)])
-> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (Pattern' DBPatVar)
Substitution' (SubstArg [NamedArg (Pattern' DBPatVar)])
rho ([NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)])
-> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
forall a b. (a -> b) -> a -> b
$ Telescope -> [NamedArg (Pattern' DBPatVar)]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs (Telescope -> [NamedArg (Pattern' DBPatVar)])
-> Telescope -> [NamedArg (Pattern' DBPatVar)]
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
        (lhsMatch, _) <- Match.matchPatterns ps $ eqLHS s
        (rhsMatch, _) <- Match.matchPatterns ps $ eqRHS s
        case (lhsMatch, rhsMatch) of
          (Match.Yes Simplification
_ IntMap (Arg Term)
lhs', Match.Yes Simplification
_ IntMap (Arg Term)
rhs') -> ([Arg Term], [Arg Term])
-> WriterT UnifyOutput (TCMT IO) ([Arg Term], [Arg Term])
forall a. a -> WriterT UnifyOutput (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return
            ([Arg Term] -> [Arg Term]
forall a. [a] -> [a]
reverse ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Empty -> Key -> IntMap (Arg Term) -> [Arg Term]
forall a. Empty -> Key -> IntMap (Arg a) -> [Arg a]
Match.matchedArgs Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> Key
forall a. Sized a => a -> Key
size Telescope
eqTel') IntMap (Arg Term)
lhs',
             [Arg Term] -> [Arg Term]
forall a. [a] -> [a]
reverse ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Empty -> Key -> IntMap (Arg Term) -> [Arg Term]
forall a. Empty -> Key -> IntMap (Arg a) -> [Arg a]
Match.matchedArgs Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> Key
forall a. Sized a => a -> Key
size Telescope
eqTel') IntMap (Arg Term)
rhs')
          (Match Term, Match Term)
_ -> WriterT UnifyOutput (TCMT IO) ([Arg Term], [Arg Term])
forall a. HasCallStack => a
__IMPOSSIBLE__

      return $ Unifies RetryNormalised s { eqTel = eqTel' , eqLHS = lhs' , eqRHS = rhs' }

unifyStep UnifyState
s Conflict
  { conflictLeft :: UnifyStep -> Term
conflictLeft  = Term
u
  , conflictRight :: UnifyStep -> Term
conflictRight = Term
v
  } =
  case Term
u of
    Con ConHead
h ConInfo
_ Elims
_ -> do
      WriterT UnifyOutput (TCMT IO) Bool
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> WriterT UnifyOutput (TCMT IO) Bool
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m Bool
consOfHIT (QName -> WriterT UnifyOutput (TCMT IO) Bool)
-> QName -> WriterT UnifyOutput (TCMT IO) Bool
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
h) (UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []) (UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
 -> UnifyStepT (TCMT IO) (UnificationResult' UnifyState))
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ do
        UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ NegativeUnification -> UnificationResult' UnifyState
forall a. NegativeUnification -> UnificationResult' a
NoUnify (NegativeUnification -> UnificationResult' UnifyState)
-> NegativeUnification -> UnificationResult' UnifyState
forall a b. (a -> b) -> a -> b
$ Telescope -> Term -> Term -> NegativeUnification
UnifyConflict (UnifyState -> Telescope
varTel UnifyState
s) Term
u Term
v
    Term
_ -> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a. HasCallStack => a
__IMPOSSIBLE__

unifyStep UnifyState
s EtaExpandVar{ expandVar :: UnifyStep -> FlexibleVar Key
expandVar = FlexibleVar Key
fi, expandVarRecordType :: UnifyStep -> QName
expandVarRecordType = QName
d , expandVarParameters :: UnifyStep -> [Arg Term]
expandVarParameters = [Arg Term]
pars } = do
  recd <- RecordData -> Maybe RecordData -> RecordData
forall a. a -> Maybe a -> a
fromMaybe RecordData
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe RecordData -> RecordData)
-> WriterT UnifyOutput (TCMT IO) (Maybe RecordData)
-> WriterT UnifyOutput (TCMT IO) RecordData
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> WriterT UnifyOutput (TCMT IO) (Maybe RecordData)
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe RecordData)
isRecord QName
d
  let delta = RecordData -> Telescope
_recTel RecordData
recd Telescope -> [Arg Term] -> Telescope
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
pars
      c     = RecordData -> ConHead
_recConHead RecordData
recd
  let nfields         = Telescope -> Key
forall a. Sized a => a -> Key
size Telescope
delta
      (varTel', rho)  = expandTelescopeVar (varTel s) (m-1-i) delta c
      projectFlexible = [ ArgInfo
-> IsForced
-> FlexibleVarKind
-> Maybe Key
-> Key
-> FlexibleVar Key
forall a.
ArgInfo
-> IsForced -> FlexibleVarKind -> Maybe Key -> a -> FlexibleVar a
FlexibleVar (FlexibleVar Key -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo FlexibleVar Key
fi) (FlexibleVar Key -> IsForced
forall a. FlexibleVar a -> IsForced
flexForced FlexibleVar Key
fi) (Key -> FlexibleVarKind
projFlexKind Key
j) (FlexibleVar Key -> Maybe Key
forall a. FlexibleVar a -> Maybe Key
flexPos FlexibleVar Key
fi) (Key
i Key -> Key -> Key
forall a. Num a => a -> a -> a
+ Key
j) |
                          Key
j <- [Key
0 .. Key
nfields Key -> Key -> Key
forall a. Num a => a -> a -> a
- Key
1] ]
  tellUnifySubst $ rho
  return $ Unifies RetryNormalised UState
    { varTel   = varTel'
    , flexVars = projectFlexible ++! liftFlexibles nfields (flexVars s)
    , eqTel    = applyPatSubst rho $ eqTel s
    , eqLHS    = applyPatSubst rho $ eqLHS s
    , eqRHS    = applyPatSubst rho $ eqRHS s
    }
  where
    i :: Key
i = FlexibleVar Key -> Key
forall a. FlexibleVar a -> a
flexVar FlexibleVar Key
fi
    m :: Key
m = UnifyState -> Key
varCount UnifyState
s

    projFlexKind :: Int -> FlexibleVarKind
    projFlexKind :: Key -> FlexibleVarKind
projFlexKind Key
j = case FlexibleVar Key -> FlexibleVarKind
forall a. FlexibleVar a -> FlexibleVarKind
flexKind FlexibleVar Key
fi of
      RecordFlex [FlexibleVarKind]
ks -> FlexibleVarKind -> [FlexibleVarKind] -> Key -> FlexibleVarKind
forall a. a -> [a] -> Key -> a
indexWithDefault FlexibleVarKind
ImplicitFlex [FlexibleVarKind]
ks Key
j
      FlexibleVarKind
ImplicitFlex  -> FlexibleVarKind
ImplicitFlex
      FlexibleVarKind
DotFlex       -> FlexibleVarKind
DotFlex
      FlexibleVarKind
OtherFlex     -> FlexibleVarKind
OtherFlex

    liftFlexible :: Int -> Int -> Maybe Int
    liftFlexible :: Key -> Key -> Maybe Key
liftFlexible Key
n Key
j = if Key
j Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
i then Maybe Key
forall a. Maybe a
Nothing else Key -> Maybe Key
forall a. a -> Maybe a
Just (if Key
j Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
> Key
i then Key
j Key -> Key -> Key
forall a. Num a => a -> a -> a
+ (Key
nKey -> Key -> Key
forall a. Num a => a -> a -> a
-Key
1) else Key
j)

    liftFlexibles :: Int -> FlexibleVars -> FlexibleVars
    liftFlexibles :: Key -> FlexibleVars -> FlexibleVars
liftFlexibles Key
n FlexibleVars
fs = (FlexibleVar Key -> Maybe (FlexibleVar Key))
-> FlexibleVars -> FlexibleVars
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((Key -> Maybe Key) -> FlexibleVar Key -> Maybe (FlexibleVar Key)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FlexibleVar a -> f (FlexibleVar b)
traverse ((Key -> Maybe Key) -> FlexibleVar Key -> Maybe (FlexibleVar Key))
-> (Key -> Maybe Key) -> FlexibleVar Key -> Maybe (FlexibleVar Key)
forall a b. (a -> b) -> a -> b
$ Key -> Key -> Maybe Key
liftFlexible Key
n) FlexibleVars
fs

unifyStep UnifyState
s EtaExpandEquation{ expandAt :: UnifyStep -> Key
expandAt = Key
k, expandRecordType :: UnifyStep -> QName
expandRecordType = QName
d, expandParameters :: UnifyStep -> [Arg Term]
expandParameters = [Arg Term]
pars } = do
  recd  <- RecordData -> Maybe RecordData -> RecordData
forall a. a -> Maybe a -> a
fromMaybe RecordData
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe RecordData -> RecordData)
-> WriterT UnifyOutput (TCMT IO) (Maybe RecordData)
-> WriterT UnifyOutput (TCMT IO) RecordData
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> WriterT UnifyOutput (TCMT IO) (Maybe RecordData)
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe RecordData)
isRecord QName
d
  let delta = RecordData -> Telescope
_recTel RecordData
recd Telescope -> [Arg Term] -> Telescope
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
pars
      c     = RecordData -> ConHead
_recConHead RecordData
recd
  lhs   <- expandKth $ eqLHS s
  rhs   <- expandKth $ eqRHS s
  let (tel, sigma) = expandTelescopeVar (eqTel s) k delta c
  tellUnifyProof sigma
  Unifies RetryNormalised <$> do
   lensEqTel reduce $ s
    { eqTel    = tel
    , eqLHS    = lhs
    , eqRHS    = rhs
    }
  where
    expandKth :: [Arg Term] -> WriterT UnifyOutput (TCMT IO) [Arg Term]
expandKth [Arg Term]
us = do
      let ([Arg Term]
us1,Arg Term
v:[Arg Term]
us2) = ([Arg Term], [Arg Term])
-> Maybe ([Arg Term], [Arg Term]) -> ([Arg Term], [Arg Term])
forall a. a -> Maybe a -> a
fromMaybe ([Arg Term], [Arg Term])
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe ([Arg Term], [Arg Term]) -> ([Arg Term], [Arg Term]))
-> Maybe ([Arg Term], [Arg Term]) -> ([Arg Term], [Arg Term])
forall a b. (a -> b) -> a -> b
$ Key -> [Arg Term] -> Maybe ([Arg Term], [Arg Term])
forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt Key
k [Arg Term]
us
      vs <- (Telescope, [Arg Term]) -> [Arg Term]
forall a b. (a, b) -> b
snd ((Telescope, [Arg Term]) -> [Arg Term])
-> WriterT UnifyOutput (TCMT IO) (Telescope, [Arg Term])
-> WriterT UnifyOutput (TCMT IO) [Arg Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName
-> [Arg Term]
-> Term
-> WriterT UnifyOutput (TCMT IO) (Telescope, [Arg Term])
forall (m :: * -> *).
HasConstInfo m =>
QName -> [Arg Term] -> Term -> m (Telescope, [Arg Term])
etaExpandRecord QName
d [Arg Term]
pars (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v)
      vs <- addContext (varTel s) $ reduce vs
      return $! us1 ++! vs ++! us2

unifyStep UnifyState
s LitConflict
  { litType :: UnifyStep -> Type
litType          = Type
a
  , litConflictLeft :: UnifyStep -> Literal
litConflictLeft  = Literal
l
  , litConflictRight :: UnifyStep -> Literal
litConflictRight = Literal
l'
  } = UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ NegativeUnification -> UnificationResult' UnifyState
forall a. NegativeUnification -> UnificationResult' a
NoUnify (NegativeUnification -> UnificationResult' UnifyState)
-> NegativeUnification -> UnificationResult' UnifyState
forall a b. (a -> b) -> a -> b
$ Telescope -> Term -> Term -> NegativeUnification
UnifyConflict (UnifyState -> Telescope
varTel UnifyState
s) (Literal -> Term
Lit Literal
l) (Literal -> Term
Lit Literal
l')

unifyStep UnifyState
s (SkipIrrelevantEquation Key
k) = do
  let lhs :: [Arg Term]
lhs = UnifyState -> [Arg Term]
eqLHS UnifyState
s
      (UnifyState
s', Substitution' (Pattern' DBPatVar)
sigma) = Key
-> Term
-> UnifyState
-> (UnifyState, Substitution' (Pattern' DBPatVar))
solveEq Key
k (Term -> Term
DontCare (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> [Arg Term] -> Key -> Arg Term
forall a. a -> [a] -> Key -> a
indexWithDefault Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ [Arg Term]
lhs Key
k) UnifyState
s
  Substitution' (Pattern' DBPatVar)
-> WriterT UnifyOutput (TCMT IO) ()
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
Substitution' (Pattern' DBPatVar) -> m ()
tellUnifyProof Substitution' (Pattern' DBPatVar)
sigma
  UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ RetryNormalised -> UnifyState -> UnificationResult' UnifyState
forall a. RetryNormalised -> a -> UnificationResult' a
Unifies RetryNormalised
RetryNormalised UnifyState
s'

unifyStep UnifyState
s (TypeConInjectivity Key
k QName
d [Arg Term]
us [Arg Term]
vs) = do
  dtype <- Definition -> Type
defType (Definition -> Type)
-> WriterT UnifyOutput (TCMT IO) Definition
-> WriterT UnifyOutput (TCMT IO) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> WriterT UnifyOutput (TCMT IO) Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
d
  TelV dtel _ <- telView dtype
  let deq = QName -> Elims -> Term
Def QName
d (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply ([Arg Term] -> Elims) -> [Arg Term] -> Elims
forall a b. (a -> b) -> a -> b
$ Telescope -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
dtel
  -- TODO: tellUnifyProof ???
  -- but d is not a constructor...
  Unifies RetryNormalised <$> do
   lensEqTel reduce $ s
    { eqTel = dtel `abstract` applyUnder k (eqTel s) (raise k deq)
    , eqLHS = us ++! dropAt k (eqLHS s)
    , eqRHS = vs ++! dropAt k (eqRHS s)
    }

solutionStep ::
     RetryNormalised
  -> UnifyState
  -> UnifyStep
  -> WriterT UnifyOutput TCM (UnificationResult' UnifyState)
solutionStep :: RetryNormalised
-> UnifyState
-> UnifyStep
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
solutionStep RetryNormalised
retry UnifyState
s
  step :: UnifyStep
step@Solution{ solutionAt :: UnifyStep -> Key
solutionAt   = Key
k
               , solutionType :: UnifyStep -> Dom Type
solutionType = dom :: Dom Type
dom@(Dom Type -> Type
forall t e. Dom' t e -> e
unDom -> Type
a)
               , solutionVar :: UnifyStep -> FlexibleVar Key
solutionVar  = fi :: FlexibleVar Key
fi@FlexibleVar{ flexVar :: forall a. FlexibleVar a -> a
flexVar = Key
i }
               , solutionTerm :: UnifyStep -> Term
solutionTerm = Term
u } = do
  let m :: Key
m = UnifyState -> Key
varCount UnifyState
s

  -- Now we have to be careful about forced variables in `u`. If they appear
  -- in pattern positions we need to bind them there rather in their forced positions. We can safely
  -- ignore non-pattern positions and forced pattern positions, because in that case there will be
  -- other equations where the variable can be bound.
  -- NOTE: If we're doing make-case we ignore forced variables. This is safe since we take the
  -- result of unification and build user clauses that will be checked again with forcing turned on.
  inMakeCase <- Lens' TCEnv Bool -> WriterT UnifyOutput (TCMT IO) Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eMakeCase
  let forcedVars | Bool
inMakeCase = IntSet
IntSet.empty
                 | Bool
otherwise  = [Key] -> IntSet
IntSet.fromList [ FlexibleVar Key -> Key
forall a. FlexibleVar a -> a
flexVar FlexibleVar Key
fi | FlexibleVar Key
fi <- UnifyState -> FlexibleVars
flexVars UnifyState
s,
                                                               FlexibleVar Key -> IsForced
forall a. FlexibleVar a -> IsForced
flexForced FlexibleVar Key
fi IsForced -> IsForced -> Bool
forall a. Eq a => a -> a -> Bool
== IsForced
Forced ]
  (p, bound) <- lift $ patternBindingForcedVars forcedVars u

  -- To maintain the invariant that each variable in varTel is bound exactly once in the pattern
  -- substitution we need to turn the bound variables in `p` into dot patterns in the rest of the
  -- substitution.
  let dotSub = (Substitution' (Pattern' DBPatVar)
 -> Substitution' (Pattern' DBPatVar)
 -> Substitution' (Pattern' DBPatVar))
-> Substitution' (Pattern' DBPatVar)
-> [Substitution' (Pattern' DBPatVar)]
-> Substitution' (Pattern' DBPatVar)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Substitution' (Pattern' DBPatVar)
-> Substitution' (Pattern' DBPatVar)
-> Substitution' (Pattern' DBPatVar)
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS Substitution' (Pattern' DBPatVar)
forall a. Substitution' a
idS [ Key -> Pattern' DBPatVar -> Substitution' (Pattern' DBPatVar)
forall a. EndoSubst a => Key -> a -> Substitution' a
inplaceS Key
i (Term -> Pattern' DBPatVar
forall a. Term -> Pattern' a
dotP (Key -> Elims -> Term
Var Key
i [])) | Key
i <- IntSet -> [Key]
IntSet.toList IntSet
bound ]

  reportSDoc "tc.lhs.unify.force" 45 $ vcat
    [ "forcedVars =" <+> pretty (IntSet.toList forcedVars)
    , "u          =" <+> prettyTCM u
    , "p          =" <+> prettyTCM p
    , "bound      =" <+> pretty (IntSet.toList bound)
    , "dotSub     =" <+> pretty dotSub ]

  -- Check that the type of the variable is equal to the type of the equation
  -- (not just a subtype), otherwise we cannot instantiate (see Issue 2407).
  let dom'@(unDom -> a') = getVarType (m-1-i) s
  equalTypes <- addContext (varTel s) $ do
    reportSDoc "tc.lhs.unify" 45 $ "Equation type: " <+> prettyTCM a
    reportSDoc "tc.lhs.unify" 45 $ "Variable type: " <+> prettyTCM a'
    lift $ pureBlockOrEqualType a a'

  case equalTypes of
    Left Blocker
block  -> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ Blocker -> UnificationResult' UnifyState
forall a. Blocker -> UnificationResult' a
UnifyBlocked Blocker
block
    Right Bool
False -> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []
    Right Bool
True ->
      case Key
-> Pattern' DBPatVar
-> UnifyState
-> Maybe
     (UnifyState, Substitution' (Pattern' DBPatVar), Permutation)
solveVar (Key
m Key -> Key -> Key
forall a. Num a => a -> a -> a
- Key
1 Key -> Key -> Key
forall a. Num a => a -> a -> a
- Key
i) Pattern' DBPatVar
p UnifyState
s of
        Maybe (UnifyState, Substitution' (Pattern' DBPatVar), Permutation)
Nothing | RetryNormalised
RetryNormalised <- RetryNormalised
retry -> do
          u <- Term -> WriterT UnifyOutput (TCMT IO) Term
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Term
u
          s <- lensVarTel normalise s
          solutionStep (DontRetryNormalised s) s step{ solutionTerm = u }
        Maybe (UnifyState, Substitution' (Pattern' DBPatVar), Permutation)
Nothing ->
          UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$! [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [Telescope -> Type -> Key -> Term -> UnificationFailure
UnifyRecursiveEq (UnifyState -> Telescope
varTel UnifyState
s) Type
a Key
i Term
u]
        Just (UnifyState
s', Substitution' (Pattern' DBPatVar)
sub, Permutation
perm) -> do
          let rho :: Substitution' (Pattern' DBPatVar)
rho = Substitution' (Pattern' DBPatVar)
sub Substitution' (Pattern' DBPatVar)
-> Substitution' (Pattern' DBPatVar)
-> Substitution' (Pattern' DBPatVar)
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution' (Pattern' DBPatVar)
dotSub
          Substitution' (Pattern' DBPatVar)
-> WriterT UnifyOutput (TCMT IO) ()
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
Substitution' (Pattern' DBPatVar) -> m ()
tellUnifySubst Substitution' (Pattern' DBPatVar)
rho
          let (UnifyState
s'', Substitution' (Pattern' DBPatVar)
sigma) = Key
-> Term
-> UnifyState
-> (UnifyState, Substitution' (Pattern' DBPatVar))
solveEq Key
k (Substitution' (Pattern' DBPatVar) -> Term -> Term
forall a.
TermSubst a =>
Substitution' (Pattern' DBPatVar) -> a -> a
applyPatSubst Substitution' (Pattern' DBPatVar)
rho Term
u) UnifyState
s'
          Substitution' (Pattern' DBPatVar)
-> WriterT UnifyOutput (TCMT IO) ()
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
Substitution' (Pattern' DBPatVar) -> m ()
tellUnifyProof Substitution' (Pattern' DBPatVar)
sigma
          Permutation -> WriterT UnifyOutput (TCMT IO) ()
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
Permutation -> m ()
tellUnifySolutionPerm Permutation
perm
          UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ RetryNormalised -> UnifyState -> UnificationResult' UnifyState
forall a. RetryNormalised -> a -> UnificationResult' a
Unifies RetryNormalised
retry UnifyState
s''
          -- Andreas, 2019-02-23, issue #3578: do not eagerly reduce
          -- Unifies <$> liftTCM (reduce s'')
solutionStep RetryNormalised
_ UnifyState
_ UnifyStep
_ = UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
forall a. HasCallStack => a
__IMPOSSIBLE__

unify :: UnifyState -> UnifyStrategy -> UnifyLogT TCM (UnificationResult' UnifyState)
unify :: UnifyState
-> UnifyStrategy
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
unify UnifyState
s UnifyStrategy
strategy = do
    String -> Key -> TCMT IO Doc -> WriterT UnifyLog' (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Key
40 (TCMT IO Doc -> WriterT UnifyLog' (TCMT IO) ())
-> TCMT IO Doc -> WriterT UnifyLog' (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"unify"
    if UnifyState -> Bool
isUnifyStateSolved UnifyState
s
    then UnificationResult' UnifyState
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyLogT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ RetryNormalised -> UnifyState -> UnificationResult' UnifyState
forall a. RetryNormalised -> a -> UnificationResult' a
Unifies RetryNormalised
RetryNormalised UnifyState
s
    else ListT (TCMT IO) UnifyStep
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
tryUnifyStepsAndContinue (UnifyStrategy
strategy UnifyState
s)
  where
    tryUnifyStepsAndContinue
      :: ListT TCM UnifyStep -> UnifyLogT TCM (UnificationResult' UnifyState)
    tryUnifyStepsAndContinue :: ListT (TCMT IO) UnifyStep
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
tryUnifyStepsAndContinue ListT (TCMT IO) UnifyStep
steps = do
      x <- (UnifyStep
 -> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
 -> UnifyLogT (TCMT IO) (UnificationResult' UnifyState))
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
-> ListT (WriterT UnifyLog' (TCMT IO)) UnifyStep
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT UnifyStep
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
tryUnifyStep UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => m (UnificationResult' a)
failure ((forall a1. TCM a1 -> WriterT UnifyLog' (TCMT IO) a1)
-> ListT (TCMT IO) UnifyStep
-> ListT (WriterT UnifyLog' (TCMT IO)) UnifyStep
forall (m :: * -> *) (m' :: * -> *) a.
(Monad m, Monad m') =>
(forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
liftListT TCM a1 -> WriterT UnifyLog' (TCMT IO) a1
forall a1. TCM a1 -> WriterT UnifyLog' (TCMT IO) a1
forall (m :: * -> *) a. Monad m => m a -> WriterT UnifyLog' m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ListT (TCMT IO) UnifyStep
steps)
      case x of
        Unifies RetryNormalised
_ UnifyState
s'   -> UnifyState
-> UnifyStrategy
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
unify UnifyState
s' UnifyStrategy
strategy
        NoUnify NegativeUnification
err    -> UnificationResult' UnifyState
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyLogT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ NegativeUnification -> UnificationResult' UnifyState
forall a. NegativeUnification -> UnificationResult' a
NoUnify NegativeUnification
err
        UnifyBlocked Blocker
b -> UnificationResult' UnifyState
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyLogT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ Blocker -> UnificationResult' UnifyState
forall a. Blocker -> UnificationResult' a
UnifyBlocked Blocker
b
        UnifyStuck [UnificationFailure]
err -> UnificationResult' UnifyState
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyLogT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [UnificationFailure]
err

    tryUnifyStep :: UnifyStep
                 -> UnifyLogT TCM (UnificationResult' UnifyState)
                 -> UnifyLogT TCM (UnificationResult' UnifyState)
    tryUnifyStep :: UnifyStep
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
tryUnifyStep UnifyStep
step UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
fallback = do
      Telescope
-> WriterT UnifyLog' (TCMT IO) () -> WriterT UnifyLog' (TCMT IO) ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) (WriterT UnifyLog' (TCMT IO) () -> WriterT UnifyLog' (TCMT IO) ())
-> WriterT UnifyLog' (TCMT IO) () -> WriterT UnifyLog' (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
        String -> Key -> TCMT IO Doc -> WriterT UnifyLog' (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Key
20 (TCMT IO Doc -> WriterT UnifyLog' (TCMT IO) ())
-> TCMT IO Doc -> WriterT UnifyLog' (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"trying unifyStep" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> UnifyStep -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
prettyTCM UnifyStep
step
      (x, output) <- TCM (UnificationResult' UnifyState, UnifyOutput)
-> WriterT
     UnifyLog' (TCMT IO) (UnificationResult' UnifyState, UnifyOutput)
forall (m :: * -> *) a. Monad m => m a -> WriterT UnifyLog' m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (UnificationResult' UnifyState, UnifyOutput)
 -> WriterT
      UnifyLog' (TCMT IO) (UnificationResult' UnifyState, UnifyOutput))
-> TCM (UnificationResult' UnifyState, UnifyOutput)
-> WriterT
     UnifyLog' (TCMT IO) (UnificationResult' UnifyState, UnifyOutput)
forall a b. (a -> b) -> a -> b
$ UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
-> TCM (UnificationResult' UnifyState, UnifyOutput)
forall w (m :: * -> *) a.
(Monoid w, Monad m) =>
WriterT w m a -> m (a, w)
runWriterT (UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
 -> TCM (UnificationResult' UnifyState, UnifyOutput))
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
-> TCM (UnificationResult' UnifyState, UnifyOutput)
forall a b. (a -> b) -> a -> b
$ UnifyState
-> UnifyStep
-> UnifyStepT (TCMT IO) (UnificationResult' UnifyState)
unifyStep UnifyState
s UnifyStep
step
      case x of
        Unifies RetryNormalised
b UnifyState
s' -> do
          String -> Key -> TCMT IO Doc -> WriterT UnifyLog' (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Key
20 (TCMT IO Doc -> WriterT UnifyLog' (TCMT IO) ())
-> TCMT IO Doc -> WriterT UnifyLog' (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"unifyStep successful."
          String -> Key -> TCMT IO Doc -> WriterT UnifyLog' (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Key -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Key
20 (TCMT IO Doc -> WriterT UnifyLog' (TCMT IO) ())
-> TCMT IO Doc -> WriterT UnifyLog' (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"new unifyState:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> UnifyState -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => UnifyState -> m Doc
prettyTCM UnifyState
s'

          let
            -- mikan#19: If the unification step is only valid assuming
            -- the old state was normalised, we have to record the
            -- normalised version in the log.
            old_s :: UnifyState
old_s = case RetryNormalised
b of
              DontRetryNormalised UnifyState
s -> UnifyState
s
              RetryNormalised
RetryNormalised       -> UnifyState
s
          (UnifyLogEntry, UnifyState) -> WriterT UnifyLog' (TCMT IO) ()
forall (m :: * -> *).
MonadWriter UnifyLog' m =>
(UnifyLogEntry, UnifyState) -> m ()
writeUnifyLog (UnifyState -> UnifyStep -> UnifyOutput -> UnifyLogEntry
UnificationStep UnifyState
old_s UnifyStep
step UnifyOutput
output, UnifyState
s')

          UnificationResult' UnifyState
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
x
        NoUnify{}       -> UnificationResult' UnifyState
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
x
        UnifyBlocked Blocker
b1 -> do
          y <- UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
fallback
          case y of
            UnifyStuck [UnificationFailure]
_    -> UnificationResult' UnifyState
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyLogT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ Blocker -> UnificationResult' UnifyState
forall a. Blocker -> UnificationResult' a
UnifyBlocked Blocker
b1
            UnifyBlocked Blocker
b2 -> UnificationResult' UnifyState
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyLogT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ Blocker -> UnificationResult' UnifyState
forall a. Blocker -> UnificationResult' a
UnifyBlocked (Blocker -> UnificationResult' UnifyState)
-> Blocker -> UnificationResult' UnifyState
forall a b. (a -> b) -> a -> b
$ Blocker -> Blocker -> Blocker
unblockOnEither Blocker
b1 Blocker
b2
            UnificationResult' UnifyState
_               -> UnificationResult' UnifyState
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
y
        UnifyStuck [UnificationFailure]
err1 -> do
          y <- UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
fallback
          case y of
            UnifyStuck [UnificationFailure]
err2 -> UnificationResult' UnifyState
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyLogT (TCMT IO) (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$! [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck ([UnificationFailure] -> UnificationResult' UnifyState)
-> [UnificationFailure] -> UnificationResult' UnifyState
forall a b. (a -> b) -> a -> b
$! [UnificationFailure]
err1 [UnificationFailure]
-> [UnificationFailure] -> [UnificationFailure]
forall a. [a] -> [a] -> [a]
++! [UnificationFailure]
err2
            UnificationResult' UnifyState
_               -> UnificationResult' UnifyState
-> UnifyLogT (TCMT IO) (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
y

    failure :: Monad m => m (UnificationResult' a)
    failure :: forall (m :: * -> *) a. Monad m => m (UnificationResult' a)
failure = UnificationResult' a -> m (UnificationResult' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' a -> m (UnificationResult' a))
-> UnificationResult' a -> m (UnificationResult' a)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' a
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []

-- | Turn a term into a pattern while binding as many of the given forced variables as possible (in
--   non-forced positions).
patternBindingForcedVars :: IntSet -> Term -> TCM (DeBruijnPattern, IntSet)
patternBindingForcedVars :: IntSet -> Term -> TCMT IO (Pattern' DBPatVar, IntSet)
patternBindingForcedVars IntSet
forced Term
v = do
  let v' :: Term
v' = Term -> Term
forall a. PrecomputeFreeVars a => a -> a
precomputeFreeVars_ Term
v
  WriterT IntSet (TCMT IO) (Pattern' DBPatVar)
-> TCMT IO (Pattern' DBPatVar, IntSet)
forall w (m :: * -> *) a.
(Monoid w, Monad m) =>
WriterT w m a -> m (a, w)
runWriterT (StateT IntSet (WriterT IntSet (TCMT IO)) (Pattern' DBPatVar)
-> IntSet -> WriterT IntSet (TCMT IO) (Pattern' DBPatVar)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Term
-> StateT IntSet (WriterT IntSet (TCMT IO)) (Pattern' DBPatVar)
forall {t :: (* -> *) -> * -> *} {t :: (* -> *) -> * -> *}
       {m :: * -> *} {a}.
(MonadState IntSet (t (t m)), MonadTrans t, MonadTrans t,
 Monad (t m), MonadReduce m, MonadWriter IntSet (t (t m)),
 DeBruijn a, HasConstInfo (t (t m))) =>
Term -> t (t m) (Pattern' a)
go Term
v') IntSet
forced)
  where
    noForced :: a -> m Bool
noForced a
v = (IntSet -> Bool) -> m Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((IntSet -> Bool) -> m Bool) -> (IntSet -> Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ VarSet -> VarSet -> Bool
VarSet.disjoint (a -> VarSet
forall a. PrecomputeFreeVars a => a -> VarSet
precomputedFreeVars a
v) (VarSet -> Bool) -> (IntSet -> VarSet) -> IntSet -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Key] -> VarSet
VarSet.fromList ([Key] -> VarSet) -> (IntSet -> [Key]) -> IntSet -> VarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Key]
IntSet.toList

    bind :: Key -> m (Pattern' a)
bind Key
i = do
      (IntSet -> Bool) -> m Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Key -> IntSet -> Bool
IntSet.member Key
i) m Bool -> (Bool -> m (Pattern' a)) -> m (Pattern' a)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Bool
True -> do
          IntSet -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell   (IntSet -> m ()) -> IntSet -> m ()
forall a b. (a -> b) -> a -> b
$! Key -> IntSet
IntSet.singleton Key
i
          (IntSet -> IntSet) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((IntSet -> IntSet) -> m ()) -> (IntSet -> IntSet) -> m ()
forall a b. (a -> b) -> a -> b
$! Key -> IntSet -> IntSet
IntSet.delete Key
i
          Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
forall a b. (a -> b) -> a -> b
$! a -> Pattern' a
forall a. a -> Pattern' a
varP (Key -> a
forall a. DeBruijn a => Key -> a
deBruijnVar Key
i)
        Bool
_ -> Pattern' a -> m (Pattern' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a)
forall a b. (a -> b) -> a -> b
$! Term -> Pattern' a
forall a. Term -> Pattern' a
dotP (Key -> Elims -> Term
Var Key
i [])

    go :: Term -> t (t m) (Pattern' a)
go Term
v = t (t m) Bool
-> t (t m) (Pattern' a)
-> t (t m) (Pattern' a)
-> t (t m) (Pattern' a)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Term -> t (t m) Bool
forall {m :: * -> *} {a}.
(MonadState IntSet m, PrecomputeFreeVars a) =>
a -> m Bool
noForced Term
v) (Pattern' a -> t (t m) (Pattern' a)
forall a. a -> t (t m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$! Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v) (t (t m) (Pattern' a) -> t (t m) (Pattern' a))
-> t (t m) (Pattern' a) -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$ do
      v' <- t m Term -> t (t m) Term
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (t m Term -> t (t m) Term) -> t m Term -> t (t m) Term
forall a b. (a -> b) -> a -> b
$ m Term -> t m Term
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Term -> t m Term) -> m Term -> t m Term
forall a b. (a -> b) -> a -> b
$ Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
      case v' of
        Var Key
i [] -> Key -> t (t m) (Pattern' a)
forall {m :: * -> *} {a}.
(MonadState IntSet m, MonadWriter IntSet m, DeBruijn a) =>
Key -> m (Pattern' a)
bind Key
i  -- we know i is forced
        Con ConHead
c ConInfo
ci Elims
es
          | Just [Arg Term]
vs <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es -> do
            fs <- Definition -> [IsForced]
defForced (Definition -> [IsForced])
-> t (t m) Definition -> t (t m) [IsForced]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> t (t m) Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo (ConHead -> QName
conName ConHead
c)
            let goArg IsForced
Forced    Arg Term
v = NamedArg (Pattern' a) -> t (t m) (NamedArg (Pattern' a))
forall a. a -> t (t m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (NamedArg (Pattern' a) -> t (t m) (NamedArg (Pattern' a)))
-> NamedArg (Pattern' a) -> t (t m) (NamedArg (Pattern' a))
forall a b. (a -> b) -> a -> b
$! (Term -> Named NamedName (Pattern' a))
-> Arg Term -> NamedArg (Pattern' a)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Pattern' a -> Named NamedName (Pattern' a)
forall a name. a -> Named name a
unnamed (Pattern' a -> Named NamedName (Pattern' a))
-> (Term -> Pattern' a) -> Term -> Named NamedName (Pattern' a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Pattern' a
forall a. Term -> Pattern' a
dotP) Arg Term
v
                goArg IsForced
NotForced Arg Term
v = (Pattern' a -> Named NamedName (Pattern' a))
-> Arg (Pattern' a) -> NamedArg (Pattern' a)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern' a -> Named NamedName (Pattern' a)
forall a name. a -> Named name a
unnamed (Arg (Pattern' a) -> NamedArg (Pattern' a))
-> t (t m) (Arg (Pattern' a)) -> t (t m) (NamedArg (Pattern' a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> t (t m) (Pattern' a))
-> Arg Term -> t (t m) (Arg (Pattern' a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse Term -> t (t m) (Pattern' a)
go Arg Term
v
            (ps, bound) <- listen $ zipWithM goArg (fs ++! repeat NotForced) vs
            if IntSet.null bound
              then return $! dotP v  -- bound nothing
              else do
                let cpi = (ConInfo -> ConPatternInfo
toConPatternInfo ConInfo
ci) { conPLazy   = True } -- Not setting conPType. Is this a problem?
                return $! ConP c cpi $! map' (setOrigin Inserted) ps
          | Bool
otherwise -> Pattern' a -> t (t m) (Pattern' a)
forall a. a -> t (t m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$! Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v   -- Higher constructor (es has IApply)

        -- Non-pattern positions
        Var Key
_ (Elim
_:Elims
_) -> Pattern' a -> t (t m) (Pattern' a)
forall a. a -> t (t m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$! Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
        Lam{}       -> Pattern' a -> t (t m) (Pattern' a)
forall a. a -> t (t m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$! Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
        Pi{}        -> Pattern' a -> t (t m) (Pattern' a)
forall a. a -> t (t m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$! Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
        Def{}       -> Pattern' a -> t (t m) (Pattern' a)
forall a. a -> t (t m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$! Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
        MetaV{}     -> Pattern' a -> t (t m) (Pattern' a)
forall a. a -> t (t m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$! Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
        Sort{}      -> Pattern' a -> t (t m) (Pattern' a)
forall a. a -> t (t m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$! Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
        Level{}     -> Pattern' a -> t (t m) (Pattern' a)
forall a. a -> t (t m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$! Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
        DontCare{}  -> Pattern' a -> t (t m) (Pattern' a)
forall a. a -> t (t m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$! Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
        Dummy{}     -> Pattern' a -> t (t m) (Pattern' a)
forall a. a -> t (t m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$! Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
        Lit{}       -> Pattern' a -> t (t m) (Pattern' a)
forall a. a -> t (t m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern' a -> t (t m) (Pattern' a))
-> Pattern' a -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$! Term -> Pattern' a
forall a. Term -> Pattern' a
dotP Term
v
          -- Andreas, 2023-08-20, issue #6767
          -- The last case is not __IMPOSSIBLE__ (regresssion in 2.6.2).
          -- It would be if we had reduced to `constructorForm`,
          -- however, turning a `LitNat` into constructors would only result in churn,
          -- since literals have no variables that could be bound.