Agda-2.3.2.2: test/fail/CompiledMustHaveHaskellType.agda
-- Compiled things must have a Haskell type given by a COMPILED_TYPE pragma
module CompiledMustHaveHaskellType where
postulate
N : Set
foo : N
-- It is necessary add something like
-- {-# COMPILED_TYPE N Int #-}
{-# COMPILED foo bar #-}