@@ -720,12 +720,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
720 [] (constraintNS info) fc id [] lhs_tm
720 [] (constraintNS info) fc id [] lhs_tm
721 else return (lhs_tm, lhs_ty)
721 else return (lhs_tm, lhs_ty)
722 let clhs = normalise ctxt [] clhs_c
722 let clhs = normalise ctxt [] clhs_c
723− let borrowed = borrowedNames [] clhs
725 -- These are the names we're not allowed to use on the RHS, because
723 -- These are the names we're not allowed to use on the RHS, because
726 -- they're UniqueTypes and borrowed from another function.
724 -- they're UniqueTypes and borrowed from another function.
727− when (not (null borrowed)) $
725+ let borrowed = borrowedNames [] clhs
728− logElab 5 ("Borrowed names on LHS: " ++ show borrowed)
730 logElab 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))
727 logElab 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))