namespace Ex

class GetElem (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) where
  getElem' (xs : Cont) (i : Idx) : Elem

export GetElem (getElem')

instance : GetElem Lean.Syntax Nat Lean.Syntax where
  getElem' xs i := xs.getArg i

instance : GetElem (Array α) Nat α where
  getElem' xs i := xs[i]'sorry

open Lean

def f (stx : Option Syntax) : Syntax :=
  stx.getD default

def bad (doFor : Syntax) : Syntax :=
  let doForDecls := (getElem' doFor 1).getArgs
  let doForDecl := getElem' doForDecls 1
  f (getElem' doForDecl 1)