@@ -668,9 +668,9 @@ checkMP ist i mp = if i > 0
668668 -- if we get to a constructor, it's fine as long as it's strictly positive
669669 tryPath desc path ((f, _) : es) arg
670670 | [TyDecl (DCon _ _ _) _] <- lookupDef f (tt_ctxt ist)
671− = case lookupTotal f (tt_ctxt ist) of
672− [Total _] -> Unchecked -- okay so far
673− [Partial _] -> Partial (Other [f])
671+ = case lookupTotalExact f (tt_ctxt ist) of
672+ Just (Total _) -> Unchecked -- okay so far
673+ Just (Partial _) -> Partial (Other [f])
674674 x -> error $ "CAN'T HAPPEN: " ++ show x ++ " for " ++ show f
675675 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
676676 = Total []