1 2module Agda.Compiler.Backend 3 ( module Agda.Syntax.Treeless 4 , Backend 5 , activeBackendMayEraseType 6 , lookupBackend 7 ) 8 where 9 10import Control.DeepSeq 11 12-- Explicitly adding the Agda.Syntax.Treeless import to the .hs-boot file 13-- so that the `Args` symbol can be hidden by the `SOURCE` import in 14-- TypeChecking.Monad.Base. 15-- 16-- Without exporting it here, a `hiding` clause there causes a compilation 17-- error. But without hiding it there, the name conflicts with the one 18-- imported from Agda.Syntax.Internal. 19-- 20-- This is only a problem with ghci, which will load a fully-compiled module if 21-- available; but that module will contain more symbols than just the few in 22-- the .hs-boot 23import Agda.Syntax.Treeless (TTerm, Args) 24 25import Agda.Syntax.Abstract.Name (QName) 26import {-# SOURCE #-} Agda.TypeChecking.Monad.Base (TCM, BackendName) 27 28data Backend 29 30instance NFData Backend 31 32activeBackendMayEraseType :: QName -> TCM Bool 33lookupBackend :: BackendName -> TCM (Maybe Backend) 34