A simple Agda tactic that just uses the first valid thing in scope.

1Lab.Reflection.Duh.agda

module 1Lab.Reflection.Duh where

open import 1Lab.Reflection
open import 1Lab.Prelude
open import Data.List
open import Data.Nat

private
  try-all : Term → Nat → Telescope → TC Term
  try-all goal _ [] = typeError $ strErr "Couldn't find anything!" ∷ []
  try-all goal n ((_ , tp) ∷ tele) =
    catchTC (unify goal (Arg.unarg tp) >> pure (var n [])) (try-all goal (suc n) tele)

macro
  duh! : Term → TC ⊤
  duh! hole = do
    ctx ← getContext
    goal ← inferType hole
    tm ← try-all goal 0 ctx
    unify hole tm

test : Nat → List Nat → Nat
test x y = duh!