# Zulip Chat Archive

## Stream: new members

### Topic: has_coe_to_sort

#### Horatiu Cheval (Mar 28 2021 at 07:55):

I think I am misunderstanding `has_coe_to_sort`

. Why does the following not work?

```
inductive formula {α : Type} [has_coe_to_sort α]
| equation {a : α} : a → a → formula
--type expected at
-- a
--term has type
-- α
```

#### Mario Carneiro (Mar 28 2021 at 08:09):

I don't think `has_coe_to_sort`

works as an assumption, because it is necessary for the first projection out of the `has_coe_to_sort`

instance to definitionally reduce to `Sort u`

, which isn't possible unless you have a concrete instance

#### Horatiu Cheval (Mar 28 2021 at 08:12):

Oh, ok. It worked indeed with concrete choices of α, and that amplified my confusion. Thanks!

#### Eric Wieser (Mar 28 2021 at 08:53):

Will this will be fixed by Yury's refactor?

#### Yury G. Kudryashov (Mar 28 2021 at 14:29):

I wouldn't call it "Yury's" refactor. It is backporting of `coe_sort`

and `coe_fun`

from Lean 4, and most of the hard work in core was done by @Gabriel Ebner.

#### Yury G. Kudryashov (Mar 28 2021 at 14:30):

We're talking about lean#557

#### Horatiu Cheval (Mar 28 2021 at 21:24):

Another problem I encountered in the same context which might be related (though, I am not sure if it's due to `has_coe_to_sort`

).

Why is the inductive definition of `proof`

wrong, why are there several `σ`

's generated?

```
inductive linear_type
| zero : linear_type
| arrow : linear_type → linear_type → linear_type
infixr `↣` : 50 := linear_type.arrow
notation `𝕋` := linear_type
instance : has_zero 𝕋 := ⟨linear_type.zero⟩
def linear_type_to_sort : 𝕋 → Type
| 0 := ℕ
| (σ ↣ τ) := (linear_type_to_sort σ) → (linear_type_to_sort τ)
instance : has_coe_to_sort linear_type := ⟨Type, linear_type_to_sort⟩
inductive formula
| equation : (0 : 𝕋) → (0 : 𝕋) → formula
| universal : ∀ (σ : 𝕋) (A : σ → formula), formula
notation `∀'` := formula.universal
def equation_ext : ∀ {σ : 𝕋}, σ → σ → formula
| 0 := λ t u, formula.equation t u
| (σ ↣ τ) := λ t u : (σ ↣ τ), ∀' σ (λ x : σ, equation_ext (t x) (u x))
inductive proof (Γ : list formula) : formula → Type
| EXT : ∀ {σ τ : 𝕋} {t u : σ} {s : (σ ↣ τ)},
proof (@equation_ext σ t u) → proof (@equation_ext τ (s t) (s u))
/-
type mismatch at application
equation_ext t
term
t
has type
↥σ_1
but is expected to have type
↥σ
types contain aliased name(s): σ
remark: the tactic `dedup` can be used to rename aliases
-/
```

#### Mario Carneiro (Mar 28 2021 at 22:51):

This looks like a bug, although I'm not sure where. As a workaround, this works:

```
inductive proof (Γ : list formula) : formula → Type
| EXT : ∀ {σ τ : 𝕋} {t u : σ} {s : (σ ↣ τ)} {f},
f = (@equation_ext τ (s t) (s u)) →
proof (@equation_ext σ t u) → proof f
```

#### Mario Carneiro (Mar 28 2021 at 22:56):

This also works:

```
inductive proof (Γ : list formula) : formula → Type
| EXT : ∀ {σ τ : 𝕋} {t u : σ} {s : (σ ↣ τ)},
proof (@equation_ext σ t u) → proof (@equation_ext τ (id s t) (s u))
```

Last updated: Dec 20 2023 at 11:08 UTC