module Issue390 where data main : Set where