@@ -640,14 +640,6 @@ convEq ctxt holes topx topy = ceq [] topx topy where
640640 | x `elem` holes || y `elem` holes = return True
641641 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True
642642 | otherwise = sameDefs ps x y
643− ceq ps x (Bind n (Lam _ t) (App _ y (V 0)))
644− = ceq ps x (substV (P Bound n t) y)
645− ceq ps (Bind n (Lam _ t) (App _ x (V 0))) y
646− = ceq ps (substV (P Bound n t) x) y
647− ceq ps x (Bind n (Lam _ t) (App _ y (P Bound n' _)))
648− | n == n' = ceq ps x y
649− ceq ps (Bind n (Lam _ t) (App _ x (P Bound n' _))) y
650− | n == n' = ceq ps x y
651643
652644 ceq ps (Bind n (PVar _ t) sc) y = ceq ps sc y
653645 ceq ps x (Bind n (PVar _ t) sc) = ceq ps x sc
@@ -668,6 +660,16 @@ convEq ctxt holes topx topy = ceq [] topx topy where
668660 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
669661 ceqB ps (Pi r i v t) (Pi r' i' v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
670662 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')
663+
664+ ceq ps x (Bind n (Lam _ t) (App _ y (V 0)))
665+ = ceq ps x (substV (P Bound n t) y)
666+ ceq ps (Bind n (Lam _ t) (App _ x (V 0))) y
667+ = ceq ps (substV (P Bound n t) x) y
668+ ceq ps x (Bind n (Lam _ t) (App _ y (P Bound n' _)))
669+ | n == n' = ceq ps x y
670+ ceq ps (Bind n (Lam _ t) (App _ x (P Bound n' _))) y
671+ | n == n' = ceq ps x y
672+
671673 -- Special case for 'case' blocks - size of scope causes complications,
672674 -- we only want to check the blocks themselves are valid and identical
673675 -- in the current scope. So, just check the bodies, and the additional