@@ -636,6 +636,15 @@ convEq ctxt holes topx topy = ceq [] topx topy where
636636 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
637637 ceqB ps (Pi i v t) (Pi i' v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
638638 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')
639+ -- Special case for 'case' blocks - size of scope causes complications,
640+ -- we only want to check the blocks themselves are valid and identical
641+ -- in the current scope. So, just check the bodies, and the additional
642+ -- arguments the case blocks are applied to.
643+ ceq ps x@(App _ _ _) y@(App _ _ _)
644+ | (P _ cx _, xargs) <- unApply x,
645+ (P _ cy _, yargs) <- unApply y,
646+ caseName cx && caseName cy = sameCase ps cx cy xargs yargs
647+
639648 ceq ps (App _ fx ax) (App _ fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay)
640649 ceq ps (Constant x) (Constant y) = return (x == y)
641650 ceq ps (TType x) (TType y) | x == y = return True
@@ -678,6 +687,24 @@ convEq ctxt holes topx topy = ceq [] topx topy where
678687 caseeq ((x,y):ps) xdef ydef
679688 _ -> return False
680689
690+ sameCase :: [(Name, Name)] -> Name -> Name -> [Term] -> [Term] ->
691+ StateT UCs TC Bool
692+ sameCase ps x y xargs yargs
693+ = case (lookupDef x ctxt, lookupDef y ctxt) of
694+ ([Function _ xdef], [Function _ ydef])
695+ -> ceq ((x,y):ps) xdef ydef
696+ ([CaseOp _ _ _ _ _ xd],
697+ [CaseOp _ _ _ _ _ yd])
698+ -> let (xin, xdef) = cases_compiletime xd
699+ (yin, ydef) = cases_compiletime yd in
700+ do liftM2 (&&)
701+ (do ok <- zipWithM (ceq ps)
702+ (drop (length xin) xargs)
703+ (drop (length yin) yargs)
704+ return (and ok))
705+ (caseeq ((x,y):ps) xdef ydef)
706+ _ -> return False
707+
681708-- SPECIALISATION -----------------------------------------------------------
682709-- We need too much control to be able to do this by tweaking the main
683710-- evaluator