From 45e8d9af43367cd80470286df754a1d296e8f717 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 22 Dec 2021 13:54:21 +0100 Subject: [PATCH] feat: support [nospecialize] on typeclasses --- src/library/compiler/specialize.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/library/compiler/specialize.cpp b/src/library/compiler/specialize.cpp index ac6f940c81..897dc5e4b1 100644 --- a/src/library/compiler/specialize.cpp +++ b/src/library/compiler/specialize.cpp @@ -180,7 +180,12 @@ environment update_spec_info(environment const & env, comp_decls const & ds) { expr fvar = lctx.mk_local_decl(ngen, binding_name(code), type); fvars.push_back(fvar); if (is_inst_implicit(binding_info(code))) { - info.second.push_back(spec_arg_kind::FixedInst); + expr const & fn = get_app_fn(type); + if (is_const(fn) && has_nospecialize_attribute(env, const_name(fn))) { + info.second.push_back(spec_arg_kind::FixedNeutral); + } else { + info.second.push_back(spec_arg_kind::FixedInst); + } } else { type_checker tc(env, lctx); type = tc.whnf(type);