Cast doesn't assign type

Stream: lean4

[Pavel Klimov]

The following code doesn't work

inductive Ty
| int
| str

def Ty.toType : Ty → Type
| .int => Int
| .str => String

structure TypedVal where
type : Ty
value : type.toType

def TypedValue.checkEqualToInt : TypedVal → Int → Bool
| ⟨ .int, val ⟩, int => (val : Int) == int
| _, _ => false

It works in this way, no proof required:

def TypedValue.checkEqualToInt : TypedVal → Int → Bool
| ⟨ .int, val ⟩, int =>
  let val' : Int := val
  val' == int
| _, _ => false

And, it also works in this way

def TypedValue.checkEqualToInt : TypedVal → Int → Bool
| ⟨ .int, val ⟩, int => (cast rfl val : Int) == int
| _, _ => false

Why (val : Int) doesn't work? :thinking: While temporary additional variable works.

[Kenny Lau]

@Pavel Klimov if you look at the error message (very useful to do in general), it says "failed to synthesize BEq Ty.int.toType", which means it failed to look beyond Ty.int.toType and see it as Int.

This is because you used def Ty.toType, which means "do not unfold me when you synthesize classes".

If you do want to unfold it automatically, you can change it to abbrev Ty.toType, and then the code you posted succeeds without error.

[Robin Arnez]

(val : Int) is only a hint while elaborating val, when it looks at val == int, it still sees val : Ty.int.toType. You can do show Int from val which is not only a hint for elaborating val but actually encodes the type in the resulting expression as (have : Int := val; this)