                           text "', of type '" <+> prettyTCM t' <+> text "'."
                         ca <- liftTCM $ runErrorT $ checkArguments ExpandLast DontExpandInstanceArguments (getRange mv) [] t' t
                         case ca of Left _ -> __IMPOSSIBLE__
                                    Right (args, t'') -> do
                                      leqType t'' t
                                      ctxArgs <- getContextArgs
                                      assignV m ctxArgs (term `apply` args)
                                      return False
      cs -> do reportSDoc "tc.constr.findInScope" 15 $
                 text ("findInScope 5: more than one candidate found: ") <+>
                 prettyTCM (List.map fst cs)