From 4544443d983929a61bc21f973fe2e9726a207311 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 21 Feb 2023 13:54:26 -0800 Subject: [PATCH] feat: reorder tc subgoals according to out-params --- src/Lean/Elab/Structure.lean | 1 - src/Lean/Meta/Instances.lean | 103 +++++++++++++++++- src/Lean/Meta/SynthInstance.lean | 88 ++++++++------- src/lake | 2 +- src/library/constructions/projection.cpp | 26 ++--- tests/lean/1007.lean | 7 +- tests/lean/1007.lean.expected.out | 9 +- tests/lean/1102.lean | 6 +- tests/lean/run/1901.lean | 6 +- tests/lean/run/602.lean | 1 - tests/lean/run/irreducibleIssue.lean | 2 +- tests/lean/run/synth1.lean | 2 +- tests/lean/run/typeclass_coerce.lean | 4 +- .../run/typeclass_metas_internal_goals1.lean | 1 + .../run/typeclass_metas_internal_goals2.lean | 1 + .../run/typeclass_metas_internal_goals3.lean | 3 +- .../run/typeclass_metas_internal_goals4.lean | 1 + tests/lean/synthorder.lean | 26 +++++ tests/lean/synthorder.lean.expected.out | 24 ++++ 19 files changed, 233 insertions(+), 80 deletions(-) create mode 100644 tests/lean/synthorder.lean create mode 100644 tests/lean/synthorder.lean.expected.out diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index adac1544d517..f776f61f4a4f 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -761,7 +761,6 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params : let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default withLocalDeclD `self structType fun source => do let mut declType ← instantiateMVars (← mkForallFVars params (← mkForallFVars #[source] parentType)) - declType := mkOutParamArgsImplicit declType if view.isClass && isClass env parentStructName then declType := setSourceInstImplicit declType declType := declType.inferImplicit params.size true diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean index 87a2bcb941c6..e4bcc753ddba 100644 --- a/src/Lean/Meta/Instances.lean +++ b/src/Lean/Meta/Instances.lean @@ -6,9 +6,15 @@ Authors: Leonardo de Moura import Lean.ScopedEnvExtension import Lean.Meta.GlobalInstances import Lean.Meta.DiscrTree +import Lean.Meta.CollectMVars namespace Lean.Meta +register_builtin_option synthInstance.checkSynthOrder : Bool := { + defValue := true + descr := "check instances do not introduce metavariable in non-out-params" +} + /- Note: we want to use iota reduction when indexing instaces. Otherwise, we cannot elaborate examples such as @@ -38,6 +44,8 @@ structure InstanceEntry where val : Expr priority : Nat globalName? : Option Name := none + /-- The order in which the instance's arguments are to be synthesized. -/ + synthOrder : Array Nat /- We store the attribute kind to be able to implement the API `getInstanceAttrKind`. TODO: add better support for retrieving the `attrKind` of any attribute. @@ -88,11 +96,103 @@ private def mkInstanceKey (e : Expr) : MetaM (Array InstanceKey) := do let (_, _, type) ← forallMetaTelescopeReducing type DiscrTree.mkPath type +/-- +Compute the order the arguments of `inst` should by synthesized. + +The synthesization order makes sure that all mvars in non-out-params of the +subgoals are assigned before we try to synthesize it. Otherwise it goes left +to right. + +For example: + - `[Add α] [Zero α] : Foo α` returns `[0, 1]` + - `[Mul A] [Mul B] [MulHomClass F A B] : FunLike F A B` returns `[2, 0, 1]` + (because A B are out-params and are only filled in once we synthesize 2) + +(The type of `inst` must not contain mvars.) +-/ +partial def computeSynthOrder (inst : Expr) : MetaM (Array Nat) := + withReducible do + let instTy ← inferType inst + + -- Gets positions of all out- and semi-out-params of `classTy` + -- (where `classTy` is e.g. something like `Inhabited Nat`) + let rec getSemiOutParamPositionsOf (classTy : Expr) : MetaM (Array Nat) := do + if let .const className .. := classTy.getAppFn then + forallTelescopeReducing (← inferType classTy.getAppFn) fun args _ => do + let mut pos := (getOutParamPositions? (← getEnv) className).getD #[] + for arg in args, i in [:args.size] do + if (← inferType arg).isAppOf ``semiOutParam then + pos := pos.push i + return pos + else + return #[] + + -- Create both metavariables and free variables for the instance args + -- We will successively pick subgoals where all non-out-params have been + -- assigned already. After picking such a "ready" subgoal, we assign the + -- mvars in its out-params by the corresponding fvars. + let (argMVars, argBIs, ty) ← forallMetaTelescopeReducing instTy + let ty ← whnf ty + forallTelescopeReducing instTy fun argVars _ => do + + -- Assigns all mvars from argMVars in e by the corresponding fvar. + let rec assignMVarsIn (e : Expr) : MetaM Unit := do + for mvarId in ← getMVars e do + if let some i := argMVars.findIdx? (·.mvarId! == mvarId) then + mvarId.assign argVars[i]! + assignMVarsIn (← inferType (.mvar mvarId)) + + -- We start by assigning all metavariables in non-out-params of the return value. + -- These are assumed to not be mvars during TC search (or at least not assignable) + let tyOutParams ← getSemiOutParamPositionsOf ty + let tyArgs := ty.getAppArgs + for tyArg in tyArgs, i in [:tyArgs.size] do + unless tyOutParams.contains i do assignMVarsIn tyArg + + -- Now we successively try to find the next ready subgoal, where all + -- non-out-params are mvar-free. + let mut synthed := #[] + let mut toSynth := List.range argMVars.size |>.filter (argBIs[·]! == .instImplicit) |>.toArray + while !toSynth.isEmpty do + let next? ← toSynth.findM? fun i => do + forallTelescopeReducing (← instantiateMVars (← inferType argMVars[i]!)) fun _ argTy => do + let argTy ← whnf argTy + let argOutParams ← getSemiOutParamPositionsOf argTy + let argTyArgs := argTy.getAppArgs + for i in [:argTyArgs.size], argTyArg in argTyArgs do + if !argOutParams.contains i && argTyArg.hasExprMVar then + return false + return true + let next ← + match next? with + | some next => pure next + | none => + if synthInstance.checkSynthOrder.get (← getOptions) then + let typeLines := ("" : MessageData).joinSep <| Array.toList <| ← toSynth.mapM fun i => do + let ty ← instantiateMVars (← inferType argMVars[i]!) + return indentExpr (ty.setPPExplicit true) + logError m!"cannot find synthesization order for instance {inst} with type{indentExpr instTy}\nall remaining arguments have metavariables:{typeLines}" + pure toSynth[0]! + synthed := synthed.push next + toSynth := toSynth.filter (· != next) + assignMVarsIn (← inferType argMVars[next]!) + assignMVarsIn argMVars[next]! + + if synthInstance.checkSynthOrder.get (← getOptions) then + let ty ← instantiateMVars ty + if ty.hasExprMVar then + logError m!"instance does not provide concrete values for (semi-)out-params{indentExpr (ty.setPPExplicit true)}" + + trace[Meta.synthOrder] "synthesizing the arguments of {inst} in the order {synthed}:{("" : MessageData).joinSep (← synthed.mapM fun i => return indentExpr (← inferType argVars[i]!)).toList}" + + return synthed + def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do let c ← mkConstWithLevelParams declName let keys ← mkInstanceKey c addGlobalInstance declName attrKind - instanceExtension.add { keys := keys, val := c, priority := prio, globalName? := declName, attrKind } attrKind + let synthOrder ← computeSynthOrder c + instanceExtension.add { keys, val := c, priority := prio, globalName? := declName, attrKind, synthOrder } attrKind builtin_initialize registerBuiltinAttribute { @@ -171,6 +271,7 @@ builtin_initialize unless kind == AttributeKind.global do throwError "invalid attribute 'default_instance', must be global" discard <| addDefaultInstance declName prio |>.run {} {} } + registerTraceClass `Meta.synthOrder def getDefaultInstancesPriorities [Monad m] [MonadEnv m] : m PrioritySet := return defaultInstanceExtension.getState (← getEnv) |>.priorities diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index ef5865195fcb..ddd2b72cb6d1 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -34,17 +34,16 @@ namespace SynthInstance def getMaxHeartbeats (opts : Options) : Nat := synthInstance.maxHeartbeats.get opts * 1000 -builtin_initialize inferTCGoalsRLAttr : TagAttribute ← - registerTagAttribute `infer_tc_goals_rl "instruct type class resolution procedure to solve goals from right to left for this instance" - -def hasInferTCGoalsRLAttribute (env : Environment) (constName : Name) : Bool := - inferTCGoalsRLAttr.hasTag env constName +structure Instance where + val : Expr + synthOrder : Array Nat + deriving Inhabited structure GeneratorNode where mvar : Expr key : Expr mctx : MetavarContext - instances : Array Expr + instances : Array Instance currInstanceIdx : Nat deriving Inhabited @@ -191,7 +190,7 @@ instance : Inhabited (SynthM α) where default := fun _ _ => default /-- Return globals and locals instances that may unify with `type` -/ -def getInstances (type : Expr) : MetaM (Array Expr) := do +def getInstances (type : Expr) : MetaM (Array Instance) := do -- We must retrieve `localInstances` before we use `forallTelescopeReducing` because it will update the set of local instances let localInstances ← getLocalInstances forallTelescopeReducing type fun _ type => do @@ -205,16 +204,27 @@ def getInstances (type : Expr) : MetaM (Array Expr) := do -- Most instances have default priority. let result := result.insertionSort fun e₁ e₂ => e₁.priority < e₂.priority let erasedInstances ← getErasedInstances - let result ← result.filterMapM fun e => match e.val with + let mut result ← result.filterMapM fun e => match e.val with | Expr.const constName us => if erasedInstances.contains constName then return none else - return some <| e.val.updateConst! (← us.mapM (fun _ => mkFreshLevelMVar)) + return some { + val := e.val.updateConst! (← us.mapM (fun _ => mkFreshLevelMVar)) + synthOrder := e.synthOrder + } | _ => panic! "global instance is not a constant" - let result := localInstances.foldl (init := result) fun (result : Array Expr) linst => - if linst.className == className then result.push linst.fvar else result - trace[Meta.synthInstance.instances] result + for linst in localInstances do + if linst.className == className then + let synthOrder ← forallTelescopeReducing (← inferType linst.fvar) fun xs _ => do + if xs.isEmpty then return #[] + let mut order := #[] + for i in [:xs.size], x in xs do + if (← getFVarLocalDecl x).binderInfo == .instImplicit then + order := order.push i + return order + result := result.push { val := linst.fvar, synthOrder } + trace[Meta.synthInstance.instances] result.map (·.val) return result def mkGeneratorNode? (key mvar : Expr) : MetaM (Option GeneratorNode) := do @@ -275,25 +285,6 @@ structure SubgoalsResult where instVal : Expr instTypeBody : Expr -private partial def getSubgoalsAux (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array Expr) - : Array Expr → Nat → List Expr → Expr → Expr → MetaM SubgoalsResult - | args, j, subgoals, instVal, Expr.forallE _ d b bi => do - let d := d.instantiateRevRange j args.size args - let mvarType ← mkForallFVars xs d - let mvar ← mkFreshExprMVarAt lctx localInsts mvarType - let arg := mkAppN mvar xs - let instVal := mkApp instVal arg - let subgoals := if bi.isInstImplicit then mvar::subgoals else subgoals - let args := args.push (mkAppN mvar xs) - getSubgoalsAux lctx localInsts xs args j subgoals instVal b - | args, j, subgoals, instVal, type => do - let type := type.instantiateRevRange j args.size args - let type ← whnf type - if type.isForall then - getSubgoalsAux lctx localInsts xs args args.size subgoals instVal type - else - return ⟨subgoals, instVal, type⟩ - /-- `getSubgoals lctx localInsts xs inst` creates the subgoals for the instance `inst`. The subgoals are in the context of the free variables `xs`, and @@ -309,21 +300,36 @@ private partial def getSubgoalsAux (lctx : LocalContext) (localInsts : LocalInst metavariables that are instance implicit arguments, and the expressions: - `inst (?m_1 xs) ... (?m_n xs)` (aka `instVal`) - `B (?m_1 xs) ... (?m_n xs)` -/ -def getSubgoals (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array Expr) (inst : Expr) : MetaM SubgoalsResult := do - let instType ← inferType inst - let result ← getSubgoalsAux lctx localInsts xs #[] 0 [] inst instType - if let .const constName _ := inst.getAppFn then - let env ← getEnv - if hasInferTCGoalsRLAttribute env constName then - return result - return { result with subgoals := result.subgoals.reverse } +def getSubgoals (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array Expr) (inst : Instance) : MetaM SubgoalsResult := do + let mut instVal := inst.val + let mut instType ← inferType instVal + let mut mvars := #[] + let mut subst := #[] + repeat do + if let .forallE _ d b _ := instType then + let d := d.instantiateRev subst + let mvar ← mkFreshExprMVarAt lctx localInsts (← mkForallFVars xs d) + subst := subst.push (mkAppN mvar xs) + instVal := mkApp instVal (mkAppN mvar xs) + instType := b + mvars := mvars.push mvar + else + instType ← whnf (instType.instantiateRev subst) + instVal := instVal.instantiateRev subst + subst := #[] + unless instType.isForall do break + return { + instVal := instVal.instantiateRev subst + instTypeBody := instType.instantiateRev subst + subgoals := inst.synthOrder.map (mvars[·]!) |>.toList + } /-- Try to synthesize metavariable `mvar` using the instance `inst`. Remark: `mctx` is set using `withMCtx`. If it succeeds, the result is a new updated metavariable context and a new list of subgoals. A subgoal is created for each instance implicit parameter of `inst`. -/ -def tryResolve (mvar : Expr) (inst : Expr) : MetaM (Option (MetavarContext × List Expr)) := do +def tryResolve (mvar : Expr) (inst : Instance) : MetaM (Option (MetavarContext × List Expr)) := do let mvarType ← inferType mvar let lctx ← getLCtx let localInsts ← getLocalInstances @@ -518,7 +524,7 @@ def generate : SynthM Unit := do let mvar := gNode.mvar discard do withMCtx mctx do withTraceNode `Meta.synthInstance - (return m!"{exceptOptionEmoji ·} apply {inst} to {← instantiateMVars (← inferType mvar)}") do + (return m!"{exceptOptionEmoji ·} apply {inst.val} to {← instantiateMVars (← inferType mvar)}") do modifyTop fun gNode => { gNode with currInstanceIdx := idx } if let some (mctx, subgoals) ← tryResolve mvar inst then consume { key, mvar, subgoals, mctx, size := 0 } diff --git a/src/lake b/src/lake index 18430cf941dc..cb3b30b51a00 160000 --- a/src/lake +++ b/src/lake @@ -1 +1 @@ -Subproject commit 18430cf941dcfc89332d0c0ff95dd356dffbb794 +Subproject commit cb3b30b51a00a0186e1b3acc9cdc563d66d16f07 diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp index 8a6ea9d6f16b..d999251fea9e 100644 --- a/src/library/constructions/projection.cpp +++ b/src/library/constructions/projection.cpp @@ -30,9 +30,6 @@ static bool is_prop(expr type) { return is_sort(type) && is_zero(sort_level(type)); } -extern "C" object * lean_mk_outparam_args_implicit(object * n); -expr mk_outparam_args_implicit(expr const & type) { return expr(lean_mk_outparam_args_implicit(type.to_obj_arg())); } - environment mk_projections(environment const & env, name const & n, buffer const & proj_names, bool inst_implicit) { local_ctx lctx; name_generator ngen = mk_constructions_name_generator(); @@ -48,21 +45,18 @@ environment mk_projections(environment const & env, name const & n, buffer throw exception(sstream() << "projection generation, '" << n << "' does not have a single constructor"); constant_info cnstr_info = env.get(head(ind_val.get_cnstrs())); expr cnstr_type = cnstr_info.get_type(); - expr cnstr_type_norm = mk_outparam_args_implicit(cnstr_type); - // The binder inference is quite messy since it is using `mk_outparam_args_implicit` and `infer_implicit_params`. - // TODO: cleanup bool is_predicate = is_prop(ind_info.get_type()); names lvl_params = ind_info.get_lparams(); levels lvls = lparams_to_levels(lvl_params); buffer params; // datatype parameters - expr cnstr_type_orig = cnstr_type; // we use the original type before `mk_outparam_args_implicit` to get the original binder info + expr cnstr_type_orig = cnstr_type; for (unsigned i = 0; i < nparams; i++) { - if (!is_pi(cnstr_type_norm)) + if (!is_pi(cnstr_type)) throw_ill_formed(n); lean_assert(is_pi(cnstr_type_orig)); - auto bi = binding_info(cnstr_type_norm); + auto bi = binding_info(cnstr_type); auto bi_orig = binding_info(cnstr_type_orig); - auto type = binding_domain(cnstr_type_norm); + auto type = binding_domain(cnstr_type); auto type_orig = binding_domain(cnstr_type_orig); if (!is_inst_implicit(bi_orig) && !is_class_out_param(type_orig)) { // We reset implicit binders in favor of having them inferred by `infer_implicit_params` later IF @@ -70,8 +64,8 @@ environment mk_projections(environment const & env, name const & n, buffer // 2. It is not originally an outparam. Outparams must be implicit. bi = mk_binder_info(); } - expr param = lctx.mk_local_decl(ngen, binding_name(cnstr_type_norm), type, bi); - cnstr_type_norm = instantiate(binding_body(cnstr_type_norm), param); + expr param = lctx.mk_local_decl(ngen, binding_name(cnstr_type), type, bi); + cnstr_type = instantiate(binding_body(cnstr_type), param); cnstr_type_orig = binding_body(cnstr_type_orig); params.push_back(param); } @@ -79,7 +73,7 @@ environment mk_projections(environment const & env, name const & n, buffer binder_info c_bi = inst_implicit ? mk_inst_implicit_binder_info() : mk_binder_info(); expr c = lctx.mk_local_decl(ngen, name("self"), C_A, c_bi); buffer cnstr_type_args; // arguments that are not parameters - expr it = cnstr_type_norm; + expr it = cnstr_type; while (is_pi(it)) { expr local = lctx.mk_local_decl(ngen, binding_name(it), binding_domain(it), binding_info(it)); cnstr_type_args.push_back(local); @@ -88,10 +82,10 @@ environment mk_projections(environment const & env, name const & n, buffer unsigned i = 0; environment new_env = env; for (name const & proj_name : proj_names) { - if (!is_pi(cnstr_type_norm)) + if (!is_pi(cnstr_type)) throw exception(sstream() << "generating projection '" << proj_name << "', '" << n << "' does not have sufficient data"); - expr result_type = consume_type_annotations(binding_domain(cnstr_type_norm)); + expr result_type = consume_type_annotations(binding_domain(cnstr_type)); if (is_predicate && !type_checker(new_env, lctx).is_prop(result_type)) { throw exception(sstream() << "failed to generate projection '" << proj_name << "' for '" << n << "', " << "type is an inductive predicate, but field is not a proposition"); @@ -110,7 +104,7 @@ environment mk_projections(environment const & env, name const & n, buffer new_env = set_reducible(new_env, proj_name, reducible_status::Reducible, true); new_env = save_projection_info(new_env, proj_name, cnstr_info.get_name(), nparams, i, inst_implicit); expr proj = mk_app(mk_app(mk_constant(proj_name, lvls), params), c); - cnstr_type_norm = instantiate(binding_body(cnstr_type_norm), proj); + cnstr_type = instantiate(binding_body(cnstr_type), proj); i++; } return new_env; diff --git a/tests/lean/1007.lean b/tests/lean/1007.lean index 9e03b0d2b6c9..4f8775000ab0 100644 --- a/tests/lean/1007.lean +++ b/tests/lean/1007.lean @@ -23,15 +23,14 @@ class Trait (X : Type u) where attribute [reducible] Trait.R -class SemiInner (X : Type u) (R : Type v) where +class SemiInner (X : Type u) (R : outParam (Type v)) where semiInner : X → X → R @[reducible] instance (X) (R : Type u) [SemiInner X R] : Trait X := ⟨R⟩ -class SemiHilbert (X) (R : Type u) [Vec R] extends Vec X, SemiInner X R +class SemiHilbert (X) (R : outParam (Type u)) [Vec R] [Vec X] extends SemiInner X R -@[infer_tc_goals_rl] -instance (X R) [Trait X] [Vec R] [SemiHilbert X R] (ι : Type v) : SemiHilbert (ι → X) R := sorry +instance (X R) [Trait X] [Vec R] [Vec X] [SemiHilbert X R] (ι : Type v) : SemiHilbert (ι → X) R := sorry instance : SemiHilbert ℝ ℝ := sorry -------------- diff --git a/tests/lean/1007.lean.expected.out b/tests/lean/1007.lean.expected.out index 4b51f2095a19..c776ae3043c1 100644 --- a/tests/lean/1007.lean.expected.out +++ b/tests/lean/1007.lean.expected.out @@ -2,10 +2,9 @@ 1007.lean:9:9-9:20: warning: declaration uses 'sorry' 1007.lean:11:33-11:41: warning: declaration uses 'sorry' 1007.lean:15:9-15:20: warning: declaration uses 'sorry' +1007.lean:33:0-33:8: warning: declaration uses 'sorry' 1007.lean:34:0-34:8: warning: declaration uses 'sorry' -1007.lean:35:0-35:8: warning: declaration uses 'sorry' -1007.lean:39:4-39:8: warning: declaration uses 'sorry' -1007.lean:40:4-40:7: warning: declaration uses 'sorry' -1007.lean:57:64-57:78: error: failed to synthesize +1007.lean:38:4-38:8: warning: declaration uses 'sorry' +1007.lean:39:4-39:7: warning: declaration uses 'sorry' +1007.lean:56:64-56:78: error: failed to synthesize instance IsLin fun x => sum fun i => norm x -(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats ' to set the limit) diff --git a/tests/lean/1102.lean b/tests/lean/1102.lean index 260b8f35cab6..0f0a0da8ce0c 100644 --- a/tests/lean/1102.lean +++ b/tests/lean/1102.lean @@ -12,9 +12,9 @@ class cls2 extends cls3 := (u2 : Unit) class cls1 extends cls2 := (u1 : Unit) class cls0 extends cls1 := (u0 : Unit) -class CommRing (n : Nat) extends cls0 := (ucr : Unit) -class Field (n) extends CommRing n := (uf : Unit) -class DVR (n) [CommRing n] := (udvr : Unit) +class CommRing (n : semiOutParam Nat) extends cls0 := (ucr : Unit) +class Field (n : semiOutParam Nat) extends CommRing n := (uf : Unit) +class DVR (n : semiOutParam Nat) [CommRing n] := (udvr : Unit) instance [c : CommRing n] : CommRing n.succ := { ucr := c.u12 } instance [Field n] : DVR n.succ := ⟨()⟩ diff --git a/tests/lean/run/1901.lean b/tests/lean/run/1901.lean index 93af42ed6cf5..0a6e7dfabb39 100644 --- a/tests/lean/run/1901.lean +++ b/tests/lean/run/1901.lean @@ -7,10 +7,10 @@ class MulHomClass (F) (A B : outParam _) [Mul A] [Mul B] extends Funny F A B class Monoid (M) extends Mul M instance [Mul A] : Mul (Id A) := ‹_› -#check @Funny.toFun -#check @MulHomClass.toFunny +#check Funny.toFun +#check MulHomClass.toFunny -example {_ : Monoid A} {_ : Monoid B} [MulHomClass F A B] : Funny F A B := +example [Monoid A] [Monoid B] [MulHomClass F A B] : Funny F A B := inferInstance -- set_option trace.Meta.synthInstance true diff --git a/tests/lean/run/602.lean b/tests/lean/run/602.lean index f7e95092957d..8231f330493c 100644 --- a/tests/lean/run/602.lean +++ b/tests/lean/run/602.lean @@ -18,7 +18,6 @@ instance Ring.toSemiring [instR : Ring α] : Semiring α := { add := instR.add } instance NormedField.toRing [instNF : NormedField α] : Ring α := { add := instNF.add } --- @[infer_tc_goals_rl] instance SemiNormedSpace.toModule [NormedField α] [SemiNormedGroup β] [SemiNormedSpace α β] : Module α β := {} opaque R : Type := Unit diff --git a/tests/lean/run/irreducibleIssue.lean b/tests/lean/run/irreducibleIssue.lean index 42cd5d789971..1fc5f5b70417 100644 --- a/tests/lean/run/irreducibleIssue.lean +++ b/tests/lean/run/irreducibleIssue.lean @@ -3,7 +3,7 @@ class Trait (X : Type u) where attribute [reducible] Trait.R -class SemiInner (X : Type u) (R : Type v) where +class SemiInner (X : Type u) (R : outParam <| Type v) where semiInner : X → X → R @[reducible] instance (X) (R : Type u) [SemiInner X R] : Trait X := ⟨R⟩ diff --git a/tests/lean/run/synth1.lean b/tests/lean/run/synth1.lean index 74477ca9bf1d..737fbe6137ab 100644 --- a/tests/lean/run/synth1.lean +++ b/tests/lean/run/synth1.lean @@ -3,7 +3,7 @@ import Lean.Meta open Lean open Lean.Meta -class HasCoerce (a b : Type) := +class HasCoerce (a : semiOutParam Type) (b : Type) := (coerce : a → b) def coerce {a b : Type} [HasCoerce a b] : a → b := diff --git a/tests/lean/run/typeclass_coerce.lean b/tests/lean/run/typeclass_coerce.lean index b72ecd458258..f3298541d879 100644 --- a/tests/lean/run/typeclass_coerce.lean +++ b/tests/lean/run/typeclass_coerce.lean @@ -7,8 +7,10 @@ Declare new, simpler coercion class without the special support for transitivity Test that new tabled typeclass resolution deals with loops and diamonds correctly. -/ +set_option synthInstance.checkSynthOrder false -class HasCoerce (a b : Type) := + +class HasCoerce (a : Type) (b : Type) := (coerce : a → b) def coerce {a b : Type} [HasCoerce a b] : a → b := diff --git a/tests/lean/run/typeclass_metas_internal_goals1.lean b/tests/lean/run/typeclass_metas_internal_goals1.lean index d08fe4451e2a..f1fc52b624ca 100644 --- a/tests/lean/run/typeclass_metas_internal_goals1.lean +++ b/tests/lean/run/typeclass_metas_internal_goals1.lean @@ -7,6 +7,7 @@ class Top : Type := (u : Unit := ()) instance FooAll (α : Type) : Foo α := {u:=()} instance BarNat : Bar Nat := {u:=()} +set_option synthInstance.checkSynthOrder false in instance FooBarToTop (α : Type) [Foo α] [Bar α] : Top := {u:=()} set_option pp.all true diff --git a/tests/lean/run/typeclass_metas_internal_goals2.lean b/tests/lean/run/typeclass_metas_internal_goals2.lean index 63a6b6198ff2..98a2df71077d 100644 --- a/tests/lean/run/typeclass_metas_internal_goals2.lean +++ b/tests/lean/run/typeclass_metas_internal_goals2.lean @@ -6,6 +6,7 @@ class Top : Type := (u : Unit := ()) instance FooNatA (β : Type) : Foo Nat β := {u:=()} instance BarANat (α : Type) : Bar α Nat := {u:=()} +set_option synthInstance.checkSynthOrder false in instance FooBarToTop (α β : Type) [Foo α β] [Bar α β] : Top := {u:=()} set_option pp.all true diff --git a/tests/lean/run/typeclass_metas_internal_goals3.lean b/tests/lean/run/typeclass_metas_internal_goals3.lean index 1ab0b26cafbe..0f201e7cb5cb 100644 --- a/tests/lean/run/typeclass_metas_internal_goals3.lean +++ b/tests/lean/run/typeclass_metas_internal_goals3.lean @@ -5,8 +5,9 @@ class Depends (α : Type) [Base α] := (u:Unit) class Top := (u:Unit) instance AllBase {α : Type} : Base α := {u:=()} -instance DependsNotConstrainingImplicit {α : Type} /- [Base α] -/ {_:Base α} : Depends α := {u:=()} +instance DependsNotConstrainingImplicit {α : Type} [Base α] : Depends α := {u:=()} +set_option synthInstance.checkSynthOrder false instance BaseAsImplicit₁ {α : Type} {_:Base α} [Depends α] : Top := {u:=()} instance BaseAsInstImplicit {α : Type} [Base α] [Depends α] : Top := {u:=()} instance BaseAsImplicit₂ {α : Type} {_:Base α} [Depends α] : Top := {u:=()} diff --git a/tests/lean/run/typeclass_metas_internal_goals4.lean b/tests/lean/run/typeclass_metas_internal_goals4.lean index 25b7e188cdeb..e148c87cfa8f 100644 --- a/tests/lean/run/typeclass_metas_internal_goals4.lean +++ b/tests/lean/run/typeclass_metas_internal_goals4.lean @@ -2,6 +2,7 @@ class Foo (α β γ : Type) := (u:Unit) class Bar (α β γ : Type) := (u:Unit) class Top := (u:Unit) +set_option synthInstance.checkSynthOrder false in instance FooBarToTop (α β γ : Type) [Foo α β γ] [Bar α β γ] : Top := {u:=()} instance Foo₁ (β γ : Type) : Foo Unit β γ := {u:=()} diff --git a/tests/lean/synthorder.lean b/tests/lean/synthorder.lean new file mode 100644 index 000000000000..416e2cab1ed8 --- /dev/null +++ b/tests/lean/synthorder.lean @@ -0,0 +1,26 @@ +class Foo (A : Type) (B : semiOutParam Type) + +-- should be rejected, because C appears by itself in an out-param +instance [Foo A B] : Foo A (B × C) where + +-- should be rejected, because non-out-param A can become an mvar +instance [Foo A Nat] : Foo Nat A where + + +set_option trace.Meta.synthOrder true + +-- both instances should synthesize [Foo A B] first: +instance [Foo A B] [Foo B C] : Foo A C where +instance [Foo B C] [Foo A B] : Foo A C where + +instance : Foo (Option A) A where + + + +class One (α : Type) +class Two (α) [One α] +class TwoHalf (α) [One α] extends Two α +class Three (α : Type) (β : outParam Type) [One β] [Two β] +-- should both be accepted and synthesize `Three α β` first: +class Four (α : Type) (β : outParam Type) [One β] [TwoHalf β] extends Three α β +instance [One β] [TwoHalf β] [Three α β] : Four α β where diff --git a/tests/lean/synthorder.lean.expected.out b/tests/lean/synthorder.lean.expected.out new file mode 100644 index 000000000000..d891c4ec711e --- /dev/null +++ b/tests/lean/synthorder.lean.expected.out @@ -0,0 +1,24 @@ +synthorder.lean:4:0-4:40: error: instance does not provide concrete values for (semi-)out-params + Foo A (B × ?C) +synthorder.lean:7:0-7:38: error: cannot find synthesization order for instance @instFooNat with type + {A : Type} → [inst : Foo A Nat] → Foo Nat A +all remaining arguments have metavariables: + Foo ?A Nat +[Meta.synthOrder] synthesizing the arguments of @instFoo in the order [3, 4]: + Foo A B + Foo B C +[Meta.synthOrder] synthesizing the arguments of @instFoo_1 in the order [4, 3]: + Foo A B + Foo B C +[Meta.synthOrder] synthesizing the arguments of @instFooOption in the order []: +[Meta.synthOrder] synthesizing the arguments of @TwoHalf.toTwo in the order [1, 2]: + One α + TwoHalf α +[Meta.synthOrder] synthesizing the arguments of @Four.toThree in the order [4, 2, 3]: + Four α β + One β + TwoHalf β +[Meta.synthOrder] synthesizing the arguments of @instFour in the order [4, 2, 3]: + Three α β + One β + TwoHalf β