fix: fixes #1907

src/Lean/Elab/Structure.lean

@@ -740,16 +740,31 @@ private def addDefaults (lctx : LocalContext) (defaultAuxDecls : Array (Name ×
       discard <| mkAuxDefinition declName type value (zeta := true)
       setReducibleAttribute declName
 
+/--
+Given `type` of the form `forall ... (source : A), B`, return `forall ... [source : A], B`.
+-/
+private def setSourceInstImplicit (type : Expr) : Expr :=
+  match type with
+  | .forallE _ d b _ =>
+    if b.isForall then
+      type.updateForallE! d (setSourceInstImplicit b)
+    else
+      type.updateForall! .instImplicit d b
+  | _ => unreachable!
+
 private partial def mkCoercionToCopiedParent (levelParams : List Name) (params : Array Expr) (view : StructView) (parentType : Expr) : MetaM Unit := do
   let env ← getEnv
   let structName := view.declName
   let sourceFieldNames := getStructureFieldsFlattened env structName
   let structType := mkAppN (Lean.mkConst structName (levelParams.map mkLevelParam)) params
   let Expr.const parentStructName _ ← pure parentType.getAppFn | unreachable!
   let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default
-  withLocalDecl `self binfo structType fun source => do
-    let declType ← instantiateMVars (← mkForallFVars params (← mkForallFVars #[source] parentType))
-    let declType := declType.inferImplicit params.size true
+  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
     let rec copyFields (parentType : Expr) : MetaM Expr := do
       let Expr.const parentStructName us ← pure parentType.getAppFn | unreachable!
       let parentCtor := getStructureCtor env parentStructName
@@ -772,7 +787,7 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
     addAndCompile <| Declaration.defnDecl {
       name        := declName
       levelParams := levelParams
-      type        := mkOutParamArgsImplicit declType
+      type        := declType
       value       := declVal
       hints       := ReducibilityHints.abbrev
       safety      := if view.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe

tests/lean/diamond4.lean.expected.out

@@ -1,4 +1,4 @@
 def D.toB : {α : Type} → [self : D α] → B α :=
 fun (α : Type) [self : D α] => self.1
 def D.toC : {α : Type} → [self : D α] → C α :=
-fun (α : Type) [self : D α] => @C.mk α (@B.toA α (@D.toB α self)) (@D.mul α self)
+fun (α : Type) (self : D α) => @C.mk α (@B.toA α (@D.toB α self)) (@D.mul α self)

tests/lean/diamond6.lean.expected.out

@@ -18,7 +18,7 @@
                 (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b a)) →
             FooAC α
 def FooAC.toFooAssoc : {α : Type} → [self : FooAC α] → FooAssoc α :=
-fun (α : Type) [self : FooAC α] =>
+fun (α : Type) (self : FooAC α) =>
   @FooAssoc.mk α (@FooComm.toFoo α (@FooAC.toFooComm α self)) (@FooAC.toMul α self) (@FooAC.add_assoc α self)
     (@FooAC.mul_assoc α self)
 @FooAC'.mk : {α : Type} →
@@ -42,7 +42,7 @@ fun (α : Type) [self : FooAC α] =>
                   (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b a)) →
               FooAC' α
 def FooAC'.toFooAssoc' : {α : Type} → [self : FooAC' α] → FooAssoc' α :=
-fun (α : Type) [self : FooAC' α] =>
+fun (α : Type) (self : FooAC' α) =>
   @FooAssoc'.mk α
     (@FooAssoc.mk α (@FooComm.toFoo α (@FooAC'.toFooComm α self)) (@FooAC'.toMul α self) (@FooAC'.add_assoc α self)
       (@FooAC'.mul_assoc α self))

tests/lean/diamond7.lean.expected.out

@@ -8,7 +8,7 @@
             (@instHMul.{u_1} α (@Semigroup.toMul.{u_1} α (@Monoid.toSemigroup.{u_1} α toMonoid))) b a)) →
       CommMonoid.{u_1} α
 def CommMonoid.toCommSemigroup.{u} : {α : Type u} → [self : CommMonoid.{u} α] → CommSemigroup.{u} α :=
-fun (α : Type u) [self : CommMonoid.{u} α] =>
+fun (α : Type u) (self : CommMonoid.{u} α) =>
   @CommSemigroup.mk.{u} α (@Monoid.toSemigroup.{u} α (@CommMonoid.toMonoid.{u} α self))
     (@CommMonoid.mul_comm.{u} α self)
 @CommGroup.mk.{u_1} : {α : Type u_1} →
@@ -25,11 +25,11 @@ fun (α : Type u) [self : CommMonoid.{u} α] =>
             b a)) →
       CommGroup.{u_1} α
 def CommGroup.toCommMonoid.{u} : {α : Type u} → [self : CommGroup.{u} α] → CommMonoid.{u} α :=
-fun (α : Type u) [self : CommGroup.{u} α] =>
+fun (α : Type u) (self : CommGroup.{u} α) =>
   @CommMonoid.mk.{u} α (@Group.toMonoid.{u} α (@CommGroup.toGroup.{u} α self)) (@CommGroup.mul_comm.{u} α self)
 @Field.mk : {α : Type u_1} → [toDivisionRing : DivisionRing α] → (∀ (a b : α), a * b = b * a) → Field α
 def Field.toDivisionRing.{u} : {α : Type u} → [self : Field.{u} α] → DivisionRing.{u} α :=
 fun (α : Type u) [self : Field.{u} α] => self.1
 def Field.toCommRing.{u} : {α : Type u} → [self : Field.{u} α] → CommRing.{u} α :=
-fun (α : Type u) [self : Field.{u} α] =>
+fun (α : Type u) (self : Field.{u} α) =>
   @CommRing.mk.{u} α (@DivisionRing.toRing.{u} α (@Field.toDivisionRing.{u} α self)) (@Field.mul_comm.{u} α self)

tests/lean/run/1907.lean

@@ -0,0 +1,78 @@
+class One (α : Type u) where
+  one : α
+
+instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
+  ofNat := ‹One α›.1
+
+class MulOneClass (M : Type u) extends One M, Mul M
+
+class FunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where
+  coe : F → ∀ a : α, β a
+
+instance (priority := 100) [FunLike F α β] : CoeFun F fun _ => ∀ a : α, β a where coe := FunLike.coe
+
+section One
+
+variable [One M] [One N]
+
+structure OneHom (M : Type _) (N : Type _) [One M] [One N] where
+  toFun : M → N
+  map_one' : toFun 1 = 1
+
+class OneHomClass (F : Type _) (M N : outParam (Type _)) [One M] [One N]
+  extends FunLike F M fun _ => N where
+  map_one : ∀ f : F, f 1 = 1
+
+@[simp]
+theorem map_one [OneHomClass F M N] (f : F) : f 1 = 1 :=
+  OneHomClass.map_one f
+
+end One
+
+section Mul
+
+variable [Mul M] [Mul N]
+
+structure MulHom (M : Type _) (N : Type _) [Mul M] [Mul N] where
+  toFun : M → N
+  map_mul' : ∀ x y, toFun (x * y) = toFun x * toFun y
+
+infixr:25 " →ₙ* " => MulHom
+
+class MulHomClass (F : Type _) (M N : outParam (Type _)) [Mul M] [Mul N]
+  extends FunLike F M fun _ => N where
+  map_mul : ∀ (f : F) (x y : M), f (x * y) = f x * f y
+
+@[simp]
+theorem map_mul [MulHomClass F M N] (f : F) (x y : M) : f (x * y) = f x * f y :=
+  MulHomClass.map_mul f x y
+
+end Mul
+
+section mul_one
+
+variable [MulOneClass M] [MulOneClass N]
+
+structure MonoidHom (M : Type _) (N : Type _) [MulOneClass M] [MulOneClass N] extends
+  OneHom M N, M →ₙ* N
+
+infixr:25 " →* " => MonoidHom
+
+class MonoidHomClass (F : Type _) (M N : outParam (Type _)) [MulOneClass M] [MulOneClass N] extends MulHomClass F M N, OneHomClass F M N
+
+instance (F : Type _) (M N : outParam (Type _)) [MulOneClass M] [MulOneClass N] [MonoidHomClass F M N] : CoeTC F (M →* N) :=
+  ⟨fun f => {
+   toFun := f,
+   map_one' := map_one f,
+   map_mul' := map_mul f
+  }⟩
+
+-- Now we reverse the order of the parents in the extends clause:
+class MonoidHomClass' (F : Type _) (M N : outParam (Type _)) [MulOneClass M] [MulOneClass N] extends OneHomClass F M N, MulHomClass F M N
+
+instance [MonoidHomClass' F M N] : CoeTC F (M →* N) :=
+  ⟨fun f => {
+    toFun := f,
+    map_one' := map_one f,
+    map_mul' := map_mul f
+  }⟩

tests/lean/run/1907orig.lean

@@ -0,0 +1,72 @@
+class One (α : Type u) where
+  one : α
+
+instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
+  ofNat := ‹One α›.1
+
+class MulOneClass (M : Type u) extends One M, Mul M
+
+class FunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where
+  coe : F → ∀ a : α, β a
+
+instance (priority := 100) [FunLike F α β] : CoeFun F fun _ => ∀ a : α, β a where coe := FunLike.coe
+
+section One
+
+variable [One M] [One N]
+
+structure OneHom (M : Type _) (N : Type _) [One M] [One N] where
+  toFun : M → N
+  map_one' : toFun 1 = 1
+
+class OneHomClass (F : Type _) (M N : outParam (Type _)) [outParam (One M)] [outParam (One N)]
+  extends FunLike F M fun _ => N where
+  map_one : ∀ f : F, f 1 = 1
+
+@[simp]
+theorem map_one [OneHomClass F M N] (f : F) : f 1 = 1 :=
+  OneHomClass.map_one f
+
+end One
+
+section Mul
+
+variable [Mul M] [Mul N]
+
+structure MulHom (M : Type _) (N : Type _) [Mul M] [Mul N] where
+  toFun : M → N
+  map_mul' : ∀ x y, toFun (x * y) = toFun x * toFun y
+
+infixr:25 " →ₙ* " => MulHom
+
+class MulHomClass (F : Type _) (M N : outParam (Type _)) [outParam (Mul M)] [outParam (Mul N)]
+  extends FunLike F M fun _ => N where
+  map_mul : ∀ (f : F) (x y : M), f (x * y) = f x * f y
+
+@[simp]
+theorem map_mul [MulHomClass F M N] (f : F) (x y : M) : f (x * y) = f x * f y :=
+  MulHomClass.map_mul f x y
+
+end Mul
+
+section mul_one
+
+variable [MulOneClass M] [MulOneClass N]
+
+structure MonoidHom (M : Type _) (N : Type _) [MulOneClass M] [MulOneClass N] extends
+  OneHom M N, M →ₙ* N
+
+infixr:25 " →* " => MonoidHom
+
+class MonoidHomClass (F : Type _) (M N : outParam (Type _)) [outParam (MulOneClass M)]
+   [outParam (MulOneClass N)] extends MulHomClass F M N, OneHomClass F M N
+
+instance [MonoidHomClass F M N] : CoeTC F (M →* N) :=
+  ⟨fun f => { toFun := f, map_one' := map_one f, map_mul' := map_mul f }⟩
+
+-- Now we reverse the order of the parents in the extends clause:
+class MonoidHomClass' (F : Type _) (M N : outParam (Type _)) [outParam (MulOneClass M)]
+   [outParam (MulOneClass N)] extends OneHomClass F M N, MulHomClass F M N
+
+instance [MonoidHomClass' F M N] : CoeTC F (M →* N) :=
+  ⟨fun f => { toFun := f, map_one' := map_one f, map_mul' := map_mul f }⟩