What's causing failure to synthesize here?

Stream: general

[nrs]

inductive myTerms where
  | var : String -> myTerms
  | other : myTerms

prefix: max "**" => myTerms.var

def myCheck : myTerms -> Type
  | **_ => myTerms
  | _ => Empty

def testFunc (t: myTerms) {_ : myCheck t} : String :=
  match t with
  | **s => s

#eval testFunc **"m"

Seems to me there's only a single possible way to resolve the type, but I'm a bit lost. Basically, I want to make a function that enforces at the type-level that t be pattern-matchable with **s. Anyone got tips/suggestions/readings?

[Bjørn Kjos-Hanssen]

We can see explicitly that there's more than way like this:

#eval @testFunc **"m" myTerms.other
#eval @testFunc **"m" <| myTerms.var "hello"

Maybe add the assumption [Nonempty (myCheck t)] instead.

[nrs]

Bjørn Kjos-Hanssen ☀️ said:

We can see explicitly that there's more than way like this:

#eval @testFunc **"m" myTerms.other
#eval @testFunc **"m" <| myTerms.var "hello"

Maybe add the assumption [Nonempty (myCheck t)] instead.

ah I see! thanks a lot for the example!