{-# 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
import Control.Monad.State
import Control.Monad.Writer (WriterT(..), MonadWriter(..))
import Control.Monad.Except

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, optCubical, optWithoutK)

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

import Agda.TypeChecking.Monad
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Monad.Builtin -- (constructorForm, getTerm, builtinPathP)
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Primitive.Cubical
import Agda.TypeChecking.Names
import Agda.TypeChecking.Conversion -- equalTerm
import Agda.TypeChecking.Conversion.Pure
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Level (reallyUnLevelView)
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.Empty
import Agda.Utils.Either
import Agda.Utils.Benchmark
import Agda.Utils.Either
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
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.Permutation
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.WithDefault
import Agda.Utils.Tuple

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 (Int -> UnificationResult' a -> ShowS
forall a. Show a => Int -> UnificationResult' a -> ShowS
forall a. Show a => [UnificationResult' a] -> ShowS
forall a. Show a => UnificationResult' a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnificationResult' a] -> ShowS
$cshowList :: forall a. Show a => [UnificationResult' a] -> ShowS
show :: UnificationResult' a -> String
$cshow :: forall a. Show a => UnificationResult' a -> String
showsPrec :: Int -> UnificationResult' a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> UnificationResult' a -> ShowS
Show, 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
<$ :: forall a b. a -> UnificationResult' b -> UnificationResult' a
$c<$ :: forall a b. a -> UnificationResult' b -> UnificationResult' a
fmap :: forall a b.
(a -> b) -> UnificationResult' a -> UnificationResult' b
$cfmap :: forall a b.
(a -> b) -> UnificationResult' a -> UnificationResult' b
Functor, 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 -> Int
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 -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => UnificationResult' a -> a
$cproduct :: forall a. Num a => UnificationResult' a -> a
sum :: forall a. Num a => UnificationResult' a -> a
$csum :: forall a. Num a => UnificationResult' a -> a
minimum :: forall a. Ord a => UnificationResult' a -> a
$cminimum :: forall a. Ord a => UnificationResult' a -> a
maximum :: forall a. Ord a => UnificationResult' a -> a
$cmaximum :: forall a. Ord a => UnificationResult' a -> a
elem :: forall a. Eq a => a -> UnificationResult' a -> Bool
$celem :: forall a. Eq a => a -> UnificationResult' a -> Bool
length :: forall a. UnificationResult' a -> Int
$clength :: forall a. UnificationResult' a -> Int
null :: forall a. UnificationResult' a -> Bool
$cnull :: forall a. UnificationResult' a -> Bool
toList :: forall a. UnificationResult' a -> [a]
$ctoList :: forall a. UnificationResult' a -> [a]
foldl1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
foldr1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
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
$cfoldl :: forall b a. (b -> a -> 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
$cfoldr :: forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
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
$cfoldMap :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
fold :: forall m. Monoid m => UnificationResult' m -> m
$cfold :: forall m. Monoid m => UnificationResult' m -> m
Foldable, Functor UnificationResult'
Foldable 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)
sequence :: forall (m :: * -> *) a.
Monad m =>
UnificationResult' (m a) -> m (UnificationResult' a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
UnificationResult' (m a) -> m (UnificationResult' a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> UnificationResult' a -> m (UnificationResult' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> UnificationResult' a -> m (UnificationResult' b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
UnificationResult' (f a) -> f (UnificationResult' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
UnificationResult' (f a) -> f (UnificationResult' a)
traverse :: 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)
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
  :: (PureTCM m, MonadBench m, BenchPhase m ~ Bench.Phase, MonadError TCErr m)
  => Maybe NoLeftInv -- ^ Do we have a reason for not computing a left inverse?
  -> Telescope       -- ^ @gamma@
  -> FlexibleVars    -- ^ @flex@
  -> Type            -- ^ @a@
  -> Args            -- ^ @us@
  -> Args            -- ^ @vs@
  -> m UnificationResult
unifyIndices :: forall (m :: * -> *).
(PureTCM m, MonadBench m, BenchPhase m ~ Phase,
 MonadError TCErr m) =>
Maybe NoLeftInv
-> Telescope
-> FlexibleVars
-> Type
-> Args
-> Args
-> m UnificationResult
unifyIndices Maybe NoLeftInv
linv Telescope
tel FlexibleVars
flex Type
a Args
us Args
vs =
  forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Typing, Phase
Bench.CheckLHS, Phase
Bench.UnifyIndices] forall a b. (a -> b) -> a -> b
$
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Telescope
a,PatternSubstitution
b,[NamedArg DeBruijnPattern]
c,Either NoLeftInv (Substitution, Substitution)
_) -> (Telescope
a,PatternSubstitution
b,[NamedArg DeBruijnPattern]
c)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Maybe NoLeftInv
-> Telescope
-> FlexibleVars
-> Type
-> Args
-> Args
-> m FullUnificationResult
unifyIndices' Maybe NoLeftInv
linv Telescope
tel FlexibleVars
flex Type
a Args
us Args
vs

unifyIndices'
  :: (PureTCM m, MonadError TCErr m)
  => Maybe NoLeftInv -- ^ Do we have a reason for not computing a left inverse?
  -> Telescope     -- ^ @gamma@
  -> FlexibleVars  -- ^ @flex@
  -> Type          -- ^ @a@
  -> Args          -- ^ @us@
  -> Args          -- ^ @vs@
  -> m FullUnificationResult
unifyIndices' :: forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Maybe NoLeftInv
-> Telescope
-> FlexibleVars
-> Type
-> Args
-> Args
-> m FullUnificationResult
unifyIndices' Maybe NoLeftInv
linv Telescope
tel FlexibleVars
flex Type
a [] [] = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> UnificationResult' a
Unifies (Telescope
tel, forall a. Substitution' a
idS, [], forall a b. b -> Either a b
Right (forall a. Substitution' a
idS, forall a. Int -> Substitution' a
raiseS Int
1))
unifyIndices' Maybe NoLeftInv
linv Telescope
tel FlexibleVars
flex Type
a Args
us Args
vs = do
    forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
10 forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"unifyIndices"
          , (TCMT IO Doc
"tel  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
          , (TCMT IO Doc
"flex =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. FlexibleVar a -> a
flexVar FlexibleVars
flex
          , (TCMT IO Doc
"a    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a)
          , (TCMT IO Doc
"us   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
us
          , (TCMT IO Doc
"vs   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
vs
          ]
    UnifyState
initialState    <- forall (m :: * -> *).
PureTCM m =>
Telescope -> FlexibleVars -> Type -> Args -> Args -> m UnifyState
initUnifyState Telescope
tel FlexibleVars
flex Type
a Args
us Args
vs
    forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"initial unifyState:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM UnifyState
initialState
    (UnificationResult' UnifyState
result,UnifyLog
log) <- forall (m :: * -> *) a.
Functor m =>
UnifyLogT m a -> m (a, UnifyLog)
runUnifyLogT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyLog' m, MonadError TCErr m) =>
UnifyState -> UnifyStrategy -> m (UnificationResult' UnifyState)
unify UnifyState
initialState UnifyStrategy
rightToLeftStrategy
    forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM UnificationResult' UnifyState
result forall a b. (a -> b) -> a -> b
$ \ UnifyState
s -> do -- Unifies case
        let output :: UnifyOutput
output = forall a. Monoid a => [a] -> a
mconcat [UnifyOutput
output | (UnificationStep UnifyState
_ UnifyStep
_ UnifyOutput
output,UnifyState
_) <- UnifyLog
log ]
        let ps :: [NamedArg DeBruijnPattern]
ps = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (UnifyOutput -> PatternSubstitution
unifyProof UnifyOutput
output) forall a b. (a -> b) -> a -> b
$ forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs (UnifyState -> Telescope
eqTel UnifyState
initialState)
        Either NoLeftInv (Substitution, Substitution)
tauInv <- do
          Bool
strict     <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envSplitOnStrict
          Bool
cubicalCompatible <- forall (m :: * -> *). HasOptions m => m Bool
cubicalCompatibleOption
          Bool
withoutK <- forall (m :: * -> *). HasOptions m => m Bool
withoutKOption
          case Maybe NoLeftInv
linv of
            Just NoLeftInv
reason -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> Either a b
Left NoLeftInv
reason)
            Maybe NoLeftInv
Nothing
              | Bool
strict            -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> Either a b
Left NoLeftInv
SplitOnStrict)
              | Bool
cubicalCompatible -> forall (tcm :: * -> *).
(PureTCM tcm, MonadError TCErr tcm) =>
UnifyState
-> UnifyLog -> tcm (Either NoLeftInv (Substitution, Substitution))
buildLeftInverse UnifyState
initialState UnifyLog
log
              | Bool
withoutK          -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> Either a b
Left NoLeftInv
NoCubical)
              | Bool
otherwise         -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> Either a b
Left NoLeftInv
WithKEnabled)
        forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [NamedArg DeBruijnPattern]
ps
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (UnifyState -> Telescope
varTel UnifyState
s, UnifyOutput -> PatternSubstitution
unifySubst UnifyOutput
output, [NamedArg DeBruijnPattern]
ps, Either NoLeftInv (Substitution, Substitution)
tauInv)



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

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

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

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

dataStrategy :: Int -> UnifyStrategy
dataStrategy :: Int -> UnifyStrategy
dataStrategy Int
k UnifyState
s = do
  Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v <- forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqConstructorForm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqUnLevel forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> UnifyState -> m Equality
getReducedEqualityUnraised Int
k UnifyState
s
  Bool
sortOk <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (forall a. LensSort a => a -> Sort
getSort Type
a) 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 forall t a. Type'' t a -> a
unEl Type
a of
    Def QName
d Elims
es | Bool
sortOk -> do
      Int
npars <- forall (m :: * -> *) a. MonadPlus m => m (Maybe a) -> m a
catMaybesMP forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Int)
getNumberOfParameters QName
d
      let (Args
pars,Args
ixs) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
npars forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
      forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
40 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s forall t. Abstract t => Telescope -> t -> t
`abstract` UnifyState -> Telescope
eqTel UnifyState
s) forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"Found equation at datatype " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d
         forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" with parameters " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size (UnifyState -> Telescope
eqTel UnifyState
s) forall a. Num a => a -> a -> a
- Int
k) Args
pars)
      case (Term
u, Term
v) of
        (Con ConHead
c ConInfo
_ Elims
_   , Con ConHead
c' ConInfo
_ Elims
_  ) | ConHead
c forall a. Eq a => a -> a -> Bool
== ConHead
c' -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Type -> QName -> Args -> Args -> ConHead -> UnifyStep
Injectivity Int
k Type
a QName
d Args
pars Args
ixs ConHead
c
        (Con ConHead
c ConInfo
_ Elims
_   , Con ConHead
c' ConInfo
_ Elims
_  ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Type -> QName -> Args -> Term -> Term -> UnifyStep
Conflict Int
k Type
a QName
d Args
pars Term
u Term
v
        (Var Int
i []  , Term
v         ) -> forall {m :: * -> *} {a} {b}.
(ForceNotFree a, Reduce a, MonadReduce m, Free a, MonadPlus m) =>
Int -> a -> m b -> m b
ifOccursStronglyRigid Int
i Term
v forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Type -> QName -> Args -> Int -> Term -> UnifyStep
Cycle Int
k Type
a QName
d Args
pars Int
i Term
v
        (Term
u         , Var Int
j []  ) -> forall {m :: * -> *} {a} {b}.
(ForceNotFree a, Reduce a, MonadReduce m, Free a, MonadPlus m) =>
Int -> a -> m b -> m b
ifOccursStronglyRigid Int
j Term
u forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Type -> QName -> Args -> Int -> Term -> UnifyStep
Cycle Int
k Type
a QName
d Args
pars Int
j Term
u
        (Term, Term)
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
    Term
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
  where
    ifOccursStronglyRigid :: Int -> a -> m b -> m b
ifOccursStronglyRigid Int
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) <- forall a (m :: * -> *).
(ForceNotFree a, Reduce a, MonadReduce m) =>
IntSet -> a -> m (IntMap IsFree, a)
forceNotFree (forall el coll. Singleton el coll => el -> coll
singleton Int
i) a
u
        case forall a. Free a => Int -> a -> Maybe FlexRig
flexRigOccurrenceIn Int
i a
u of
          Just FlexRig
StronglyRigid -> m b
ret
          Maybe FlexRig
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero

checkEqualityStrategy :: Int -> UnifyStrategy
checkEqualityStrategy :: Int -> UnifyStrategy
checkEqualityStrategy Int
k UnifyState
s = do
  let Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v = Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
      n :: Int
n = UnifyState -> Int
eqCount UnifyState
s
  Type
ha <- forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP forall a b. (a -> b) -> a -> b
$ forall a. (Free a, Subst a) => Int -> a -> Maybe a
isHom Int
n Type
a
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Type -> Term -> Term -> UnifyStep
Deletion Int
k Type
ha Term
u Term
v

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

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

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

etaExpandEquationStrategy :: Int -> UnifyStrategy
etaExpandEquationStrategy :: Int -> UnifyStrategy
etaExpandEquationStrategy Int
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 <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> UnifyState -> m Equality
getReducedEqualityUnraised Int
k UnifyState
s
  (QName
d, Args
pars) <- forall (m :: * -> *) a. MonadPlus m => m (Maybe a) -> m a
catMaybesMP forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
HasConstInfo m =>
Type -> m (Maybe (QName, Args))
isEtaRecordType Type
a
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
orM
    [ (forall a b. b -> Either a b
Right Bool
True forall a. Eq a => a -> a -> Bool
==) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
QName -> Args -> m Bool
isSingletonRecord QName
d Args
pars)
    , forall (m :: * -> *). PureTCM m => Term -> m Bool
shouldProject Term
u
    , forall (m :: * -> *). PureTCM m => Term -> m Bool
shouldProject Term
v
    ]
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> QName -> Args -> UnifyStep
EtaExpandEquation Int
k QName
d Args
pars
  where
    shouldProject :: PureTCM m => Term -> m Bool
    shouldProject :: forall (m :: * -> *). PureTCM m => Term -> m Bool
shouldProject = \case
      Def QName
f Elims
es   -> forall (m :: * -> *). HasConstInfo m => QName -> m Bool
usesCopatterns QName
f
      Con ConHead
c ConInfo
_ Elims
_  -> forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, Defn))
isRecordConstructor (ConHead -> QName
conName ConHead
c)

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

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

simplifySizesStrategy :: Int -> UnifyStrategy
simplifySizesStrategy :: Int -> UnifyStrategy
simplifySizesStrategy Int
k UnifyState
s = do
  QName -> Bool
isSizeName <- 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 <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> UnifyState -> m Equality
getReducedEquality Int
k UnifyState
s
  case forall t a. Type'' t a -> a
unEl Type
a of
    Def QName
d Elims
_ -> do
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ QName -> Bool
isSizeName QName
d
      SizeView
su <- forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
u
      SizeView
sv <- 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) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Term -> Term -> UnifyStep
StripSizeSuc Int
k Term
u Term
v
        (SizeSuc Term
u, SizeView
SizeInf  ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Term -> Term -> UnifyStep
StripSizeSuc Int
k Term
u Term
v
        (SizeView
SizeInf  , SizeSuc Term
v) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Term -> Term -> UnifyStep
StripSizeSuc Int
k Term
u Term
v
        (SizeView, SizeView)
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
    Term
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero

injectiveTypeConStrategy :: Int -> UnifyStrategy
injectiveTypeConStrategy :: Int -> UnifyStrategy
injectiveTypeConStrategy Int
k UnifyState
s = do
  Bool
injTyCon <- PragmaOptions -> Bool
optInjectiveTypeConstructors forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
injTyCon
  Equality
eq <- forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqUnLevel forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> UnifyState -> m Equality
getReducedEquality Int
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 forall a. Eq a => a -> a -> Bool
== QName
d' -> do
      -- d must be a data, record or axiom
      Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard 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{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
                GeneralizableVar{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
                Constructor{} -> forall a. HasCallStack => a
__IMPOSSIBLE__  -- Never a type!
      let us :: Args
us = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
          vs :: Args
vs = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es'
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> QName -> Args -> Args -> UnifyStep
TypeConInjectivity Int
k QName
d Args
us Args
vs
    Equality
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero

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

skipIrrelevantStrategy :: Int -> UnifyStrategy
skipIrrelevantStrategy :: Int -> UnifyStrategy
skipIrrelevantStrategy Int
k UnifyState
s = do
  let Equal Dom Type
a Term
_ Term
_ = Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s                                 -- reduce not necessary
  forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s forall t. Abstract t => Telescope -> t -> t
`abstract` UnifyState -> Telescope
eqTel UnifyState
s) forall a b. (a -> b) -> a -> b
$
    forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Eq a => a -> a -> Bool
== forall a b. b -> Either a b
Right Bool
True) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (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`)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> UnifyStep
SkipIrrelevantEquation Int
k


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

unifyStep
  :: (PureTCM m, MonadWriter UnifyOutput m, MonadError TCErr m)
  => UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
unifyStep :: forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m, MonadError TCErr m) =>
UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
unifyStep UnifyState
s Deletion{ deleteAt :: UnifyStep -> Int
deleteAt = Int
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 <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> Term -> Term -> m Bool
pureEqualTerm Type
a Term
u Term
v
    Bool
withoutK <- forall (m :: * -> *). HasOptions m => m Bool
withoutKOption
    Bool
splitOnStrict <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envSplitOnStrict
    case Either Blocker Bool
isReflexive of
      Left Blocker
block   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Blocker -> UnificationResult' a
UnifyBlocked Blocker
block
      Right Bool
False  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []
      Right Bool
True | Bool
withoutK Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
splitOnStrict
                   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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) = Int -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
solveEq Int
k Term
u UnifyState
s
        forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
sigma
        forall a. a -> UnificationResult' a
Unifies forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' Telescope UnifyState
lensEqTel forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce UnifyState
s'

unifyStep UnifyState
s step :: UnifyStep
step@Solution{} = forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m) =>
RetryNormalised
-> UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
solutionStep RetryNormalised
RetryNormalised UnifyState
s UnifyStep
step

unifyStep UnifyState
s (Injectivity Int
k Type
a QName
d Args
pars Args
ixs ConHead
c) = do
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *). HasConstInfo m => QName -> m Bool
consOfHIT forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []) forall a b. (a -> b) -> a -> b
$ do
  Bool
withoutK <- 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) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
k forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (String, t)]
telToList 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  <- forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
getConInfo ConHead
c
  let ctype :: Type
ctype  = Definition -> Type
defType Definition
cdef Type -> Args -> Type
`piApply` Args
pars
  forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
eqTel1) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
40 forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Constructor type: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
ctype
  TelV Telescope
ctel Type
ctarget <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
eqTel1) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
ctype
  let cixs :: Args
cixs = case forall t a. Type'' t a -> a
unEl Type
ctarget of
               Def QName
d' Elims
es | QName
d forall a. Eq a => a -> a -> Bool
== QName
d' ->
                 let args :: Args
args = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
                 in  forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
pars) Args
args
               Term
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

  -- Get index telescope of the datatype
  Type
dtype    <- (Type -> Args -> Type
`piApply` Args
pars) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
  forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
eqTel1) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
40 forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Datatype type: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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 forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
ctel
      notforced :: [IsForced]
notforced = forall a. Int -> a -> [a]
replicate (forall a. Sized a => a -> Int
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.
  FullUnificationResult
res <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Maybe NoLeftInv
-> Telescope
-> FlexibleVars
-> Type
-> Args
-> Args
-> m FullUnificationResult
unifyIndices' (forall a. a -> Maybe a
Just forall a. HasCallStack => a
__IMPOSSIBLE__)
           Telescope
hduTel
           ([IsForced] -> Telescope -> FlexibleVars
allFlexVars [IsForced]
notforced Telescope
hduTel)
           (forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size Telescope
ctel) Type
dtype)
           (forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size Telescope
ctel) Args
ixs)
           Args
cixs
  case FullUnificationResult
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
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Higher-dimensional unification is blocked: propagate
    UnifyBlocked Blocker
block -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
ctel
          rho1 :: PatternSubstitution
rho1    = forall a. Int -> Substitution' a
raiseS (forall a. Sized a => a -> Int
size Telescope
ctel)
          ceq :: DeBruijnPattern
ceq     = forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
noConPatternInfo forall a b. (a -> b) -> a -> b
$ forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
ctel
          rho3 :: PatternSubstitution
rho3    = forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS DeBruijnPattern
ceq PatternSubstitution
rho1
          eqTel2' :: Telescope
eqTel2' = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho3 Telescope
eqTel2
          eqTel' :: Telescope
eqTel'  = Telescope
eqTel1' forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
eqTel2'
          rho :: PatternSubstitution
rho     = forall a. Int -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Int
size Telescope
eqTel2) PatternSubstitution
rho3

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

      Telescope
eqTel' <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) forall a b. (a -> b) -> a -> b
$ 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
      (Args
lhs', Args
rhs') <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) forall a b. (a -> b) -> a -> b
$ do
        let ps :: [NamedArg DeBruijnPattern]
ps = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst PatternSubstitution
rho forall a b. (a -> b) -> a -> b
$ forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
        (Match Term
lhsMatch, Args
_) <- forall (m :: * -> *).
MonadMatch m =>
[NamedArg DeBruijnPattern] -> Args -> m (Match Term, Args)
Match.matchPatterns [NamedArg DeBruijnPattern]
ps forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
eqLHS UnifyState
s
        (Match Term
rhsMatch, Args
_) <- forall (m :: * -> *).
MonadMatch m =>
[NamedArg DeBruijnPattern] -> Args -> m (Match Term, Args)
Match.matchPatterns [NamedArg DeBruijnPattern]
ps forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
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') -> forall (m :: * -> *) a. Monad m => a -> m a
return
            (forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a. Empty -> Int -> IntMap (Arg a) -> [Arg a]
Match.matchedArgs forall a. HasCallStack => a
__IMPOSSIBLE__ (forall a. Sized a => a -> Int
size Telescope
eqTel') IntMap (Arg Term)
lhs',
             forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a. Empty -> Int -> IntMap (Arg a) -> [Arg a]
Match.matchedArgs forall a. HasCallStack => a
__IMPOSSIBLE__ (forall a. Sized a => a -> Int
size Telescope
eqTel') IntMap (Arg Term)
rhs')
          (Match Term, Match Term)
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

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


    UnifyStuck [UnificationFailure]
_ -> let n :: Int
n           = UnifyState -> Int
eqCount UnifyState
s
                        Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v = Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
                    in forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [Telescope -> Type -> Term -> Term -> Args -> UnificationFailure
UnifyIndicesNotVars
                         (UnifyState -> Telescope
varTel UnifyState
s forall t. Abstract t => Telescope -> t -> t
`abstract` UnifyState -> Telescope
eqTel UnifyState
s) Type
a
                         (forall a. Subst a => Int -> a -> a
raise Int
n Term
u) (forall a. Subst a => Int -> a -> a
raise Int
n Term
v) (forall a. Subst a => Int -> a -> a
raise (Int
nforall a. Num a => a -> a -> a
-Int
k) Args
ixs)]

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

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

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

      Telescope
eqTel' <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) forall a b. (a -> b) -> a -> b
$ 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
      (Args
lhs', Args
rhs') <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) forall a b. (a -> b) -> a -> b
$ do
        let ps :: [NamedArg DeBruijnPattern]
ps = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst PatternSubstitution
rho forall a b. (a -> b) -> a -> b
$ forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
        (Match Term
lhsMatch, Args
_) <- forall (m :: * -> *).
MonadMatch m =>
[NamedArg DeBruijnPattern] -> Args -> m (Match Term, Args)
Match.matchPatterns [NamedArg DeBruijnPattern]
ps forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
eqLHS UnifyState
s
        (Match Term
rhsMatch, Args
_) <- forall (m :: * -> *).
MonadMatch m =>
[NamedArg DeBruijnPattern] -> Args -> m (Match Term, Args)
Match.matchPatterns [NamedArg DeBruijnPattern]
ps forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
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') -> forall (m :: * -> *) a. Monad m => a -> m a
return
            (forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a. Empty -> Int -> IntMap (Arg a) -> [Arg a]
Match.matchedArgs forall a. HasCallStack => a
__IMPOSSIBLE__ (forall a. Sized a => a -> Int
size Telescope
eqTel') IntMap (Arg Term)
lhs',
             forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a. Empty -> Int -> IntMap (Arg a) -> [Arg a]
Match.matchedArgs forall a. HasCallStack => a
__IMPOSSIBLE__ (forall a. Sized a => a -> Int
size Telescope
eqTel') IntMap (Arg Term)
rhs')
          (Match Term, Match Term)
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

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

unifyStep UnifyState
s EtaExpandEquation{ expandAt :: UnifyStep -> Int
expandAt = Int
k, expandRecordType :: UnifyStep -> QName
expandRecordType = QName
d, expandParameters :: UnifyStep -> Args
expandParameters = Args
pars } = do
  Defn
recd  <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
d
  let delta :: Telescope
delta = Defn -> Telescope
recTel Defn
recd forall t. Apply t => t -> Args -> t
`apply` Args
pars
      c :: ConHead
c     = Defn -> ConHead
recConHead Defn
recd
  Args
lhs   <- Args -> m Args
expandKth forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
eqLHS UnifyState
s
  Args
rhs   <- Args -> m Args
expandKth forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
eqRHS UnifyState
s
  let (Telescope
tel, PatternSubstitution
sigma) = Telescope
-> Int -> Telescope -> ConHead -> (Telescope, PatternSubstitution)
expandTelescopeVar (UnifyState -> Telescope
eqTel UnifyState
s) Int
k Telescope
delta ConHead
c
  forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
sigma
  forall a. a -> UnificationResult' a
Unifies forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
   Lens' Telescope UnifyState
lensEqTel forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ UnifyState
s
    { eqTel :: Telescope
eqTel    = Telescope
tel
    , eqLHS :: Args
eqLHS    = Args
lhs
    , eqRHS :: Args
eqRHS    = Args
rhs
    }
  where
    expandKth :: Args -> m Args
expandKth Args
us = do
      let (Args
us1,Arg Term
v:Args
us2) = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt Int
k Args
us
      Args
vs <- forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasConstInfo m, MonadDebug m, ReadTCState m) =>
QName -> Args -> Term -> m (Telescope, Args)
etaExpandRecord QName
d Args
pars (forall e. Arg e -> e
unArg Arg Term
v)
      Args
vs <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Args
vs
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Args
us1 forall a. [a] -> [a] -> [a]
++ Args
vs forall a. [a] -> [a] -> [a]
++ Args
us2

unifyStep UnifyState
s LitConflict
  { litType :: UnifyStep -> Type
litType          = Type
a
  , litConflictLeft :: UnifyStep -> Literal
litConflictLeft  = Literal
l
  , litConflictRight :: UnifyStep -> Literal
litConflictRight = Literal
l'
  } = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. NegativeUnification -> UnificationResult' a
NoUnify 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 Int
k Term
u Term
v) = do
  Type
sizeTy <- forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType
  Term
sizeSu <- forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc Int
1 (Int -> Term
var Int
0)
  let n :: Int
n          = UnifyState -> Int
eqCount UnifyState
s
      sub :: Substitution
sub        = forall a. Int -> Substitution' a -> Substitution' a
liftS (Int
nforall a. Num a => a -> a -> a
-Int
kforall a. Num a => a -> a -> a
-Int
1) forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
sizeSu forall a b. (a -> b) -> a -> b
$ forall a. Int -> Substitution' a
raiseS Int
1
      eqFlatTel :: [Dom Type]
eqFlatTel  = forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
      eqFlatTel' :: [Dom Type]
eqFlatTel' = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sub forall a b. (a -> b) -> a -> b
$ forall a. Int -> (a -> a) -> [a] -> [a]
updateAt Int
k (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Type
sizeTy) forall a b. (a -> b) -> a -> b
$ [Dom Type]
eqFlatTel
      eqTel' :: Telescope
eqTel'     = [String] -> [Dom Type] -> Telescope
unflattenTel (Telescope -> [String]
teleNames 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!
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> UnificationResult' a
Unifies forall a b. (a -> b) -> a -> b
$ UnifyState
s
    { eqTel :: Telescope
eqTel = Telescope
eqTel'
    , eqLHS :: Args
eqLHS = forall a. Int -> (a -> a) -> [a] -> [a]
updateAt Int
k (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg Term
u) forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
eqLHS UnifyState
s
    , eqRHS :: Args
eqRHS = forall a. Int -> (a -> a) -> [a] -> [a]
updateAt Int
k (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg Term
v) forall a b. (a -> b) -> a -> b
$ UnifyState -> Args
eqRHS UnifyState
s
    }

unifyStep UnifyState
s (SkipIrrelevantEquation Int
k) = do
  let lhs :: Args
lhs = UnifyState -> Args
eqLHS UnifyState
s
      (UnifyState
s', PatternSubstitution
sigma) = Int -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
solveEq Int
k (Term -> Term
DontCare forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ Args
lhs Int
k) UnifyState
s
  forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
sigma
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> UnificationResult' a
Unifies UnifyState
s'

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

data RetryNormalised = RetryNormalised | DontRetryNormalised
  deriving (RetryNormalised -> RetryNormalised -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RetryNormalised -> RetryNormalised -> Bool
$c/= :: RetryNormalised -> RetryNormalised -> Bool
== :: RetryNormalised -> RetryNormalised -> Bool
$c== :: RetryNormalised -> RetryNormalised -> Bool
Eq, Int -> RetryNormalised -> ShowS
[RetryNormalised] -> ShowS
RetryNormalised -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RetryNormalised] -> ShowS
$cshowList :: [RetryNormalised] -> ShowS
show :: RetryNormalised -> String
$cshow :: RetryNormalised -> String
showsPrec :: Int -> RetryNormalised -> ShowS
$cshowsPrec :: Int -> 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 -> Int
solutionAt   = Int
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 Int
solutionVar  = fi :: FlexibleVar Int
fi@FlexibleVar{ flexVar :: forall a. FlexibleVar a -> a
flexVar = Int
i }
               , solutionTerm :: UnifyStep -> Term
solutionTerm = Term
u } = do
  let m :: Int
m = UnifyState -> Int
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 <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Bool TCEnv
eMakeCase
  let forcedVars :: IntMap Modality
forcedVars | Bool
inMakeCase = forall a. IntMap a
IntMap.empty
                 | Bool
otherwise  = forall a. [(Int, a)] -> IntMap a
IntMap.fromList [ (forall a. FlexibleVar a -> a
flexVar FlexibleVar Int
fi, forall a. LensModality a => a -> Modality
getModality FlexibleVar Int
fi) | FlexibleVar Int
fi <- UnifyState -> FlexibleVars
flexVars UnifyState
s,
                                                                                 forall a. FlexibleVar a -> IsForced
flexForced FlexibleVar Int
fi forall a. Eq a => a -> a -> Bool
== IsForced
Forced ]
  (DeBruijnPattern
p, IntMap Modality
bound) <- forall (m :: * -> *).
PureTCM m =>
IntMap Modality -> Term -> m (DeBruijnPattern, 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS forall a. Substitution' a
idS [ forall a. EndoSubst a => Int -> a -> Substitution' a
inplaceS Int
i (forall a. Term -> Pattern' a
dotP (Int -> Elims -> Term
Var Int
i [])) | Int
i <- forall a. IntMap a -> [Int]
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
        | forall a. IntMap a -> Bool
IntMap.null IntMap Modality
vars = Telescope
tel
        | Bool
otherwise        = ListTel -> Telescope
telFromList forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Dom (String, Type) -> Dom (String, Type)
upd (forall a. Integral a => a -> [a]
downFrom forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Int
size Telescope
tel) (forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel)
        where
          upd :: Int -> Dom (String, Type) -> Dom (String, Type)
upd Int
i Dom (String, Type)
a | Just Modality
md' <- forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap Modality
vars = 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 <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ UnifyState
s { varTel :: Telescope
varTel = Modality -> IntMap Modality -> Telescope -> Telescope
updModality (forall a. LensModality a => a -> Modality
getModality FlexibleVar Int
fi) IntMap Modality
bound (UnifyState -> Telescope
varTel UnifyState
s) }

  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.force" Int
45 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"forcedVars =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall a. IntMap a -> [Int]
IntMap.keys IntMap Modality
forcedVars)
    , TCMT IO Doc
"u          =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
    , TCMT IO Doc
"p          =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM DeBruijnPattern
p
    , TCMT IO Doc
"bound      =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall a. IntMap a -> [Int]
IntMap.keys IntMap Modality
bound)
    , TCMT IO Doc
"dotSub     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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' } = Int -> UnifyState -> Dom Type
getVarType (Int
mforall a. Num a => a -> a -> a
-Int
1forall a. Num a => a -> a -> a
-Int
i) UnifyState
s
  Either Blocker Bool
equalTypes <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
45 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Equation type: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
    forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
45 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Variable type: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a'
    forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> Type -> m Bool
pureEqualType 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 <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Modality TCEnv
eModality
  let eqrel :: Relevance
eqrel  = forall a. LensRelevance a => a -> Relevance
getRelevance Dom Type
dom
      eqmod :: Modality
eqmod  = forall a. LensModality a => a -> Modality
getModality Dom Type
dom
      varmod :: Modality
varmod = forall a. LensModality a => a -> Modality
getModality Dom Type
dom'
      mod :: Modality
mod    = forall a. Bool -> (a -> a) -> a -> a
applyUnless (Relevance
NonStrict Relevance -> Relevance -> Bool
`moreRelevant` Relevance
eqrel) (forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
eqrel)
             forall a b. (a -> b) -> a -> b
$ forall a. Bool -> (a -> a) -> a -> a
applyUnless (forall a. LensQuantity a => a -> Bool
usableQuantity Modality
envmod) (forall a. LensQuantity a => Quantity -> a -> a
setQuantity Quantity
zeroQuantity)
             forall a b. (a -> b) -> a -> b
$ Modality
varmod
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
65 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> m Doc
text forall a b. (a -> b) -> a -> b
$ String
"Equation modality: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. LensModality a => a -> Modality
getModality Dom Type
dom)
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
65 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> m Doc
text forall a b. (a -> b) -> a -> b
$ String
"Variable modality: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Modality
varmod
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
65 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> m Doc
text forall a b. (a -> b) -> a -> b
$ String
"Solution must be usable in a " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Modality
mod 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 <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
 MonadAddContext m, MonadDebug m, MonadReduce m,
 MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Term
u
  forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (forall (m :: * -> *) a. Monad m => a -> m a
return Either Blocker Bool
eusable) (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Blocker -> UnificationResult' a
UnifyBlocked) forall a b. (a -> b) -> a -> b
$ \ Bool
usable -> do

  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
45 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Modality ok: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Bool
usable
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
usable forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
65 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Rejected solution: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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 (forall a. LensCohesion a => a -> Cohesion
getCohesion Modality
eqmod Cohesion -> Cohesion -> Bool
`moreCohesion` forall a. LensCohesion a => a -> Cohesion
getCohesion Modality
varmod) then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [] else do

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

unify
  :: (PureTCM m, MonadWriter UnifyLog' m, MonadError TCErr m)
  => UnifyState -> UnifyStrategy -> m (UnificationResult' UnifyState)
unify :: forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyLog' m, MonadError TCErr m) =>
UnifyState -> UnifyStrategy -> m (UnificationResult' UnifyState)
unify UnifyState
s UnifyStrategy
strategy = if UnifyState -> Bool
isUnifyStateSolved UnifyState
s
                   then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> UnificationResult' a
Unifies UnifyState
s
                   else forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyLog' m, MonadError TCErr m) =>
ListT m UnifyStep -> m (UnificationResult' UnifyState)
tryUnifyStepsAndContinue (UnifyStrategy
strategy UnifyState
s)
  where
    tryUnifyStepsAndContinue
      :: (PureTCM m, MonadWriter UnifyLog' m, MonadError TCErr m)
      => ListT m UnifyStep -> m (UnificationResult' UnifyState)
    tryUnifyStepsAndContinue :: forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyLog' m, MonadError TCErr m) =>
ListT m UnifyStep -> m (UnificationResult' UnifyState)
tryUnifyStepsAndContinue ListT m UnifyStep
steps = do
      UnificationResult' UnifyState
x <- forall (m :: * -> *) a b.
Monad m =>
(a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyLog' m, MonadError TCErr m) =>
UnifyStep
-> m (UnificationResult' UnifyState)
-> m (UnificationResult' UnifyState)
tryUnifyStep forall (m :: * -> *) a. Monad m => m (UnificationResult' a)
failure ListT m UnifyStep
steps
      case UnificationResult' UnifyState
x of
        Unifies UnifyState
s'     -> forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyLog' m, MonadError TCErr m) =>
UnifyState -> UnifyStrategy -> m (UnificationResult' UnifyState)
unify UnifyState
s' UnifyStrategy
strategy
        NoUnify NegativeUnification
err    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. NegativeUnification -> UnificationResult' a
NoUnify NegativeUnification
err
        UnifyBlocked Blocker
b -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Blocker -> UnificationResult' a
UnifyBlocked Blocker
b
        UnifyStuck [UnificationFailure]
err -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [UnificationFailure]
err

    tryUnifyStep :: (PureTCM m, MonadWriter UnifyLog' m, MonadError TCErr m)
                 => UnifyStep
                 -> m (UnificationResult' UnifyState)
                 -> m (UnificationResult' UnifyState)
    tryUnifyStep :: forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyLog' m, MonadError TCErr m) =>
UnifyStep
-> m (UnificationResult' UnifyState)
-> m (UnificationResult' UnifyState)
tryUnifyStep UnifyStep
step m (UnificationResult' UnifyState)
fallback = do
      forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"trying unifyStep" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM UnifyStep
step
      (UnificationResult' UnifyState
x, UnifyOutput
output) <- forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m, MonadError TCErr m) =>
UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
unifyStep UnifyState
s UnifyStep
step
      case UnificationResult' UnifyState
x of
        Unifies UnifyState
s'   -> do
          forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"unifyStep successful."
          forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"new unifyState:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM UnifyState
s'
          -- tell output
          forall (m :: * -> *).
MonadWriter UnifyLog' m =>
(UnifyLogEntry, UnifyState) -> m ()
writeUnifyLog forall a b. (a -> b) -> a -> b
$ (UnifyState -> UnifyStep -> UnifyOutput -> UnifyLogEntry
UnificationStep UnifyState
s UnifyStep
step UnifyOutput
output,UnifyState
s')
          forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
x
        NoUnify{}       -> forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
x
        UnifyBlocked Blocker
b1 -> do
          UnificationResult' UnifyState
y <- m (UnificationResult' UnifyState)
fallback
          case UnificationResult' UnifyState
y of
            UnifyStuck [UnificationFailure]
_    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Blocker -> UnificationResult' a
UnifyBlocked Blocker
b1
            UnifyBlocked Blocker
b2 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Blocker -> UnificationResult' a
UnifyBlocked forall a b. (a -> b) -> a -> b
$ Blocker -> Blocker -> Blocker
unblockOnEither Blocker
b1 Blocker
b2
            UnificationResult' UnifyState
_               -> forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
y
        UnifyStuck [UnificationFailure]
err1 -> do
          UnificationResult' UnifyState
y <- m (UnificationResult' UnifyState)
fallback
          case UnificationResult' UnifyState
y of
            UnifyStuck [UnificationFailure]
err2 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck forall a b. (a -> b) -> a -> b
$ [UnificationFailure]
err1 forall a. [a] -> [a] -> [a]
++ [UnificationFailure]
err2
            UnificationResult' UnifyState
_               -> 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 (DeBruijnPattern, IntMap Modality)
patternBindingForcedVars IntMap Modality
forced Term
v = do
  let v' :: Term
v' = forall a. PrecomputeFreeVars a => a -> a
precomputeFreeVars_ Term
v
  forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (forall {t :: (* -> *) -> * -> *} {t :: (* -> *) -> * -> *}
       {m :: * -> *} {a}.
(MonadWriter (IntMap Modality) (t (t m)), HasConstInfo (t (t m)),
 DeBruijn a, MonadTrans t, MonadTrans t, Monad (t m), MonadReduce m,
 MonadState (IntMap Modality) (t (t m))) =>
Modality -> Term -> t (t m) (Pattern' a)
go Modality
defaultModality Term
v') IntMap Modality
forced)
  where
    noForced :: a -> m Bool
noForced a
v = forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a -> b) -> a -> b
$ IntSet -> IntSet -> Bool
IntSet.disjoint (forall a. PrecomputeFreeVars a => a -> IntSet
precomputedFreeVars a
v) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IntMap a -> IntSet
IntMap.keysSet

    bind :: a -> Int -> m (Pattern' a)
bind a
md Int
i = do
      forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just a
md' | 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
          forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell   forall a b. (a -> b) -> a -> b
$ forall a. Int -> a -> IntMap a
IntMap.singleton Int
i a
md
          forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall a. Int -> IntMap a -> IntMap a
IntMap.delete Int
i
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Pattern' a
varP (forall a. DeBruijn a => Int -> a
deBruijnVar Int
i)
        Maybe a
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP (Int -> Elims -> Term
Var Int
i [])

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

        -- Non-pattern positions
        Var Int
_ (Elim
_:Elims
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
        Lam{}       -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
        Pi{}        -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
        Def{}       -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
        MetaV{}     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
        Sort{}      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
        Level{}     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
        DontCare{}  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
        Dummy{}     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
        Lit{}       -> forall a. HasCallStack => a
__IMPOSSIBLE__