-- {-# OPTIONS -v tc.with:100 #-}
module Issue818 where

data ⊤ : Set where
  tt : ⊤

Foo : {x : ⊤} → Set₁
Foo with tt
Foo {x = _} | tt = Set

-- Panic: wrong number of arguments in with clause: given 1, expected
-- 0
-- when checking that the clause
-- Foo with tt
-- Foo {x = _} | tt = Set
-- has type {⊤} → Set₁

-- The code above type-checks using Agda 2.3.0.1, but not with Agda
-- 2.3.2.

-- Andreas, 2013-03-08: same error thrown by

-- foo : ⊤ → Set₁
-- foo with tt
-- foo x | tt = Set

-- Implicit arguments are no longer eagerly introduced (see release notes
-- for 2.3.2, text for issue 679).

-- WAS: Should now throw a proper error message (not a panic).

-- 2015-07-07: May succeed.
