Error: pattern matching lambdas must take a single argument

[jespercockx]

The following example (minimized from some real-life code) produces an error "Pattern matching lambdas must take a single argument":

open import Haskell.Prelude

Scope = List Bool

data Telescope (@0 α : Scope) : @0 Scope → Set where
  ExtendTel : ∀ {@0 x β} → Bool → Telescope (x ∷ α) β  → Telescope α (x ∷ β)
{-# COMPILE AGDA2HS Telescope #-}

caseTelBind : ∀ {@0 x α β} (tel : Telescope α (x ∷ β))
            → ((a : Bool) (rest : Telescope (x ∷ α) β) → @0 tel ≡ ExtendTel a rest → d)
            → d
caseTelBind (ExtendTel a tel) f = f a tel refl
{-# COMPILE AGDA2HS caseTelBind #-}

checkSubst : ∀ {@0 x α β} (t : Telescope α (x ∷ β)) → Bool
checkSubst t = caseTelBind t λ ty rest → λ where refl → True
{-# COMPILE AGDA2HS checkSubst #-}