{-# 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 : Set i@ where @D@ is a datatype. This rule is only used
--     if --injective-type-constructors is enabled.
--
--   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 : Φ → Set ℓ@, 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 Agda.TypeChecking.Rules.LHS.Unify
  ( UnificationResult
  , UnificationResult'(..)
  , NoLeftInv(..)
  , unifyIndices'
  , unifyIndices ) where

import Prelude hiding (null)

import Control.Monad.State  ( gets, modify, evalStateT )
import Control.Monad.Writer ( WriterT(..), MonadWriter(..) )
import Control.Monad.Except ( runExceptT )

import Data.Semigroup hiding (Arg)
import qualified Data.List as List
import qualified Data.IntSet as IntSet
import qualified Data.IntMap as IntMap
import Data.IntMap (IntMap)

import qualified Agda.Benchmarking as Bench

import Agda.Interaction.Options (optInjectiveTypeConstructors)

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

import Agda.TypeChecking.Monad
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Conversion.Pure (pureEqualTermB, pureEqualTypeB)
import Agda.TypeChecking.Constraints ()
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Reduce
import qualified Agda.TypeChecking.Patterns.Match as Match
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Free
import Agda.TypeChecking.Free.Precompute
import Agda.TypeChecking.Free.Reduce
import Agda.TypeChecking.Records

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

import Agda.Utils.Either
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.ListT
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.PartialOrd
import Agda.Utils.Singleton
import Agda.Utils.Size

import Agda.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 @
  , Either NoLeftInv (Substitution, Substitution) -- (τ,leftInv)
  )

data UnificationResult' a
  = Unifies  a                        -- ^ Unification succeeded.
  | NoUnify  NegativeUnification      -- ^ Terms are not unifiable.
  | UnifyBlocked Blocker              -- ^ Unification got blocked on a metavariable
  | UnifyStuck   [UnificationFailure] -- ^ Some other error happened, unification got stuck.
  deriving (Nat -> UnificationResult' a -> ShowS
[UnificationResult' a] -> ShowS
UnificationResult' a -> String
(Nat -> UnificationResult' a -> ShowS)
-> (UnificationResult' a -> String)
-> ([UnificationResult' a] -> ShowS)
-> Show (UnificationResult' a)
forall a. Show a => Nat -> UnificationResult' a -> ShowS
forall a. Show a => [UnificationResult' a] -> ShowS
forall a. Show a => UnificationResult' a -> String
forall a.
(Nat -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Nat -> UnificationResult' a -> ShowS
showsPrec :: Nat -> 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 -> Nat)
-> (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 -> Nat
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 -> Nat)
-> (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 -> Nat
length :: forall a. UnificationResult' a -> Nat
$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) variabes 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 =
  Account (BenchPhase TCM)
-> TCM UnificationResult -> TCM UnificationResult
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase TCM
Phase
Bench.Typing, BenchPhase TCM
Phase
Bench.CheckLHS, BenchPhase TCM
Phase
Bench.UnifyIndices] (TCM UnificationResult -> TCM UnificationResult)
-> TCM UnificationResult -> TCM UnificationResult
forall a b. (a -> b) -> a -> b
$
    ((Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
  Either NoLeftInv (Substitution, Substitution))
 -> (Telescope, PatternSubstitution,
     [NamedArg (Pattern' DBPatVar)]))
-> UnificationResult'
     (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
      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,PatternSubstitution
b,[NamedArg (Pattern' DBPatVar)]
c,Either NoLeftInv (Substitution, Substitution)
_) -> (Telescope
a,PatternSubstitution
b,[NamedArg (Pattern' DBPatVar)]
c)) (UnificationResult'
   (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
    Either NoLeftInv (Substitution, Substitution))
 -> UnificationResult)
-> TCMT
     IO
     (UnificationResult'
        (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
         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, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
         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, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
         Either NoLeftInv (Substitution, Substitution)))
unifyIndices' Maybe NoLeftInv
linv Telescope
tel FlexibleVars
flex Type
a [] [] = UnificationResult'
  (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
   Either NoLeftInv (Substitution, Substitution))
-> TCMT
     IO
     (UnificationResult'
        (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
         Either NoLeftInv (Substitution, Substitution)))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult'
   (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
    Either NoLeftInv (Substitution, Substitution))
 -> TCMT
      IO
      (UnificationResult'
         (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
          Either NoLeftInv (Substitution, Substitution))))
-> UnificationResult'
     (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
      Either NoLeftInv (Substitution, Substitution))
-> TCMT
     IO
     (UnificationResult'
        (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
         Either NoLeftInv (Substitution, Substitution)))
forall a b. (a -> b) -> a -> b
$ (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
 Either NoLeftInv (Substitution, Substitution))
-> UnificationResult'
     (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
      Either NoLeftInv (Substitution, Substitution))
forall a. a -> UnificationResult' a
Unifies (Telescope
tel, PatternSubstitution
forall a. Substitution' a
idS, [], (Substitution, Substitution)
-> Either NoLeftInv (Substitution, Substitution)
forall a b. b -> Either a b
Right (Substitution
forall a. Substitution' a
idS, Nat -> Substitution
forall a. Nat -> Substitution' a
raiseS Nat
1))
unifyIndices' Maybe NoLeftInv
linv Telescope
tel FlexibleVars
flex Type
a [Arg Term]
us [Arg Term]
vs = do
    String -> Nat -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
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
$ Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
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
$ Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
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
$ [Nat] -> String
forall a. Show a => a -> String
show ([Nat] -> String) -> [Nat] -> String
forall a b. (a -> b) -> a -> b
$ (FlexibleVar Nat -> Nat) -> FlexibleVars -> [Nat]
forall a b. (a -> b) -> [a] -> [b]
map FlexibleVar Nat -> Nat
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
$ Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
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
$ Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
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
$ Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
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
          ]
    UnifyState
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
    String -> Nat -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"initial 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
initialState
    (UnificationResult' UnifyState
result,UnifyLog
log) <- UnifyLogT TCM (UnificationResult' UnifyState)
-> TCM (UnificationResult' UnifyState, UnifyLog)
forall (m :: * -> *) a.
Functor m =>
UnifyLogT m a -> m (a, UnifyLog)
runUnifyLogT (UnifyLogT TCM (UnificationResult' UnifyState)
 -> TCM (UnificationResult' UnifyState, UnifyLog))
-> UnifyLogT TCM (UnificationResult' UnifyState)
-> TCM (UnificationResult' UnifyState, UnifyLog)
forall a b. (a -> b) -> a -> b
$ UnifyState
-> UnifyStrategy -> UnifyLogT TCM (UnificationResult' UnifyState)
unify UnifyState
initialState UnifyStrategy
rightToLeftStrategy
    UnificationResult' UnifyState
-> (UnifyState
    -> TCMT
         IO
         (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
          Either NoLeftInv (Substitution, Substitution)))
-> TCMT
     IO
     (UnificationResult'
        (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
         Either NoLeftInv (Substitution, Substitution)))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM UnificationResult' UnifyState
result ((UnifyState
  -> TCMT
       IO
       (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
        Either NoLeftInv (Substitution, Substitution)))
 -> TCMT
      IO
      (UnificationResult'
         (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
          Either NoLeftInv (Substitution, Substitution))))
-> (UnifyState
    -> TCMT
         IO
         (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
          Either NoLeftInv (Substitution, Substitution)))
-> TCMT
     IO
     (UnificationResult'
        (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
         Either NoLeftInv (Substitution, Substitution)))
forall a b. (a -> b) -> a -> b
$ \ 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 -> PatternSubstitution
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)
        Either NoLeftInv (Substitution, Substitution)
tauInv <- do
          Bool
strict     <- (TCEnv -> Bool) -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envSplitOnStrict
          Bool
cubicalCompatible <- TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
cubicalCompatibleOption
          Bool
withoutK <- TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
withoutKOption
          case Maybe NoLeftInv
linv of
            Just NoLeftInv
reason -> Either NoLeftInv (Substitution, Substitution)
-> TCMT IO (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)
-> TCMT IO (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
cubicalCompatible -> UnifyState
-> UnifyLog
-> TCMT IO (Either NoLeftInv (Substitution, Substitution))
forall (tcm :: * -> *).
(PureTCM tcm, MonadError TCErr tcm) =>
UnifyState
-> UnifyLog -> tcm (Either NoLeftInv (Substitution, Substitution))
buildLeftInverse UnifyState
initialState UnifyLog
log
              | Bool
withoutK          -> Either NoLeftInv (Substitution, Substitution)
-> TCMT IO (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
NoCubical)
              | Bool
otherwise         -> Either NoLeftInv (Substitution, Substitution)
-> TCMT IO (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
WithKEnabled)
        String -> Nat -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
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, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
 Either NoLeftInv (Substitution, Substitution))
-> TCMT
     IO
     (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
      Either NoLeftInv (Substitution, Substitution))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
  Either NoLeftInv (Substitution, Substitution))
 -> TCMT
      IO
      (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
       Either NoLeftInv (Substitution, Substitution)))
-> (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
    Either NoLeftInv (Substitution, Substitution))
-> TCMT
     IO
     (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
      Either NoLeftInv (Substitution, Substitution))
forall a b. (a -> b) -> a -> b
$ (UnifyState -> Telescope
varTel UnifyState
s, UnifyOutput -> PatternSubstitution
unifySubst UnifyOutput
output, [NamedArg (Pattern' DBPatVar)]
ps, Either NoLeftInv (Substitution, Substitution)
tauInv)



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 TCM UnifyStep] -> ListT TCM UnifyStep
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([Nat] -> (Nat -> ListT TCM UnifyStep) -> [ListT TCM UnifyStep]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for (Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom Nat
n) ((Nat -> ListT TCM UnifyStep) -> [ListT TCM UnifyStep])
-> (Nat -> ListT TCM UnifyStep) -> [ListT TCM UnifyStep]
forall a b. (a -> b) -> a -> b
$ \Nat
k -> Nat -> UnifyStrategy
completeStrategyAt Nat
k UnifyState
s)
  where n :: Nat
n = Telescope -> Nat
forall a. Sized a => a -> Nat
size (Telescope -> Nat) -> Telescope -> Nat
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s

completeStrategyAt :: Int -> UnifyStrategy
completeStrategyAt :: Nat -> UnifyStrategy
completeStrategyAt Nat
k UnifyState
s = [ListT TCM UnifyStep] -> ListT TCM UnifyStep
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([ListT TCM UnifyStep] -> ListT TCM UnifyStep)
-> [ListT TCM UnifyStep] -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ ((Nat -> UnifyStrategy) -> ListT TCM UnifyStep)
-> [Nat -> UnifyStrategy] -> [ListT TCM UnifyStep]
forall a b. (a -> b) -> [a] -> [b]
map (\Nat -> UnifyStrategy
strat -> Nat -> UnifyStrategy
strat Nat
k UnifyState
s) ([Nat -> UnifyStrategy] -> [ListT TCM UnifyStep])
-> [Nat -> UnifyStrategy] -> [ListT TCM 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).
    [ (\Nat
n -> Nat -> UnifyStrategy
skipIrrelevantStrategy Nat
n)
    , (\Nat
n -> Nat -> UnifyStrategy
basicUnifyStrategy Nat
n)
    , (\Nat
n -> Nat -> UnifyStrategy
literalStrategy Nat
n)
    , (\Nat
n -> Nat -> UnifyStrategy
dataStrategy Nat
n)
    , (\Nat
n -> Nat -> UnifyStrategy
etaExpandVarStrategy  Nat
n)
    , (\Nat
n -> Nat -> UnifyStrategy
etaExpandEquationStrategy Nat
n)
    , (\Nat
n -> Nat -> UnifyStrategy
injectiveTypeConStrategy Nat
n)
    , (\Nat
n -> Nat -> UnifyStrategy
injectivePragmaStrategy Nat
n)
    , (\Nat
n -> Nat -> UnifyStrategy
simplifySizesStrategy Nat
n)
    , (\Nat
n -> Nat -> UnifyStrategy
checkEqualityStrategy Nat
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) => Nat -> a -> Maybe a
isHom Nat
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
$ All -> Bool
getAll (All -> Bool) -> All -> Bool
forall a b. (a -> b) -> a -> b
$ SingleVar All -> IgnoreSorts -> a -> All
forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree (Bool -> All
All (Bool -> All) -> (Nat -> Bool) -> SingleVar All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
>= Nat
n)) IgnoreSorts
IgnoreNot 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
$ Nat -> a -> a
forall a. Subst a => Nat -> a -> a
raise (-Nat
n) a
x

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

basicUnifyStrategy :: Int -> UnifyStrategy
basicUnifyStrategy :: Nat -> UnifyStrategy
basicUnifyStrategy Nat
k UnifyState
s = do
  Equal dom :: Dom Type
dom@Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v <- Equality -> ListT TCM Equality
forall (m :: * -> *).
(HasBuiltins m, HasOptions m) =>
Equality -> m Equality
eqUnLevel (Nat -> UnifyState -> Equality
getEquality Nat
k UnifyState
s)
    -- Andreas, 2019-02-23: reduce equality for the sake of isHom?
  Type
ha <- Maybe Type -> ListT TCM Type
forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP (Maybe Type -> ListT TCM Type) -> Maybe Type -> ListT TCM Type
forall a b. (a -> b) -> a -> b
$ Nat -> Type -> Maybe Type
forall a. (Free a, Subst a) => Nat -> a -> Maybe a
isHom Nat
n Type
a
  (Maybe Nat
mi, Maybe Nat
mj) <- Telescope
-> ListT TCM (Maybe Nat, Maybe Nat)
-> ListT TCM (Maybe Nat, Maybe Nat)
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) (ListT TCM (Maybe Nat, Maybe Nat)
 -> ListT TCM (Maybe Nat, Maybe Nat))
-> ListT TCM (Maybe Nat, Maybe Nat)
-> ListT TCM (Maybe Nat, Maybe Nat)
forall a b. (a -> b) -> a -> b
$ (,) (Maybe Nat -> Maybe Nat -> (Maybe Nat, Maybe Nat))
-> ListT TCM (Maybe Nat)
-> ListT TCM (Maybe Nat -> (Maybe Nat, Maybe Nat))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Type -> ListT TCM (Maybe Nat)
forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Nat)
isEtaVar Term
u Type
ha ListT TCM (Maybe Nat -> (Maybe Nat, Maybe Nat))
-> ListT TCM (Maybe Nat) -> ListT TCM (Maybe Nat, Maybe Nat)
forall a b. ListT TCM (a -> b) -> ListT TCM a -> ListT TCM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> Type -> ListT TCM (Maybe Nat)
forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Nat)
isEtaVar Term
v Type
ha
  String -> Nat -> TCMT IO Doc -> ListT TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
30 (TCMT IO Doc -> ListT TCM ()) -> TCMT IO Doc -> ListT TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"isEtaVar results: " 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 ([Maybe Nat] -> String
forall a. Show a => a -> String
show [Maybe Nat
mi,Maybe Nat
mj])
  case (Maybe Nat
mi, Maybe Nat
mj) of
    (Just Nat
i, Just Nat
j)
     | Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
j -> ListT TCM UnifyStep
forall a. ListT TCM a
forall (m :: * -> *) a. MonadPlus m => m a
mzero -- Taken care of by checkEqualityStrategy
    (Just Nat
i, Just Nat
j)
     | Just FlexibleVar Nat
fi <- Nat -> FlexibleVars -> Maybe (FlexibleVar Nat)
findFlexible Nat
i FlexibleVars
flex
     , Just FlexibleVar Nat
fj <- Nat -> FlexibleVars -> Maybe (FlexibleVar Nat)
findFlexible Nat
j FlexibleVars
flex -> do
       let choice :: FlexChoice
choice = FlexibleVar Nat -> FlexibleVar Nat -> FlexChoice
forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex FlexibleVar Nat
fi FlexibleVar Nat
fj
           firstTryLeft :: ListT TCM UnifyStep
firstTryLeft  = [ListT TCM UnifyStep] -> ListT TCM UnifyStep
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ UnifyStep -> ListT TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Nat
-> Dom Type -> FlexibleVar Nat -> Term -> Either () () -> UnifyStep
Solution Nat
k Dom Type
dom{unDom = ha} FlexibleVar Nat
fi Term
v Either () ()
forall {b}. Either () b
left)
                                , UnifyStep -> ListT TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Nat
-> Dom Type -> FlexibleVar Nat -> Term -> Either () () -> UnifyStep
Solution Nat
k Dom Type
dom{unDom = ha} FlexibleVar Nat
fj Term
u Either () ()
forall {a}. Either a ()
right)]
           firstTryRight :: ListT TCM UnifyStep
firstTryRight = [ListT TCM UnifyStep] -> ListT TCM UnifyStep
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ UnifyStep -> ListT TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Nat
-> Dom Type -> FlexibleVar Nat -> Term -> Either () () -> UnifyStep
Solution Nat
k Dom Type
dom{unDom = ha} FlexibleVar Nat
fj Term
u Either () ()
forall {a}. Either a ()
right)
                                , UnifyStep -> ListT TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Nat
-> Dom Type -> FlexibleVar Nat -> Term -> Either () () -> UnifyStep
Solution Nat
k Dom Type
dom{unDom = ha} FlexibleVar Nat
fi Term
v Either () ()
forall {b}. Either () b
left)]
       String -> Nat -> TCMT IO Doc -> ListT TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
40 (TCMT IO Doc -> ListT TCM ()) -> TCMT IO Doc -> ListT TCM ()
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 Nat -> String
forall a. Show a => a -> String
show FlexibleVar Nat
fi)
       String -> Nat -> TCMT IO Doc -> ListT TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
40 (TCMT IO Doc -> ListT TCM ()) -> TCMT IO Doc -> ListT TCM ()
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 Nat -> String
forall a. Show a => a -> String
show FlexibleVar Nat
fj)
       String -> Nat -> TCMT IO Doc -> ListT TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
40 (TCMT IO Doc -> ListT TCM ()) -> TCMT IO Doc -> ListT TCM ()
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 TCM UnifyStep
firstTryLeft
         FlexChoice
ChooseRight  -> ListT TCM UnifyStep
firstTryRight
         FlexChoice
ExpandBoth   -> ListT TCM UnifyStep
forall a. ListT TCM a
forall (m :: * -> *) a. MonadPlus m => m a
mzero -- This should be taken care of by etaExpandEquationStrategy
         FlexChoice
ChooseEither -> ListT TCM UnifyStep
firstTryRight
    (Just Nat
i, Maybe Nat
_)
     | Just FlexibleVar Nat
fi <- Nat -> FlexibleVars -> Maybe (FlexibleVar Nat)
findFlexible Nat
i FlexibleVars
flex -> UnifyStep -> ListT TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Nat
-> Dom Type -> FlexibleVar Nat -> Term -> Either () () -> UnifyStep
Solution Nat
k Dom Type
dom{unDom = ha} FlexibleVar Nat
fi Term
v Either () ()
forall {b}. Either () b
left
    (Maybe Nat
_, Just Nat
j)
     | Just FlexibleVar Nat
fj <- Nat -> FlexibleVars -> Maybe (FlexibleVar Nat)
findFlexible Nat
j FlexibleVars
flex -> UnifyStep -> ListT TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Nat
-> Dom Type -> FlexibleVar Nat -> Term -> Either () () -> UnifyStep
Solution Nat
k Dom Type
dom{unDom = ha} FlexibleVar Nat
fj Term
u Either () ()
forall {a}. Either a ()
right
    (Maybe Nat, Maybe Nat)
_ -> ListT TCM UnifyStep
forall a. ListT TCM a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  where
    flex :: FlexibleVars
flex = UnifyState -> FlexibleVars
flexVars UnifyState
s
    n :: Nat
n = UnifyState -> Nat
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 :: Nat -> UnifyStrategy
dataStrategy Nat
k UnifyState
s = do
  Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v <- Equality -> ListT TCM Equality
forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqConstructorForm (Equality -> ListT TCM Equality)
-> ListT TCM Equality -> ListT TCM Equality
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Equality -> ListT TCM Equality
forall (m :: * -> *).
(HasBuiltins m, HasOptions m) =>
Equality -> m Equality
eqUnLevel (Equality -> ListT TCM Equality)
-> ListT TCM Equality -> ListT TCM Equality
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Nat -> UnifyState -> ListT TCM Equality
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Nat -> UnifyState -> m Equality
getReducedEqualityUnraised Nat
k UnifyState
s
  Bool
sortOk <- Sort -> ListT TCM Sort
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
a) ListT TCM Sort -> (Sort -> Bool) -> ListT TCM Bool
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
    Type{} -> Bool
True
    Inf{}  -> Bool
True
    SSet{} -> Bool
True
    Sort
_      -> Bool
False
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
a of
    Def QName
d Elims
es | Bool
sortOk -> do
      Nat
npars <- ListT TCM (Maybe Nat) -> ListT TCM Nat
forall (m :: * -> *) a. MonadPlus m => m (Maybe a) -> m a
catMaybesMP (ListT TCM (Maybe Nat) -> ListT TCM Nat)
-> ListT TCM (Maybe Nat) -> ListT TCM Nat
forall a b. (a -> b) -> a -> b
$ QName -> ListT TCM (Maybe Nat)
forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Nat)
getNumberOfParameters QName
d
      let ([Arg Term]
pars,[Arg Term]
ixs) = Nat -> [Arg Term] -> ([Arg Term], [Arg Term])
forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
npars ([Arg Term] -> ([Arg Term], [Arg Term]))
-> [Arg Term] -> ([Arg Term], [Arg Term])
forall a b. (a -> b) -> a -> b
$ [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
      String -> Nat -> TCMT IO Doc -> ListT TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
40 (TCMT IO Doc -> ListT TCM ()) -> TCMT IO Doc -> ListT TCM ()
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 (UnifyState -> Telescope
varTel UnifyState
s Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` UnifyState -> Telescope
eqTel UnifyState
s) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"Found equation at datatype " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d
         TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" with parameters " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Arg Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
prettyTCM (Nat -> [Arg Term] -> [Arg Term]
forall a. Subst a => Nat -> a -> a
raise (Telescope -> Nat
forall a. Sized a => a -> Nat
size (UnifyState -> Telescope
eqTel UnifyState
s) Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
k) [Arg Term]
pars)
      case (Term
u, Term
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 TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Nat
-> Type
-> QName
-> [Arg Term]
-> [Arg Term]
-> ConHead
-> UnifyStep
Injectivity Nat
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 TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Nat -> Type -> QName -> [Arg Term] -> Term -> Term -> UnifyStep
Conflict Nat
k Type
a QName
d [Arg Term]
pars Term
u Term
v
        (Var Nat
i []  , Term
v         ) -> Nat -> Term -> ListT TCM UnifyStep -> ListT TCM UnifyStep
forall {m :: * -> *} {a} {b}.
(ForceNotFree a, Reduce a, MonadReduce m, Free a, MonadPlus m) =>
Nat -> a -> m b -> m b
ifOccursStronglyRigid Nat
i Term
v (ListT TCM UnifyStep -> ListT TCM UnifyStep)
-> ListT TCM UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ UnifyStep -> ListT TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Nat -> Type -> QName -> [Arg Term] -> Nat -> Term -> UnifyStep
Cycle Nat
k Type
a QName
d [Arg Term]
pars Nat
i Term
v
        (Term
u         , Var Nat
j []  ) -> Nat -> Term -> ListT TCM UnifyStep -> ListT TCM UnifyStep
forall {m :: * -> *} {a} {b}.
(ForceNotFree a, Reduce a, MonadReduce m, Free a, MonadPlus m) =>
Nat -> a -> m b -> m b
ifOccursStronglyRigid Nat
j Term
u (ListT TCM UnifyStep -> ListT TCM UnifyStep)
-> ListT TCM UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ UnifyStep -> ListT TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Nat -> Type -> QName -> [Arg Term] -> Nat -> Term -> UnifyStep
Cycle Nat
k Type
a QName
d [Arg Term]
pars Nat
j Term
u
        (Term, Term)
_ -> ListT TCM UnifyStep
forall a. ListT TCM a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    Term
_ -> ListT TCM UnifyStep
forall a. ListT TCM a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  where
    ifOccursStronglyRigid :: Nat -> a -> m b -> m b
ifOccursStronglyRigid Nat
i a
u m b
ret = do
        -- Call forceNotFree to reduce u as far as possible
        -- around any occurrences of i
        (IntMap IsFree
_ , a
u) <- IntSet -> a -> m (IntMap IsFree, a)
forall a (m :: * -> *).
(ForceNotFree a, Reduce a, MonadReduce m) =>
IntSet -> a -> m (IntMap IsFree, a)
forceNotFree (Nat -> IntSet
forall el coll. Singleton el coll => el -> coll
singleton Nat
i) a
u
        case Nat -> a -> Maybe FlexRig
forall a. Free a => Nat -> a -> Maybe FlexRig
flexRigOccurrenceIn Nat
i a
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 :: Nat -> UnifyStrategy
checkEqualityStrategy Nat
k UnifyState
s = do
  let Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v = Nat -> UnifyState -> Equality
getEquality Nat
k UnifyState
s
      n :: Nat
n = UnifyState -> Nat
eqCount UnifyState
s
  Type
ha <- Maybe Type -> ListT TCM Type
forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP (Maybe Type -> ListT TCM Type) -> Maybe Type -> ListT TCM Type
forall a b. (a -> b) -> a -> b
$ Nat -> Type -> Maybe Type
forall a. (Free a, Subst a) => Nat -> a -> Maybe a
isHom Nat
n Type
a
  UnifyStep -> ListT TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Nat -> Type -> Term -> Term -> UnifyStep
Deletion Nat
k Type
ha Term
u Term
v

literalStrategy :: Int -> UnifyStrategy
literalStrategy :: Nat -> UnifyStrategy
literalStrategy Nat
k UnifyState
s = do
  let n :: Nat
n = UnifyState -> Nat
eqCount UnifyState
s
  Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v <- Equality -> ListT TCM Equality
forall (m :: * -> *).
(HasBuiltins m, HasOptions m) =>
Equality -> m Equality
eqUnLevel (Equality -> ListT TCM Equality) -> Equality -> ListT TCM Equality
forall a b. (a -> b) -> a -> b
$ Nat -> UnifyState -> Equality
getEquality Nat
k UnifyState
s
  Type
ha <- Maybe Type -> ListT TCM Type
forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP (Maybe Type -> ListT TCM Type) -> Maybe Type -> ListT TCM Type
forall a b. (a -> b) -> a -> b
$ Nat -> Type -> Maybe Type
forall a. (Free a, Subst a) => Nat -> a -> Maybe a
isHom Nat
n Type
a
  (Term
u, Term
v) <- (Term, Term) -> ListT TCM (Term, Term)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term
u, Term
v)
  case (Term
u , Term
v) of
    (Lit Literal
l1 , Lit Literal
l2)
     | Literal
l1 Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l2  -> UnifyStep -> ListT TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Nat -> Type -> Term -> Term -> UnifyStep
Deletion Nat
k Type
ha Term
u Term
v
     | Bool
otherwise -> UnifyStep -> ListT TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Nat -> Type -> Literal -> Literal -> UnifyStep
LitConflict Nat
k Type
ha Literal
l1 Literal
l2
    (Term, Term)
_ -> ListT TCM UnifyStep
forall a. ListT TCM a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

etaExpandVarStrategy :: Int -> UnifyStrategy
etaExpandVarStrategy :: Nat -> UnifyStrategy
etaExpandVarStrategy Nat
k UnifyState
s = do
  Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v <- Equality -> ListT TCM Equality
forall (m :: * -> *).
(HasBuiltins m, HasOptions m) =>
Equality -> m Equality
eqUnLevel (Equality -> ListT TCM Equality)
-> ListT TCM Equality -> ListT TCM Equality
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Nat -> UnifyState -> ListT TCM Equality
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Nat -> UnifyState -> m Equality
getReducedEquality Nat
k UnifyState
s
  Term -> Term -> Type -> UnifyStrategy
shouldEtaExpand Term
u Term
v Type
a UnifyState
s ListT TCM UnifyStep -> ListT TCM UnifyStep -> ListT TCM UnifyStep
forall a. ListT TCM a -> ListT TCM a -> ListT TCM a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Term -> Term -> Type -> UnifyStrategy
shouldEtaExpand Term
v Term
u Type
a UnifyState
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 Nat
i Elims
es) Term
v Type
a UnifyState
s = do
      FlexibleVar Nat
fi       <- Maybe (FlexibleVar Nat) -> ListT TCM (FlexibleVar Nat)
forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP (Maybe (FlexibleVar Nat) -> ListT TCM (FlexibleVar Nat))
-> Maybe (FlexibleVar Nat) -> ListT TCM (FlexibleVar Nat)
forall a b. (a -> b) -> a -> b
$ Nat -> FlexibleVars -> Maybe (FlexibleVar Nat)
findFlexible Nat
i (UnifyState -> FlexibleVars
flexVars UnifyState
s)
      String -> Nat -> TCMT IO Doc -> ListT TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
50 (TCMT IO Doc -> ListT TCM ()) -> TCMT IO Doc -> ListT TCM ()
forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"Found flexible variable " 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 (Nat -> String
forall a. Show a => a -> String
show Nat
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 :: Nat
k  = UnifyState -> Nat
varCount UnifyState
s Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
i -- position of var i in telescope
          b0 :: Type
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
$ Nat -> UnifyState -> Dom Type
getVarTypeUnraised Nat
k UnifyState
s
      Type
b         <- Telescope -> ListT TCM Type -> ListT TCM Type
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (ListTel -> Telescope
telFromList (ListTel -> Telescope) -> ListTel -> Telescope
forall a b. (a -> b) -> a -> b
$ Nat -> ListTel -> ListTel
forall a. Nat -> [a] -> [a]
take Nat
k (ListTel -> ListTel) -> ListTel -> ListTel
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList (Telescope -> ListTel) -> Telescope -> ListTel
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
varTel UnifyState
s) (ListT TCM Type -> ListT TCM Type)
-> ListT TCM Type -> ListT TCM Type
forall a b. (a -> b) -> a -> b
$ Type -> ListT TCM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
b0
      (QName
d, [Arg Term]
pars) <- ListT TCM (Maybe (QName, [Arg Term]))
-> ListT TCM (QName, [Arg Term])
forall (m :: * -> *) a. MonadPlus m => m (Maybe a) -> m a
catMaybesMP (ListT TCM (Maybe (QName, [Arg Term]))
 -> ListT TCM (QName, [Arg Term]))
-> ListT TCM (Maybe (QName, [Arg Term]))
-> ListT TCM (QName, [Arg Term])
forall a b. (a -> b) -> a -> b
$ Type -> ListT TCM (Maybe (QName, [Arg Term]))
forall (m :: * -> *).
HasConstInfo m =>
Type -> m (Maybe (QName, [Arg Term]))
isEtaRecordType Type
b
      [(ProjOrigin, QName)]
ps        <- Maybe [(ProjOrigin, QName)] -> ListT TCM [(ProjOrigin, QName)]
forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP (Maybe [(ProjOrigin, QName)] -> ListT TCM [(ProjOrigin, QName)])
-> Maybe [(ProjOrigin, QName)] -> ListT TCM [(ProjOrigin, QName)]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [(ProjOrigin, QName)]
forall t. [Elim' t] -> Maybe [(ProjOrigin, QName)]
allProjElims Elims
es
      Bool -> ListT TCM ()
forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
guard (Bool -> ListT TCM ()) -> ListT TCM Bool -> ListT TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [ListT TCM Bool] -> ListT TCM Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
orM
        [ Bool -> ListT TCM Bool
forall a. a -> ListT TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> ListT TCM Bool) -> Bool -> ListT TCM Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [(ProjOrigin, QName)] -> Bool
forall a. Null a => a -> Bool
null [(ProjOrigin, QName)]
ps
        , Term -> ListT TCM Bool
forall {f :: * -> *}. HasConstInfo f => Term -> f Bool
isRecCon Term
v  -- is the other term a record constructor?
        , (Bool -> Either Blocker Bool
forall a b. b -> Either a b
Right Bool
True Either Blocker Bool -> Either Blocker Bool -> Bool
forall a. Eq a => a -> a -> Bool
==) (Either Blocker Bool -> Bool)
-> ListT TCM (Either Blocker Bool) -> ListT TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BlockT (ListT TCM) Bool -> ListT TCM (Either Blocker Bool)
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (QName -> [Arg Term] -> BlockT (ListT TCM) Bool
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
QName -> [Arg Term] -> m Bool
isSingletonRecord QName
d [Arg Term]
pars)
        ]
      String -> Nat -> TCMT IO Doc -> ListT TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
50 (TCMT IO Doc -> ListT TCM ()) -> TCMT IO Doc -> ListT TCM ()
forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"with projections " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [QName] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [QName] -> m Doc
prettyTCM (((ProjOrigin, QName) -> QName) -> [(ProjOrigin, QName)] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map (ProjOrigin, QName) -> QName
forall a b. (a, b) -> b
snd [(ProjOrigin, QName)]
ps)
      String -> Nat -> TCMT IO Doc -> ListT TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
50 (TCMT IO Doc -> ListT TCM ()) -> TCMT IO Doc -> ListT TCM ()
forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"at record type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d
      UnifyStep -> ListT TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ FlexibleVar Nat -> QName -> [Arg Term] -> UnifyStep
EtaExpandVar FlexibleVar Nat
fi QName
d [Arg Term]
pars
    shouldEtaExpand Term
_ Term
_ Type
_ UnifyState
_ = ListT TCM UnifyStep
forall a. ListT TCM 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 :: * -> *).
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 :: Nat -> UnifyStrategy
etaExpandEquationStrategy Nat
k UnifyState
s = do
  -- Andreas, 2019-02-23, re #3578, is the following reduce redundant?
  Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v <- Nat -> UnifyState -> ListT TCM Equality
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Nat -> UnifyState -> m Equality
getReducedEqualityUnraised Nat
k UnifyState
s
  (QName
d, [Arg Term]
pars) <- ListT TCM (Maybe (QName, [Arg Term]))
-> ListT TCM (QName, [Arg Term])
forall (m :: * -> *) a. MonadPlus m => m (Maybe a) -> m a
catMaybesMP (ListT TCM (Maybe (QName, [Arg Term]))
 -> ListT TCM (QName, [Arg Term]))
-> ListT TCM (Maybe (QName, [Arg Term]))
-> ListT TCM (QName, [Arg Term])
forall a b. (a -> b) -> a -> b
$ Telescope
-> ListT TCM (Maybe (QName, [Arg Term]))
-> ListT TCM (Maybe (QName, [Arg Term]))
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 (ListT TCM (Maybe (QName, [Arg Term]))
 -> ListT TCM (Maybe (QName, [Arg Term])))
-> ListT TCM (Maybe (QName, [Arg Term]))
-> ListT TCM (Maybe (QName, [Arg Term]))
forall a b. (a -> b) -> a -> b
$ Type -> ListT TCM (Maybe (QName, [Arg Term]))
forall (m :: * -> *).
HasConstInfo m =>
Type -> m (Maybe (QName, [Arg Term]))
isEtaRecordType Type
a
  Bool -> ListT TCM ()
forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
guard (Bool -> ListT TCM ()) -> ListT TCM Bool -> ListT TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [ListT TCM Bool] -> ListT TCM Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
orM
    [ (Bool -> Either Blocker Bool
forall a b. b -> Either a b
Right Bool
True Either Blocker Bool -> Either Blocker Bool -> Bool
forall a. Eq a => a -> a -> Bool
==) (Either Blocker Bool -> Bool)
-> ListT TCM (Either Blocker Bool) -> ListT TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BlockT (ListT TCM) Bool -> ListT TCM (Either Blocker Bool)
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (QName -> [Arg Term] -> BlockT (ListT TCM) Bool
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
QName -> [Arg Term] -> m Bool
isSingletonRecord QName
d [Arg Term]
pars)
    , Term -> ListT TCM Bool
forall (m :: * -> *). PureTCM m => Term -> m Bool
shouldProject Term
u
    , Term -> ListT TCM Bool
forall (m :: * -> *). PureTCM m => Term -> m Bool
shouldProject Term
v
    ]
  UnifyStep -> ListT TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Nat -> QName -> [Arg Term] -> UnifyStep
EtaExpandEquation Nat
k QName
d [Arg Term]
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, HasBuiltins 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 :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, RecordData))
isRecordConstructor (ConHead -> QName
conName ConHead
c)

      Var Nat
_ 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 String
s Elims
_  -> String -> m Bool
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
s

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

simplifySizesStrategy :: Int -> UnifyStrategy
simplifySizesStrategy :: Nat -> UnifyStrategy
simplifySizesStrategy Nat
k UnifyState
s = do
  QName -> Bool
isSizeName <- ListT TCM (QName -> Bool)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (QName -> Bool)
isSizeNameTest
  Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v <- Nat -> UnifyState -> ListT TCM Equality
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Nat -> UnifyState -> m Equality
getReducedEquality Nat
k UnifyState
s
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
a of
    Def QName
d Elims
_ -> do
      Bool -> ListT TCM ()
forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
guard (Bool -> ListT TCM ()) -> Bool -> ListT TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Bool
isSizeName QName
d
      SizeView
su <- Term -> ListT TCM SizeView
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
u
      SizeView
sv <- Term -> ListT TCM SizeView
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
v
      case (SizeView
su, SizeView
sv) of
        (SizeSuc Term
u, SizeSuc Term
v) -> UnifyStep -> ListT TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Nat -> Term -> Term -> UnifyStep
StripSizeSuc Nat
k Term
u Term
v
        (SizeSuc Term
u, SizeView
SizeInf  ) -> UnifyStep -> ListT TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Nat -> Term -> Term -> UnifyStep
StripSizeSuc Nat
k Term
u Term
v
        (SizeView
SizeInf  , SizeSuc Term
v) -> UnifyStep -> ListT TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Nat -> Term -> Term -> UnifyStep
StripSizeSuc Nat
k Term
u Term
v
        (SizeView, SizeView)
_ -> ListT TCM UnifyStep
forall a. ListT TCM a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    Term
_ -> ListT TCM UnifyStep
forall a. ListT TCM a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

injectiveTypeConStrategy :: Int -> UnifyStrategy
injectiveTypeConStrategy :: Nat -> UnifyStrategy
injectiveTypeConStrategy Nat
k UnifyState
s = do
  Bool
injTyCon <- PragmaOptions -> Bool
optInjectiveTypeConstructors (PragmaOptions -> Bool)
-> ListT TCM PragmaOptions -> ListT TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ListT TCM PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  Bool -> ListT TCM ()
forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
guard Bool
injTyCon
  Equality
eq <- Equality -> ListT TCM Equality
forall (m :: * -> *).
(HasBuiltins m, HasOptions m) =>
Equality -> m Equality
eqUnLevel (Equality -> ListT TCM Equality)
-> ListT TCM Equality -> ListT TCM Equality
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Nat -> UnifyState -> ListT TCM Equality
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Nat -> UnifyState -> m Equality
getReducedEquality Nat
k UnifyState
s
  case Equality
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 be a data, record or axiom
      Definition
def <- QName -> ListT TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
      Bool -> ListT TCM ()
forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
guard (Bool -> ListT TCM ()) -> Bool -> ListT TCM ()
forall a b. (a -> b) -> a -> b
$ case Definition -> Defn
theDef Definition
def of
                Datatype{} -> Bool
True
                Record{}   -> Bool
True
                Axiom{}    -> Bool
True
                DataOrRecSig{} -> Bool
True
                AbstractDefn{} -> Bool
False -- True triggers issue #2250
                Function{}   -> Bool
False
                Primitive{}  -> Bool
False
                PrimitiveSort{} -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
                GeneralizableVar{} -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
                Constructor{} -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__  -- Never a type!
      let us :: [Arg Term]
us = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
          vs :: [Arg Term]
vs = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es'
      UnifyStep -> ListT TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Nat -> QName -> [Arg Term] -> [Arg Term] -> UnifyStep
TypeConInjectivity Nat
k QName
d [Arg Term]
us [Arg Term]
vs
    Equality
_ -> ListT TCM UnifyStep
forall a. ListT TCM a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

injectivePragmaStrategy :: Int -> UnifyStrategy
injectivePragmaStrategy :: Nat -> UnifyStrategy
injectivePragmaStrategy Nat
k UnifyState
s = do
  Equality
eq <- Equality -> ListT TCM Equality
forall (m :: * -> *).
(HasBuiltins m, HasOptions m) =>
Equality -> m Equality
eqUnLevel (Equality -> ListT TCM Equality)
-> ListT TCM Equality -> ListT TCM Equality
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Nat -> UnifyState -> ListT TCM Equality
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Nat -> UnifyState -> m Equality
getReducedEquality Nat
k UnifyState
s
  case Equality
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
      Definition
def <- QName -> ListT TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
      Bool -> ListT TCM ()
forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
guard (Bool -> ListT TCM ()) -> Bool -> ListT TCM ()
forall a b. (a -> b) -> a -> b
$ Definition -> Bool
defInjective Definition
def
      let us :: [Arg Term]
us = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
          vs :: [Arg Term]
vs = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es'
      UnifyStep -> ListT TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Nat -> QName -> [Arg Term] -> [Arg Term] -> UnifyStep
TypeConInjectivity Nat
k QName
d [Arg Term]
us [Arg Term]
vs
    Equality
_ -> ListT TCM UnifyStep
forall a. ListT TCM a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

skipIrrelevantStrategy :: Int -> UnifyStrategy
skipIrrelevantStrategy :: Nat -> UnifyStrategy
skipIrrelevantStrategy Nat
k UnifyState
s = do
  let Equal Dom Type
a Term
_ Term
_ = Nat -> UnifyState -> Equality
getEquality Nat
k UnifyState
s                                 -- reduce not necessary
  Telescope -> ListT TCM () -> ListT TCM ()
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 TCM () -> ListT TCM ()) -> ListT TCM () -> ListT TCM ()
forall a b. (a -> b) -> a -> b
$
    Bool -> ListT TCM ()
forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
guard (Bool -> ListT TCM ())
-> (Either Blocker Bool -> Bool)
-> Either Blocker Bool
-> ListT TCM ()
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 TCM ())
-> ListT TCM (Either Blocker Bool) -> ListT TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< BlockT (ListT TCM) Bool -> ListT TCM (Either Blocker Bool)
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (Dom Type -> BlockT (ListT TCM) Bool
forall a (m :: * -> *).
(LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
 MonadBlock m) =>
a -> m Bool
isIrrelevantOrPropM Dom Type
a)  -- reduction takes place here
  -- TODO: do something in case the above is blocked (i.e. `Left b`)
  UnifyStep -> ListT TCM UnifyStep
forall a. a -> ListT TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyStep -> ListT TCM UnifyStep)
-> UnifyStep -> ListT TCM UnifyStep
forall a b. (a -> b) -> a -> b
$ Nat -> UnifyStep
SkipIrrelevantEquation Nat
k


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

unifyStep
  :: UnifyState -> UnifyStep -> UnifyStepT TCM (UnificationResult' UnifyState)
unifyStep :: UnifyState
-> UnifyStep -> UnifyStepT TCM (UnificationResult' UnifyState)
unifyStep UnifyState
s Deletion{ deleteAt :: UnifyStep -> Nat
deleteAt = Nat
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
    Either Blocker Bool
isReflexive <- Telescope
-> WriterT UnifyOutput TCM (Either Blocker Bool)
-> WriterT UnifyOutput TCM (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 TCM (Either Blocker Bool)
 -> WriterT UnifyOutput TCM (Either Blocker Bool))
-> WriterT UnifyOutput TCM (Either Blocker Bool)
-> WriterT UnifyOutput TCM (Either Blocker Bool)
forall a b. (a -> b) -> a -> b
$ Type
-> Term -> Term -> WriterT UnifyOutput TCM (Either Blocker Bool)
forall (m :: * -> *).
PureTCM m =>
Type -> Term -> Term -> m (Either Blocker Bool)
pureEqualTermB Type
a Term
u Term
v
    Bool
withoutK <- WriterT UnifyOutput TCM Bool
forall (m :: * -> *). HasOptions m => m Bool
withoutKOption
    Bool
splitOnStrict <- (TCEnv -> Bool) -> WriterT UnifyOutput TCM Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envSplitOnStrict
    case Either Blocker Bool
isReflexive of
      Left Blocker
block   -> UnificationResult' UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT TCM (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 TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []
      Right Bool
True | Bool
withoutK Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
splitOnStrict
                   -> UnificationResult' UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT TCM (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', PatternSubstitution
sigma) = Nat -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
solveEq Nat
k Term
u UnifyState
s
        PatternSubstitution -> WriterT UnifyOutput TCM ()
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
sigma
        UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies (UnifyState -> UnificationResult' UnifyState)
-> WriterT UnifyOutput TCM UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Telescope -> WriterT UnifyOutput TCM Telescope)
-> UnifyState -> WriterT UnifyOutput TCM UnifyState
Lens' UnifyState Telescope
lensEqTel Telescope -> WriterT UnifyOutput TCM 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 TCM (UnificationResult' UnifyState)
forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m) =>
RetryNormalised
-> UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
solutionStep RetryNormalised
RetryNormalised UnifyState
s UnifyStep
step

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

  -- Split equation telescope into parts before and after current equation
  let (ListTel
eqListTel1, Dom (String, Type)
_ : ListTel
eqListTel2) = Nat -> ListTel -> (ListTel, ListTel)
forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
k (ListTel -> (ListTel, ListTel)) -> ListTel -> (ListTel, ListTel)
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (String, 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
  Definition
cdef  <- ConHead -> WriterT UnifyOutput TCM Definition
forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
getConInfo ConHead
c
  let ctype :: Type
ctype  = Definition -> Type
defType Definition
cdef Type -> [Arg Term] -> Type
`piApply` [Arg Term]
pars
  Telescope
-> WriterT UnifyOutput TCM () -> WriterT UnifyOutput TCM ()
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` Telescope
eqTel1) (WriterT UnifyOutput TCM () -> WriterT UnifyOutput TCM ())
-> WriterT UnifyOutput TCM () -> WriterT UnifyOutput TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Nat -> TCMT IO Doc -> WriterT UnifyOutput TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
40 (TCMT IO Doc -> WriterT UnifyOutput TCM ())
-> TCMT IO Doc -> WriterT UnifyOutput TCM ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Constructor type: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
ctype
  TelV Telescope
ctel Type
ctarget <- Telescope
-> WriterT UnifyOutput TCM (TelV Type)
-> WriterT UnifyOutput TCM (TelV Type)
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` Telescope
eqTel1) (WriterT UnifyOutput TCM (TelV Type)
 -> WriterT UnifyOutput TCM (TelV Type))
-> WriterT UnifyOutput TCM (TelV Type)
-> WriterT UnifyOutput TCM (TelV Type)
forall a b. (a -> b) -> a -> b
$ Type -> WriterT UnifyOutput TCM (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
ctype
  let cixs :: [Arg Term]
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 = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
                 in  Nat -> [Arg Term] -> [Arg Term]
forall a. Nat -> [a] -> [a]
drop ([Arg Term] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Arg Term]
pars) [Arg Term]
args
               Term
_ -> [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__

  -- Get index telescope of the datatype
  Type
dtype    <- (Type -> [Arg Term] -> Type
`piApply` [Arg Term]
pars) (Type -> Type) -> (Definition -> Type) -> Definition -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType (Definition -> Type)
-> WriterT UnifyOutput TCM Definition
-> WriterT UnifyOutput TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> WriterT UnifyOutput TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
  Telescope
-> WriterT UnifyOutput TCM () -> WriterT UnifyOutput TCM ()
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` Telescope
eqTel1) (WriterT UnifyOutput TCM () -> WriterT UnifyOutput TCM ())
-> WriterT UnifyOutput TCM () -> WriterT UnifyOutput TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Nat -> TCMT IO Doc -> WriterT UnifyOutput TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
40 (TCMT IO Doc -> WriterT UnifyOutput TCM ())
-> TCMT IO Doc -> WriterT UnifyOutput TCM ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Datatype type: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
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
hduTel = Telescope
eqTel1 Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
ctel
      notforced :: [IsForced]
notforced = Nat -> IsForced -> [IsForced]
forall a. Nat -> a -> [a]
replicate (Telescope -> Nat
forall a. Sized a => a -> Nat
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.
  UnificationResult'
  (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
   Either NoLeftInv (Substitution, Substitution))
res <- TCMT
  IO
  (UnificationResult'
     (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
      Either NoLeftInv (Substitution, Substitution)))
-> WriterT
     UnifyOutput
     TCM
     (UnificationResult'
        (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
         Either NoLeftInv (Substitution, Substitution)))
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
   (UnificationResult'
      (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
       Either NoLeftInv (Substitution, Substitution)))
 -> WriterT
      UnifyOutput
      TCM
      (UnificationResult'
         (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
          Either NoLeftInv (Substitution, Substitution))))
-> TCMT
     IO
     (UnificationResult'
        (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
         Either NoLeftInv (Substitution, Substitution)))
-> WriterT
     UnifyOutput
     TCM
     (UnificationResult'
        (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
         Either NoLeftInv (Substitution, Substitution)))
forall a b. (a -> b) -> a -> b
$ Telescope
-> TCMT
     IO
     (UnificationResult'
        (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
         Either NoLeftInv (Substitution, Substitution)))
-> TCMT
     IO
     (UnificationResult'
        (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
         Either NoLeftInv (Substitution, Substitution)))
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) (TCMT
   IO
   (UnificationResult'
      (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
       Either NoLeftInv (Substitution, Substitution)))
 -> TCMT
      IO
      (UnificationResult'
         (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
          Either NoLeftInv (Substitution, Substitution))))
-> TCMT
     IO
     (UnificationResult'
        (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
         Either NoLeftInv (Substitution, Substitution)))
-> TCMT
     IO
     (UnificationResult'
        (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
         Either NoLeftInv (Substitution, Substitution)))
forall a b. (a -> b) -> a -> b
$ Maybe NoLeftInv
-> Telescope
-> FlexibleVars
-> Type
-> [Arg Term]
-> [Arg Term]
-> TCMT
     IO
     (UnificationResult'
        (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
         Either NoLeftInv (Substitution, Substitution)))
unifyIndices' (NoLeftInv -> Maybe NoLeftInv
forall a. a -> Maybe a
Just NoLeftInv
forall a. HasCallStack => a
__IMPOSSIBLE__)
           Telescope
hduTel
           ([IsForced] -> Telescope -> FlexibleVars
allFlexVars [IsForced]
notforced Telescope
hduTel)
           (Nat -> Type -> Type
forall a. Subst a => Nat -> a -> a
raise (Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
ctel) Type
dtype)
           (Nat -> [Arg Term] -> [Arg Term]
forall a. Subst a => Nat -> a -> a
raise (Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
ctel) [Arg Term]
ixs)
           [Arg Term]
cixs
  case UnificationResult'
  (Telescope, PatternSubstitution, [NamedArg (Pattern' DBPatVar)],
   Either NoLeftInv (Substitution, Substitution))
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 TCM (UnificationResult' UnifyState)
forall a. HasCallStack => a
__IMPOSSIBLE__

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

    -- Higher-dimensional unification has failed. If not --without-K,
    -- we can simply ignore the higher-dimensional equations and
    -- simplify the equation as in the non-indexed case.
    UnifyStuck [UnificationFailure]
_ | Bool -> Bool
not Bool
withoutK -> do
      -- using the same variable names as in the case where hdu succeeds.
      let eqTel1' :: Telescope
eqTel1' = Telescope
eqTel1 Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
ctel
          rho1 :: PatternSubstitution
rho1    = Nat -> PatternSubstitution
forall a. Nat -> Substitution' a
raiseS (Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
ctel)
          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
$ Telescope -> [NamedArg (Pattern' DBPatVar)]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
ctel
          rho3 :: PatternSubstitution
rho3    = Pattern' DBPatVar -> PatternSubstitution -> PatternSubstitution
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Pattern' DBPatVar
ceq PatternSubstitution
rho1
          eqTel2' :: Telescope
eqTel2' = PatternSubstitution -> Telescope -> Telescope
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho3 Telescope
eqTel2
          eqTel' :: Telescope
eqTel'  = Telescope
eqTel1' Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
eqTel2'
          rho :: PatternSubstitution
rho     = Nat -> PatternSubstitution -> PatternSubstitution
forall a. Nat -> Substitution' a -> Substitution' a
liftS (Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
eqTel2) PatternSubstitution
rho3

      PatternSubstitution -> WriterT UnifyOutput TCM ()
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
rho

      Telescope
eqTel' <- Telescope
-> WriterT UnifyOutput TCM Telescope
-> WriterT UnifyOutput TCM 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 TCM Telescope
 -> WriterT UnifyOutput TCM Telescope)
-> WriterT UnifyOutput TCM Telescope
-> WriterT UnifyOutput TCM Telescope
forall a b. (a -> b) -> a -> b
$ Telescope -> WriterT UnifyOutput TCM 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
      ([Arg Term]
lhs', [Arg Term]
rhs') <- Telescope
-> WriterT UnifyOutput TCM ([Arg Term], [Arg Term])
-> WriterT UnifyOutput TCM ([Arg Term], [Arg Term])
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 TCM ([Arg Term], [Arg Term])
 -> WriterT UnifyOutput TCM ([Arg Term], [Arg Term]))
-> WriterT UnifyOutput TCM ([Arg Term], [Arg Term])
-> WriterT UnifyOutput TCM ([Arg Term], [Arg Term])
forall a b. (a -> b) -> a -> b
$ do
        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 PatternSubstitution
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
        (Match Term
lhsMatch, [Arg Term]
_) <- [NamedArg (Pattern' DBPatVar)]
-> [Arg Term] -> WriterT UnifyOutput TCM (Match Term, [Arg Term])
forall (m :: * -> *).
MonadMatch m =>
[NamedArg (Pattern' DBPatVar)]
-> [Arg Term] -> m (Match Term, [Arg Term])
Match.matchPatterns [NamedArg (Pattern' DBPatVar)]
ps ([Arg Term] -> WriterT UnifyOutput TCM (Match Term, [Arg Term]))
-> [Arg Term] -> WriterT UnifyOutput TCM (Match Term, [Arg Term])
forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqLHS UnifyState
s
        (Match Term
rhsMatch, [Arg Term]
_) <- [NamedArg (Pattern' DBPatVar)]
-> [Arg Term] -> WriterT UnifyOutput TCM (Match Term, [Arg Term])
forall (m :: * -> *).
MonadMatch m =>
[NamedArg (Pattern' DBPatVar)]
-> [Arg Term] -> m (Match Term, [Arg Term])
Match.matchPatterns [NamedArg (Pattern' DBPatVar)]
ps ([Arg Term] -> WriterT UnifyOutput TCM (Match Term, [Arg Term]))
-> [Arg Term] -> WriterT UnifyOutput TCM (Match Term, [Arg Term])
forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqRHS UnifyState
s
        case (Match Term
lhsMatch, Match Term
rhsMatch) of
          (Match.Yes Simplification
_ IntMap (Arg Term)
lhs', Match.Yes Simplification
_ IntMap (Arg Term)
rhs') -> ([Arg Term], [Arg Term])
-> WriterT UnifyOutput TCM ([Arg Term], [Arg Term])
forall a. a -> WriterT UnifyOutput TCM 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 -> Nat -> IntMap (Arg Term) -> [Arg Term]
forall a. Empty -> Nat -> IntMap (Arg a) -> [Arg a]
Match.matchedArgs Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> Nat
forall a. Sized a => a -> Nat
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 -> Nat -> IntMap (Arg Term) -> [Arg Term]
forall a. Empty -> Nat -> IntMap (Arg a) -> [Arg a]
Match.matchedArgs Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
eqTel') IntMap (Arg Term)
rhs')
          (Match Term, Match Term)
_ -> WriterT UnifyOutput TCM ([Arg Term], [Arg Term])
forall a. HasCallStack => a
__IMPOSSIBLE__

      UnificationResult' UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies (UnifyState -> UnificationResult' UnifyState)
-> UnifyState -> UnificationResult' UnifyState
forall a b. (a -> b) -> a -> b
$ UnifyState
s { eqTel = eqTel' , eqLHS = lhs' , eqRHS = rhs' }


    UnifyStuck [UnificationFailure]
_ -> let n :: Nat
n           = UnifyState -> Nat
eqCount UnifyState
s
                        Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v = Nat -> UnifyState -> Equality
getEquality Nat
k UnifyState
s
                    in UnificationResult' UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT TCM (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
                         (Nat -> Term -> Term
forall a. Subst a => Nat -> a -> a
raise Nat
n Term
u) (Nat -> Term -> Term
forall a. Subst a => Nat -> a -> a
raise Nat
n Term
v) (Nat -> [Arg Term] -> [Arg Term]
forall a. Subst a => Nat -> a -> a
raise (Nat
nNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
k) [Arg Term]
ixs)]

    Unifies (Telescope
eqTel1', PatternSubstitution
rho0, [NamedArg (Pattern' DBPatVar)]
_, Either NoLeftInv (Substitution, Substitution)
_) -> do
      -- Split ps0 into parts for eqTel1 and ctel
      let (PatternSubstitution
rho1, PatternSubstitution
rho2) = Nat
-> PatternSubstitution
-> (PatternSubstitution, PatternSubstitution)
forall a.
Nat -> Substitution' a -> (Substitution' a, Substitution' a)
splitS (Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
ctel) PatternSubstitution
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 PatternSubstitution
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 :: PatternSubstitution
rho3    = Pattern' DBPatVar -> PatternSubstitution -> PatternSubstitution
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Pattern' DBPatVar
ceq PatternSubstitution
rho1
          eqTel2' :: Telescope
eqTel2' = PatternSubstitution -> Telescope -> Telescope
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho3 Telescope
eqTel2
          eqTel' :: Telescope
eqTel'  = Telescope
eqTel1' Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
eqTel2'
          rho :: PatternSubstitution
rho     = Nat -> PatternSubstitution -> PatternSubstitution
forall a. Nat -> Substitution' a -> Substitution' a
liftS (Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
eqTel2) PatternSubstitution
rho3

      PatternSubstitution -> WriterT UnifyOutput TCM ()
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
rho

      Telescope
eqTel' <- Telescope
-> WriterT UnifyOutput TCM Telescope
-> WriterT UnifyOutput TCM 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 TCM Telescope
 -> WriterT UnifyOutput TCM Telescope)
-> WriterT UnifyOutput TCM Telescope
-> WriterT UnifyOutput TCM Telescope
forall a b. (a -> b) -> a -> b
$ Telescope -> WriterT UnifyOutput TCM 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
      ([Arg Term]
lhs', [Arg Term]
rhs') <- Telescope
-> WriterT UnifyOutput TCM ([Arg Term], [Arg Term])
-> WriterT UnifyOutput TCM ([Arg Term], [Arg Term])
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 TCM ([Arg Term], [Arg Term])
 -> WriterT UnifyOutput TCM ([Arg Term], [Arg Term]))
-> WriterT UnifyOutput TCM ([Arg Term], [Arg Term])
-> WriterT UnifyOutput TCM ([Arg Term], [Arg Term])
forall a b. (a -> b) -> a -> b
$ do
        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 PatternSubstitution
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
        (Match Term
lhsMatch, [Arg Term]
_) <- [NamedArg (Pattern' DBPatVar)]
-> [Arg Term] -> WriterT UnifyOutput TCM (Match Term, [Arg Term])
forall (m :: * -> *).
MonadMatch m =>
[NamedArg (Pattern' DBPatVar)]
-> [Arg Term] -> m (Match Term, [Arg Term])
Match.matchPatterns [NamedArg (Pattern' DBPatVar)]
ps ([Arg Term] -> WriterT UnifyOutput TCM (Match Term, [Arg Term]))
-> [Arg Term] -> WriterT UnifyOutput TCM (Match Term, [Arg Term])
forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqLHS UnifyState
s
        (Match Term
rhsMatch, [Arg Term]
_) <- [NamedArg (Pattern' DBPatVar)]
-> [Arg Term] -> WriterT UnifyOutput TCM (Match Term, [Arg Term])
forall (m :: * -> *).
MonadMatch m =>
[NamedArg (Pattern' DBPatVar)]
-> [Arg Term] -> m (Match Term, [Arg Term])
Match.matchPatterns [NamedArg (Pattern' DBPatVar)]
ps ([Arg Term] -> WriterT UnifyOutput TCM (Match Term, [Arg Term]))
-> [Arg Term] -> WriterT UnifyOutput TCM (Match Term, [Arg Term])
forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqRHS UnifyState
s
        case (Match Term
lhsMatch, Match Term
rhsMatch) of
          (Match.Yes Simplification
_ IntMap (Arg Term)
lhs', Match.Yes Simplification
_ IntMap (Arg Term)
rhs') -> ([Arg Term], [Arg Term])
-> WriterT UnifyOutput TCM ([Arg Term], [Arg Term])
forall a. a -> WriterT UnifyOutput TCM 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 -> Nat -> IntMap (Arg Term) -> [Arg Term]
forall a. Empty -> Nat -> IntMap (Arg a) -> [Arg a]
Match.matchedArgs Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> Nat
forall a. Sized a => a -> Nat
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 -> Nat -> IntMap (Arg Term) -> [Arg Term]
forall a. Empty -> Nat -> IntMap (Arg a) -> [Arg a]
Match.matchedArgs Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
eqTel') IntMap (Arg Term)
rhs')
          (Match Term, Match Term)
_ -> WriterT UnifyOutput TCM ([Arg Term], [Arg Term])
forall a. HasCallStack => a
__IMPOSSIBLE__

      UnificationResult' UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies (UnifyState -> UnificationResult' UnifyState)
-> UnifyState -> UnificationResult' UnifyState
forall a b. (a -> b) -> a -> b
$ UnifyState
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 TCM Bool
-> UnifyStepT TCM (UnificationResult' UnifyState)
-> UnifyStepT TCM (UnificationResult' UnifyState)
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> WriterT UnifyOutput TCM Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
consOfHIT (QName -> WriterT UnifyOutput TCM Bool)
-> QName -> WriterT UnifyOutput TCM Bool
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
h) (UnificationResult' UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []) (UnifyStepT TCM (UnificationResult' UnifyState)
 -> UnifyStepT TCM (UnificationResult' UnifyState))
-> UnifyStepT TCM (UnificationResult' UnifyState)
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ do
        UnificationResult' UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT TCM (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 TCM (UnificationResult' UnifyState)
forall a. HasCallStack => a
__IMPOSSIBLE__
unifyStep UnifyState
s Cycle
  { cycleVar :: UnifyStep -> Nat
cycleVar        = Nat
i
  , cycleOccursIn :: UnifyStep -> Term
cycleOccursIn   = Term
u
  } =
  case Term
u of
    Con ConHead
h ConInfo
_ Elims
_ -> do
      WriterT UnifyOutput TCM Bool
-> UnifyStepT TCM (UnificationResult' UnifyState)
-> UnifyStepT TCM (UnificationResult' UnifyState)
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> WriterT UnifyOutput TCM Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
consOfHIT (QName -> WriterT UnifyOutput TCM Bool)
-> QName -> WriterT UnifyOutput TCM Bool
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
h) (UnificationResult' UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []) (UnifyStepT TCM (UnificationResult' UnifyState)
 -> UnifyStepT TCM (UnificationResult' UnifyState))
-> UnifyStepT TCM (UnificationResult' UnifyState)
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ do
        UnificationResult' UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT TCM (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 -> Nat -> Term -> NegativeUnification
UnifyCycle (UnifyState -> Telescope
varTel UnifyState
s) Nat
i Term
u
    Term
_ -> UnifyStepT TCM (UnificationResult' UnifyState)
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

    liftFlexibles :: Int -> FlexibleVars -> FlexibleVars
    liftFlexibles :: Nat -> FlexibleVars -> FlexibleVars
liftFlexibles Nat
n FlexibleVars
fs = (FlexibleVar Nat -> Maybe (FlexibleVar Nat))
-> FlexibleVars -> FlexibleVars
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((Nat -> Maybe Nat) -> FlexibleVar Nat -> Maybe (FlexibleVar Nat)
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 ((Nat -> Maybe Nat) -> FlexibleVar Nat -> Maybe (FlexibleVar Nat))
-> (Nat -> Maybe Nat) -> FlexibleVar Nat -> Maybe (FlexibleVar Nat)
forall a b. (a -> b) -> a -> b
$ Nat -> Nat -> Maybe Nat
liftFlexible Nat
n) FlexibleVars
fs

unifyStep UnifyState
s EtaExpandEquation{ expandAt :: UnifyStep -> Nat
expandAt = Nat
k, expandRecordType :: UnifyStep -> QName
expandRecordType = QName
d, expandParameters :: UnifyStep -> [Arg Term]
expandParameters = [Arg Term]
pars } = do
  RecordData
recd  <- RecordData -> Maybe RecordData -> RecordData
forall a. a -> Maybe a -> a
fromMaybe RecordData
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe RecordData -> RecordData)
-> WriterT UnifyOutput TCM (Maybe RecordData)
-> WriterT UnifyOutput TCM RecordData
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> WriterT UnifyOutput TCM (Maybe RecordData)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe RecordData)
isRecord QName
d
  let delta :: Telescope
delta = RecordData -> Telescope
_recTel RecordData
recd Telescope -> [Arg Term] -> Telescope
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
pars
      c :: ConHead
c     = RecordData -> ConHead
_recConHead RecordData
recd
  [Arg Term]
lhs   <- [Arg Term] -> WriterT UnifyOutput TCM [Arg Term]
expandKth ([Arg Term] -> WriterT UnifyOutput TCM [Arg Term])
-> [Arg Term] -> WriterT UnifyOutput TCM [Arg Term]
forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqLHS UnifyState
s
  [Arg Term]
rhs   <- [Arg Term] -> WriterT UnifyOutput TCM [Arg Term]
expandKth ([Arg Term] -> WriterT UnifyOutput TCM [Arg Term])
-> [Arg Term] -> WriterT UnifyOutput TCM [Arg Term]
forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqRHS UnifyState
s
  let (Telescope
tel, PatternSubstitution
sigma) = Telescope
-> Nat -> Telescope -> ConHead -> (Telescope, PatternSubstitution)
expandTelescopeVar (UnifyState -> Telescope
eqTel UnifyState
s) Nat
k Telescope
delta ConHead
c
  PatternSubstitution -> WriterT UnifyOutput TCM ()
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
sigma
  UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies (UnifyState -> UnificationResult' UnifyState)
-> WriterT UnifyOutput TCM UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
   (Telescope -> WriterT UnifyOutput TCM Telescope)
-> UnifyState -> WriterT UnifyOutput TCM UnifyState
Lens' UnifyState Telescope
lensEqTel Telescope -> WriterT UnifyOutput TCM Telescope
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (UnifyState -> WriterT UnifyOutput TCM UnifyState)
-> UnifyState -> WriterT UnifyOutput TCM UnifyState
forall a b. (a -> b) -> a -> b
$ UnifyState
s
    { eqTel    = tel
    , eqLHS    = lhs
    , eqRHS    = rhs
    }
  where
    expandKth :: [Arg Term] -> WriterT UnifyOutput TCM [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
$ Nat -> [Arg Term] -> Maybe ([Arg Term], [Arg Term])
forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt Nat
k [Arg Term]
us
      [Arg Term]
vs <- (Telescope, [Arg Term]) -> [Arg Term]
forall a b. (a, b) -> b
snd ((Telescope, [Arg Term]) -> [Arg Term])
-> WriterT UnifyOutput TCM (Telescope, [Arg Term])
-> WriterT UnifyOutput TCM [Arg Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName
-> [Arg Term]
-> Term
-> WriterT UnifyOutput TCM (Telescope, [Arg Term])
forall (m :: * -> *).
(HasConstInfo m, MonadDebug m, ReadTCState 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)
      [Arg Term]
vs <- [Arg Term] -> WriterT UnifyOutput TCM [Arg Term]
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce [Arg Term]
vs
      [Arg Term] -> WriterT UnifyOutput TCM [Arg Term]
forall a. a -> WriterT UnifyOutput TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Arg Term] -> WriterT UnifyOutput TCM [Arg Term])
-> [Arg Term] -> WriterT UnifyOutput TCM [Arg Term]
forall a b. (a -> b) -> a -> b
$ [Arg Term]
us1 [Arg Term] -> [Arg Term] -> [Arg Term]
forall a. [a] -> [a] -> [a]
++ [Arg Term]
vs [Arg Term] -> [Arg Term] -> [Arg Term]
forall a. [a] -> [a] -> [a]
++ [Arg Term]
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 TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT TCM (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 (StripSizeSuc Nat
k Term
u Term
v) = do
  Type
sizeTy <- WriterT UnifyOutput TCM Type
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType
  Term
sizeSu <- Nat -> Term -> WriterT UnifyOutput TCM Term
forall (m :: * -> *). HasBuiltins m => Nat -> Term -> m Term
sizeSuc Nat
1 (Nat -> Term
var Nat
0)
  let n :: Nat
n          = UnifyState -> Nat
eqCount UnifyState
s
      sub :: Substitution
sub        = Nat -> Substitution -> Substitution
forall a. Nat -> Substitution' a -> Substitution' a
liftS (Nat
nNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
kNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
1) (Substitution -> Substitution) -> Substitution -> Substitution
forall a b. (a -> b) -> a -> b
$ Term -> Substitution -> Substitution
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
sizeSu (Substitution -> Substitution) -> Substitution -> Substitution
forall a b. (a -> b) -> a -> b
$ Nat -> Substitution
forall a. Nat -> Substitution' a
raiseS Nat
1
      eqFlatTel :: [Dom Type]
eqFlatTel  = Telescope -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel (Telescope -> [Dom Type]) -> Telescope -> [Dom Type]
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
      eqFlatTel' :: [Dom Type]
eqFlatTel' = Substitution' (SubstArg [Dom Type]) -> [Dom Type] -> [Dom Type]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg [Dom Type])
sub ([Dom Type] -> [Dom Type]) -> [Dom Type] -> [Dom Type]
forall a b. (a -> b) -> a -> b
$ Nat -> (Dom Type -> Dom Type) -> [Dom Type] -> [Dom Type]
forall a. Nat -> (a -> a) -> [a] -> [a]
updateAt Nat
k ((Type -> Type) -> Dom Type -> Dom Type
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Type -> Type) -> Dom Type -> Dom Type)
-> (Type -> Type) -> Dom Type -> Dom Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
forall a b. a -> b -> a
const Type
sizeTy) ([Dom Type] -> [Dom Type]) -> [Dom Type] -> [Dom Type]
forall a b. (a -> b) -> a -> b
$ [Dom Type]
eqFlatTel
      eqTel' :: Telescope
eqTel'     = [String] -> [Dom Type] -> Telescope
unflattenTel (Telescope -> [String]
teleNames (Telescope -> [String]) -> Telescope -> [String]
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s) [Dom Type]
eqFlatTel'
  -- TODO: tellUnifyProof sub
  -- but sizeSu is not a constructor, so sub is not a PatternSubstitution!
  UnificationResult' UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies (UnifyState -> UnificationResult' UnifyState)
-> UnifyState -> UnificationResult' UnifyState
forall a b. (a -> b) -> a -> b
$ UnifyState
s
    { eqTel = eqTel'
    , eqLHS = updateAt k (const $ defaultArg u) $ eqLHS s
    , eqRHS = updateAt k (const $ defaultArg v) $ eqRHS s
    }

unifyStep UnifyState
s (SkipIrrelevantEquation Nat
k) = do
  let lhs :: [Arg Term]
lhs = UnifyState -> [Arg Term]
eqLHS UnifyState
s
      (UnifyState
s', PatternSubstitution
sigma) = Nat -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
solveEq Nat
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] -> Nat -> Arg Term
forall a. a -> [a] -> Nat -> a
indexWithDefault Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ [Arg Term]
lhs Nat
k) UnifyState
s
  PatternSubstitution -> WriterT UnifyOutput TCM ()
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
sigma
  UnificationResult' UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyOutput TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyStepT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies UnifyState
s'

unifyStep UnifyState
s (TypeConInjectivity Nat
k QName
d [Arg Term]
us [Arg Term]
vs) = do
  Type
dtype <- Definition -> Type
defType (Definition -> Type)
-> WriterT UnifyOutput TCM Definition
-> WriterT UnifyOutput TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> WriterT UnifyOutput TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
  TelV Telescope
dtel Type
_ <- Type -> WriterT UnifyOutput TCM (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
dtype
  let deq :: Term
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...
  UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies (UnifyState -> UnificationResult' UnifyState)
-> WriterT UnifyOutput TCM UnifyState
-> UnifyStepT TCM (UnificationResult' UnifyState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
   (Telescope -> WriterT UnifyOutput TCM Telescope)
-> UnifyState -> WriterT UnifyOutput TCM UnifyState
Lens' UnifyState Telescope
lensEqTel Telescope -> WriterT UnifyOutput TCM Telescope
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (UnifyState -> WriterT UnifyOutput TCM UnifyState)
-> UnifyState -> WriterT UnifyOutput TCM UnifyState
forall a b. (a -> b) -> a -> b
$ UnifyState
s
    { eqTel = dtel `abstract` applyUnder k (eqTel s) (raise k deq)
    , eqLHS = us ++ dropAt k (eqLHS s)
    , eqRHS = vs ++ dropAt k (eqRHS s)
    }

data RetryNormalised = RetryNormalised | DontRetryNormalised
  deriving (RetryNormalised -> RetryNormalised -> Bool
(RetryNormalised -> RetryNormalised -> Bool)
-> (RetryNormalised -> RetryNormalised -> Bool)
-> Eq RetryNormalised
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RetryNormalised -> RetryNormalised -> Bool
== :: RetryNormalised -> RetryNormalised -> Bool
$c/= :: RetryNormalised -> RetryNormalised -> Bool
/= :: RetryNormalised -> RetryNormalised -> Bool
Eq, Nat -> RetryNormalised -> ShowS
[RetryNormalised] -> ShowS
RetryNormalised -> String
(Nat -> RetryNormalised -> ShowS)
-> (RetryNormalised -> String)
-> ([RetryNormalised] -> ShowS)
-> Show RetryNormalised
forall a.
(Nat -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Nat -> RetryNormalised -> ShowS
showsPrec :: Nat -> RetryNormalised -> ShowS
$cshow :: RetryNormalised -> String
show :: RetryNormalised -> String
$cshowList :: [RetryNormalised] -> ShowS
showList :: [RetryNormalised] -> ShowS
Show)

solutionStep
  :: (PureTCM m, MonadWriter UnifyOutput m)
  => RetryNormalised
  -> UnifyState
  -> UnifyStep
  -> m (UnificationResult' UnifyState)
solutionStep :: forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m) =>
RetryNormalised
-> UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
solutionStep RetryNormalised
retry UnifyState
s
  step :: UnifyStep
step@Solution{ solutionAt :: UnifyStep -> Nat
solutionAt   = Nat
k
               , solutionType :: UnifyStep -> Dom Type
solutionType = dom :: Dom Type
dom@Dom{ unDom :: forall t e. Dom' t e -> e
unDom = Type
a }
               , solutionVar :: UnifyStep -> FlexibleVar Nat
solutionVar  = fi :: FlexibleVar Nat
fi@FlexibleVar{ flexVar :: forall a. FlexibleVar a -> a
flexVar = Nat
i }
               , solutionTerm :: UnifyStep -> Term
solutionTerm = Term
u } = do
  let m :: Nat
m = UnifyState -> Nat
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.
  Bool
inMakeCase <- Lens' TCEnv Bool -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eMakeCase
  let forcedVars :: IntMap Modality
forcedVars | Bool
inMakeCase = IntMap Modality
forall a. IntMap a
IntMap.empty
                 | Bool
otherwise  = [(Nat, Modality)] -> IntMap Modality
forall a. [(Nat, a)] -> IntMap a
IntMap.fromList [ (FlexibleVar Nat -> Nat
forall a. FlexibleVar a -> a
flexVar FlexibleVar Nat
fi, FlexibleVar Nat -> Modality
forall a. LensModality a => a -> Modality
getModality FlexibleVar Nat
fi) | FlexibleVar Nat
fi <- UnifyState -> FlexibleVars
flexVars UnifyState
s,
                                                                                 FlexibleVar Nat -> IsForced
forall a. FlexibleVar a -> IsForced
flexForced FlexibleVar Nat
fi IsForced -> IsForced -> Bool
forall a. Eq a => a -> a -> Bool
== IsForced
Forced ]
  (Pattern' DBPatVar
p, IntMap Modality
bound) <- IntMap Modality -> Term -> m (Pattern' DBPatVar, IntMap Modality)
forall (m :: * -> *).
PureTCM m =>
IntMap Modality -> Term -> m (Pattern' DBPatVar, IntMap Modality)
patternBindingForcedVars IntMap Modality
forcedVars Term
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 :: PatternSubstitution
dotSub = (PatternSubstitution -> PatternSubstitution -> PatternSubstitution)
-> PatternSubstitution
-> [PatternSubstitution]
-> PatternSubstitution
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr PatternSubstitution -> PatternSubstitution -> PatternSubstitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS PatternSubstitution
forall a. Substitution' a
idS [ Nat -> Pattern' DBPatVar -> PatternSubstitution
forall a. EndoSubst a => Nat -> a -> Substitution' a
inplaceS Nat
i (Term -> Pattern' DBPatVar
forall a. Term -> Pattern' a
dotP (Nat -> Elims -> Term
Var Nat
i [])) | Nat
i <- IntMap Modality -> [Nat]
forall a. IntMap a -> [Nat]
IntMap.keys IntMap Modality
bound ]

  -- We moved the binding site of some forced variables, so we need to update their modalities in
  -- the telescope. The new modality is the combination of the modality of the variable we are
  -- instantiating and the modality of the binding site in the pattern (returned by
  -- patternBindingForcedVars).
  let updModality :: Modality -> IntMap Modality -> Telescope -> Telescope
updModality Modality
md IntMap Modality
vars Telescope
tel
        | IntMap Modality -> Bool
forall a. IntMap a -> Bool
IntMap.null IntMap Modality
vars = Telescope
tel
        | Bool
otherwise        = ListTel -> Telescope
telFromList (ListTel -> Telescope) -> ListTel -> Telescope
forall a b. (a -> b) -> a -> b
$ (Nat -> Dom (String, Type) -> Dom (String, Type))
-> [Nat] -> ListTel -> ListTel
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Nat -> Dom (String, Type) -> Dom (String, Type)
upd (Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom (Nat -> [Nat]) -> Nat -> [Nat]
forall a b. (a -> b) -> a -> b
$ Telescope -> Nat
forall a. Sized a => a -> Nat
size Telescope
tel) (Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel)
        where
          upd :: Nat -> Dom (String, Type) -> Dom (String, Type)
upd Nat
i Dom (String, Type)
a | Just Modality
md' <- Nat -> IntMap Modality -> Maybe Modality
forall a. Nat -> IntMap a -> Maybe a
IntMap.lookup Nat
i IntMap Modality
vars = Modality -> Dom (String, Type) -> Dom (String, Type)
forall a. LensModality a => Modality -> a -> a
setModality (Modality -> Modality -> Modality
composeModality Modality
md Modality
md') Dom (String, Type)
a
                  | Bool
otherwise                        = Dom (String, Type)
a
  UnifyState
s <- UnifyState -> m UnifyState
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnifyState -> m UnifyState) -> UnifyState -> m UnifyState
forall a b. (a -> b) -> a -> b
$ UnifyState
s { varTel = updModality (getModality fi) bound (varTel s) }

  String -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.force" Nat
45 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
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
vcat
    [ TCMT IO Doc
"forcedVars =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Nat] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (IntMap Modality -> [Nat]
forall a. IntMap a -> [Nat]
IntMap.keys IntMap Modality
forcedVars)
    , TCMT IO Doc
"u          =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
    , TCMT IO Doc
"p          =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Pattern' DBPatVar -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Pattern' DBPatVar -> m Doc
prettyTCM Pattern' DBPatVar
p
    , TCMT IO Doc
"bound      =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Nat] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (IntMap Modality -> [Nat]
forall a. IntMap a -> [Nat]
IntMap.keys IntMap Modality
bound)
    , TCMT IO Doc
"dotSub     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> PatternSubstitution -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty PatternSubstitution
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' :: Dom Type
dom'@Dom{ unDom :: forall t e. Dom' t e -> e
unDom = Type
a' } = Nat -> UnifyState -> Dom Type
getVarType (Nat
mNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
1Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
i) UnifyState
s
  Either Blocker Bool
equalTypes <- Telescope -> m (Either Blocker Bool) -> m (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) (m (Either Blocker Bool) -> m (Either Blocker Bool))
-> m (Either Blocker Bool) -> m (Either Blocker Bool)
forall a b. (a -> b) -> a -> b
$ do
    String -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
45 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Equation type: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
    String -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
45 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Variable type: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a'
    Type -> Type -> m (Either Blocker Bool)
forall (m :: * -> *).
PureTCM m =>
Type -> Type -> m (Either Blocker Bool)
pureEqualTypeB Type
a Type
a'

  -- The conditions on the relevances are as follows (see #2640):
  -- - If the type of the equation is relevant, then the solution must be
  --   usable in a relevant position.
  -- - If the type of the equation is (shape-)irrelevant, then the solution
  --   must be usable in a μ-relevant position where μ is the relevance
  --   of the variable being solved.
  --
  -- Jesper, Andreas, 2018-10-17: the quantity of the equation is morally
  -- always @Quantity0@, since the indices of the data type are runtime erased.
  -- Thus, we need not change the quantity of the solution.
  Modality
envmod <- m Modality
forall (m :: * -> *). MonadTCEnv m => m Modality
currentModality
  let eqrel :: Relevance
eqrel  = Dom Type -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Dom Type
dom
      eqmod :: Modality
eqmod  = Dom Type -> Modality
forall a. LensModality a => a -> Modality
getModality Dom Type
dom
      varmod :: Modality
varmod = Dom Type -> Modality
forall a. LensModality a => a -> Modality
getModality Dom Type
dom'
      mod :: Modality
mod    = Bool -> (Modality -> Modality) -> Modality -> Modality
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless (Relevance
shapeIrrelevant Relevance -> Relevance -> Bool
`moreRelevant` Relevance
eqrel) (Relevance -> Modality -> Modality
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
eqrel)
             (Modality -> Modality) -> Modality -> Modality
forall a b. (a -> b) -> a -> b
$ Bool -> (Modality -> Modality) -> Modality -> Modality
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless (Modality -> Bool
forall a. LensQuantity a => a -> Bool
usableQuantity Modality
envmod) (Quantity -> Modality -> Modality
forall a. LensQuantity a => Quantity -> a -> a
setQuantity Quantity
zeroQuantity)
             (Modality -> Modality) -> Modality -> Modality
forall a b. (a -> b) -> a -> b
$ Modality
varmod
  String -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
65 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
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
$ String
"Equation modality: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Modality -> String
forall a. Show a => a -> String
show (Dom Type -> Modality
forall a. LensModality a => a -> Modality
getModality Dom Type
dom)
  String -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
65 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
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
$ String
"Variable modality: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Modality -> String
forall a. Show a => a -> String
show Modality
varmod
  String -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
65 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
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
$ String
"Solution must be usable in a " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Modality -> String
forall a. Show a => a -> String
show Modality
mod String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" position."
  -- Andreas, 2018-10-18
  -- Currently, the modality check has problems with meta-variables created in the type signature,
  -- and thus, in quantity 0, that get into terms using the unifier, and there are checked to be
  -- non-erased, i.e., have quantity ω.
  -- Ulf, 2019-12-13. We still do it though.
  -- Andrea, 2020-10-15: It looks at meta instantiations now.
  Either Blocker Bool
eusable <- Telescope -> m (Either Blocker Bool) -> m (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) (m (Either Blocker Bool) -> m (Either Blocker Bool))
-> m (Either Blocker Bool) -> m (Either Blocker Bool)
forall a b. (a -> b) -> a -> b
$ ExceptT Blocker m Bool -> m (Either Blocker Bool)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT Blocker m Bool -> m (Either Blocker Bool))
-> ExceptT Blocker m Bool -> m (Either Blocker Bool)
forall a b. (a -> b) -> a -> b
$ Modality -> Term -> ExceptT Blocker m Bool
forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m, MonadReduce m,
 MonadError Blocker m) =>
Modality -> a -> m Bool
forall (m :: * -> *).
(ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m,
 MonadDebug m, MonadReduce m, MonadError Blocker m) =>
Modality -> Term -> m Bool
usableMod Modality
mod Term
u
  m (Either Blocker Bool)
-> (Blocker -> m (UnificationResult' UnifyState))
-> (Bool -> m (UnificationResult' UnifyState))
-> m (UnificationResult' UnifyState)
forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (Either Blocker Bool -> m (Either Blocker Bool)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Either Blocker Bool
eusable) (UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> (Blocker -> UnificationResult' UnifyState)
-> Blocker
-> m (UnificationResult' UnifyState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocker -> UnificationResult' UnifyState
forall a. Blocker -> UnificationResult' a
UnifyBlocked) ((Bool -> m (UnificationResult' UnifyState))
 -> m (UnificationResult' UnifyState))
-> (Bool -> m (UnificationResult' UnifyState))
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ \ Bool
usable -> do

  String -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
45 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Modality ok: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Bool -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Bool -> m Doc
prettyTCM Bool
usable
  Bool -> m () -> m ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless Bool
usable (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
65 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Rejected solution: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u

  -- We need a Flat equality to solve a Flat variable.
  -- This also ought to take care of the need for a usableCohesion check.
  if Bool -> Bool
not (Modality -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion Modality
eqmod Cohesion -> Cohesion -> Bool
`moreCohesion` Modality -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion Modality
varmod) then UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [] else do

  case Either Blocker Bool
equalTypes of
    Left Blocker
block  -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (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 -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []
    Right Bool
True | Bool
usable ->
      case Nat
-> Pattern' DBPatVar
-> UnifyState
-> Maybe (UnifyState, PatternSubstitution)
solveVar (Nat
m Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
i) Pattern' DBPatVar
p UnifyState
s of
        Maybe (UnifyState, PatternSubstitution)
Nothing | RetryNormalised
retry RetryNormalised -> RetryNormalised -> Bool
forall a. Eq a => a -> a -> Bool
== RetryNormalised
RetryNormalised -> do
          Term
u <- Term -> m Term
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Term
u
          UnifyState
s <- (Telescope -> m Telescope) -> UnifyState -> m UnifyState
Lens' UnifyState Telescope
lensVarTel Telescope -> m Telescope
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise UnifyState
s
          RetryNormalised
-> UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m) =>
RetryNormalised
-> UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
solutionStep RetryNormalised
DontRetryNormalised UnifyState
s UnifyStep
step{ solutionTerm = u }
        Maybe (UnifyState, PatternSubstitution)
Nothing ->
          UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [Telescope -> Type -> Nat -> Term -> UnificationFailure
UnifyRecursiveEq (UnifyState -> Telescope
varTel UnifyState
s) Type
a Nat
i Term
u]
        Just (UnifyState
s', PatternSubstitution
sub) -> do
          let rho :: PatternSubstitution
rho = PatternSubstitution
sub PatternSubstitution -> PatternSubstitution -> PatternSubstitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` PatternSubstitution
dotSub
          PatternSubstitution -> m ()
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifySubst PatternSubstitution
rho
          let (UnifyState
s'', PatternSubstitution
sigma) = Nat -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
solveEq Nat
k (PatternSubstitution -> Term -> Term
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho Term
u) UnifyState
s'
          PatternSubstitution -> m ()
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
sigma
          UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies UnifyState
s''
          -- Andreas, 2019-02-23, issue #3578: do not eagerly reduce
          -- Unifies <$> liftTCM (reduce s'')
    Right Bool
True -> UnificationResult' UnifyState -> m (UnificationResult' UnifyState)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> m (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> m (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ [UnificationFailure] -> UnificationResult' UnifyState
forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [Telescope -> Type -> Nat -> Term -> Modality -> UnificationFailure
UnifyUnusableModality (UnifyState -> Telescope
varTel UnifyState
s) Type
a Nat
i Term
u Modality
mod]
solutionStep RetryNormalised
_ UnifyState
_ UnifyStep
_ = m (UnificationResult' UnifyState)
forall a. HasCallStack => a
__IMPOSSIBLE__

unify :: UnifyState -> UnifyStrategy -> UnifyLogT TCM (UnificationResult' UnifyState)
unify :: UnifyState
-> UnifyStrategy -> UnifyLogT TCM (UnificationResult' UnifyState)
unify UnifyState
s UnifyStrategy
strategy = if UnifyState -> Bool
isUnifyStateSolved UnifyState
s
                   then UnificationResult' UnifyState
-> UnifyLogT TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyLogT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyLogT TCM (UnificationResult' UnifyState)
forall a b. (a -> b) -> a -> b
$ UnifyState -> UnificationResult' UnifyState
forall a. a -> UnificationResult' a
Unifies UnifyState
s
                   else ListT TCM UnifyStep
-> UnifyLogT TCM (UnificationResult' UnifyState)
tryUnifyStepsAndContinue (UnifyStrategy
strategy UnifyState
s)
  where
    tryUnifyStepsAndContinue
      :: ListT TCM UnifyStep -> UnifyLogT TCM (UnificationResult' UnifyState)
    tryUnifyStepsAndContinue :: ListT TCM UnifyStep
-> UnifyLogT TCM (UnificationResult' UnifyState)
tryUnifyStepsAndContinue ListT TCM UnifyStep
steps = do
      UnificationResult' UnifyState
x <- (UnifyStep
 -> UnifyLogT TCM (UnificationResult' UnifyState)
 -> UnifyLogT TCM (UnificationResult' UnifyState))
-> UnifyLogT TCM (UnificationResult' UnifyState)
-> ListT (WriterT UnifyLog' TCM) UnifyStep
-> UnifyLogT TCM (UnificationResult' UnifyState)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT UnifyStep
-> UnifyLogT TCM (UnificationResult' UnifyState)
-> UnifyLogT TCM (UnificationResult' UnifyState)
tryUnifyStep UnifyLogT TCM (UnificationResult' UnifyState)
forall (m :: * -> *) a. Monad m => m (UnificationResult' a)
failure ((forall a1. TCM a1 -> WriterT UnifyLog' TCM a1)
-> ListT TCM UnifyStep -> ListT (WriterT UnifyLog' TCM) 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' TCM a1
forall a1. TCM a1 -> WriterT UnifyLog' TCM 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 TCM UnifyStep
steps)
      case UnificationResult' UnifyState
x of
        Unifies UnifyState
s'     -> UnifyState
-> UnifyStrategy -> UnifyLogT TCM (UnificationResult' UnifyState)
unify UnifyState
s' UnifyStrategy
strategy
        NoUnify NegativeUnification
err    -> UnificationResult' UnifyState
-> UnifyLogT TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyLogT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyLogT TCM (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 TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyLogT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyLogT TCM (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 TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyLogT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyLogT TCM (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 TCM (UnificationResult' UnifyState)
-> UnifyLogT TCM (UnificationResult' UnifyState)
tryUnifyStep UnifyStep
step UnifyLogT TCM (UnificationResult' UnifyState)
fallback = do
      Telescope -> WriterT UnifyLog' TCM () -> WriterT UnifyLog' TCM ()
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' TCM () -> WriterT UnifyLog' TCM ())
-> WriterT UnifyLog' TCM () -> WriterT UnifyLog' TCM ()
forall a b. (a -> b) -> a -> b
$
        String -> Nat -> TCMT IO Doc -> WriterT UnifyLog' TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
20 (TCMT IO Doc -> WriterT UnifyLog' TCM ())
-> TCMT IO Doc -> WriterT UnifyLog' TCM ()
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
      (UnificationResult' UnifyState
x, UnifyOutput
output) <- TCM (UnificationResult' UnifyState, UnifyOutput)
-> WriterT
     UnifyLog' TCM (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' TCM (UnificationResult' UnifyState, UnifyOutput))
-> TCM (UnificationResult' UnifyState, UnifyOutput)
-> WriterT
     UnifyLog' TCM (UnificationResult' UnifyState, UnifyOutput)
forall a b. (a -> b) -> a -> b
$ UnifyStepT TCM (UnificationResult' UnifyState)
-> TCM (UnificationResult' UnifyState, UnifyOutput)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (UnifyStepT TCM (UnificationResult' UnifyState)
 -> TCM (UnificationResult' UnifyState, UnifyOutput))
-> UnifyStepT TCM (UnificationResult' UnifyState)
-> TCM (UnificationResult' UnifyState, UnifyOutput)
forall a b. (a -> b) -> a -> b
$ UnifyState
-> UnifyStep -> UnifyStepT TCM (UnificationResult' UnifyState)
unifyStep UnifyState
s UnifyStep
step
      case UnificationResult' UnifyState
x of
        Unifies UnifyState
s'   -> do
          String -> Nat -> TCMT IO Doc -> WriterT UnifyLog' TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
20 (TCMT IO Doc -> WriterT UnifyLog' TCM ())
-> TCMT IO Doc -> WriterT UnifyLog' TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"unifyStep successful."
          String -> Nat -> TCMT IO Doc -> WriterT UnifyLog' TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Nat
20 (TCMT IO Doc -> WriterT UnifyLog' TCM ())
-> TCMT IO Doc -> WriterT UnifyLog' TCM ()
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'
          -- tell output
          (UnifyLogEntry, UnifyState) -> WriterT UnifyLog' TCM ()
forall (m :: * -> *).
MonadWriter UnifyLog' m =>
(UnifyLogEntry, UnifyState) -> m ()
writeUnifyLog ((UnifyLogEntry, UnifyState) -> WriterT UnifyLog' TCM ())
-> (UnifyLogEntry, UnifyState) -> WriterT UnifyLog' TCM ()
forall a b. (a -> b) -> a -> b
$ (UnifyState -> UnifyStep -> UnifyOutput -> UnifyLogEntry
UnificationStep UnifyState
s UnifyStep
step UnifyOutput
output,UnifyState
s')
          UnificationResult' UnifyState
-> UnifyLogT TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
x
        NoUnify{}       -> UnificationResult' UnifyState
-> UnifyLogT TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
x
        UnifyBlocked Blocker
b1 -> do
          UnificationResult' UnifyState
y <- UnifyLogT TCM (UnificationResult' UnifyState)
fallback
          case UnificationResult' UnifyState
y of
            UnifyStuck [UnificationFailure]
_    -> UnificationResult' UnifyState
-> UnifyLogT TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyLogT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyLogT TCM (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 TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyLogT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyLogT TCM (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 TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
y
        UnifyStuck [UnificationFailure]
err1 -> do
          UnificationResult' UnifyState
y <- UnifyLogT TCM (UnificationResult' UnifyState)
fallback
          case UnificationResult' UnifyState
y of
            UnifyStuck [UnificationFailure]
err2 -> UnificationResult' UnifyState
-> UnifyLogT TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnificationResult' UnifyState
 -> UnifyLogT TCM (UnificationResult' UnifyState))
-> UnificationResult' UnifyState
-> UnifyLogT TCM (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 TCM (UnificationResult' UnifyState)
forall a. a -> WriterT UnifyLog' TCM 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 :: PureTCM m => IntMap Modality -> Term -> m (DeBruijnPattern, IntMap Modality)
patternBindingForcedVars :: forall (m :: * -> *).
PureTCM m =>
IntMap Modality -> Term -> m (Pattern' DBPatVar, IntMap Modality)
patternBindingForcedVars IntMap Modality
forced Term
v = do
  let v' :: Term
v' = Term -> Term
forall a. PrecomputeFreeVars a => a -> a
precomputeFreeVars_ Term
v
  WriterT (IntMap Modality) m (Pattern' DBPatVar)
-> m (Pattern' DBPatVar, IntMap Modality)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (StateT
  (IntMap Modality) (WriterT (IntMap Modality) m) (Pattern' DBPatVar)
-> IntMap Modality
-> WriterT (IntMap Modality) m (Pattern' DBPatVar)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Modality
-> Term
-> StateT
     (IntMap Modality) (WriterT (IntMap Modality) m) (Pattern' DBPatVar)
forall {t :: (* -> *) -> * -> *} {t :: (* -> *) -> * -> *}
       {m :: * -> *} {a}.
(HasConstInfo (t (t m)), DeBruijn a,
 MonadWriter (IntMap Modality) (t (t m)),
 MonadState (IntMap Modality) (t (t m)), MonadTrans t, MonadTrans t,
 Monad (t m), MonadReduce m) =>
Modality -> Term -> t (t m) (Pattern' a)
go Modality
unitModality Term
v') IntMap Modality
forced)
  where
    noForced :: a -> m Bool
noForced a
v = (IntMap a -> Bool) -> m Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((IntMap a -> Bool) -> m Bool) -> (IntMap a -> Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ IntSet -> IntSet -> Bool
IntSet.disjoint (a -> IntSet
forall a. PrecomputeFreeVars a => a -> IntSet
precomputedFreeVars a
v) (IntSet -> Bool) -> (IntMap a -> IntSet) -> IntMap a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntMap a -> IntSet
forall a. IntMap a -> IntSet
IntMap.keysSet

    bind :: a -> Nat -> m (Pattern' a)
bind a
md Nat
i = do
      (IntMap a -> Maybe a) -> m (Maybe a)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Nat -> IntMap a -> Maybe a
forall a. Nat -> IntMap a -> Maybe a
IntMap.lookup Nat
i) m (Maybe a) -> (Maybe a -> 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
        Just a
md' | a -> PartialOrdering -> a -> Bool
forall a. PartialOrd a => a -> PartialOrdering -> a -> Bool
related a
md PartialOrdering
POLE a
md' -> do
          -- The new binding site must be more relevant (more relevant = smaller).
          -- "The forcing analysis guarantees that there exists such a position."
          -- Really? Andreas, 2021-08-18, issue #5506
          IntMap a -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell   (IntMap a -> m ()) -> IntMap a -> m ()
forall a b. (a -> b) -> a -> b
$ Nat -> a -> IntMap a
forall a. Nat -> a -> IntMap a
IntMap.singleton Nat
i a
md
          (IntMap a -> IntMap a) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((IntMap a -> IntMap a) -> m ()) -> (IntMap a -> IntMap a) -> m ()
forall a b. (a -> b) -> a -> b
$ Nat -> IntMap a -> IntMap a
forall a. Nat -> IntMap a -> IntMap a
IntMap.delete Nat
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 (Nat -> a
forall a. DeBruijn a => Nat -> a
deBruijnVar Nat
i)
        Maybe a
_ -> 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 (Nat -> Elims -> Term
Var Nat
i [])

    go :: Modality -> Term -> t (t m) (Pattern' a)
go Modality
md 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 {a} {m :: * -> *} {a}.
(MonadState (IntMap a) 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
      Term
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 Term
v' of
        Var Nat
i [] -> Modality -> Nat -> t (t m) (Pattern' a)
forall {m :: * -> *} {a} {a}.
(MonadState (IntMap a) m, PartialOrd a, MonadWriter (IntMap a) m,
 DeBruijn a) =>
a -> Nat -> m (Pattern' a)
bind Modality
md Nat
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
            [IsForced]
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 => QName -> m Definition
getConstInfo (ConHead -> QName
conName ConHead
c)
            let goArg :: IsForced -> Arg Term -> t (t m) (NamedArg (Pattern' a))
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 (Modality -> Term -> t (t m) (Pattern' a)
go (Modality -> Term -> t (t m) (Pattern' a))
-> Modality -> Term -> t (t m) (Pattern' a)
forall a b. (a -> b) -> a -> b
$ Modality -> Modality -> Modality
composeModality Modality
md (Modality -> Modality) -> Modality -> Modality
forall a b. (a -> b) -> a -> b
$ Arg Term -> Modality
forall a. LensModality a => a -> Modality
getModality Arg Term
v) Arg Term
v
            ([NamedArg (Pattern' a)]
ps, IntMap Modality
bound) <- t (t m) [NamedArg (Pattern' a)]
-> t (t m) ([NamedArg (Pattern' a)], IntMap Modality)
forall a. t (t m) a -> t (t m) (a, IntMap Modality)
forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
listen (t (t m) [NamedArg (Pattern' a)]
 -> t (t m) ([NamedArg (Pattern' a)], IntMap Modality))
-> t (t m) [NamedArg (Pattern' a)]
-> t (t m) ([NamedArg (Pattern' a)], IntMap Modality)
forall a b. (a -> b) -> a -> b
$ (IsForced -> Arg Term -> t (t m) (NamedArg (Pattern' a)))
-> [IsForced] -> [Arg Term] -> t (t m) [NamedArg (Pattern' a)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM IsForced -> Arg Term -> t (t m) (NamedArg (Pattern' a))
goArg ([IsForced]
fs [IsForced] -> [IsForced] -> [IsForced]
forall a. [a] -> [a] -> [a]
++ IsForced -> [IsForced]
forall a. a -> [a]
repeat IsForced
NotForced) [Arg Term]
vs
            if IntMap Modality -> Bool
forall a. IntMap a -> Bool
IntMap.null IntMap Modality
bound
              then 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  -- bound nothing
              else do
                let cpi :: ConPatternInfo
cpi = (ConInfo -> ConPatternInfo
toConPatternInfo ConInfo
ci) { conPLazy   = True } -- Not setting conPType. Is this a problem?
                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
$ ConHead -> ConPatternInfo -> [NamedArg (Pattern' a)] -> Pattern' a
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
cpi ([NamedArg (Pattern' a)] -> Pattern' a)
-> [NamedArg (Pattern' a)] -> Pattern' a
forall a b. (a -> b) -> a -> b
$ (NamedArg (Pattern' a) -> NamedArg (Pattern' a))
-> [NamedArg (Pattern' a)] -> [NamedArg (Pattern' a)]
forall a b. (a -> b) -> [a] -> [b]
map (Origin -> NamedArg (Pattern' a) -> NamedArg (Pattern' a)
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted) [NamedArg (Pattern' a)]
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 Nat
_ (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.