max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: convert inductive type instance implicit parameters to implicit when building SizeOf instance

Browse source 
It is better for TC resolution since the parameter can be inferred by
typing constraints, and it addresses issue #1373
This commit is contained in:
Leonardo de Moura 2022-07-26 12:37:04 -07:00
parent 642b30ab47
commit e68e448070
5 changed files with 140 additions and 127 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

85
src/Lean/Meta/SizeOf.lean
View file

@ -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

86
tests/lean/infoTree.lean.expected.out
View file

@ -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⟩

66
tests/lean/jason1.lean.expected.out
View file

@ -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:

4
tests/lean/run/1373.lean Normal file
View file

@ -0,0 +1,4 @@
class Foo (d: Nat)
inductive Bar [i: ∀ d', d ≤ d' → Foo d']
| mk: Bar (i:=i)

26
tests/lean/syntheticHolesAsPatterns.lean.expected.out
View file

@ -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