Issue818.agda:8,1-9,23 Unexpected implicit argument when checking that the clause Foo with tt Foo {x = _} | tt = Set has type {x : ⊤} → Set₁