diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 1773f0b349..6e59a4e013 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -65,7 +65,7 @@ instance : MonadRef CoreM where instance : MonadEnv CoreM where getEnv := return (← get).env - modifyEnv f := modify fun s => { s with env := f s.env } + modifyEnv f := modify fun s => { s with env := f s.env, cache := {} } instance : MonadOptions CoreM where getOptions := return (← read).options diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 4df35abacc..942d02c4b4 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -207,6 +207,10 @@ instance : MonadMCtx MetaM where getMCtx := return (← get).mctx modifyMCtx f := modify fun s => { s with mctx := f s.mctx } +instance : MonadEnv MetaM where + getEnv := return (← getThe Core.State).env + modifyEnv f := do modifyThe Core.State fun s => { s with env := f s.env, cache := {} }; modify fun s => { s with cache := {} } + instance : AddMessageContext MetaM where addMessageContext := addMessageContextFull diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out index 65bfdd689f..3b57ae4bc9 100644 --- a/tests/lean/1018unknowMVarIssue.lean.expected.out +++ b/tests/lean/1018unknowMVarIssue.lean.expected.out @@ -14,7 +14,7 @@ a : α α : Type @ ⟨7, 13⟩-⟨7, 14⟩ a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩ Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp - [.] `Fam2 : some Sort.{?_uniq.272} @ ⟨7, 21⟩-⟨7, 25⟩ + [.] `Fam2 : some Sort.{?_uniq.317} @ ⟨7, 21⟩-⟨7, 25⟩ Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩ α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @@ -45,7 +45,7 @@ a : α ?α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible ?α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole Fam2.any : Fam2 ?α ?α @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabApp - [.] `Fam2.any : some Fam2 ([mdata _inaccessible:1 ?_uniq.602]) ([mdata _inaccessible:1 ?_uniq.603]) @ ⟨9, 4⟩-⟨9, 12⟩ + [.] `Fam2.any : some Fam2 ([mdata _inaccessible:1 ?_uniq.647]) ([mdata _inaccessible:1 ?_uniq.648]) @ ⟨9, 4⟩-⟨9, 12⟩ @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩ ?α : Type @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabInaccessible ?α : Type @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabHole @@ -61,7 +61,7 @@ a : α Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩ @ Lean.Elab.Term.elabApp - [.] `Fam2.nat : some Fam2 ([mdata _inaccessible:1 ?_uniq.634]) ([mdata _inaccessible:1 ?_uniq.635]) @ ⟨10, 4⟩-⟨10, 12⟩ + [.] `Fam2.nat : some Fam2 ([mdata _inaccessible:1 ?_uniq.679]) ([mdata _inaccessible:1 ?_uniq.680]) @ ⟨10, 4⟩-⟨10, 12⟩ Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩ n : Nat @ ⟨10, 13⟩-⟨10, 14⟩ @ Lean.Elab.Term.elabIdent n : Nat @ ⟨10, 13⟩-⟨10, 14⟩ diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out index fd2709f924..147335e190 100644 --- a/tests/lean/infoTree.lean.expected.out +++ b/tests/lean/infoTree.lean.expected.out @@ -1,6 +1,6 @@ [Elab.info] command @ ⟨13, 0⟩-⟨15, 6⟩ @ Lean.Elab.Command.elabDeclaration Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.385} @ ⟨13, 11⟩-⟨13, 14⟩ + [.] `Nat : some Sort.{?_uniq.422} @ ⟨13, 11⟩-⟨13, 14⟩ Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩ x (isBinder := true) : Nat @ ⟨13, 7⟩-⟨13, 8⟩ Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩ @ «_aux_Init_Notation___macroRules_term_×__1» @@ -11,10 +11,10 @@ Nat × Nat : Type @ ⟨13, 18⟩†-⟨13, 27⟩ @ Lean.Elab.Term.elabApp Prod : Type → Type → Type @ ⟨13, 18⟩†-⟨13, 27⟩† Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.389} @ ⟨13, 18⟩-⟨13, 21⟩ + [.] `Nat : some Type.{?_uniq.426} @ ⟨13, 18⟩-⟨13, 21⟩ Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩ Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.388} @ ⟨13, 24⟩-⟨13, 27⟩ + [.] `Nat : some Type.{?_uniq.425} @ ⟨13, 24⟩-⟨13, 27⟩ Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩ x (isBinder := true) : Nat @ ⟨13, 7⟩-⟨13, 8⟩ let y := (x, x); @@ -41,16 +41,16 @@ [Elab.info] command @ ⟨17, 0⟩-⟨19, 8⟩ @ Lean.Elab.Command.elabDeclaration ∀ (x y : Nat), Bool → x + 0 = x : Prop @ ⟨17, 8⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabDepArrow Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.418} @ ⟨17, 15⟩-⟨17, 18⟩ + [.] `Nat : some Sort.{?_uniq.455} @ ⟨17, 15⟩-⟨17, 18⟩ Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ x (isBinder := true) : Nat @ ⟨17, 9⟩-⟨17, 10⟩ Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.420} @ ⟨17, 15⟩-⟨17, 18⟩ + [.] `Nat : some Sort.{?_uniq.457} @ ⟨17, 15⟩-⟨17, 18⟩ Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ y (isBinder := true) : Nat @ ⟨17, 11⟩-⟨17, 12⟩ Bool → x + 0 = x : Prop @ ⟨17, 22⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabDepArrow Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩ @ Lean.Elab.Term.elabIdent - [.] `Bool : some Sort.{?_uniq.423} @ ⟨17, 27⟩-⟨17, 31⟩ + [.] `Bool : some Sort.{?_uniq.460} @ ⟨17, 27⟩-⟨17, 31⟩ Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩ b (isBinder := true) : Bool @ ⟨17, 23⟩-⟨17, 24⟩ x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩ @ «_aux_Init_Notation___macroRules_term_=__2» @@ -112,20 +112,20 @@ [Elab.info] command @ ⟨21, 0⟩-⟨25, 10⟩ @ Lean.Elab.Command.elabDeclaration Nat → Nat → Bool → Nat : Type @ ⟨21, 9⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.542} @ ⟨21, 16⟩-⟨21, 19⟩ + [.] `Nat : some Sort.{?_uniq.579} @ ⟨21, 16⟩-⟨21, 19⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ x (isBinder := true) : Nat @ ⟨21, 10⟩-⟨21, 11⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.544} @ ⟨21, 16⟩-⟨21, 19⟩ + [.] `Nat : some Sort.{?_uniq.581} @ ⟨21, 16⟩-⟨21, 19⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ y (isBinder := true) : Nat @ ⟨21, 12⟩-⟨21, 13⟩ Bool → Nat : Type @ ⟨21, 23⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩ @ Lean.Elab.Term.elabIdent - [.] `Bool : some Sort.{?_uniq.547} @ ⟨21, 28⟩-⟨21, 32⟩ + [.] `Bool : some Sort.{?_uniq.584} @ ⟨21, 28⟩-⟨21, 32⟩ Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩ b (isBinder := true) : Bool @ ⟨21, 24⟩-⟨21, 25⟩ Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.549} @ ⟨21, 36⟩-⟨21, 39⟩ + [.] `Nat : some Sort.{?_uniq.586} @ ⟨21, 36⟩-⟨21, 39⟩ Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ fun x y b => let x := (x + y, x - y); @@ -238,10 +238,10 @@ Nat × Array (Array Nat) : Type @ ⟨27, 12⟩†-⟨27, 35⟩ @ Lean.Elab.Term.elabApp Prod : Type → Type → Type @ ⟨27, 12⟩†-⟨27, 35⟩† Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.763} @ ⟨27, 12⟩-⟨27, 15⟩ + [.] `Nat : some Type.{?_uniq.800} @ ⟨27, 12⟩-⟨27, 15⟩ Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩ Array (Array Nat) : Type @ ⟨27, 18⟩-⟨27, 35⟩ @ Lean.Elab.Term.elabApp - [.] `Array : some Type.{?_uniq.762} @ ⟨27, 18⟩-⟨27, 23⟩ + [.] `Array : some Type.{?_uniq.799} @ ⟨27, 18⟩-⟨27, 23⟩ Array : Type → Type @ ⟨27, 18⟩-⟨27, 23⟩ Array Nat : Type @ ⟨27, 24⟩-⟨27, 35⟩ @ Lean.Elab.Term.expandParen Macro expansion @@ -249,17 +249,17 @@ ===> Array Nat Array Nat : Type @ ⟨27, 25⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabApp - [.] `Array : some Type.{?_uniq.764} @ ⟨27, 25⟩-⟨27, 30⟩ + [.] `Array : some Type.{?_uniq.801} @ ⟨27, 25⟩-⟨27, 30⟩ Array : Type → Type @ ⟨27, 25⟩-⟨27, 30⟩ Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.765} @ ⟨27, 31⟩-⟨27, 34⟩ + [.] `Nat : some Type.{?_uniq.802} @ ⟨27, 31⟩-⟨27, 34⟩ Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩ s (isBinder := true) : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩ Array Nat : Type @ ⟨27, 39⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabApp - [.] `Array : some Sort.{?_uniq.767} @ ⟨27, 39⟩-⟨27, 44⟩ + [.] `Array : some Sort.{?_uniq.804} @ ⟨27, 39⟩-⟨27, 44⟩ Array : Type → Type @ ⟨27, 39⟩-⟨27, 44⟩ Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.768} @ ⟨27, 45⟩-⟨27, 48⟩ + [.] `Nat : some Type.{?_uniq.805} @ ⟨27, 45⟩-⟨27, 48⟩ Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ s (isBinder := true) : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩ Array.push (Array.getOp s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 17⟩ @ Lean.Elab.Term.elabApp @@ -275,11 +275,11 @@ f3 (isBinder := true) : Nat × Array (Array Nat) → Array Nat @ ⟨27, 4⟩-⟨27, 6⟩ [Elab.info] command @ ⟨30, 0⟩-⟨31, 20⟩ @ Lean.Elab.Command.elabDeclaration B : Type @ ⟨30, 14⟩-⟨30, 15⟩ @ Lean.Elab.Term.elabIdent - [.] `B : some Sort.{?_uniq.810} @ ⟨30, 14⟩-⟨30, 15⟩ + [.] `B : some Sort.{?_uniq.847} @ ⟨30, 14⟩-⟨30, 15⟩ B : Type @ ⟨30, 14⟩-⟨30, 15⟩ arg (isBinder := true) : B @ ⟨30, 8⟩-⟨30, 11⟩ Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.812} @ ⟨30, 19⟩-⟨30, 22⟩ + [.] `Nat : some Sort.{?_uniq.849} @ ⟨30, 19⟩-⟨30, 22⟩ Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ arg (isBinder := true) : B @ ⟨30, 8⟩-⟨30, 11⟩ A.val arg.pair.fst 0 : Nat @ ⟨31, 2⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabApp @@ -294,11 +294,11 @@ f4 (isBinder := true) : B → Nat @ ⟨30, 4⟩-⟨30, 6⟩ [Elab.info] command @ ⟨33, 0⟩-⟨35, 1⟩ @ Lean.Elab.Command.elabDeclaration Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.833} @ ⟨33, 12⟩-⟨33, 15⟩ + [.] `Nat : some Sort.{?_uniq.870} @ ⟨33, 12⟩-⟨33, 15⟩ Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩ x (isBinder := true) : Nat @ ⟨33, 8⟩-⟨33, 9⟩ B : Type @ ⟨33, 19⟩-⟨33, 20⟩ @ Lean.Elab.Term.elabIdent - [.] `B : some Sort.{?_uniq.835} @ ⟨33, 19⟩-⟨33, 20⟩ + [.] `B : some Sort.{?_uniq.872} @ ⟨33, 19⟩-⟨33, 20⟩ B : Type @ ⟨33, 19⟩-⟨33, 20⟩ x (isBinder := true) : Nat @ ⟨33, 8⟩-⟨33, 9⟩ { pair := ({ val := id }, { val := id }) } : B @ ⟨33, 24⟩-⟨35, 1⟩ @ Lean.Elab.Term.StructInst.elabStructInst @@ -338,73 +338,73 @@ infoTree.lean:44:0: error: expected stx [.] (Command.set_option "set_option" `pp.raw) @ ⟨44, 0⟩-⟨44, 17⟩ [Elab.info] command @ ⟨45, 0⟩-⟨47, 8⟩ @ Lean.Elab.Command.elabDeclaration Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.857} @ ⟨45, 14⟩-⟨45, 17⟩ + [.] `Nat : some Sort.{?_uniq.894} @ ⟨45, 14⟩-⟨45, 17⟩ Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ - _uniq.858 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ + _uniq.895 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.859} @ ⟨45, 14⟩-⟨45, 17⟩ + [.] `Nat : some Sort.{?_uniq.896} @ ⟨45, 14⟩-⟨45, 17⟩ Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ - _uniq.860 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ - Eq.{1} Nat _uniq.858 _uniq.858 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2» + _uniq.897 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ + Eq.{1} Nat _uniq.895 _uniq.895 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2» Macro expansion («term_=_» `x "=" `x) ===> (Term.binrel "binrel%" `Eq._@.infoTree._hyg.177 `x `x) - Eq.{1} Nat _uniq.858 _uniq.858 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.elabBinRel - _uniq.858 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent - _uniq.858 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ - _uniq.858 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent - _uniq.858 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ - _uniq.867 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ - _uniq.868 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ - (fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.867 _uniq.868]) f6.f7 : Eq.{1} Nat _uniq.867 _uniq.867 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec + Eq.{1} Nat _uniq.895 _uniq.895 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.elabBinRel + _uniq.895 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent + _uniq.895 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ + _uniq.895 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent + _uniq.895 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ + _uniq.904 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩ + _uniq.905 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩ + (fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.904 _uniq.905]) f6.f7 : Eq.{1} Nat _uniq.904 _uniq.904 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.869} @ ⟨46, 20⟩-⟨46, 23⟩ + [.] `Nat : some Sort.{?_uniq.906} @ ⟨46, 20⟩-⟨46, 23⟩ Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ - _uniq.870 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ + _uniq.907 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.871} @ ⟨46, 20⟩-⟨46, 23⟩ + [.] `Nat : some Sort.{?_uniq.908} @ ⟨46, 20⟩-⟨46, 23⟩ Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ - _uniq.872 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ - Eq.{1} Nat _uniq.870 _uniq.870 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2» + _uniq.909 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ + Eq.{1} Nat _uniq.907 _uniq.907 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2» Macro expansion («term_=_» `x "=" `x) ===> (Term.binrel "binrel%" `Eq._@.infoTree._hyg.185 `x `x) - Eq.{1} Nat _uniq.870 _uniq.870 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.elabBinRel - _uniq.870 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent - _uniq.870 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ - _uniq.870 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent - _uniq.870 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ - _uniq.877 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩ - _uniq.880 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ - _uniq.881 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ - Eq.refl.{1} Nat _uniq.880 : Eq.{1} Nat _uniq.880 _uniq.880 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp - [.] `Eq.refl : some Eq.{?_uniq.874} Nat _uniq.880 _uniq.880 @ ⟨46, 36⟩-⟨46, 43⟩ + Eq.{1} Nat _uniq.907 _uniq.907 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.elabBinRel + _uniq.907 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent + _uniq.907 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ + _uniq.907 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent + _uniq.907 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ + _uniq.914 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩ + _uniq.917 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩ + _uniq.918 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩ + Eq.refl.{1} Nat _uniq.917 : Eq.{1} Nat _uniq.917 _uniq.917 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp + [.] `Eq.refl : some Eq.{?_uniq.911} Nat _uniq.917 _uniq.917 @ ⟨46, 36⟩-⟨46, 43⟩ Eq.refl.{1} : forall {α : Type} (a : α), Eq.{1} α a a @ ⟨46, 36⟩-⟨46, 43⟩ - _uniq.880 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent - _uniq.880 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ - [mdata _recApp: _uniq.877 _uniq.867 _uniq.868] : Eq.{1} Nat _uniq.867 _uniq.867 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp - _uniq.877 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩ - _uniq.867 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent - _uniq.867 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ - _uniq.868 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent - _uniq.868 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ + _uniq.917 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent + _uniq.917 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ + [mdata _recApp: _uniq.914 _uniq.904 _uniq.905] : Eq.{1} Nat _uniq.904 _uniq.904 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp + _uniq.914 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩ + _uniq.904 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent + _uniq.904 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ + _uniq.905 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent + _uniq.905 : 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.905} @ ⟨50, 12⟩-⟨50, 13⟩ + [.] `B : some Sort.{?_uniq.942} @ ⟨50, 12⟩-⟨50, 13⟩ B : Type @ ⟨50, 12⟩-⟨50, 13⟩ - _uniq.906 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ + _uniq.943 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ B : Type @ ⟨50, 17⟩-⟨50, 18⟩ @ Lean.Elab.Term.elabIdent - [.] `B : some Sort.{?_uniq.907} @ ⟨50, 17⟩-⟨50, 18⟩ + [.] `B : some Sort.{?_uniq.944} @ ⟨50, 17⟩-⟨50, 18⟩ B : Type @ ⟨50, 17⟩-⟨50, 18⟩ - _uniq.910 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ - B.mk (B.pair _uniq.910) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst - B.pair _uniq.910 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj - _uniq.910 : B @ ⟨50, 24⟩-⟨50, 25⟩ - [.] _uniq.910 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A + _uniq.947 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩ + B.mk (B.pair _uniq.947) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst + B.pair _uniq.947 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj + _uniq.947 : B @ ⟨50, 24⟩-⟨50, 25⟩ + [.] _uniq.947 : 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.910 @ ⟨50, 22⟩†-⟨50, 32⟩ + pair : Prod.{0 0} A A := B.pair _uniq.947 @ ⟨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 ac1158f85d..d04baf0c58 100644 --- a/tests/lean/jason1.lean.expected.out +++ b/tests/lean/jason1.lean.expected.out @@ -1,3 +1,53 @@ +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 x✝¹ x✝) +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 +x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra +x✝ : G +⊢ G +jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument + @TySyntaxLayer.arrow G T EG getCtx + (getCtx + (TAlgebra + (@TySyntaxLayer.nat G T EG getCtx + (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))) + (TAlgebra + (@TySyntaxLayer.nat G T EG getCtx + (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))) + (TAlgebra + (@TySyntaxLayer.nat G T EG getCtx + (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))) + (@EGrfl + (getCtx + (TAlgebra + (@TySyntaxLayer.nat G T EG getCtx + (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))) + (@EGrfl + (getCtx + (TAlgebra + (@TySyntaxLayer.nat G T EG getCtx + (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))) +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 +x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra +x✝ : G +⊢ G 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 x✝¹ x✝) context: @@ -13,6 +63,21 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra x✝ : 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 x✝¹ x✝) +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 +x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra +x✝ : 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 x✝¹ x✝) context: @@ -66,68 +131,3 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra x✝ : 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 x✝¹ x✝) -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 -x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra -x✝ : G -⊢ G -jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument - @TySyntaxLayer.arrow G T EG getCtx - (getCtx - (TAlgebra - (@TySyntaxLayer.nat G T EG getCtx - (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)))) - (TAlgebra - (@TySyntaxLayer.nat G T EG getCtx - (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))) - (TAlgebra - (@TySyntaxLayer.nat G T EG getCtx - (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))) - (@EGrfl - (getCtx - (TAlgebra - (@TySyntaxLayer.nat G T EG getCtx - (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))) - (@EGrfl - (getCtx - (TAlgebra - (@TySyntaxLayer.nat G T EG getCtx - (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))) -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 -x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra -x✝ : 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 x✝¹ x✝) -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 -x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra -x✝ : G -⊢ G diff --git a/tests/lean/run/1051.lean b/tests/lean/run/1051.lean new file mode 100644 index 0000000000..51fa451dc6 --- /dev/null +++ b/tests/lean/run/1051.lean @@ -0,0 +1,26 @@ +inductive SF : Type u → Type u → Type (u+1) where +| seq {as bs cs: Type u}: SF as bs → SF bs cs → SF as cs +| fan {as bs cs: Type u}: SF as (bs × cs) + +inductive SF' (m: Type (u+1) → Type u)[Monad m]: Type u → Type u → Type (u+1) where +| seq {as bs cs: Type u}: SF' m as bs → SF' m bs cs → SF' m as cs +| fan {as bs cs: Type u}: SF' m as (bs × cs) +| rswitcher {as bs cs: Type u}: SF' m as (bs × cs) → SF' m as bs + +def SF.step [Monad m] (sa: as): SF as bs → SF' m as bs × bs +| seq sf₁ sf₂ => + let (sf₁', sb) := sf₁.step sa + let (sf₂', sc) := sf₂.step sb + (sf₁'.seq sf₂', sc) +| fan => sorry + +def SF'.step [Monad m] (sa: as): SF' m as bs → SF'.{u} m as bs × bs +| seq sf₁ sf₂ => + let (sf₁', sb) := sf₁.step sa + let (sf₂', sc) := sf₂.step sb + (sf₁'.seq sf₂', sc) +| fan => sorry +| rswitcher f => + let x := f.step sa + let (_, (sb, _)) := x + (rswitcher f, sb)