From e68e448070d07461a6eb5df34613d8aff8a804e3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 26 Jul 2022 12:37:04 -0700 Subject: [PATCH] fix: convert inductive type instance implicit parameters to implicit when building `SizeOf` instance It is better for TC resolution since the parameter can be inferred by typing constraints, and it addresses issue #1373 --- src/Lean/Meta/SizeOf.lean | 85 ++++++++++-------- tests/lean/infoTree.lean.expected.out | 86 +++++++++---------- tests/lean/jason1.lean.expected.out | 66 +++++++------- tests/lean/run/1373.lean | 4 + ...syntheticHolesAsPatterns.lean.expected.out | 26 +++--- 5 files changed, 140 insertions(+), 127 deletions(-) create mode 100644 tests/lean/run/1373.lean diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean index fe00dcdb12..9d5f136738 100644 --- a/src/Lean/Meta/SizeOf.lean +++ b/src/Lean/Meta/SizeOf.lean @@ -9,7 +9,7 @@ import Lean.Meta.Instances namespace Lean.Meta /-- Create `SizeOf` local instances for applicable parameters, and execute `k` using them. -/ -private partial def mkLocalInstances {α} (params : Array Expr) (k : Array Expr → MetaM α) : MetaM α := +private partial def mkLocalInstances (params : Array Expr) (k : Array Expr → MetaM α) : MetaM α := loop 0 #[] where loop (i : Nat) (insts : Array Expr) : MetaM α := do @@ -60,7 +60,7 @@ private def isRecField? (motiveFVars : Array Expr) (minorFVars : Array Expr) (fv idx := idx + 1 return none -private partial def mkSizeOfMotives {α} (motiveFVars : Array Expr) (k : Array Expr → MetaM α) : MetaM α := +private partial def mkSizeOfMotives (motiveFVars : Array Expr) (k : Array Expr → MetaM α) : MetaM α := loop 0 #[] where loop (i : Nat) (motives : Array Expr) : MetaM α := do @@ -91,7 +91,7 @@ private partial def mkSizeOfRecFieldFormIH (ih : Expr) : MetaM Expr := do else return ih -private partial def mkSizeOfMinors {α} (motiveFVars : Array Expr) (minorFVars : Array Expr) (minorFVars' : Array Expr) (k : Array Expr → MetaM α) : MetaM α := +private partial def mkSizeOfMinors (motiveFVars : Array Expr) (minorFVars : Array Expr) (minorFVars' : Array Expr) (k : Array Expr → MetaM α) : MetaM α := assert! minorFVars.size == minorFVars'.size loop 0 #[] where @@ -133,19 +133,22 @@ partial def mkSizeOfFn (recName : Name) (declName : Name): MetaM Unit := do let val := mkAppN recFn (params ++ motives) forallBoundedTelescope (← inferType val) recInfo.numMinors fun minorFVars' _ => mkSizeOfMinors motiveFVars minorFVars minorFVars' fun minors => do - let sizeOfParams := params ++ localInsts ++ indices ++ #[major] - let sizeOfType ← mkForallFVars sizeOfParams nat - let val := mkAppN val (minors ++ indices ++ #[major]) - trace[Meta.sizeOf] "val: {val}" - let sizeOfValue ← mkLambdaFVars sizeOfParams val - addDecl <| Declaration.defnDecl { - name := declName - levelParams := levelParams - type := sizeOfType - value := sizeOfValue - safety := DefinitionSafety.safe - hints := ReducibilityHints.abbrev - } + withInstImplicitAsImplict params do + let sizeOfParams := params ++ localInsts ++ indices ++ #[major] + let sizeOfType ← mkForallFVars sizeOfParams nat + let val := mkAppN val (minors ++ indices ++ #[major]) + let sizeOfValue ← mkLambdaFVars sizeOfParams val + trace[Meta.sizeOf] "declName: {declName}" + trace[Meta.sizeOf] "type: {sizeOfType}" + trace[Meta.sizeOf] "val: {sizeOfValue}" + addDecl <| Declaration.defnDecl { + name := declName + levelParams := levelParams + type := sizeOfType + value := sizeOfValue + safety := DefinitionSafety.safe + hints := ReducibilityHints.abbrev + } /-- Create `sizeOf` functions for all inductive datatypes in the mutual inductive declaration containing `typeName` @@ -430,12 +433,16 @@ private def mkSizeOfSpecTheorem (indInfo : InductiveVal) (sizeOfFns : Array Name let thmType ← mkForallFVars thmParams target let thmValue ← if indInfo.isNested then SizeOfSpecNested.main lhs rhs |>.run { - indInfo := indInfo, sizeOfFns := sizeOfFns, ctorName := ctorName, params := params, localInsts := localInsts, recMap := recMap + indInfo, sizeOfFns, ctorName, params, localInsts, recMap } else mkEqRefl rhs let thmValue ← mkLambdaFVars thmParams thmValue - trace[Meta.sizeOf] "sizeOf spec theorem: {thmName}" + trace[Meta.sizeOf] "sizeOf spec theorem name: {thmName}" + trace[Meta.sizeOf] "sizeOf spec theorem type: {thmType}" + trace[Meta.sizeOf] "sizeOf spec theorem value: {thmValue}" + unless (← isDefEq (← inferType thmValue) thmType) do + throwError "type mismatch" addDecl <| Declaration.thmDecl { name := thmName levelParams := ctorInfo.levelParams @@ -470,26 +477,28 @@ def mkSizeOfInstances (typeName : Name) : MetaM Unit := do let indInfo ← getConstInfoInduct indTypeName forallTelescopeReducing indInfo.type fun xs _ => let params := xs[:indInfo.numParams] - let indices := xs[indInfo.numParams:] - mkLocalInstances params fun localInsts => do - let us := indInfo.levelParams.map mkLevelParam - let indType := mkAppN (mkConst indTypeName us) xs - let sizeOfIndType ← mkAppM ``SizeOf #[indType] - withLocalDeclD `m indType fun m => do - let v ← mkLambdaFVars #[m] <| mkAppN (mkConst fn us) (params ++ localInsts ++ indices ++ #[m]) - let sizeOfMk ← mkAppM ``SizeOf.mk #[v] - let instDeclName := indTypeName ++ `_sizeOf_inst - let instDeclType ← mkForallFVars (xs ++ localInsts) sizeOfIndType - let instDeclValue ← mkLambdaFVars (xs ++ localInsts) sizeOfMk - addDecl <| Declaration.defnDecl { - name := instDeclName - levelParams := indInfo.levelParams - type := instDeclType - value := instDeclValue - safety := DefinitionSafety.safe - hints := ReducibilityHints.abbrev - } - addInstance instDeclName AttributeKind.global (eval_prio default) + withInstImplicitAsImplict params do + let indices := xs[indInfo.numParams:] + mkLocalInstances params fun localInsts => do + let us := indInfo.levelParams.map mkLevelParam + let indType := mkAppN (mkConst indTypeName us) xs + let sizeOfIndType ← mkAppM ``SizeOf #[indType] + withLocalDeclD `m indType fun m => do + let v ← mkLambdaFVars #[m] <| mkAppN (mkConst fn us) (params ++ localInsts ++ indices ++ #[m]) + let sizeOfMk ← mkAppM ``SizeOf.mk #[v] + let instDeclName := indTypeName ++ `_sizeOf_inst + let instDeclType ← mkForallFVars (xs ++ localInsts) sizeOfIndType + let instDeclValue ← mkLambdaFVars (xs ++ localInsts) sizeOfMk + trace[Meta.sizeOf] ">> {instDeclName} : {instDeclType}" + addDecl <| Declaration.defnDecl { + name := instDeclName + levelParams := indInfo.levelParams + type := instDeclType + value := instDeclValue + safety := .safe + hints := .abbrev + } + addInstance instDeclName AttributeKind.global (eval_prio default) if genSizeOfSpec.get (← getOptions) then mkSizeOfSpecTheorems indInfo.all.toArray fns recMap diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out index a0b68cb6e0..e21a3174d4 100644 --- a/tests/lean/infoTree.lean.expected.out +++ b/tests/lean/infoTree.lean.expected.out @@ -405,85 +405,85 @@ infoTree.lean:44:0: error: expected stx Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent [.] `Nat : some Sort.{?_uniq} @ ⟨45, 14⟩-⟨45, 17⟩ Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ - _uniq.1182 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ + _uniq.1209 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent [.] `Nat : some Sort.{?_uniq} @ ⟨45, 14⟩-⟨45, 17⟩ Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ - _uniq.1184 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ - Eq.{1} Nat _uniq.1182 _uniq.1182 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2» + _uniq.1211 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ + Eq.{1} Nat _uniq.1209 _uniq.1209 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2» Macro expansion («term_=_» `x "=" `x) ===> (Term.binrel "binrel%" `Eq._@.infoTree._hyg.182 `x `x) - Eq.{1} Nat _uniq.1182 _uniq.1182 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.BinOp.elabBinRel + Eq.{1} Nat _uniq.1209 _uniq.1209 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.BinOp.elabBinRel [.] `Eq._@.infoTree._hyg.182 : none @ ⟨45, 21⟩†-⟨45, 26⟩† - _uniq.1182 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent + _uniq.1209 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent [.] `x : none @ ⟨45, 21⟩-⟨45, 22⟩ - _uniq.1182 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ - _uniq.1182 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent + _uniq.1209 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ + _uniq.1209 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent [.] `x : none @ ⟨45, 25⟩-⟨45, 26⟩ - _uniq.1182 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ - _uniq.1188 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩ - _uniq.1189 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ - _uniq.1190 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ - (fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.1189 _uniq.1190]) f6.f7 : Eq.{1} Nat _uniq.1189 _uniq.1189 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec + _uniq.1209 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ + _uniq.1215 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩ + _uniq.1216 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ + _uniq.1217 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ + (fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.1216 _uniq.1217]) f6.f7 : Eq.{1} Nat _uniq.1216 _uniq.1216 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent [.] `Nat : some Sort.{?_uniq} @ ⟨46, 20⟩-⟨46, 23⟩ Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ - _uniq.1192 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ + _uniq.1219 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent [.] `Nat : some Sort.{?_uniq} @ ⟨46, 20⟩-⟨46, 23⟩ Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ - _uniq.1194 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ - Eq.{1} Nat _uniq.1192 _uniq.1192 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2» + _uniq.1221 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ + Eq.{1} Nat _uniq.1219 _uniq.1219 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2» Macro expansion («term_=_» `x "=" `x) ===> (Term.binrel "binrel%" `Eq._@.infoTree._hyg.190 `x `x) - Eq.{1} Nat _uniq.1192 _uniq.1192 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.BinOp.elabBinRel + Eq.{1} Nat _uniq.1219 _uniq.1219 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.BinOp.elabBinRel [.] `Eq._@.infoTree._hyg.190 : none @ ⟨46, 27⟩†-⟨46, 32⟩† - _uniq.1192 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent + _uniq.1219 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent [.] `x : none @ ⟨46, 27⟩-⟨46, 28⟩ - _uniq.1192 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ - _uniq.1192 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent + _uniq.1219 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ + _uniq.1219 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent [.] `x : none @ ⟨46, 31⟩-⟨46, 32⟩ - _uniq.1192 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ - _uniq.1199 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩ - _uniq.1200 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ - _uniq.1201 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ - Eq.refl.{1} Nat _uniq.1200 : Eq.{1} Nat _uniq.1200 _uniq.1200 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp - [.] `Eq.refl : some Eq.{?_uniq} Nat _uniq.1200 _uniq.1200 @ ⟨46, 36⟩-⟨46, 43⟩ + _uniq.1219 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ + _uniq.1226 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩ + _uniq.1227 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ + _uniq.1228 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ + Eq.refl.{1} Nat _uniq.1227 : Eq.{1} Nat _uniq.1227 _uniq.1227 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp + [.] `Eq.refl : some Eq.{?_uniq} Nat _uniq.1227 _uniq.1227 @ ⟨46, 36⟩-⟨46, 43⟩ Eq.refl.{1} : forall {α : Type} (a : α), Eq.{1} α a a @ ⟨46, 36⟩-⟨46, 43⟩ - _uniq.1200 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent + _uniq.1227 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent [.] `x : some ?_uniq @ ⟨46, 44⟩-⟨46, 45⟩ - _uniq.1200 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ - [mdata _recApp: _uniq.1199 _uniq.1189 _uniq.1190] : Eq.{1} Nat _uniq.1189 _uniq.1189 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp - [.] `f7 : some Eq.{1} Nat _uniq.1189 _uniq.1189 @ ⟨47, 2⟩-⟨47, 4⟩ - _uniq.1199 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩ - _uniq.1189 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent + _uniq.1227 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ + [mdata _recApp: _uniq.1226 _uniq.1216 _uniq.1217] : Eq.{1} Nat _uniq.1216 _uniq.1216 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp + [.] `f7 : some Eq.{1} Nat _uniq.1216 _uniq.1216 @ ⟨47, 2⟩-⟨47, 4⟩ + _uniq.1226 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩ + _uniq.1216 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent [.] `x : some Nat @ ⟨47, 5⟩-⟨47, 6⟩ - _uniq.1189 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ - _uniq.1190 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent + _uniq.1216 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ + _uniq.1217 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent [.] `y : some Nat @ ⟨47, 7⟩-⟨47, 8⟩ - _uniq.1190 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ + _uniq.1217 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ f6.f7 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩ f6 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩ [Elab.info] command @ ⟨50, 0⟩-⟨50, 32⟩ @ Lean.Elab.Command.elabDeclaration B : Type @ ⟨50, 12⟩-⟨50, 13⟩ @ Lean.Elab.Term.elabIdent [.] `B : some Sort.{?_uniq} @ ⟨50, 12⟩-⟨50, 13⟩ B : Type @ ⟨50, 12⟩-⟨50, 13⟩ - _uniq.1224 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ + _uniq.1251 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ B : Type @ ⟨50, 17⟩-⟨50, 18⟩ @ Lean.Elab.Term.elabIdent [.] `B : some Sort.{?_uniq} @ ⟨50, 17⟩-⟨50, 18⟩ B : Type @ ⟨50, 17⟩-⟨50, 18⟩ - _uniq.1226 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩ - _uniq.1227 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ - B.mk (B.pair _uniq.1227) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst - _uniq.1227 : B @ ⟨50, 24⟩-⟨50, 25⟩ - B.pair _uniq.1227 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj + _uniq.1253 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩ + _uniq.1254 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ + B.mk (B.pair _uniq.1254) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst + _uniq.1254 : B @ ⟨50, 24⟩-⟨50, 25⟩ + B.pair _uniq.1254 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj [.] `b : some Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩ - _uniq.1227 : B @ ⟨50, 24⟩-⟨50, 25⟩ - [.] _uniq.1227 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A + _uniq.1254 : B @ ⟨50, 24⟩-⟨50, 25⟩ + [.] _uniq.1254 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A B.pair : B -> (Prod.{0 0} A A) @ ⟨50, 24⟩†-⟨50, 25⟩† - pair : Prod.{0 0} A A := B.pair _uniq.1227 @ ⟨50, 22⟩†-⟨50, 32⟩ + pair : Prod.{0 0} A A := B.pair _uniq.1254 @ ⟨50, 22⟩†-⟨50, 32⟩ f7 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩ diff --git a/tests/lean/jason1.lean.expected.out b/tests/lean/jason1.lean.expected.out index 9242c670a8..6fbc287391 100644 --- a/tests/lean/jason1.lean.expected.out +++ b/tests/lean/jason1.lean.expected.out @@ -1,3 +1,17 @@ +jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument + @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝) +context: +G T Tm : Type +EG : G → G → Type +ET : T → T → Type +ETm : Tm → Tm → Type +EGrfl : {Γ : G} → EG Γ Γ +getCtx : T → G +getTy : Tm → T +GAlgebra : CtxSyntaxLayer G T EG getCtx → G +TAlgebra : TySyntaxLayer G T EG getCtx → T +Γ✝ : G +⊢ G jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝) context: @@ -30,38 +44,6 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G TAlgebra : TySyntaxLayer G T EG getCtx → T Γ✝ : G ⊢ G -jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument - @EGrfl - (getCtx - (TAlgebra - (@TySyntaxLayer.nat G T EG getCtx - (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))) -context: -G T Tm : Type -EG : G → G → Type -ET : T → T → Type -ETm : Tm → Tm → Type -EGrfl : {Γ : G} → EG Γ Γ -getCtx : T → G -getTy : Tm → T -GAlgebra : CtxSyntaxLayer G T EG getCtx → G -TAlgebra : TySyntaxLayer G T EG getCtx → T -Γ✝ : G -⊢ G -jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument - @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝) -context: -G T Tm : Type -EG : G → G → Type -ET : T → T → Type -ETm : Tm → Tm → Type -EGrfl : {Γ : G} → EG Γ Γ -getCtx : T → G -getTy : Tm → T -GAlgebra : CtxSyntaxLayer G T EG getCtx → G -TAlgebra : TySyntaxLayer G T EG getCtx → T -Γ✝ : G -⊢ G jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument @TySyntaxLayer.arrow G T EG getCtx (getCtx @@ -94,7 +76,7 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G TAlgebra : TySyntaxLayer G T EG getCtx → T Γ✝ : G ⊢ G -jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument +jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝) context: G T Tm : Type @@ -108,6 +90,24 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G TAlgebra : TySyntaxLayer G T EG getCtx → T Γ✝ : G ⊢ G +jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument + @EGrfl + (getCtx + (TAlgebra + (@TySyntaxLayer.nat G T EG getCtx + (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))) +context: +G T Tm : Type +EG : G → G → Type +ET : T → T → Type +ETm : Tm → Tm → Type +EGrfl : {Γ : G} → EG Γ Γ +getCtx : T → G +getTy : Tm → T +GAlgebra : CtxSyntaxLayer G T EG getCtx → G +TAlgebra : TySyntaxLayer G T EG getCtx → T +Γ✝ : G +⊢ G jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument @TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝) context: diff --git a/tests/lean/run/1373.lean b/tests/lean/run/1373.lean new file mode 100644 index 0000000000..a7dfa866bb --- /dev/null +++ b/tests/lean/run/1373.lean @@ -0,0 +1,4 @@ +class Foo (d: Nat) + +inductive Bar [i: ∀ d', d ≤ d' → Foo d'] + | mk: Bar (i:=i) diff --git a/tests/lean/syntheticHolesAsPatterns.lean.expected.out b/tests/lean/syntheticHolesAsPatterns.lean.expected.out index 6f87351734..627be6e06d 100644 --- a/tests/lean/syntheticHolesAsPatterns.lean.expected.out +++ b/tests/lean/syntheticHolesAsPatterns.lean.expected.out @@ -1,3 +1,10 @@ +syntheticHolesAsPatterns.lean:8:30-8:31: error: don't know how to synthesize placeholder +context: +α β : Type +a✝ : α +x : Fam2 α β +a n : Nat +⊢ Nat syntheticHolesAsPatterns.lean:7:30-7:31: error: don't know how to synthesize placeholder context: α✝ β : Type @@ -6,19 +13,6 @@ x : Fam2 α✝ β α : Type a : α ⊢ α -syntheticHolesAsPatterns.lean:8:30-8:31: error: don't know how to synthesize placeholder -context: -α β : Type -a✝ : α -x : Fam2 α β -a n : Nat -⊢ Nat -syntheticHolesAsPatterns.lean:13:18-13:19: error: don't know how to synthesize placeholder -context: -α β : Type -x : Fam2 α β -n a : Nat -⊢ Nat syntheticHolesAsPatterns.lean:12:18-12:19: error: don't know how to synthesize placeholder context: α✝ β : Type @@ -26,3 +20,9 @@ x : Fam2 α✝ β α : Type a : α ⊢ α +syntheticHolesAsPatterns.lean:13:18-13:19: error: don't know how to synthesize placeholder +context: +α β : Type +x : Fam2 α β +n a : Nat +⊢ Nat