Small example about unification order

Stream: lean4

[nrs]

The following will fail to unify because MyType does not correspond to the instantiated implicit ?t. Yet, it seems to me that writing down MyType.a will unambiguously bind what ?t can be. Is there a way of writing this that will allow us to declare Composite directly by giving MyType.a on the left side of the product, without needing to specify that it should be of type MyType?

inductive MyType | a
def Composite : {t : Type} -> t × (t -> Nat) := ⟨MyType.a, fun _ => 0⟩

[Mario Carneiro]

This isn't an issue of type inference, you can't construct an element of that type using MyType.a at all because the type t is an input and not an output

[Mario Carneiro]

that is, you have to be able to produce an element of type t for any t, which is impossible

[Mario Carneiro]

if you want to give t as an output, you need to use (t : Type) × t × (t -> Nat)

[Mario Carneiro]

def Composite : (t : Type) × t × (t -> Nat) := ⟨_, MyType.a, fun _ => 0⟩

[Mario Carneiro]

(there is no {} version of this type constructor, but as you can see you can omit it using _)

[nrs]

hm right, this makes a lot of sense

[nrs]

thanks for the answer!!

[nrs]

Probably not recommendable to do the following

instance (α : Type) (a : α) (f : α -> Nat) : CoeDep (α × (α -> Nat)) ⟨a, f⟩ ((t : Type) × t ×  (t -> Nat)) where
  coe := ⟨α, a, f⟩

def test : (t : Type) × t × (t -> Nat) := Prod.mk (2 : Nat) (fun _ : Nat => 0) -- coerces as expected

(but maybe this might be what we might mean by sigma curly brackets?)