module BadRefine where

data Bool : Set where
  false true : Bool

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

ap : {A B : Set} {x y : A} (f : A → B) → x ≡ y → f x ≡ f y
ap f refl = refl

id : Bool → Bool
id x = x

{-
refining this leads to ({!!} true) to be inserted in place of the hole
-}
bad-refine : id false ≡ id false
bad-refine = ap {!λ f → f true!} id=id
  where
    id=id : id ≡ id
    id=id = refl

{-
attempting to refine self-application leads to confusing message
"Cannot refine functions with 10 or more arguments"
-}
bad : (Bool → Bool) → Bool
bad = λ x → {!x x!}
