Agda-2.3.2.2: test/succeed/Issue395.agda

module Issue395 where

foo : Set → Set₁
foo foo with Set
... | _ = Set