dependent elimination failed, failed to solve equation

Stream: new members

[James Randolf]

I have the following code:

inductive Wrapper.{u} : Type u → Type (u + 1) where
  | value {T : Type u} (t : T) : Wrapper T
  | extra : Wrapper (ULift Nat)

-- dependent elimination failed, failed to solve equation Wrapper T = ULift Nat
def Wrapper.join {T : Type} (t : Wrapper (Wrapper T)) : Wrapper T := match t with
  | Wrapper.value t => t

I don't get why match can't figure out that the extra case is impossible. How can I fix this?

[James Randolf]

My second attempt is change Wrapper to not be an inductive type family, but in this case I have a new problem

inductive Wrapper' (T : Type) : Type
  | value : T → Wrapper' T
  | extra : (T = Nat) → Wrapper' T

def Wrapper'.join {T : Type} (t : Wrapper' (Wrapper' T)) : Wrapper' T := match t with
  | value t => t
  | extra e => sorry

I don't know how to prove that Wrapper' T ≠ Nat.

[Ruben Van de Velde]

It's highly discouraged to use type equality

[Timo Carlin-Burns]

I don't think it's possible to prove that Wrapper' T \ne Nat since Wrapper' Nat \equiv Nat and there is a consistent axiom that equivalence implies type equality.