Another tweak to cong!

src/Tactic/Cong.agda

@@ -31,14 +31,17 @@ open import Function.Base using (_$_)
 open import Data.Bool.Base            using (true; false; if_then_else_; _∧_)
 open import Data.Char.Base   as Char  using (toℕ)
 open import Data.Float.Base  as Float using (_≡ᵇ_)
-open import Data.List.Base   as List  using ([]; _∷_)
+open import Data.List.Base   as List  using (List; []; _∷_; _++_)
 open import Data.Maybe.Base  as Maybe using (Maybe; just; nothing)
 open import Data.Nat.Base    as ℕ     using (ℕ; zero; suc; _≡ᵇ_; _+_)
-open import Data.Unit.Base            using (⊤)
+open import Data.Unit.Base            using (⊤; tt)
 open import Data.Word.Base   as Word  using (toℕ)
 open import Data.Product.Base         using (_×_; map₁; _,_)
+open import Effect.Applicative        using (RawApplicative; mkRawApplicative)
+open import Function                  using (flip; case_of_)
 
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
+open import Relation.Nullary.Decidable.Core            using (yes; no)
 
 -- 'Data.String.Properties' defines this via 'Dec', so let's use the
 -- builtin for maximum speed.
@@ -54,6 +57,7 @@ open import Reflection.AST.Literal              as Literal
 open import Reflection.AST.Meta                 as Meta
 open import Reflection.AST.Name                 as Name
 open import Reflection.AST.Term                 as Term
+import Reflection.AST.Traversal                 as Traversal
 
 open import Reflection.TCM.Syntax
 
@@ -102,6 +106,16 @@ private
   notEqualityError : ∀ {A : Set} Term → TC A
   notEqualityError goal = typeError (strErr "Cannot rewrite a goal that is not equality: " ∷ termErr goal ∷ [])
 
+  unificationError : ∀ {A : Set} → TC Term → TC Term → TC A
+  unificationError term symTerm = do
+    term' ← term
+    symTerm' ← symTerm
+    -- Don't show the same term twice.
+    let symErr = case term' Term.≟ symTerm' of λ where
+      (yes _) → []
+      (no _) → strErr "\n" ∷ termErr symTerm' ∷ []
+    typeError (strErr "cong! failed, tried:\n" ∷ termErr term' ∷ symErr)
+
   record EqualityGoal : Set where
     constructor equals
     field
@@ -132,6 +146,21 @@ private
     `y ← quoteTC y
     pure $ def (quote cong) $ `a ⟅∷⟆ `A ⟅∷⟆ level ⟅∷⟆ type ⟅∷⟆ vLam "ϕ" f ⟨∷⟩ `x ⟅∷⟆ `y ⟅∷⟆ eq ⟨∷⟩ []
 
+  module _ where
+    private
+      applicative : ∀ {ℓ} → RawApplicative {ℓ} λ _ → List Meta
+      applicative = mkRawApplicative (λ _ → List Meta) (λ _ → []) _++_
+
+      open Traversal applicative
+
+      actions : Actions
+      actions = record defaultActions { onMeta = λ _ x → x ∷ [] }
+
+    blockOnMetas : Term → TC ⊤
+    blockOnMetas t with traverseTerm actions (0 , []) t
+    ... | []         = pure tt
+    ... | xs@(_ ∷ _) = blockTC (blockerAll (List.map blockerMeta xs))
+
 ------------------------------------------------------------------------
 -- Anti-Unification
 --
@@ -236,12 +265,17 @@ macro
     withNormalisation false $ do
       goal ← inferType hole
       eqGoal ← destructEqualityGoal goal
-      let uni = λ lhs rhs → do
-        let cong-lam = antiUnify 0 lhs rhs
-        cong-tm ← `cong eqGoal cong-lam x≡y
-        unify cong-tm hole
+      let makeTerm = λ lhs rhs → `cong eqGoal (antiUnify 0 lhs rhs) x≡y
       let lhs = EqualityGoal.lhs eqGoal
       let rhs = EqualityGoal.rhs eqGoal
-      -- When using ⌞_⌟ with ≡⟨ ... ⟨, (uni lhs rhs) fails and
-      -- (uni rhs lhs) succeeds.
-      catchTC (uni lhs rhs) (uni rhs lhs)
+      let term = makeTerm lhs rhs
+      let symTerm = makeTerm rhs lhs
+      let uni = _>>= flip unify hole
+      catchTC
+        -- When using ⌞_⌟ with ≡⟨ ... ⟨, (uni term) fails and
+        -- (uni symTerm) succeeds.
+        (catchTC (uni term) (uni symTerm)) $ do
+          -- If we failed because of unresolved metas, restart.
+          blockOnMetas goal
+          -- If we failed for a different reason, show an error.
+          unificationError term symTerm