feat: `outParam` and coercions experiment
diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 708eece..a4cb4e5 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean
@@ -300,7 +300,10 @@ unless fTypeBody.hasLooseBVars do unless (← hasOptAutoParams fTypeBody) do trace[Elab.app.propagateExpectedType] "{expectedType} =?= {fTypeBody}" - if (← isDefEq expectedType fTypeBody) then + if (← isSyntheticMVar fTypeBody) then + trace[Elab.app.propagateExpectedType] "{fTypeBody} is sythethic, skipping propagation" + modify fun s => { s with propagateExpected := false } + else if (← isDefEq expectedType fTypeBody) then /- Note that we only set `propagateExpected := false` when propagation has succeeded. -/ modify fun s => { s with propagateExpected := false } @@ -326,9 +329,10 @@ match s.expectedType? with | none => pure () | some expectedType => - trace[Elab.app.finalize] "expected type: {expectedType}" - -- Try to propagate expected type. Ignore if types are not definitionally equal, caller must handle it. - discard <| isDefEq expectedType eType + unless (← isSyntheticMVar eType) do + -- Try to propagate expected type. Ignore if types are not definitionally equal, caller must handle it. + trace[Elab.app.finalize] "expected type: {expectedType}" + discard <| isDefEq expectedType eType synthesizeAppInstMVars return e @@ -353,12 +357,68 @@ let s ← get return !s.args.isEmpty || !s.namedArgs.isEmpty -/- Return true if the next argument at `args` is of the form `_` -/ +/- Return `true` if the next argument at `args` is of the form `_` -/ private def isNextArgHole : M Bool := do match (← get).args with | Arg.stx (Syntax.node _ ``Lean.Parser.Term.hole _) :: _ => pure true | _ => pure false +/-- + Return `true` if the next argument to be processed is the outparam of a local instance. + For example, suppose we have the class + ```lean + class Get (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) where + get (xs : Cont) (i : Idx) : Elem + ``` + And the current value of `fType` is + ``` + {Cont : Type u_1} → {Idx : Type u_2} → {Elem : Type u_3} → [self : Get Cont Idx Elem] → Cont → Idx → Elem + ``` + then the result returned by this method is `false` since `Cont` is not the output param of any local instance. + Now assume `fType` is + ``` + {Elem : Type u_3} → [self : Get Cont Idx Elem] → Cont → Idx → Elem + ``` + then, the method returns `true` because `Elem` is an output parameter for the local instance `[self : Get Cont Idx Elem]`. +-/ +private partial def isNextOutParamOfLocalInstance : M Bool := do + let type := (← get).fType.bindingBody! + if (← hasLocalInstaceWithOutParams type) then + let x := mkFVar (← mkFreshFVarId) + isOutParamOfLocalInstance x (type.instantiate1 x) + else + return false +where + /- (quick filter) Return true if `type` constains a binder `[C ...]` where `C` is a class containing outparams. -/ + hasLocalInstaceWithOutParams (type : Expr) : CoreM Bool := do + let .forallE _ d b c := type | return false + if c.binderInfo.isInstImplicit then + if let .const declName .. := d.getAppFn then + if hasOutParams (← getEnv) declName then + return true + hasLocalInstaceWithOutParams b + + isOutParamOfLocalInstance (x : Expr) (type : Expr) : MetaM Bool := do + let .forallE _ d b c := type | return false + if c.binderInfo.isInstImplicit then + if let .const declName .. := d.getAppFn then + if hasOutParams (← getEnv) declName then + let cType ← inferType d.getAppFn + if (← isOutParamOf x 0 d.getAppArgs cType) then + return true + isOutParamOfLocalInstance x b + + isOutParamOf (x : Expr) (i : Nat) (args : Array Expr) (cType : Expr) : MetaM Bool := do + if h : i < args.size then + match (← whnf cType) with + | .forallE _ d b _ => + let arg := args.get ⟨i, h⟩ + if arg == x && d.isOutParam then + return true + isOutParamOf x (i+1) args b + | _ => return false + else + return false mutual /- @@ -374,7 +434,10 @@ private partial def addImplicitArg (argName : Name) : M Expr := do let argType ← getArgExpectedType - let arg ← mkFreshExprMVar argType + let arg ← if (← isNextOutParamOfLocalInstance) then + mkFreshExprMVar argType .synthetic + else + mkFreshExprMVar argType modify fun s => { s with toSetErrorCtx := s.toSetErrorCtx.push arg.mvarId! } addNewArg argName arg main
diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean index 6d5e881..029cec8 100644 --- a/src/Lean/Elab/Extra.lean +++ b/src/Lean/Elab/Extra.lean
@@ -292,11 +292,11 @@ trace[Elab.binop] "hasUncomparable: {r.hasUncomparable}, maxType: {r.max?}" if r.hasUncomparable || r.max?.isNone then let result ← toExpr tree - ensureHasType expectedType? result + ensureHasType expectedType? result (coeAtSyntheticMVar := false) else let result ← toExpr (← applyCoe tree r.max?.get!) trace[Elab.binop] "result: {result}" - ensureHasType expectedType? result + ensureHasType expectedType? result (coeAtSyntheticMVar := false) @[builtinTermElab binop_lazy] def elabBinOpLazy : TermElab := elabBinOp @@ -324,7 +324,7 @@ let lhs ← toBoolIfNecessary lhs let rhs ← toBoolIfNecessary rhs let lhsType ← inferType lhs - let rhs ← ensureHasType lhsType rhs + let rhs ← ensureHasType lhsType rhs (coeAtSyntheticMVar := false) elabAppArgs f #[] #[Arg.expr lhs, Arg.expr rhs] expectedType? (explicit := false) (ellipsis := false) else let mut maxType := r.max?.get! @@ -342,7 +342,7 @@ if noProp then -- We use `withNewMCtxDepth` to make sure metavariables are not assigned if (← withNewMCtxDepth <| isDefEq (← inferType e) (mkSort levelZero)) then - return (← ensureHasType (Lean.mkConst ``Bool) e) + return (← ensureHasType (Lean.mkConst ``Bool) e (coeAtSyntheticMVar := false)) return e @[builtinTermElab binrel] def elabBinRel : TermElab := elabBinRelCore false @@ -404,7 +404,7 @@ throwErrorAt stepStxs[i]! "invalid 'calc' step, step result is not a relation{indentExpr resultType}" | _ => throwErrorAt stepStxs[i]! "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}" pure () - ensureHasType expectedType? result + ensureHasType expectedType? result (coeAtSyntheticMVar := false) @[builtinTermElab defaultOrOfNonempty] def elabDefaultOrNonempty : TermElab := fun stx expectedType? => do
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index e127133..e8540d8 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -71,10 +71,14 @@ If `mvar` can be synthesized, then assign `auxMVarId := (expandCoe eNew)`. -/ private def synthesizePendingCoeInstMVar - (auxMVarId : MVarId) (errorMsgHeader? : Option String) (eNew : Expr) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr) : TermElabM Bool := do + (auxMVarId : MVarId) (errorMsgHeader? : Option String) (eNew : Expr) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr) (postponeOnSyntheticCoe : Bool) : TermElabM Bool := do let instMVarId := eNew.appArg!.mvarId! withMVarContext instMVarId do - if (← isDefEq expectedType eType) then + let eType ← instantiateMVars eType + if postponeOnSyntheticCoe then + if (← isSyntheticMVar eType) then + return false + if (← withDefault (isDefEq expectedType eType)) then /- This case may seem counterintuitive since we created the coercion because the `isDefEq expectedType eType` test failed before. However, it may succeed here because we have more information, for example, metavariables @@ -312,11 +316,11 @@ reportUnsolvedGoals remainingGoals /-- Try to synthesize the given pending synthetic metavariable. -/ - private partial def synthesizeSyntheticMVar (mvarSyntheticDecl : SyntheticMVarDecl) (postponeOnError : Bool) (runTactics : Bool) : TermElabM Bool := + private partial def synthesizeSyntheticMVar (mvarSyntheticDecl : SyntheticMVarDecl) (postponeOnError : Bool) (runTactics : Bool) (postponeOnSyntheticCoe : Bool) : TermElabM Bool := withRef mvarSyntheticDecl.stx do match mvarSyntheticDecl.kind with | SyntheticMVarKind.typeClass => synthesizePendingInstMVar mvarSyntheticDecl.mvarId - | SyntheticMVarKind.coe header? eNew expectedType eType e f? => synthesizePendingCoeInstMVar mvarSyntheticDecl.mvarId header? eNew expectedType eType e f? + | SyntheticMVarKind.coe header? eNew expectedType eType e f? => synthesizePendingCoeInstMVar mvarSyntheticDecl.mvarId header? eNew expectedType eType e f? (postponeOnSyntheticCoe := postponeOnSyntheticCoe) -- NOTE: actual processing at `synthesizeSyntheticMVarsAux` | SyntheticMVarKind.postponed savedContext => resumePostponed savedContext mvarSyntheticDecl.stx mvarSyntheticDecl.mvarId postponeOnError | SyntheticMVarKind.tactic tacticCode savedContext => @@ -329,7 +333,7 @@ /-- Try to synthesize the current list of pending synthetic metavariables. Return `true` if at least one of them was synthesized. -/ - private partial def synthesizeSyntheticMVarsStep (postponeOnError : Bool) (runTactics : Bool) : TermElabM Bool := do + private partial def synthesizeSyntheticMVarsStep (postponeOnError : Bool) (runTactics : Bool) (postponeOnSyntheticCoe : Bool) : TermElabM Bool := do let ctx ← read traceAtCmdPos `Elab.resuming fun _ => m!"resuming synthetic metavariables, mayPostpone: {ctx.mayPostpone}, postponeOnError: {postponeOnError}" @@ -343,7 +347,7 @@ let remainingSyntheticMVars ← syntheticMVars.filterRevM fun mvarDecl => do -- We use `traceM` because we want to make sure the metavar local context is used to trace the message traceM `Elab.postpone (withMVarContext mvarDecl.mvarId do addMessageContext m!"resuming {mkMVar mvarDecl.mvarId}") - let succeeded ← synthesizeSyntheticMVar mvarDecl postponeOnError runTactics + let succeeded ← synthesizeSyntheticMVar mvarDecl postponeOnError runTactics postponeOnSyntheticCoe trace[Elab.postpone] if succeeded then format "succeeded" else format "not ready yet" pure !succeeded -- Merge new synthetic metavariables with `remainingSyntheticMVars`, i.e., metavariables that still couldn't be synthesized @@ -367,7 +371,7 @@ let rec loop (_ : Unit) : TermElabM Unit := do withRef (← getSomeSynthethicMVarsRef) <| withIncRecDepth do unless (← get).syntheticMVars.isEmpty do - if ← synthesizeSyntheticMVarsStep (postponeOnError := false) (runTactics := false) then + if ← synthesizeSyntheticMVarsStep (postponeOnError := false) (runTactics := false) (postponeOnSyntheticCoe := true) then loop () else if !mayPostpone then /- Resume pending metavariables with "elaboration postponement" disabled. @@ -386,13 +390,13 @@ We the type of `x` may learn later its type and it may contain implicit and/or auto arguments. By disabling postponement, we are essentially giving up the opportunity of learning `x`s type and assume it does not have implict and/or auto arguments. -/ - if ← withoutPostponing <| synthesizeSyntheticMVarsStep (postponeOnError := true) (runTactics := false) then + if ← withoutPostponing <| synthesizeSyntheticMVarsStep (postponeOnError := true) (runTactics := false) (postponeOnSyntheticCoe := true) then loop () else if ← synthesizeUsingDefault then loop () - else if ← withoutPostponing <| synthesizeSyntheticMVarsStep (postponeOnError := false) (runTactics := false) then + else if ← withoutPostponing <| synthesizeSyntheticMVarsStep (postponeOnError := false) (runTactics := false) (postponeOnSyntheticCoe := false) then loop () - else if ← synthesizeSyntheticMVarsStep (postponeOnError := false) (runTactics := true) then + else if ← synthesizeSyntheticMVarsStep (postponeOnError := false) (runTactics := true) (postponeOnSyntheticCoe := true) then loop () else reportStuckSyntheticMVars ignoreStuckTC
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index d8b57fb..d3dafb0 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean
@@ -949,10 +949,14 @@ Argument `f?` is used only for generating error messages. -/ def ensureHasTypeAux (expectedType? : Option Expr) (eType : Expr) (e : Expr) - (f? : Option Expr := none) (errorMsgHeader? : Option String := none) : TermElabM Expr := do + (f? : Option Expr := none) (errorMsgHeader? : Option String := none) (coeAtSyntheticMVar : Bool := true) : TermElabM Expr := do match expectedType? with | none => return e | some expectedType => + if coeAtSyntheticMVar then + if (← isSyntheticMVar eType) && !(← read).inPattern && (← getEnv).contains ``Lean.Internal.coeM then + if !e.isAppOf ``OfNat.ofNat then + return (← mkCoe expectedType eType e f? errorMsgHeader?) if (← isDefEq eType expectedType) then return e else @@ -961,12 +965,12 @@ /-- If `expectedType?` is `some t`, then ensure `t` and type of `e` are definitionally equal. If they are not, then try coercions. -/ -def ensureHasType (expectedType? : Option Expr) (e : Expr) (errorMsgHeader? : Option String := none) : TermElabM Expr := +def ensureHasType (expectedType? : Option Expr) (e : Expr) (errorMsgHeader? : Option String := none) (coeAtSyntheticMVar : Bool := true) : TermElabM Expr := match expectedType? with | none => return e | _ => do let eType ← inferType e - ensureHasTypeAux expectedType? eType e none errorMsgHeader? + ensureHasTypeAux expectedType? eType e none errorMsgHeader? coeAtSyntheticMVar /-- Create a synthetic sorry for the given expected type. If `expectedType? = none`, then a fresh
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 2bc154b..43e970f 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean
@@ -496,6 +496,16 @@ | some d => pure d | none => throwError "unknown metavariable '?{mvarId.name}'" +def getMVarDeclKind (mvarId : MVarId) : MetaM MetavarKind := + return (← getMVarDecl mvarId).kind + +/-- Reture `true` if `e` is a synthetic (or synthetic opaque) metavariable -/ +def isSyntheticMVar (e : Expr) : MetaM Bool := do + if e.isMVar then + return (← getMVarDeclKind e.mvarId!) matches .synthetic | .syntheticOpaque + else + return false + def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : MetaM Unit := modifyMCtx fun mctx => mctx.setMVarKind mvarId kind
diff --git a/tests/lean/run/coeOutParamIssue.lean b/tests/lean/run/coeOutParamIssue.lean new file mode 100644 index 0000000..e63f64e --- /dev/null +++ b/tests/lean/run/coeOutParamIssue.lean
@@ -0,0 +1,22 @@ +namespace Ex + +class Get (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) where + get (xs : Cont) (i : Idx) : Elem + +export Get (get) + +instance [Inhabited α] : Get (Array α) Nat α where + get xs i := xs.get! i + +instance : Coe Bool Nat where + coe b := if b then 1 else 0 + +def g (as : Array (Array Bool)) : Nat := + let bs := get as 0 + get bs 1 + +def h (as : Array (Array Bool)) (i : Nat) : Nat := + let bs := get as i + f (get bs i) + +end Ex