1{-# LANGUAGE NondecreasingIndentation #-} 2 3-- | Unification algorithm for specializing datatype indices, as described in 4-- \"Unifiers as Equivalences: Proof-Relevant Unification of Dependently 5-- Typed Data\" by Jesper Cockx, Dominique Devriese, and Frank Piessens 6-- (ICFP 2016). 7-- 8-- This is the unification algorithm used for checking the left-hand side 9-- of clauses (see @Agda.TypeChecking.Rules.LHS@), coverage checking (see 10-- @Agda.TypeChecking.Coverage@) and indirectly also for interactive case 11-- splitting (see @Agda.Interaction.MakeCase@). 12-- 13-- A unification problem (of type @UnifyState@) consists of: 14-- 15-- 1. A telescope @varTel@ of free variables, some or all of which are 16-- flexible (as indicated by @flexVars@). 17-- 18-- 2. A telescope @eqTel@ containing the types of the equations. 19-- 20-- 3. Left- and right-hand sides for each equation: 21-- @varTel ⊢ eqLHS : eqTel@ and @varTel ⊢ eqRHS : eqTel@. 22-- 23-- The unification algorithm can end in three different ways: 24-- (type @UnificationResult@): 25-- 26-- - A *positive success* @Unifies (tel, sigma, ps)@ with @tel ⊢ sigma : varTel@, 27-- @tel ⊢ eqLHS [ varTel ↦ sigma ] ≡ eqRHS [ varTel ↦ sigma ] : eqTel@, 28-- and @tel ⊢ ps : eqTel@. In this case, @sigma;ps@ is an *equivalence* 29-- between the telescopes @tel@ and @varTel(eqLHS ≡ eqRHS)@. 30-- 31-- - A *negative success* @NoUnify err@ means that a conflicting equation 32-- was found (e.g an equation between two distinct constructors or a cycle). 33-- 34-- - A *failure* @UnifyStuck err@ means that the unifier got stuck. 35-- 36-- The unification algorithm itself consists of two parts: 37-- 38-- 1. A *unification strategy* takes a unification problem and produces a 39-- list of suggested unification rules (of type @UnifyStep@). Strategies 40-- can be constructed by composing simpler strategies (see for example the 41-- definition of @completeStrategyAt@). 42-- 43-- 2. The *unification engine* @unifyStep@ takes a unification rule and tries 44-- to apply it to the given state, writing the result to the UnifyOutput 45-- on a success. 46-- 47-- The unification steps (of type @UnifyStep@) are the following: 48-- 49-- - *Deletion* removes a reflexive equation @u =?= v : a@ if the left- and 50-- right-hand side @u@ and @v@ are (definitionally) equal. This rule results 51-- in a failure if --without-K is enabled (see \"Pattern Matching Without K\" 52-- by Jesper Cockx, Dominique Devriese, and Frank Piessens (ICFP 2014). 53-- 54-- - *Solution* solves an equation if one side is (eta-equivalent to) a 55-- flexible variable. In case both sides are flexible variables, the 56-- unification strategy makes a choice according to the @chooseFlex@ 57-- function in @Agda.TypeChecking.Rules.LHS.Problem@. 58-- 59-- - *Injectivity* decomposes an equation of the form 60-- @c us =?= c vs : D pars is@ where @c : Δc → D pars js@ is a constructor 61-- of the inductive datatype @D@ into a sequence of equations 62-- @us =?= vs : delta@. In case @D@ is an indexed datatype, 63-- *higher-dimensional unification* is applied (see below). 64-- 65-- - *Conflict* detects absurd equations of the form 66-- @c₁ us =?= c₂ vs : D pars is@ where @c₁@ and @c₂@ are two distinct 67-- constructors of the datatype @D@. 68-- 69-- - *Cycle* detects absurd equations of the form @x =?= v : D pars is@ where 70-- @x@ is a variable of the datatype @D@ that occurs strongly rigid in @v@. 71-- 72-- - *EtaExpandVar* eta-expands a single flexible variable @x : R@ where @R@ 73-- is a (eta-expandable) record type, replacing it by one variable for each 74-- field of @R@. 75-- 76-- - *EtaExpandEquation* eta-expands an equation @u =?= v : R@ where @R@ is a 77-- (eta-expandable) record type, replacing it by one equation for each field 78-- of @R@. The left- and right-hand sides of these equations are the 79-- projections of @u@ and @v@. 80-- 81-- - *LitConflict* detects absurd equations of the form @l₁ =?= l₂ : A@ where 82-- @l₁@ and @l₂@ are distinct literal terms. 83-- 84-- - *StripSizeSuc* simplifies an equation of the form 85-- @sizeSuc x =?= sizeSuc y : Size@ to @x =?= y : Size@. 86-- 87-- - *SkipIrrelevantEquation@ removes an equation between irrelevant terms. 88-- 89-- - *TypeConInjectivity* decomposes an equation of the form 90-- @D us =?= D vs : Set i@ where @D@ is a datatype. This rule is only used 91-- if --injective-type-constructors is enabled. 92-- 93-- Higher-dimensional unification (new, does not yet appear in any paper): 94-- If an equation of the form @c us =?= c vs : D pars is@ is encountered where 95-- @c : Δc → D pars js@ is a constructor of an indexed datatype 96-- @D pars : Φ → Set ℓ@, it is in general unsound to just simplify this 97-- equation to @us =?= vs : Δc@. For this reason, the injectivity rule in the 98-- paper restricts the indices @is@ to be distinct variables that are bound in 99-- the telescope @eqTel@. But we can be more general by introducing new 100-- variables @ks@ to the telescope @eqTel@ and equating these to @is@: 101-- @ 102-- Δ₁(x : D pars is)Δ₂ 103-- ≃ 104-- Δ₁(ks : Φ)(x : D pars ks)(ps : is ≡Φ ks)Δ₂ 105-- @ 106-- Since @ks@ are distinct variables, it's now possible to apply injectivity 107-- to the equation @x@, resulting in the following new equation telescope: 108-- @ 109-- Δ₁(ys : Δc)(ps : is ≡Φ js[Δc ↦ ys])Δ₂ 110-- @ 111-- Now we can solve the equations @ps@ by recursively calling the unification 112-- algorithm with flexible variables @Δ₁(ys : Δc)@. This is called 113-- *higher-dimensional unification* since we are unifying equality proofs 114-- rather than terms. If the higher-dimensional unification succeeds, the 115-- resulting telescope serves as the new equation telescope for the original 116-- unification problem. 117 118module Agda.TypeChecking.Rules.LHS.Unify 119 ( UnificationResult 120 , UnificationResult'(..) 121 , unifyIndices ) where 122 123import Prelude hiding (null) 124 125import Control.Monad 126import Control.Monad.State 127import Control.Monad.Writer (WriterT(..), MonadWriter(..)) 128import Control.Monad.Except 129 130import Data.Semigroup hiding (Arg) 131import qualified Data.List as List 132import qualified Data.IntSet as IntSet 133import qualified Data.IntMap as IntMap 134import Data.IntMap (IntMap) 135 136import qualified Agda.Benchmarking as Bench 137 138import Agda.Interaction.Options (optInjectiveTypeConstructors) 139 140import Agda.Syntax.Common 141import Agda.Syntax.Internal 142import Agda.Syntax.Literal 143 144import Agda.TypeChecking.Monad 145import qualified Agda.TypeChecking.Monad.Benchmark as Bench 146import Agda.TypeChecking.Conversion.Pure 147import Agda.TypeChecking.Constraints 148import Agda.TypeChecking.Datatypes 149import Agda.TypeChecking.Irrelevance 150import Agda.TypeChecking.Level (reallyUnLevelView) 151import Agda.TypeChecking.Reduce 152import qualified Agda.TypeChecking.Patterns.Match as Match 153import Agda.TypeChecking.Pretty 154import Agda.TypeChecking.Substitute 155import Agda.TypeChecking.Telescope 156import Agda.TypeChecking.Free 157import Agda.TypeChecking.Free.Precompute 158import Agda.TypeChecking.Free.Reduce 159import Agda.TypeChecking.Records 160 161import Agda.TypeChecking.Rules.LHS.Problem 162 163import Agda.Utils.Benchmark 164import Agda.Utils.Either 165import Agda.Utils.Function 166import Agda.Utils.Functor 167import Agda.Utils.Lens 168import Agda.Utils.List 169import Agda.Utils.ListT 170import Agda.Utils.Maybe 171import Agda.Utils.Monad 172import Agda.Utils.Null 173import Agda.Utils.PartialOrd 174import Agda.Utils.Permutation 175import Agda.Utils.Singleton 176import Agda.Utils.Size 177import Agda.Utils.Tuple 178 179import Agda.Utils.Impossible 180 181-- | Result of 'unifyIndices'. 182type UnificationResult = UnificationResult' 183 ( Telescope -- @tel@ 184 , PatternSubstitution -- @sigma@ s.t. @tel ⊢ sigma : varTel@ 185 , [NamedArg DeBruijnPattern] -- @ps@ s.t. @tel ⊢ ps : eqTel @ 186 ) 187 188data UnificationResult' a 189 = Unifies a -- ^ Unification succeeded. 190 | NoUnify NegativeUnification -- ^ Terms are not unifiable. 191 | UnifyBlocked Blocker -- ^ Unification got blocked on a metavariable 192 | UnifyStuck [UnificationFailure] -- ^ Some other error happened, unification got stuck. 193 deriving (Show, Functor, Foldable, Traversable) 194 195-- | Unify indices. 196-- 197-- In @unifyIndices gamma flex a us vs@, 198-- 199-- * @us@ and @vs@ are the argument lists to unify, eliminating type @a@. 200-- 201-- * @gamma@ is the telescope of free variables in @us@ and @vs@. 202-- 203-- * @flex@ is the set of flexible (instantiable) variabes in @us@ and @vs@. 204-- 205-- The result is the most general unifier of @us@ and @vs@. 206unifyIndices 207 :: (PureTCM m, MonadBench m, BenchPhase m ~ Bench.Phase) 208 => Telescope -- ^ @gamma@ 209 -> FlexibleVars -- ^ @flex@ 210 -> Type -- ^ @a@ 211 -> Args -- ^ @us@ 212 -> Args -- ^ @vs@ 213 -> m UnificationResult 214unifyIndices tel flex a us vs = 215 Bench.billTo [Bench.Typing, Bench.CheckLHS, Bench.UnifyIndices] $ 216 unifyIndices' tel flex a us vs 217 218unifyIndices' 219 :: (PureTCM m) 220 => Telescope -- ^ @gamma@ 221 -> FlexibleVars -- ^ @flex@ 222 -> Type -- ^ @a@ 223 -> Args -- ^ @us@ 224 -> Args -- ^ @vs@ 225 -> m UnificationResult 226unifyIndices' tel flex a [] [] = return $ Unifies (tel, idS, []) 227unifyIndices' tel flex a us vs = do 228 reportSDoc "tc.lhs.unify" 10 $ 229 sep [ "unifyIndices" 230 , ("tel =" <+>) $ nest 2 $ prettyTCM tel 231 , ("flex =" <+>) $ nest 2 $ addContext tel $ text $ show $ map flexVar flex 232 , ("a =" <+>) $ nest 2 $ addContext tel $ parens (prettyTCM a) 233 , ("us =" <+>) $ nest 2 $ addContext tel $ prettyList $ map prettyTCM us 234 , ("vs =" <+>) $ nest 2 $ addContext tel $ prettyList $ map prettyTCM vs 235 ] 236 initialState <- initUnifyState tel flex a us vs 237 reportSDoc "tc.lhs.unify" 20 $ "initial unifyState:" <+> prettyTCM initialState 238 reportSDoc "tc.lhs.unify" 70 $ "initial unifyState:" <+> text (show initialState) 239 (result,output) <- runUnifyLogT $ unify initialState rightToLeftStrategy 240 let ps = applySubst (unifyProof output) $ teleNamedArgs (eqTel initialState) 241 return $ fmap (\s -> (varTel s , unifySubst output , ps)) result 242 243---------------------------------------------------- 244-- Equalities 245---------------------------------------------------- 246 247data Equality = Equal 248 { _eqType :: Dom Type 249 , _eqLeft :: Term 250 , _eqRight :: Term 251 } 252 253instance Reduce Equality where 254 reduce' (Equal a u v) = Equal <$> reduce' a <*> reduce' u <*> reduce' v 255 256eqConstructorForm :: HasBuiltins m => Equality -> m Equality 257eqConstructorForm (Equal a u v) = Equal a <$> constructorForm u <*> constructorForm v 258 259eqUnLevel :: HasBuiltins m => Equality -> m Equality 260eqUnLevel (Equal a u v) = Equal a <$> unLevel u <*> unLevel v 261 where 262 unLevel (Level l) = reallyUnLevelView l 263 unLevel u = return u 264 265---------------------------------------------------- 266-- Unify state 267---------------------------------------------------- 268 269data UnifyState = UState 270 { varTel :: Telescope -- ^ Don't reduce! 271 , flexVars :: FlexibleVars 272 , eqTel :: Telescope -- ^ Can be reduced eagerly. 273 , eqLHS :: [Arg Term] -- ^ Ends up in dot patterns (should not be reduced eagerly). 274 , eqRHS :: [Arg Term] -- ^ Ends up in dot patterns (should not be reduced eagerly). 275 } deriving (Show) 276-- Issues #3578 and #4125: avoid unnecessary reduction in unifier. 277 278lensVarTel :: Lens' Telescope UnifyState 279lensVarTel f s = f (varTel s) <&> \ tel -> s { varTel = tel } 280--UNUSED Liang-Ting Chen 2019-07-16 281--lensFlexVars :: Lens' FlexibleVars UnifyState 282--lensFlexVars f s = f (flexVars s) <&> \ flex -> s { flexVars = flex } 283 284lensEqTel :: Lens' Telescope UnifyState 285lensEqTel f s = f (eqTel s) <&> \ x -> s { eqTel = x } 286 287--UNUSED Liang-Ting Chen 2019-07-16 288--lensEqLHS :: Lens' Args UnifyState 289--lensEqLHS f s = f (eqLHS s) <&> \ x -> s { eqLHS = x } 290 291--UNUSED Liang-Ting Chen 2019-07-16 292--lensEqRHS :: Lens' Args UnifyState 293--lensEqRHS f s = f (eqRHS s) <&> \ x -> s { eqRHS = x } 294 295-- UNUSED Andreas, 2019-10-14 296-- instance Reduce UnifyState where 297-- reduce' (UState var flex eq lhs rhs) = 298-- UState <$> reduce' var 299-- <*> pure flex 300-- <*> reduce' eq 301-- <*> reduce' lhs 302-- <*> reduce' rhs 303 304-- Andreas, 2019-10-14, issues #3578 and #4125: 305-- | Don't ever reduce the whole 'varTel', as it will destroy 306-- readability of the context in interactive editing! 307-- To make sure this insight is not lost, the following 308-- dummy instance should prevent a proper 'Reduce' instance for 'UnifyState'. 309instance Reduce UnifyState where 310 reduce' = __IMPOSSIBLE__ 311 312--UNUSED Liang-Ting Chen 2019-07-16 313--reduceEqTel :: UnifyState -> TCM UnifyState 314--reduceEqTel = lensEqTel reduce 315 316-- UNUSED Andreas, 2019-10-14 317-- instance Normalise UnifyState where 318-- normalise' (UState var flex eq lhs rhs) = 319-- UState <$> normalise' var 320-- <*> pure flex 321-- <*> normalise' eq 322-- <*> normalise' lhs 323-- <*> normalise' rhs 324 325instance PrettyTCM UnifyState where 326 prettyTCM state = "UnifyState" $$ nest 2 (vcat $ 327 [ "variable tel: " <+> prettyTCM gamma 328 , "flexible vars: " <+> pshow (map flexVarF $ flexVars state) 329 , "equation tel: " <+> addContext gamma (prettyTCM delta) 330 , "equations: " <+> addContext gamma (prettyList_ (zipWith prettyEquality (eqLHS state) (eqRHS state))) 331 ]) 332 where 333 flexVarF fi = (flexVar fi, flexForced fi) 334 gamma = varTel state 335 delta = eqTel state 336 prettyEquality x y = prettyTCM x <+> "=?=" <+> prettyTCM y 337 338initUnifyState 339 :: PureTCM m 340 => Telescope -> FlexibleVars -> Type -> Args -> Args -> m UnifyState 341initUnifyState tel flex a lhs rhs = do 342 (tel, a, lhs, rhs) <- instantiateFull (tel, a, lhs, rhs) 343 let n = size lhs 344 unless (n == size rhs) __IMPOSSIBLE__ 345 TelV eqTel _ <- telView a 346 unless (n == size eqTel) __IMPOSSIBLE__ 347 return $ UState tel flex eqTel lhs rhs 348 -- Andreas, 2019-02-23, issue #3578: do not eagerly reduce 349 -- reduce $ UState tel flex eqTel lhs rhs 350 351isUnifyStateSolved :: UnifyState -> Bool 352isUnifyStateSolved = null . eqTel 353 354varCount :: UnifyState -> Int 355varCount = size . varTel 356 357-- | Get the type of the i'th variable in the given state 358getVarType :: Int -> UnifyState -> Dom Type 359getVarType i s = indexWithDefault __IMPOSSIBLE__ (flattenTel $ varTel s) i 360 361getVarTypeUnraised :: Int -> UnifyState -> Dom Type 362getVarTypeUnraised i s = snd <$> indexWithDefault __IMPOSSIBLE__ (telToList $ varTel s) i 363 364eqCount :: UnifyState -> Int 365eqCount = size . eqTel 366 367-- | Get the k'th equality in the given state. The left- and right-hand sides 368-- of the equality live in the varTel telescope, and the type of the equality 369-- lives in the varTel++eqTel telescope 370getEquality :: Int -> UnifyState -> Equality 371getEquality k UState { eqTel = eqs, eqLHS = lhs, eqRHS = rhs } = 372 Equal (indexWithDefault __IMPOSSIBLE__ (flattenTel eqs) k) 373 (unArg $ indexWithDefault __IMPOSSIBLE__ lhs k) 374 (unArg $ indexWithDefault __IMPOSSIBLE__ rhs k) 375 376-- | As getEquality, but with the unraised type 377getEqualityUnraised :: Int -> UnifyState -> Equality 378getEqualityUnraised k UState { eqTel = eqs, eqLHS = lhs, eqRHS = rhs } = 379 Equal (snd <$> indexWithDefault __IMPOSSIBLE__ (telToList eqs) k) 380 (unArg $ indexWithDefault __IMPOSSIBLE__ lhs k) 381 (unArg $ indexWithDefault __IMPOSSIBLE__ rhs k) 382 383--UNUSED Liang-Ting Chen 2019-07-16 384--getEqInfo :: Int -> UnifyState -> ArgInfo 385--getEqInfo k UState { eqTel = eqs } = 386-- domInfo $ indexWithDefault __IMPOSSIBLE__ (telToList eqs) k 387-- 388---- | Add a list of equations to the front of the equation telescope 389--addEqs :: Telescope -> [Arg Term] -> [Arg Term] -> UnifyState -> UnifyState 390--addEqs tel us vs s = 391-- s { eqTel = tel `abstract` eqTel s 392-- , eqLHS = us ++ eqLHS s 393-- , eqRHS = vs ++ eqRHS s 394-- } 395-- where k = size tel 396-- 397--addEq :: Type -> Arg Term -> Arg Term -> UnifyState -> UnifyState 398--addEq a u v = addEqs (ExtendTel (defaultDom a) (Abs underscore EmptyTel)) [u] [v] 399 400 401 402-- | Instantiate the k'th variable with the given value. 403-- Returns Nothing if there is a cycle. 404solveVar :: Int -- ^ Index @k@ 405 -> DeBruijnPattern -- ^ Solution @u@ 406 -> UnifyState -> Maybe (UnifyState, PatternSubstitution) 407solveVar k u s = case instantiateTelescope (varTel s) k u of 408 Nothing -> Nothing 409 Just (tel' , sigma , rho) -> Just $ (,sigma) $ UState 410 { varTel = tel' 411 , flexVars = permuteFlex (reverseP rho) $ flexVars s 412 , eqTel = applyPatSubst sigma $ eqTel s 413 , eqLHS = applyPatSubst sigma $ eqLHS s 414 , eqRHS = applyPatSubst sigma $ eqRHS s 415 } 416 where 417 permuteFlex :: Permutation -> FlexibleVars -> FlexibleVars 418 permuteFlex perm = 419 mapMaybe $ \(FlexibleVar ai fc k p x) -> 420 FlexibleVar ai fc k p <$> List.elemIndex x (permPicks perm) 421 422applyUnder :: Int -> Telescope -> Term -> Telescope 423applyUnder k tel u 424 | k < 0 = __IMPOSSIBLE__ 425 | k == 0 = tel `apply1` u 426 | otherwise = case tel of 427 EmptyTel -> __IMPOSSIBLE__ 428 ExtendTel a tel' -> ExtendTel a $ 429 Abs (absName tel') $ applyUnder (k-1) (absBody tel') u 430 431dropAt :: Int -> [a] -> [a] 432dropAt _ [] = __IMPOSSIBLE__ 433dropAt k (x:xs) 434 | k < 0 = __IMPOSSIBLE__ 435 | k == 0 = xs 436 | otherwise = x : dropAt (k-1) xs 437 438-- | Solve the k'th equation with the given value, which can depend on 439-- regular variables but not on other equation variables. 440solveEq :: Int -> Term -> UnifyState -> (UnifyState, PatternSubstitution) 441solveEq k u s = (,sigma) $ s 442 { eqTel = applyUnder k (eqTel s) u' 443 , eqLHS = dropAt k $ eqLHS s 444 , eqRHS = dropAt k $ eqRHS s 445 } 446 where 447 u' = raise k u 448 n = eqCount s 449 sigma = liftS (n-k-1) $ consS (dotP u') idS 450 451--UNUSED Liang-Ting Chen 2019-07-16 452---- | Simplify the k'th equation with the given value (which can depend on other 453---- equation variables). Returns Nothing if there is a cycle. 454--simplifyEq :: Int -> Term -> UnifyState -> Maybe (UnifyState, PatternSubstitution) 455--simplifyEq k u s = case instantiateTelescope (eqTel s) k u of 456-- Nothing -> Nothing 457-- Just (tel' , sigma , rho) -> Just $ (,sigma) $ UState 458-- { varTel = varTel s 459-- , flexVars = flexVars s 460-- , eqTel = tel' 461-- , eqLHS = permute rho $ eqLHS s 462-- , eqRHS = permute rho $ eqRHS s 463-- } 464-- 465---------------------------------------------------- 466-- Unification strategies 467---------------------------------------------------- 468 469data UnifyStep 470 = Deletion 471 { deleteAt :: Int 472 , deleteType :: Type 473 , deleteLeft :: Term 474 , deleteRight :: Term 475 } 476 | Solution 477 { solutionAt :: Int 478 , solutionType :: Dom Type 479 , solutionVar :: FlexibleVar Int 480 , solutionTerm :: Term 481 } 482 | Injectivity 483 { injectAt :: Int 484 , injectType :: Type 485 , injectDatatype :: QName 486 , injectParameters :: Args 487 , injectIndices :: Args 488 , injectConstructor :: ConHead 489 } 490 | Conflict 491 { conflictAt :: Int 492 , conflictType :: Type 493 , conflictDatatype :: QName 494 , conflictParameters :: Args 495 , conflictLeft :: Term 496 , conflictRight :: Term 497 } 498 | Cycle 499 { cycleAt :: Int 500 , cycleType :: Type 501 , cycleDatatype :: QName 502 , cycleParameters :: Args 503 , cycleVar :: Int 504 , cycleOccursIn :: Term 505 } 506 | EtaExpandVar 507 { expandVar :: FlexibleVar Int 508 , expandVarRecordType :: QName 509 , expandVarParameters :: Args 510 } 511 | EtaExpandEquation 512 { expandAt :: Int 513 , expandRecordType :: QName 514 , expandParameters :: Args 515 } 516 | LitConflict 517 { litConflictAt :: Int 518 , litType :: Type 519 , litConflictLeft :: Literal 520 , litConflictRight :: Literal 521 } 522 | StripSizeSuc 523 { stripAt :: Int 524 , stripArgLeft :: Term 525 , stripArgRight :: Term 526 } 527 | SkipIrrelevantEquation 528 { skipIrrelevantAt :: Int 529 } 530 | TypeConInjectivity 531 { typeConInjectAt :: Int 532 , typeConstructor :: QName 533 , typeConArgsLeft :: Args 534 , typeConArgsRight :: Args 535 } deriving (Show) 536 537instance PrettyTCM UnifyStep where 538 prettyTCM step = case step of 539 Deletion k a u v -> "Deletion" $$ nest 2 (vcat $ 540 [ "position: " <+> text (show k) 541 , "type: " <+> prettyTCM a 542 , "lhs: " <+> prettyTCM u 543 , "rhs: " <+> prettyTCM v 544 ]) 545 Solution k a i u -> "Solution" $$ nest 2 (vcat $ 546 [ "position: " <+> text (show k) 547 , "type: " <+> prettyTCM a 548 , "variable: " <+> text (show (flexVar i, flexPos i, flexForced i, flexKind i)) 549 , "term: " <+> prettyTCM u 550 ]) 551 Injectivity k a d pars ixs c -> "Injectivity" $$ nest 2 (vcat $ 552 [ "position: " <+> text (show k) 553 , "type: " <+> prettyTCM a 554 , "datatype: " <+> prettyTCM d 555 , "parameters: " <+> prettyList_ (map prettyTCM pars) 556 , "indices: " <+> prettyList_ (map prettyTCM ixs) 557 , "constructor:" <+> prettyTCM c 558 ]) 559 Conflict k a d pars u v -> "Conflict" $$ nest 2 (vcat $ 560 [ "position: " <+> text (show k) 561 , "type: " <+> prettyTCM a 562 , "datatype: " <+> prettyTCM d 563 , "parameters: " <+> prettyList_ (map prettyTCM pars) 564 , "lhs: " <+> prettyTCM u 565 , "rhs: " <+> prettyTCM v 566 ]) 567 Cycle k a d pars i u -> "Cycle" $$ nest 2 (vcat $ 568 [ "position: " <+> text (show k) 569 , "type: " <+> prettyTCM a 570 , "datatype: " <+> prettyTCM d 571 , "parameters: " <+> prettyList_ (map prettyTCM pars) 572 , "variable: " <+> text (show i) 573 , "term: " <+> prettyTCM u 574 ]) 575 EtaExpandVar fi r pars -> "EtaExpandVar" $$ nest 2 (vcat $ 576 [ "variable: " <+> text (show fi) 577 , "record type:" <+> prettyTCM r 578 , "parameters: " <+> prettyTCM pars 579 ]) 580 EtaExpandEquation k r pars -> "EtaExpandEquation" $$ nest 2 (vcat $ 581 [ "position: " <+> text (show k) 582 , "record type:" <+> prettyTCM r 583 , "parameters: " <+> prettyTCM pars 584 ]) 585 LitConflict k a u v -> "LitConflict" $$ nest 2 (vcat $ 586 [ "position: " <+> text (show k) 587 , "type: " <+> prettyTCM a 588 , "lhs: " <+> prettyTCM u 589 , "rhs: " <+> prettyTCM v 590 ]) 591 StripSizeSuc k u v -> "StripSizeSuc" $$ nest 2 (vcat $ 592 [ "position: " <+> text (show k) 593 , "lhs: " <+> prettyTCM u 594 , "rhs: " <+> prettyTCM v 595 ]) 596 SkipIrrelevantEquation k -> "SkipIrrelevantEquation" $$ nest 2 (vcat $ 597 [ "position: " <+> text (show k) 598 ]) 599 TypeConInjectivity k d us vs -> "TypeConInjectivity" $$ nest 2 (vcat $ 600 [ "position: " <+> text (show k) 601 , "datatype: " <+> prettyTCM d 602 , "lhs: " <+> prettyList_ (map prettyTCM us) 603 , "rhs: " <+> prettyList_ (map prettyTCM vs) 604 ]) 605 606type UnifyStrategy = forall m. (PureTCM m, MonadPlus m) => UnifyState -> m UnifyStep 607 608--UNUSED Liang-Ting Chen 2019-07-16 609--leftToRightStrategy :: UnifyStrategy 610--leftToRightStrategy s = 611-- msum (for [0..n-1] $ \k -> completeStrategyAt k s) 612-- where n = size $ eqTel s 613 614rightToLeftStrategy :: UnifyStrategy 615rightToLeftStrategy s = 616 msum (for (downFrom n) $ \k -> completeStrategyAt k s) 617 where n = size $ eqTel s 618 619completeStrategyAt :: Int -> UnifyStrategy 620completeStrategyAt k s = msum $ map (\strat -> strat k s) $ 621-- ASR (2021-02-07). The below eta-expansions are required by GHC >= 622-- 9.0.1 (see Issue #4955). 623 [ (\n -> skipIrrelevantStrategy n) 624 , (\n -> basicUnifyStrategy n) 625 , (\n -> literalStrategy n) 626 , (\n -> dataStrategy n) 627 , (\n -> etaExpandVarStrategy n) 628 , (\n -> etaExpandEquationStrategy n) 629 , (\n -> injectiveTypeConStrategy n) 630 , (\n -> injectivePragmaStrategy n) 631 , (\n -> simplifySizesStrategy n) 632 , (\n -> checkEqualityStrategy n) 633 ] 634 635-- | @isHom n x@ returns x lowered by n if the variables 0..n-1 don't occur in x. 636-- 637-- This is naturally sensitive to normalization. 638isHom :: (Free a, Subst a) => Int -> a -> Maybe a 639isHom n x = do 640 guard $ getAll $ runFree (All . (>= n)) IgnoreNot x 641 return $ raise (-n) x 642 643findFlexible :: Int -> FlexibleVars -> Maybe (FlexibleVar Nat) 644findFlexible i flex = List.find ((i ==) . flexVar) flex 645 646basicUnifyStrategy :: Int -> UnifyStrategy 647basicUnifyStrategy k s = do 648 Equal dom@Dom{unDom = a} u v <- eqUnLevel (getEquality k s) 649 -- Andreas, 2019-02-23: reduce equality for the sake of isHom? 650 ha <- fromMaybeMP $ isHom n a 651 (mi, mj) <- addContext (varTel s) $ (,) <$> isEtaVar u ha <*> isEtaVar v ha 652 reportSDoc "tc.lhs.unify" 30 $ "isEtaVar results: " <+> text (show [mi,mj]) 653 case (mi, mj) of 654 (Just i, Just j) 655 | i == j -> mzero -- Taken care of by checkEqualityStrategy 656 (Just i, Just j) 657 | Just fi <- findFlexible i flex 658 , Just fj <- findFlexible j flex -> do 659 let choice = chooseFlex fi fj 660 firstTryLeft = msum [ return (Solution k dom{unDom = ha} fi v) 661 , return (Solution k dom{unDom = ha} fj u)] 662 firstTryRight = msum [ return (Solution k dom{unDom = ha} fj u) 663 , return (Solution k dom{unDom = ha} fi v)] 664 reportSDoc "tc.lhs.unify" 40 $ "fi = " <+> text (show fi) 665 reportSDoc "tc.lhs.unify" 40 $ "fj = " <+> text (show fj) 666 reportSDoc "tc.lhs.unify" 40 $ "chooseFlex: " <+> text (show choice) 667 case choice of 668 ChooseLeft -> firstTryLeft 669 ChooseRight -> firstTryRight 670 ExpandBoth -> mzero -- This should be taken care of by etaExpandEquationStrategy 671 ChooseEither -> firstTryRight 672 (Just i, _) 673 | Just fi <- findFlexible i flex -> return $ Solution k dom{unDom = ha} fi v 674 (_, Just j) 675 | Just fj <- findFlexible j flex -> return $ Solution k dom{unDom = ha} fj u 676 _ -> mzero 677 where 678 flex = flexVars s 679 n = eqCount s 680 681dataStrategy :: Int -> UnifyStrategy 682dataStrategy k s = do 683 Equal Dom{unDom = a} u v <- eqConstructorForm =<< eqUnLevel =<< reduce (getEqualityUnraised k s) 684 sa <- reduce $ getSort a 685 case unEl a of 686 Def d es | Type{} <- sa -> do 687 npars <- catMaybesMP $ getNumberOfParameters d 688 let (pars,ixs) = splitAt npars $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es 689 reportSDoc "tc.lhs.unify" 40 $ addContext (varTel s `abstract` eqTel s) $ 690 "Found equation at datatype " <+> prettyTCM d 691 <+> " with parameters " <+> prettyTCM (raise (size (eqTel s) - k) pars) 692 case (u, v) of 693 (Con c _ _ , Con c' _ _ ) | c == c' -> return $ Injectivity k a d pars ixs c 694 (Con c _ _ , Con c' _ _ ) -> return $ Conflict k a d pars u v 695 (Var i [] , v ) -> ifOccursStronglyRigid i v $ return $ Cycle k a d pars i v 696 (u , Var j [] ) -> ifOccursStronglyRigid j u $ return $ Cycle k a d pars j u 697 _ -> mzero 698 _ -> mzero 699 where 700 ifOccursStronglyRigid i u ret = do 701 -- Call forceNotFree to reduce u as far as possible 702 -- around any occurrences of i 703 (_ , u) <- forceNotFree (singleton i) u 704 case flexRigOccurrenceIn i u of 705 Just StronglyRigid -> ret 706 _ -> mzero 707 708checkEqualityStrategy :: Int -> UnifyStrategy 709checkEqualityStrategy k s = do 710 let Equal Dom{unDom = a} u v = getEquality k s 711 n = eqCount s 712 ha <- fromMaybeMP $ isHom n a 713 return $ Deletion k ha u v 714 715literalStrategy :: Int -> UnifyStrategy 716literalStrategy k s = do 717 let n = eqCount s 718 Equal Dom{unDom = a} u v <- eqUnLevel $ getEquality k s 719 ha <- fromMaybeMP $ isHom n a 720 (u, v) <- reduce (u, v) 721 case (u , v) of 722 (Lit l1 , Lit l2) 723 | l1 == l2 -> return $ Deletion k ha u v 724 | otherwise -> return $ LitConflict k ha l1 l2 725 _ -> mzero 726 727etaExpandVarStrategy :: Int -> UnifyStrategy 728etaExpandVarStrategy k s = do 729 Equal Dom{unDom = a} u v <- eqUnLevel <=< reduce $ getEquality k s 730 shouldEtaExpand u v a s `mplus` shouldEtaExpand v u a s 731 where 732 -- TODO: use IsEtaVar to check if the term is a variable 733 shouldEtaExpand :: Term -> Term -> Type -> UnifyStrategy 734 shouldEtaExpand (Var i es) v a s = do 735 fi <- fromMaybeMP $ findFlexible i (flexVars s) 736 reportSDoc "tc.lhs.unify" 50 $ 737 "Found flexible variable " <+> text (show i) 738 -- Issue 2888: Do this if there are only projections or if it's a singleton 739 -- record or if it's unified against a record constructor term. Basically 740 -- we need to avoid EtaExpandEquation if EtaExpandVar is possible, or the 741 -- forcing translation is unhappy. 742 b <- reduce $ unDom $ getVarTypeUnraised (varCount s - 1 - i) s 743 (d, pars) <- catMaybesMP $ isEtaRecordType b 744 ps <- fromMaybeMP $ allProjElims es 745 guard =<< orM 746 [ pure $ not $ null ps 747 , isRecCon v -- is the other term a record constructor? 748 , (Right True ==) <$> runBlocked (isSingletonRecord d pars) 749 ] 750 reportSDoc "tc.lhs.unify" 50 $ 751 "with projections " <+> prettyTCM (map snd ps) 752 reportSDoc "tc.lhs.unify" 50 $ 753 "at record type " <+> prettyTCM d 754 return $ EtaExpandVar fi d pars 755 shouldEtaExpand _ _ _ _ = mzero 756 757 isRecCon (Con c _ _) = isJust <$> isRecordConstructor (conName c) 758 isRecCon _ = return False 759 760etaExpandEquationStrategy :: Int -> UnifyStrategy 761etaExpandEquationStrategy k s = do 762 -- Andreas, 2019-02-23, re #3578, is the following reduce redundant? 763 Equal Dom{unDom = a} u v <- reduce $ getEqualityUnraised k s 764 (d, pars) <- catMaybesMP $ addContext tel $ isEtaRecordType a 765 guard =<< orM 766 [ (Right True ==) <$> runBlocked (isSingletonRecord d pars) 767 , shouldProject u 768 , shouldProject v 769 ] 770 return $ EtaExpandEquation k d pars 771 where 772 shouldProject :: PureTCM m => Term -> m Bool 773 shouldProject = \case 774 Def f es -> usesCopatterns f 775 Con c _ _ -> isJust <$> isRecordConstructor (conName c) 776 777 Var _ _ -> return False 778 Lam _ _ -> __IMPOSSIBLE__ 779 Lit _ -> __IMPOSSIBLE__ 780 Pi _ _ -> __IMPOSSIBLE__ 781 Sort _ -> __IMPOSSIBLE__ 782 Level _ -> __IMPOSSIBLE__ 783 MetaV _ _ -> return False 784 DontCare _ -> return False 785 Dummy s _ -> __IMPOSSIBLE_VERBOSE__ s 786 787 tel = varTel s `abstract` telFromList (take k $ telToList $ eqTel s) 788 789simplifySizesStrategy :: Int -> UnifyStrategy 790simplifySizesStrategy k s = do 791 isSizeName <- isSizeNameTest 792 Equal Dom{unDom = a} u v <- reduce $ getEquality k s 793 case unEl a of 794 Def d _ -> do 795 guard $ isSizeName d 796 su <- sizeView u 797 sv <- sizeView v 798 case (su, sv) of 799 (SizeSuc u, SizeSuc v) -> return $ StripSizeSuc k u v 800 (SizeSuc u, SizeInf ) -> return $ StripSizeSuc k u v 801 (SizeInf , SizeSuc v) -> return $ StripSizeSuc k u v 802 _ -> mzero 803 _ -> mzero 804 805injectiveTypeConStrategy :: Int -> UnifyStrategy 806injectiveTypeConStrategy k s = do 807 injTyCon <- optInjectiveTypeConstructors <$> pragmaOptions 808 guard injTyCon 809 eq <- eqUnLevel <=< reduce $ getEquality k s 810 case eq of 811 Equal a u@(Def d es) v@(Def d' es') | d == d' -> do 812 -- d must be a data, record or axiom 813 def <- getConstInfo d 814 guard $ case theDef def of 815 Datatype{} -> True 816 Record{} -> True 817 Axiom{} -> True 818 DataOrRecSig{} -> True 819 AbstractDefn{} -> False -- True triggers issue #2250 820 Function{} -> False 821 Primitive{} -> False 822 PrimitiveSort{} -> __IMPOSSIBLE__ 823 GeneralizableVar{} -> __IMPOSSIBLE__ 824 Constructor{} -> __IMPOSSIBLE__ -- Never a type! 825 let us = fromMaybe __IMPOSSIBLE__ $ allApplyElims es 826 vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es' 827 return $ TypeConInjectivity k d us vs 828 _ -> mzero 829 830injectivePragmaStrategy :: Int -> UnifyStrategy 831injectivePragmaStrategy k s = do 832 eq <- eqUnLevel <=< reduce $ getEquality k s 833 case eq of 834 Equal a u@(Def d es) v@(Def d' es') | d == d' -> do 835 -- d must have an injective pragma 836 def <- getConstInfo d 837 guard $ defInjective def 838 let us = fromMaybe __IMPOSSIBLE__ $ allApplyElims es 839 vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es' 840 return $ TypeConInjectivity k d us vs 841 _ -> mzero 842 843skipIrrelevantStrategy :: Int -> UnifyStrategy 844skipIrrelevantStrategy k s = do 845 let Equal a _ _ = getEquality k s -- reduce not necessary 846 guard . (== Right True) =<< runBlocked (isIrrelevantOrPropM a) -- reduction takes place here 847 -- TODO: do something in case the above is blocked (i.e. `Left b`) 848 return $ SkipIrrelevantEquation k 849 850 851---------------------------------------------------- 852-- Actually doing the unification 853---------------------------------------------------- 854 855data UnifyLogEntry 856 = UnificationStep UnifyState UnifyStep 857-- | UnificationDone UnifyState -- unused? 858 859type UnifyLog = [UnifyLogEntry] 860 861data UnifyOutput = UnifyOutput 862 { unifySubst :: PatternSubstitution 863 , unifyProof :: PatternSubstitution 864 , unifyLog :: UnifyLog 865 } 866 867instance Semigroup UnifyOutput where 868 x <> y = UnifyOutput 869 { unifySubst = unifySubst y `composeS` unifySubst x 870 , unifyProof = unifyProof y `composeS` unifyProof x 871 , unifyLog = unifyLog x ++ unifyLog y 872 } 873 874instance Monoid UnifyOutput where 875 mempty = UnifyOutput IdS IdS [] 876 mappend = (<>) 877 878type UnifyLogT m a = WriterT UnifyOutput m a 879 880tellUnifySubst :: MonadWriter UnifyOutput m => PatternSubstitution -> m () 881tellUnifySubst sub = tell $ UnifyOutput sub IdS [] 882 883tellUnifyProof :: MonadWriter UnifyOutput m => PatternSubstitution -> m () 884tellUnifyProof sub = tell $ UnifyOutput IdS sub [] 885 886writeUnifyLog :: MonadWriter UnifyOutput m => UnifyLogEntry -> m () 887writeUnifyLog x = tell $ UnifyOutput IdS IdS [x] 888 889runUnifyLogT :: UnifyLogT m a -> m (a,UnifyOutput) 890runUnifyLogT = runWriterT 891 892unifyStep 893 :: (PureTCM m, MonadWriter UnifyOutput m) 894 => UnifyState -> UnifyStep -> m (UnificationResult' UnifyState) 895 896unifyStep s Deletion{ deleteAt = k , deleteType = a , deleteLeft = u , deleteRight = v } = do 897 -- Check definitional equality of u and v 898 isReflexive <- addContext (varTel s) $ runBlocked $ pureEqualTerm a u v 899 withoutK <- withoutKOption 900 splitOnStrict <- asksTC envSplitOnStrict 901 case isReflexive of 902 Left block -> return $ UnifyBlocked block 903 Right False -> return $ UnifyStuck [] 904 Right True | withoutK && not splitOnStrict 905 -> return $ UnifyStuck [UnifyReflexiveEq (varTel s) a u] 906 Right True -> do 907 let (s', sigma) = solveEq k u s 908 tellUnifyProof sigma 909 Unifies <$> lensEqTel reduce s' 910 911unifyStep s step@Solution{} = solutionStep RetryNormalised s step 912 913unifyStep s (Injectivity k a d pars ixs c) = do 914 ifM (consOfHIT $ conName c) (return $ UnifyStuck []) $ do 915 withoutK <- withoutKOption 916 917 -- Split equation telescope into parts before and after current equation 918 let (eqListTel1, _ : eqListTel2) = splitAt k $ telToList $ eqTel s 919 (eqTel1, eqTel2) = (telFromList eqListTel1, telFromList eqListTel2) 920 921 -- Get constructor telescope and target indices 922 cdef <- getConInfo c 923 let ctype = defType cdef `piApply` pars 924 addContext (varTel s `abstract` eqTel1) $ reportSDoc "tc.lhs.unify" 40 $ 925 "Constructor type: " <+> prettyTCM ctype 926 TelV ctel ctarget <- telView ctype 927 let cixs = case unEl ctarget of 928 Def d' es | d == d' -> 929 let args = fromMaybe __IMPOSSIBLE__ $ allApplyElims es 930 in drop (length pars) args 931 _ -> __IMPOSSIBLE__ 932 933 -- Get index telescope of the datatype 934 dtype <- (`piApply` pars) . defType <$> getConstInfo d 935 addContext (varTel s `abstract` eqTel1) $ reportSDoc "tc.lhs.unify" 40 $ 936 "Datatype type: " <+> prettyTCM dtype 937 938 -- This is where the magic of higher-dimensional unification happens 939 -- We need to generalize the indices `ixs` to the target indices of the 940 -- constructor `cixs`. This is done by calling the unification algorithm 941 -- recursively (this doesn't get stuck in a loop because a type should 942 -- never be indexed over itself). Note the similarity with the 943 -- computeNeighbourhood function in Agda.TypeChecking.Coverage. 944 let hduTel = eqTel1 `abstract` ctel 945 notforced = replicate (size hduTel) NotForced 946 res <- addContext (varTel s) $ unifyIndices' 947 hduTel 948 (allFlexVars notforced hduTel) 949 (raise (size ctel) dtype) 950 (raise (size ctel) ixs) 951 cixs 952 case res of 953 -- Higher-dimensional unification can never end in a conflict, 954 -- because `cong c1 ...` and `cong c2 ...` don't even have the 955 -- same type for distinct constructors c1 and c2. 956 NoUnify _ -> __IMPOSSIBLE__ 957 958 -- Higher-dimensional unification is blocked: propagate 959 UnifyBlocked block -> return $ UnifyBlocked block 960 961 -- Higher-dimensional unification has failed. If not --without-K, 962 -- we can simply ignore the higher-dimensional equations and 963 -- simplify the equation as in the non-indexed case. 964 UnifyStuck _ | not withoutK -> do 965 -- using the same variable names as in the case where hdu succeeds. 966 let eqTel1' = eqTel1 `abstract` ctel 967 rho1 = raiseS (size ctel) 968 ceq = ConP c noConPatternInfo $ teleNamedArgs ctel 969 rho3 = consS ceq rho1 970 eqTel2' = applyPatSubst rho3 eqTel2 971 eqTel' = eqTel1' `abstract` eqTel2' 972 rho = liftS (size eqTel2) rho3 973 974 tellUnifyProof rho 975 976 eqTel' <- reduce eqTel' 977 978 -- Compute new lhs and rhs by matching the old ones against rho 979 (lhs', rhs') <- do 980 let ps = applySubst rho $ teleNamedArgs $ eqTel s 981 (lhsMatch, _) <- Match.matchPatterns ps $ eqLHS s 982 (rhsMatch, _) <- Match.matchPatterns ps $ eqRHS s 983 case (lhsMatch, rhsMatch) of 984 (Match.Yes _ lhs', Match.Yes _ rhs') -> return 985 (reverse $ Match.matchedArgs __IMPOSSIBLE__ (size eqTel') lhs', 986 reverse $ Match.matchedArgs __IMPOSSIBLE__ (size eqTel') rhs') 987 _ -> __IMPOSSIBLE__ 988 989 return $ Unifies $ s { eqTel = eqTel' , eqLHS = lhs' , eqRHS = rhs' } 990 991 992 UnifyStuck _ -> let n = eqCount s 993 Equal Dom{unDom = a} u v = getEquality k s 994 in return $ UnifyStuck [UnifyIndicesNotVars 995 (varTel s `abstract` eqTel s) a 996 (raise n u) (raise n v) (raise (n-k) ixs)] 997 998 Unifies (eqTel1', rho0, _) -> do 999 -- Split ps0 into parts for eqTel1 and ctel 1000 let (rho1, rho2) = splitS (size ctel) rho0 1001 1002 -- Compute new equation telescope context and substitution 1003 let ceq = ConP c noConPatternInfo $ applySubst rho2 $ teleNamedArgs ctel 1004 rho3 = consS ceq rho1 1005 eqTel2' = applyPatSubst rho3 eqTel2 1006 eqTel' = eqTel1' `abstract` eqTel2' 1007 rho = liftS (size eqTel2) rho3 1008 1009 tellUnifyProof rho 1010 1011 eqTel' <- reduce eqTel' 1012 1013 -- Compute new lhs and rhs by matching the old ones against rho 1014 (lhs', rhs') <- do 1015 let ps = applySubst rho $ teleNamedArgs $ eqTel s 1016 (lhsMatch, _) <- Match.matchPatterns ps $ eqLHS s 1017 (rhsMatch, _) <- Match.matchPatterns ps $ eqRHS s 1018 case (lhsMatch, rhsMatch) of 1019 (Match.Yes _ lhs', Match.Yes _ rhs') -> return 1020 (reverse $ Match.matchedArgs __IMPOSSIBLE__ (size eqTel') lhs', 1021 reverse $ Match.matchedArgs __IMPOSSIBLE__ (size eqTel') rhs') 1022 _ -> __IMPOSSIBLE__ 1023 1024 return $ Unifies $ s { eqTel = eqTel' , eqLHS = lhs' , eqRHS = rhs' } 1025 1026unifyStep s Conflict 1027 { conflictLeft = u 1028 , conflictRight = v 1029 } = 1030 case u of 1031 Con h _ _ -> do 1032 ifM (consOfHIT $ conName h) (return $ UnifyStuck []) $ do 1033 return $ NoUnify $ UnifyConflict (varTel s) u v 1034 _ -> __IMPOSSIBLE__ 1035unifyStep s Cycle 1036 { cycleVar = i 1037 , cycleOccursIn = u 1038 } = 1039 case u of 1040 Con h _ _ -> do 1041 ifM (consOfHIT $ conName h) (return $ UnifyStuck []) $ do 1042 return $ NoUnify $ UnifyCycle (varTel s) i u 1043 _ -> __IMPOSSIBLE__ 1044 1045unifyStep s EtaExpandVar{ expandVar = fi, expandVarRecordType = d , expandVarParameters = pars } = do 1046 recd <- fromMaybe __IMPOSSIBLE__ <$> isRecord d 1047 let delta = recTel recd `apply` pars 1048 c = recConHead recd 1049 let nfields = size delta 1050 (varTel', rho) = expandTelescopeVar (varTel s) (m-1-i) delta c 1051 projectFlexible = [ FlexibleVar (getArgInfo fi) (flexForced fi) (projFlexKind j) (flexPos fi) (i+j) | j <- [0..nfields-1] ] 1052 tellUnifySubst $ rho 1053 return $ Unifies $ UState 1054 { varTel = varTel' 1055 , flexVars = projectFlexible ++ liftFlexibles nfields (flexVars s) 1056 , eqTel = applyPatSubst rho $ eqTel s 1057 , eqLHS = applyPatSubst rho $ eqLHS s 1058 , eqRHS = applyPatSubst rho $ eqRHS s 1059 } 1060 where 1061 i = flexVar fi 1062 m = varCount s 1063 1064 projFlexKind :: Int -> FlexibleVarKind 1065 projFlexKind j = case flexKind fi of 1066 RecordFlex ks -> indexWithDefault ImplicitFlex ks j 1067 ImplicitFlex -> ImplicitFlex 1068 DotFlex -> DotFlex 1069 OtherFlex -> OtherFlex 1070 1071 liftFlexible :: Int -> Int -> Maybe Int 1072 liftFlexible n j = if j == i then Nothing else Just (if j > i then j + (n-1) else j) 1073 1074 liftFlexibles :: Int -> FlexibleVars -> FlexibleVars 1075 liftFlexibles n fs = mapMaybe (traverse $ liftFlexible n) fs 1076 1077unifyStep s EtaExpandEquation{ expandAt = k, expandRecordType = d, expandParameters = pars } = do 1078 recd <- fromMaybe __IMPOSSIBLE__ <$> isRecord d 1079 let delta = recTel recd `apply` pars 1080 c = recConHead recd 1081 lhs <- expandKth $ eqLHS s 1082 rhs <- expandKth $ eqRHS s 1083 let (tel, sigma) = expandTelescopeVar (eqTel s) k delta c 1084 tellUnifyProof sigma 1085 Unifies <$> do 1086 lensEqTel reduce $ s 1087 { eqTel = tel 1088 , eqLHS = lhs 1089 , eqRHS = rhs 1090 } 1091 where 1092 expandKth us = do 1093 let (us1,v:us2) = fromMaybe __IMPOSSIBLE__ $ splitExactlyAt k us 1094 vs <- snd <$> etaExpandRecord d pars (unArg v) 1095 vs <- reduce vs 1096 return $ us1 ++ vs ++ us2 1097 1098unifyStep s LitConflict 1099 { litType = a 1100 , litConflictLeft = l 1101 , litConflictRight = l' 1102 } = return $ NoUnify $ UnifyConflict (varTel s) (Lit l) (Lit l') 1103 1104unifyStep s (StripSizeSuc k u v) = do 1105 sizeTy <- sizeType 1106 sizeSu <- sizeSuc 1 (var 0) 1107 let n = eqCount s 1108 sub = liftS (n-k-1) $ consS sizeSu $ raiseS 1 1109 eqFlatTel = flattenTel $ eqTel s 1110 eqFlatTel' = applySubst sub $ updateAt k (fmap $ const sizeTy) $ eqFlatTel 1111 eqTel' = unflattenTel (teleNames $ eqTel s) eqFlatTel' 1112 -- TODO: tellUnifyProof sub 1113 -- but sizeSu is not a constructor, so sub is not a PatternSubstitution! 1114 return $ Unifies $ s 1115 { eqTel = eqTel' 1116 , eqLHS = updateAt k (const $ defaultArg u) $ eqLHS s 1117 , eqRHS = updateAt k (const $ defaultArg v) $ eqRHS s 1118 } 1119 1120unifyStep s (SkipIrrelevantEquation k) = do 1121 let lhs = eqLHS s 1122 (s', sigma) = solveEq k (DontCare $ unArg $ indexWithDefault __IMPOSSIBLE__ lhs k) s 1123 tellUnifyProof sigma 1124 return $ Unifies s' 1125 1126unifyStep s (TypeConInjectivity k d us vs) = do 1127 dtype <- defType <$> getConstInfo d 1128 TelV dtel _ <- telView dtype 1129 let deq = Def d $ map Apply $ teleArgs dtel 1130 -- TODO: tellUnifyProof ??? 1131 -- but d is not a constructor... 1132 Unifies <$> do 1133 lensEqTel reduce $ s 1134 { eqTel = dtel `abstract` applyUnder k (eqTel s) (raise k deq) 1135 , eqLHS = us ++ dropAt k (eqLHS s) 1136 , eqRHS = vs ++ dropAt k (eqRHS s) 1137 } 1138 1139data RetryNormalised = RetryNormalised | DontRetryNormalised 1140 deriving (Eq, Show) 1141 1142solutionStep 1143 :: (PureTCM m, MonadWriter UnifyOutput m) 1144 => RetryNormalised 1145 -> UnifyState 1146 -> UnifyStep 1147 -> m (UnificationResult' UnifyState) 1148solutionStep retry s 1149 step@Solution{ solutionAt = k 1150 , solutionType = dom@Dom{ unDom = a } 1151 , solutionVar = fi@FlexibleVar{ flexVar = i } 1152 , solutionTerm = u } = do 1153 let m = varCount s 1154 1155 -- Now we have to be careful about forced variables in `u`. If they appear 1156 -- in pattern positions we need to bind them there rather in their forced positions. We can safely 1157 -- ignore non-pattern positions and forced pattern positions, because in that case there will be 1158 -- other equations where the variable can be bound. 1159 -- NOTE: If we're doing make-case we ignore forced variables. This is safe since we take the 1160 -- result of unification and build user clauses that will be checked again with forcing turned on. 1161 inMakeCase <- viewTC eMakeCase 1162 let forcedVars | inMakeCase = IntMap.empty 1163 | otherwise = IntMap.fromList [ (flexVar fi, getModality fi) | fi <- flexVars s, 1164 flexForced fi == Forced ] 1165 (p, bound) <- patternBindingForcedVars forcedVars u 1166 1167 -- To maintain the invariant that each variable in varTel is bound exactly once in the pattern 1168 -- substitution we need to turn the bound variables in `p` into dot patterns in the rest of the 1169 -- substitution. 1170 let dotSub = foldr composeS idS [ inplaceS i (dotP (Var i [])) | i <- IntMap.keys bound ] 1171 1172 -- We moved the binding site of some forced variables, so we need to update their modalities in 1173 -- the telescope. The new modality is the combination of the modality of the variable we are 1174 -- instantiating and the modality of the binding site in the pattern (returned by 1175 -- patternBindingForcedVars). 1176 let updModality md vars tel 1177 | IntMap.null vars = tel 1178 | otherwise = telFromList $ zipWith upd (downFrom $ size tel) (telToList tel) 1179 where 1180 upd i a | Just md' <- IntMap.lookup i vars = setModality (composeModality md md') a 1181 | otherwise = a 1182 s <- return $ s { varTel = updModality (getModality fi) bound (varTel s) } 1183 1184 reportSDoc "tc.lhs.unify.force" 45 $ vcat 1185 [ "forcedVars =" <+> pretty (IntMap.keys forcedVars) 1186 , "u =" <+> prettyTCM u 1187 , "p =" <+> prettyTCM p 1188 , "bound =" <+> pretty (IntMap.keys bound) 1189 , "dotSub =" <+> pretty dotSub ] 1190 1191 -- Check that the type of the variable is equal to the type of the equation 1192 -- (not just a subtype), otherwise we cannot instantiate (see Issue 2407). 1193 let dom'@Dom{ unDom = a' } = getVarType (m-1-i) s 1194 equalTypes <- addContext (varTel s) $ runBlocked $ do 1195 reportSDoc "tc.lhs.unify" 45 $ "Equation type: " <+> prettyTCM a 1196 reportSDoc "tc.lhs.unify" 45 $ "Variable type: " <+> prettyTCM a' 1197 pureEqualType a a' 1198 1199 -- The conditions on the relevances are as follows (see #2640): 1200 -- - If the type of the equation is relevant, then the solution must be 1201 -- usable in a relevant position. 1202 -- - If the type of the equation is (shape-)irrelevant, then the solution 1203 -- must be usable in a μ-relevant position where μ is the relevance 1204 -- of the variable being solved. 1205 -- 1206 -- Jesper, Andreas, 2018-10-17: the quantity of the equation is morally 1207 -- always @Quantity0@, since the indices of the data type are runtime erased. 1208 -- Thus, we need not change the quantity of the solution. 1209 let eqrel = getRelevance dom 1210 eqmod = getModality dom 1211 varmod = getModality dom' 1212 mod = applyUnless (NonStrict `moreRelevant` eqrel) (setRelevance eqrel) 1213 $ varmod 1214 reportSDoc "tc.lhs.unify" 65 $ text $ "Equation modality: " ++ show (getModality dom) 1215 reportSDoc "tc.lhs.unify" 65 $ text $ "Variable modality: " ++ show varmod 1216 reportSDoc "tc.lhs.unify" 65 $ text $ "Solution must be usable in a " ++ show mod ++ " position." 1217 -- Andreas, 2018-10-18 1218 -- Currently, the modality check has problems with meta-variables created in the type signature, 1219 -- and thus, in quantity 0, that get into terms using the unifier, and there are checked to be 1220 -- non-erased, i.e., have quantity ω. 1221 -- Ulf, 2019-12-13. We still do it though. 1222 -- Andrea, 2020-10-15: It looks at meta instantiations now. 1223 eusable <- addContext (varTel s) $ runExceptT $ usableMod mod u 1224 caseEitherM (return eusable) (return . UnifyBlocked) $ \ usable -> do 1225 1226 reportSDoc "tc.lhs.unify" 45 $ "Modality ok: " <+> prettyTCM usable 1227 unless usable $ reportSLn "tc.lhs.unify" 65 $ "Rejected solution: " ++ show u 1228 1229 -- We need a Flat equality to solve a Flat variable. 1230 -- This also ought to take care of the need for a usableCohesion check. 1231 if not (getCohesion eqmod `moreCohesion` getCohesion varmod) then return $ UnifyStuck [] else do 1232 1233 case equalTypes of 1234 Left block -> return $ UnifyBlocked block 1235 Right False -> return $ UnifyStuck [] 1236 Right True | usable -> 1237 case solveVar (m - 1 - i) p s of 1238 Nothing | retry == RetryNormalised -> do 1239 u <- normalise u 1240 s <- lensVarTel normalise s 1241 solutionStep DontRetryNormalised s step{ solutionTerm = u } 1242 Nothing -> 1243 return $ UnifyStuck [UnifyRecursiveEq (varTel s) a i u] 1244 Just (s', sub) -> do 1245 let rho = sub `composeS` dotSub 1246 tellUnifySubst rho 1247 let (s'', sigma) = solveEq k (applyPatSubst rho u) s' 1248 tellUnifyProof sigma 1249 return $ Unifies s'' 1250 -- Andreas, 2019-02-23, issue #3578: do not eagerly reduce 1251 -- Unifies <$> liftTCM (reduce s'') 1252 Right True -> return $ UnifyStuck [UnifyUnusableModality (varTel s) a i u mod] 1253solutionStep _ _ _ = __IMPOSSIBLE__ 1254 1255unify 1256 :: (PureTCM m, MonadWriter UnifyOutput m) 1257 => UnifyState -> UnifyStrategy -> m (UnificationResult' UnifyState) 1258unify s strategy = if isUnifyStateSolved s 1259 then return $ Unifies s 1260 else tryUnifyStepsAndContinue (strategy s) 1261 where 1262 tryUnifyStepsAndContinue 1263 :: (PureTCM m, MonadWriter UnifyOutput m) 1264 => ListT m UnifyStep -> m (UnificationResult' UnifyState) 1265 tryUnifyStepsAndContinue steps = do 1266 x <- foldListT tryUnifyStep failure steps 1267 case x of 1268 Unifies s' -> unify s' strategy 1269 NoUnify err -> return $ NoUnify err 1270 UnifyBlocked b -> return $ UnifyBlocked b 1271 UnifyStuck err -> return $ UnifyStuck err 1272 1273 tryUnifyStep :: (PureTCM m, MonadWriter UnifyOutput m) 1274 => UnifyStep 1275 -> m (UnificationResult' UnifyState) 1276 -> m (UnificationResult' UnifyState) 1277 tryUnifyStep step fallback = do 1278 addContext (varTel s) $ 1279 reportSDoc "tc.lhs.unify" 20 $ "trying unifyStep" <+> prettyTCM step 1280 x <- unifyStep s step 1281 case x of 1282 Unifies s' -> do 1283 reportSDoc "tc.lhs.unify" 20 $ "unifyStep successful." 1284 reportSDoc "tc.lhs.unify" 20 $ "new unifyState:" <+> prettyTCM s' 1285 writeUnifyLog $ UnificationStep s step 1286 return x 1287 NoUnify{} -> return x 1288 UnifyBlocked b1 -> do 1289 y <- fallback 1290 case y of 1291 UnifyStuck _ -> return $ UnifyBlocked b1 1292 UnifyBlocked b2 -> return $ UnifyBlocked $ unblockOnEither b1 b2 1293 _ -> return y 1294 UnifyStuck err1 -> do 1295 y <- fallback 1296 case y of 1297 UnifyStuck err2 -> return $ UnifyStuck $ err1 ++ err2 1298 _ -> return y 1299 1300 failure :: Monad m => m (UnificationResult' a) 1301 failure = return $ UnifyStuck [] 1302 1303-- | Turn a term into a pattern while binding as many of the given forced variables as possible (in 1304-- non-forced positions). 1305patternBindingForcedVars :: PureTCM m => IntMap Modality -> Term -> m (DeBruijnPattern, IntMap Modality) 1306patternBindingForcedVars forced v = do 1307 let v' = precomputeFreeVars_ v 1308 runWriterT (evalStateT (go defaultModality v') forced) 1309 where 1310 noForced v = gets $ IntSet.disjoint (precomputedFreeVars v) . IntMap.keysSet 1311 1312 bind md i = do 1313 Just md' <- gets $ IntMap.lookup i 1314 if related md POLE md' -- The new binding site must be more relevant (more relevant = smaller). 1315 then do -- The forcing analysis guarantees that there exists such a position. 1316 tell $ IntMap.singleton i md 1317 modify $ IntMap.delete i 1318 return $ varP (deBruijnVar i) 1319 else return $ dotP (Var i []) 1320 1321 go md v = ifM (noForced v) (return $ dotP v) $ do 1322 v' <- lift $ lift $ reduce v 1323 case v' of 1324 Var i [] -> bind md i -- we know i is forced 1325 Con c ci es 1326 | Just vs <- allApplyElims es -> do 1327 fs <- defForced <$> getConstInfo (conName c) 1328 let goArg Forced v = return $ fmap (unnamed . dotP) v 1329 goArg NotForced v = fmap unnamed <$> traverse (go $ composeModality md $ getModality v) v 1330 (ps, bound) <- listen $ zipWithM goArg (fs ++ repeat NotForced) vs 1331 if IntMap.null bound 1332 then return $ dotP v -- bound nothing 1333 else do 1334 let cpi = (toConPatternInfo ci) { conPLazy = True } -- Not setting conPType. Is this a problem? 1335 return $ ConP c cpi $ map (setOrigin Inserted) ps 1336 | otherwise -> return $ dotP v -- Higher constructor (es has IApply) 1337 1338 -- Non-pattern positions 1339 Var _ (_:_) -> return $ dotP v 1340 Lam{} -> return $ dotP v 1341 Pi{} -> return $ dotP v 1342 Def{} -> return $ dotP v 1343 MetaV{} -> return $ dotP v 1344 Sort{} -> return $ dotP v 1345 Level{} -> return $ dotP v 1346 DontCare{} -> return $ dotP v 1347 Dummy{} -> return $ dotP v 1348 Lit{} -> __IMPOSSIBLE__ 1349