Missing coercions

[dselsam]

import Mathlib.Analysis.NormedSpace.HahnBanach
import Mathlib.PostPort

namespace Real.Playground

set_option synthInstance.maxHeartbeats 5000

universe u v w
variable {E : Type u} [instSNG : SemiNormedGroup E] [instSNS : SemiNormedSpace ℝ E]
variable (p : Subspace ℝ E)

-- Here is the Lean3 statement:
-- theorem exists_extension_norm_eq (p : subspace ℝ E) (f : p →L[ℝ] ℝ) :
--  ∃ g : E →L[ℝ] ℝ, (∀ x : p, g x = f x) ∧ ∥g∥ = ∥f∥ :=

-- This works:
#synth CoeSort (Subspace ℝ E) _

-- This works:
example (p : Subspace ℝ E) (f : { x : E // x ∈ p } →L[ℝ] ℝ) :
  ∃ g : E →L[ℝ] ℝ, (∀ x : { x : E // x∈p }, g x = f x) ∧ ∥g∥ = ∥f∥ := sorry

-- But we cannot leave out either of the `Subtype`s:
example (p : Subspace ℝ E) (f : p →L[ℝ] ℝ) :
  ∃ g : E →L[ℝ] ℝ, (∀ x : { x : E // x∈p }, g x = f x) ∧ ∥g∥ = ∥f∥ := sorry

/-
error: application type mismatch
  ContinuousLinearMap ℝ p
argument
  p
has type
  Subspace ℝ E : Type u
but is expected to have type
  Type ?u.3943 : Type (?u.3943 + 1)
-/

example (p : Subspace ℝ E) (f : { x : E // x ∈ p } →L[ℝ] ℝ) :
  ∃ g : E →L[ℝ] ℝ, (∀ x : p, g x = f x) ∧ ∥g∥ = ∥f∥ := sorry

/-
error: application type mismatch
  HasCoeToFun.coe _ x
argument
  x
has type
  HasCoeToSort.coe p : HasCoeToSort.S (Subspace ℝ E)
but is expected to have type
  E : Type u
-/

-- Adding this instance changes the error message:
-- (note that `CoeSort` and `Coe` differ by the `outParam` in the second argument)
instance [inst : CoeSort α β] : Coe α β := { inst with }

example (p : Subspace ℝ E) (f : p →L[ℝ] ℝ) :
  ∃ g : E →L[ℝ] ℝ, (∀ x : { x : E // x∈p }, g x = f x) ∧ ∥g∥ = ∥f∥ := sorry

/-
error: typeclass instance problem is stuck, it is often due to metavariables
  HasNorm (?m.23242 →L[ℝ] ℝ)
-/

end Real.Playground

[dselsam]

The following works in Lean3:

class Foo (α : Type) := (x : α)

instance (α : Type) : has_coe_to_sort (Foo α) := {
  S := Type,
  coe := fun _, unit
}

#check @id (Foo.mk ()) () -- works

whereas the following fails in Lean4:

class Foo (α : Type) where x : α
instance : CoeSort (Foo α) Type where coe _ := α
#check @id (Foo.mk ()) () -- fails

It seems that in Lean3, if a function argument type is sort, then has_coe_to_sort is considered.

[dselsam]

Note that if we add the instance instance coeSortToCoe [inst : CoeSort α β] : Coe α β := { coe := inst.coe } it will still fail because of the universe metavariable in the target type, i.e.

...
    [Meta.synthInstance.generate] instance @fooCoeSort
    [Meta.synthInstance.tryResolve] 
      [Meta.synthInstance.tryResolve] CoeSort.{1, ?u.82 + 1} (Foo Unit)
        (Sort ?u.82) =?= CoeSort.{1, 2} (Foo ?m.161) Type
      [Meta.isDefEq] 
        [Meta.isDefEq.step] CoeSort.{1, ?u.82 + 1} (Foo Unit) (Sort ?u.82) =?= CoeSort.{1, 2} (Foo ?m.161) Type
        [Meta.isDefEq.step] Foo Unit =?= Foo ?m.161
          [Meta.isDefEq.step] Foo Unit =?= Foo ?m.161
            [Meta.isDefEq.step] Unit =?= ?m.161
              [Meta.isDefEq] Unit [nonassignable] =?= ?m.161 [assignable]
                [Meta.isDefEq.assign] 
                  [Meta.isDefEq.assign] ?m.161 := Unit
                  [Meta.isDefEq.assign.beforeMkLambda] ?m.161 [] := Unit
                  [Meta.isDefEq.assign.checkTypes] 
                    [Meta.isDefEq.step] Type =?= Type
                    [Meta.isDefEq.assign.final] ?m.161 := Unit
          [Meta.isDefEq.step] Sort ?u.82 =?= Type
          [Meta.isLevelDefEq.step] ?u.82 =?= 1
            [Meta.isLevelDefEq.stuck] ?u.82 =?= 1

[gebner]

Function coercion is missing as well. That is, if you have x : Equiv A B, then (x : A → B) won't work.