[ constraints ] anti-unification when getting stuck checking argument…

… spines

fixes agda#2384

TODO: doesn't pass the test suite!

src/full/Agda/TypeChecking/Conversion.hs

@@ -612,6 +612,72 @@ compareRelevance :: Comparison -> Relevance -> Relevance -> Bool
 compareRelevance CmpEq  = (==)
 compareRelevance CmpLeq = (<=)
 
+-- | When comparing argument spines (in compareElims) where the first arguments
+--   don't match, we keep going, substituting the anti-unification of the two
+--   terms in the telescope. More precisely:
+--
+--  @@
+--    (u = v : A)[pid]   w = antiUnify pid A u v   us = vs : Δ[w/x]
+--    -------------------------------------------------------------
+--                    u us = v vs : (x : A) Δ
+--  @@
+--
+--   The simplest case of anti-unification is to return a fresh metavariable
+--   (created by blockTermOnProblem), but if there's shared structure between
+--   the two terms we can expose that.
+--
+--   This is really a crutch that lets us get away with things that otherwise
+--   would require heterogenous conversion checking. See for instance issue
+--   #2384.
+antiUnify :: ProblemId -> Type -> Term -> Term -> TCM Term
+antiUnify pid a u v = do
+  ((u, v), eq) <- runReduceM (SynEq.checkSyntacticEquality u v)
+  case (ignoreSharing u, ignoreSharing v) of
+    _ | eq -> return u
+    (Pi ua ub, Pi va vb) -> do
+      wa0 <- antiUnifyType pid (unDom ua) (unDom va)
+      let wa = wa0 <$ ua
+      wb <- addContext wa $ antiUnifyType pid (unAbs ub) (unAbs vb)
+      return $ Pi wa (wb <$ ub)
+    (Lam i u, Lam _ v) ->
+      case ignoreSharing $ unEl a of
+        Pi a b -> Lam i . (<$ u) <$> addContext a (antiUnify pid (unAbs b) (unAbs u) (unAbs v))
+        _      -> fallback
+    (Var i us, Var j vs) | i == j -> do
+      a <- typeOfBV i
+      antiUnifyElims pid a (var i) us vs
+    (Con x ci us, Con y _ vs) | x == y -> maybeGiveUp $ do
+      a <- maybe patternViolation return =<< getConType x a
+      antiUnifyElims pid a (Con x ci []) (map Apply us) (map Apply vs)
+    (Def f us, Def g vs) | f == g, length us == length vs -> maybeGiveUp $ do
+      a <- computeElimHeadType f us vs
+      antiUnifyElims pid a (Def f []) us vs
+    _ -> fallback
+  where
+    fallback = blockTermOnProblem a u pid
+    maybeGiveUp m = m `catchError_` \ err ->
+      case err of
+        PatternErr{} -> fallback
+        _            -> throwError err
+
+antiUnifyType :: ProblemId -> Type -> Type -> TCM Type
+antiUnifyType pid (El s a) (El _ b) = El s <$> antiUnify pid (sort s) a b
+
+antiUnifyElims :: ProblemId -> Type -> Term -> Elims -> Elims -> TCM Term
+antiUnifyElims pid a self [] [] = return self
+antiUnifyElims pid a self (Proj o f : es1) (Proj _ g : es2) | f == g = do
+  res <- projectTyped self a o f
+  case res of
+    Just (_, self, a) -> antiUnifyElims pid a self es1 es2
+    Nothing -> patternViolation -- can fail for projection like
+antiUnifyElims pid a self (Apply u : es1) (Apply v : es2) = do
+  case ignoreSharing $ unEl a of
+    Pi a b -> do
+      w <- antiUnify pid (unDom a) (unArg u) (unArg v)
+      antiUnifyElims pid (b `lazyAbsApp` w) (apply self [w <$ u]) es1 es2
+    _ -> patternViolation
+antiUnifyElims _ _ _ _ _ = patternViolation -- trigger maybeGiveUp in antiUnify
+
 -- | @compareElims pols a v els1 els2@ performs type-directed equality on eliminator spines.
 --   @t@ is the type of the head @v@.
 compareElims :: [Polarity] -> Type -> Term -> [Elim] -> [Elim] -> TCM ()
@@ -680,7 +746,7 @@ compareElims pols0 a v els01 els02 = catchConstraint (ElimCmp pols0 a v els01 el
                                   (unArg arg1) (unArg arg2)
             -- if comparison got stuck and function type is dependent, block arg
             arg <- if dependent
-                   then (arg1 $>) <$> blockTermOnProblem b (unArg arg1) pid
+                   then (arg1 $>) <$> antiUnify pid b (unArg arg1) (unArg arg2)
                    else return arg1
             -- continue, possibly with blocked instantiation
             compareElims pols (codom `lazyAbsApp` unArg arg) (apply v [arg]) els1 els2

test/Fail/Issue1258-2.err

@@ -1,11 +1,11 @@
 Failed to solve the following constraints:
-  _34 := refl [blocked on problem 49]
-  [49, 52, 56] true , wrap zero = Beta , Beta : _33
-  [49, 52] _32 := Bool × Wrap Nat [blocked on problem 53]
+  _36 := refl [blocked on problem 49]
+  [49, 52, 56, 58] wrap zero = true : _35
+  [49, 52] _34 := Wrap Nat [blocked on problem 53]
+  [49, 52] _32 := Bool [blocked on problem 53]
   [49, 52, 53, 55] Wrap Nat = Foo _28 : Set
   [49, 52, 53] _30 := Bool [blocked on problem 54]
   [49, 52, 53, 54] Bool = Foo _28 : Set
 Unsolved metas at the following locations:
   Issue1258-2.agda:36,9-10
-  Issue1258-2.agda:37,9-10
   Issue1258-2.agda:38,9-13

test/Fail/Issue1258.err

@@ -1,8 +1,8 @@
 Failed to solve the following constraints:
   _20 := refl [blocked on problem 25]
-  _16 := Alpha [blocked on problem 24]
   [25, 28] _18 := Foo Alpha [blocked on problem 29]
   [25, 28, 29] Foo _15 = Bool : Set
+  _16 := Alpha [blocked on problem 24]
   [24] Bool =< Foo _15 : Set
 Unsolved metas at the following locations:
   Issue1258.agda:20,9-10

test/Fail/Issue1982.err

@@ -5,12 +5,12 @@ Failed to solve the following constraints:
   [166, 171, 173] _116 := λ {.Γ} {.Γ′} {.t} {.A} η j → suc _103
                     [blocked on problem 174]
   [166, 171, 173, 174] suc _103 = _103 : Nat
-  [166] _114 := λ {.Γ} {.Γ′} {.t} {.A} η j → suc (suc (suc _103))
+  [166] _114 := λ {.Γ} {.Γ′} {.t} {.A} η j → suc _103
           [blocked on problem 168]
   [166, 168, 169, 170] suc _103 = _103 : Nat
-  [153] _110 := (λ {.Γ} {.Γ′} {.t} {.A} η j → suc _103)
-          [blocked on problem 155]
   _112 := (λ {.Γ} {.Γ′} {.t} {.A} η j → j) [blocked on problem 153]
+  [153] _110 := (λ {.Γ} {.Γ′} {.t} {.A} η j → _103)
+          [blocked on problem 155]
   [153, 155, 156] _103 = (suc _103) : Nat
 Unsolved metas at the following locations:
   Issue1982.agda:28,40-46

test/Fail/Issue399.err

@@ -3,8 +3,6 @@ Failed to solve the following constraints:
   _11 := (_ : _1) [a] :? Set (_10 m mzero)
   _8 := (_ : _1) [a] :? Set (_7 m mzero)
   _3 := (_ : _1) [a] :? Set (_2 m)
-  _31 := Maybe [blocked on problem 30]
-  _34 := λ {.a} → mymaybemzero [blocked on problem 33]
   [38, 39] _9 _32 (λ {.a} → _35) =< Maybe .a
              : Set (_7 _32 (λ {.a} → _35))
   [38, 40] _12 _32 (λ {.a} → _35) =< Maybe .a
@@ -13,9 +11,11 @@ Failed to solve the following constraints:
   .Agda.Primitive.lzero = _10 _32 (λ {.a} → _35)
   _7 _32 (λ {.a} → _35) = .Agda.Primitive.lzero
   .Agda.Primitive.lzero = _7 _32 (λ {.a} → _35)
+  _34 := λ {.a} → mymaybemzero [blocked on problem 33]
   [33, 34] _4 _32 =< Maybe .a : Set (_2 _32)
   _2 _32 = .Agda.Primitive.lzero
   .Agda.Primitive.lzero = _2 _32
+  _31 := Maybe [blocked on problem 30]
   [30] (Set _a_30 → Set _a_30) =< _1
          : (Set (.Agda.Primitive.lsuc _a_30))
   (.Agda.Primitive.lsuc _a_30) = _0

test/Fail/Issue585.err

@@ -1,9 +1,9 @@
 Failed to solve the following constraints:
   _148 := λ τ → ƛ (var · var) · ƛ (_142 τ · var)
     [blocked on problem 226]
-  _141 := (λ τ → var) [blocked on problem 204]
   [226, 242] ♭ (_τ_139 τ) = τ : Ty
   [204, 208, 244] .Issue585.♯-2 = _τ_139 τ : ∞ Ty
+  _141 := (λ τ → var) [blocked on problem 204]
 Unsolved metas at the following locations:
   Issue585.agda:54,49-50
   Issue585.agda:54,45-48

test/Fail/Issue920a.err

@@ -1,8 +1,8 @@
 Failed to solve the following constraints:
   _64 := λ {.A} {x} E → J (_56 E) E [blocked on problem 63]
-  _55 := (λ {.A} {x} E → refl) [blocked on problem 53]
   [63, 75] _63 .A = x : .A
   [53, 57] x = (_63 .A) : .A
+  _55 := (λ {.A} {x} E → refl) [blocked on problem 53]
 Unsolved metas at the following locations:
   Issue920a.agda:26,52-56
   Issue920a.agda:26,49-50

test/interaction/Issue1353.out

@@ -4,7 +4,7 @@
 (agda2-info-action "*Type-checking*" "Checking Issue1353 (Issue1353.agda). " t)
 (agda2-verbose "Found interaction point ?0 : (Pow I) ")
 (agda2-status-action "ShowImplicit")
-(agda2-info-action "*All Goals, Errors*" "?0 : Pow I _239 : (a : Arity Ω {i} p) → _X_241 {I} {X} {i} (input Ω {i} p a) [ at Issue1353.agda:89,71-72 ] _240 : (a : Arity Ω {i} p) → _X_241 {I} {X} {i} (input Ω {i} p a) [ at Issue1353.agda:89,71-72 ] _X_241 : Pow I [ at Issue1353.agda:89,60-65 ] _242 : Σ (Parameter Ψ i) (λ p → (a : Arity Ψ {i} p) → X (input Ψ {i} p a)) [ at Issue1353.agda:89,54-73 ] _243 : Σ (Parameter Ψ i) (λ p → (a : Arity Ψ {i} p) → X (input Ψ {i} p a)) [ at Issue1353.agda:89,54-73 ] ———— Errors ———————————————————————————————————————————————— Failed to solve the following constraints: _242 := λ {I} {Ω} {Ψ} {X} φ m {i} p k → ⟪_⟫ {I} {Ω} {Ψ} m (_X_241 {I} {X} {i}) {i} (p , _240 {I} {Ω} {Ψ} {X} φ m {i} p k) [blocked on problem 360] _239 := (λ {I} {Ω} {Ψ} {X} φ m {i} p k → k) [blocked on problem 357] [357] X (input Ω {i} p a) =< _X_241 {I} {X} {i} (input Ω {i} p a) : Set [360, 362] _X_241 {I} {X} {i} (input Ψ {i} x a) =< X (input Ψ {i} x a) : Set " nil)
+(agda2-info-action "*All Goals, Errors*" "?0 : Pow I _239 : (a : Arity Ω {i} p) → _X_241 {I} {X} {i} (input Ω {i} p a) [ at Issue1353.agda:89,71-72 ] _240 : (a : Arity Ω {i} p) → _X_241 {I} {X} {i} (input Ω {i} p a) [ at Issue1353.agda:89,71-72 ] _X_241 : Pow I [ at Issue1353.agda:89,60-65 ] _242 : Σ (Parameter Ψ i) (λ p → (a : Arity Ψ {i} p) → X (input Ψ {i} p a)) [ at Issue1353.agda:89,54-73 ] _243 : Σ (Parameter Ψ i) (λ p → (a : Arity Ψ {i} p) → X (input Ψ {i} p a)) [ at Issue1353.agda:89,54-73 ] ———— Errors ———————————————————————————————————————————————— Failed to solve the following constraints: _242 := λ {I} {Ω} {Ψ} {X} φ m {i} p k → ⟪_⟫ {I} {Ω} {Ψ} m (_X_241 {I} {X} {i}) {i} (p , _240 {I} {Ω} {Ψ} {X} φ m {i} p k) [blocked on problem 360] [357] X (input Ω {i} p a) =< _X_241 {I} {X} {i} (input Ω {i} p a) : Set [360, 362] _X_241 {I} {X} {i} (input Ψ {i} x a) =< X (input Ψ {i} x a) : Set _239 := (λ {I} {Ω} {Ψ} {X} φ m {i} p k → k) [blocked on problem 357] " nil)
 ((last . 1) . (agda2-goals-action '(0)))
 (agda2-give-action 0 "X")
 (agda2-status-action "ShowImplicit")

test/interaction/Issue1365.out

@@ -5,11 +5,11 @@
 (agda2-status-action "")
 (agda2-info-action "*All Goals, Errors*" "?0 : Alg (_Ψ_548 φ m p k v) (_X_549 φ m p k v) ?1 : _Ω_547 φ m p k v ⇛[ _f_550 φ m p k v ] _Ψ_548 φ m p k v ?2 : _x_553 φ m p k v ∈ ⟦ _Ω_547 φ m p k v ⟧ ((λ {.x} → _X_549 φ m p k v) ∘ _f_550 φ m p k v) _I_545 : Set [ at Issue1365.agda:165,37-43 ] _J_546 : Set [ at Issue1365.agda:165,37-43 ] _Ω_547 : Sig (_I_545 φ m p k v) [ at Issue1365.agda:165,37-43 ] _Ψ_548 : Sig (_J_546 φ m p k v) [ at Issue1365.agda:165,37-43 ] _X_549 : Pow (_J_546 φ m p k v) [ at Issue1365.agda:165,37-43 ] _f_550 : _I_545 φ m p k v → _J_546 φ m p k v [ at Issue1365.agda:165,37-43 ] _x_553 : _I_545 φ m p k v [ at Issue1365.agda:165,37-59 ] _555 : μ (.Ω″ ⋆^C .W) (proj₂ (.f .i)) [ at Issue1365.agda:165,37-64 ] _556 : μ (.Ω″ ⋆^C .W) (proj₂ (.f .i)) [ at Issue1365.agda:165,37-64 ] ———— Errors ———————————————————————————————————————————————— Failed to solve the following constraints: _555 := λ {.I} {.i} {.J} {.K} {.Ω} {.Ω′} {.Ω″} {.U} {.V} {.W} {.f} φ m p k v → weaken (?0 φ m p k v) (?1 φ m p k v) (?2 φ m p k v) [blocked on problem 982] [982] _X_549 φ m p k v (_f_550 φ m p k v (_x_553 φ m p k v)) =< μ (.Ω″ ⋆^C .W) (proj₂ (.f .i)) : Set " nil)
 ((last . 1) . (agda2-goals-action '(0 1 2)))
-(agda2-info-action "*Error*" "Issue1365.agda:165,37-64 (_591 φ m p k v , _592 φ m p k v) ∈ ((λ {.x} → _V_561 φ m p k v) ∘ proj₁) → (_591 φ m p k v , _592 φ m p k v) ∈ ((λ {.x} → ((λ o → Parameter .Ω″ o) ◃ (λ {o} → Arity .Ω″) / (λ {o} → input .Ω″)) ⋆ (λ z → .W z)) ∘ proj₂) !=< μ (.Ω″ ⋆^C .W) (proj₂ (.f .i)) of type Set when checking that the expression weaken ? ? ? has type proj₂ (.f .i) ∈ (.Ω″ ⋆ .W)" nil)
+(agda2-info-action "*Error*" "Issue1365.agda:165,37-64 (_651 φ m p k v , _652 φ m p k v) ∈ ((λ {.x} → _V_561 φ m p k v) ∘ proj₁) → (_651 φ m p k v , _652 φ m p k v) ∈ ((λ {.x} → ((λ o → Parameter .Ω″ o) ◃ (λ {o} → Arity .Ω″) / (λ {o} → input .Ω″)) ⋆ (λ z → .W z)) ∘ proj₂) !=< μ (.Ω″ ⋆^C .W) (proj₂ (.f .i)) of type Set when checking that the expression weaken ? ? ? has type proj₂ (.f .i) ∈ (.Ω″ ⋆ .W)" nil)
 ((last . 3) . (agda2-maybe-goto '("Issue1365.agda" . 4945)))
 (agda2-highlight-load-and-delete-action)
 (agda2-status-action "")
-(agda2-info-action "*Error*" "Issue1365.agda:165,37-64 (_591 φ m p k v , _592 φ m p k v) ∈ ((λ {.x} → _V_561 φ m p k v) ∘ proj₁) → (_591 φ m p k v , _592 φ m p k v) ∈ ((λ {.x} → ((λ o → Parameter .Ω″ o) ◃ (λ {o} → Arity .Ω″) / (λ {o} → input .Ω″)) ⋆ (λ z → .W z)) ∘ proj₂) !=< μ (.Ω″ ⋆^C .W) (proj₂ (.f .i)) of type Set when checking that the expression weaken ? ? ? has type proj₂ (.f .i) ∈ (.Ω″ ⋆ .W)" nil)
+(agda2-info-action "*Error*" "Issue1365.agda:165,37-64 (_651 φ m p k v , _652 φ m p k v) ∈ ((λ {.x} → _V_561 φ m p k v) ∘ proj₁) → (_651 φ m p k v , _652 φ m p k v) ∈ ((λ {.x} → ((λ o → Parameter .Ω″ o) ◃ (λ {o} → Arity .Ω″) / (λ {o} → input .Ω″)) ⋆ (λ z → .W z)) ∘ proj₂) !=< μ (.Ω″ ⋆^C .W) (proj₂ (.f .i)) of type Set when checking that the expression weaken ? ? ? has type proj₂ (.f .i) ∈ (.Ω″ ⋆ .W)" nil)
 ((last . 3) . (agda2-maybe-goto '("Issue1365.agda" . 4945)))
 (agda2-highlight-load-and-delete-action)
 (agda2-status-action "")

test/interaction/Issue903.out

@@ -7,5 +7,5 @@
 ((last . 1) . (agda2-goals-action '(0 1 2 3)))
 (agda2-give-action 3 "h")
 (agda2-status-action "")
-(agda2-info-action "*All Goals, Errors*" "?0 : Set → Set ?1 : ?0 T ?2 : Set _17 : Set [ at Issue903.agda:18,18-32 ] _18 : Set [ at Issue903.agda:18,18-32 ] _19 : Id (?0 T) ?1 [ at Issue903.agda:18,18-32 ] _20 : Id (?0 T) ?1 [ at Issue903.agda:18,18-32 ] _21 : Id T (?1 tt) [ at 1,1-2 ] _22 : Id T (?1 tt) [ at 1,1-2 ] ———— Errors ———————————————————————————————————————————————— Failed to solve the following constraints: _19 := e T ?1 _22 [blocked on problem 24] [24] _17 := T → T [blocked on problem 25] _21 := h [blocked on problem 28] [24, 25] T → T = ?0 T : Set [28, 30] tt = (?1 tt) : T " nil)
+(agda2-info-action "*All Goals, Errors*" "?0 : Set → Set ?1 : ?0 T ?2 : Set _17 : Set [ at Issue903.agda:18,18-32 ] _18 : Set [ at Issue903.agda:18,18-32 ] _19 : Id (?0 T) ?1 [ at Issue903.agda:18,18-32 ] _20 : Id (?0 T) ?1 [ at Issue903.agda:18,18-32 ] _21 : Id T (?1 tt) [ at 1,1-2 ] _22 : Id T (?1 tt) [ at 1,1-2 ] ———— Errors ———————————————————————————————————————————————— Failed to solve the following constraints: _21 := h [blocked on problem 28] [24, 25] T → T = ?0 T : Set [28, 30] tt = (?1 tt) : T _19 := e T ?1 _22 [blocked on problem 24] [24] _17 := T → T [blocked on problem 25] " nil)
 ((last . 1) . (agda2-goals-action '(0 1 2)))