Hi Cafe, I'm currently writing a simple GHC Typechecker plugin to augment typelevel naturals with a presburger arithmetic solver [^1]. I want to use type-class constraints to give premisses to the solver, for example, `Empty a` constraint means "a is false (empty type)". So I have to get TyCon information in TcPluginM monad and I wrote as follows: ```haskell do md <- lookupModule (mkModuleName "Proof.Propositional.Empty") (fsLit "equational-reasoning") classTyCon <$> (tcLookupClass =<< lookupOrig md (mkTcOcc "Empty")) ``` But this code doesn't work as expected. For example, the code ```haskell {-# LANGUAGE DataKinds, TypeOperators, GADTs, TypeFamilies, ExplicitForAll, FlexibleContexts #-} import Data.Type.Equality import GHC.TypeLits (type (+), type (<=), type (<=?)) import Proof.Propositional (Empty(..)) predSucc :: Empty (n :~: 0) => proxy n -> (n + 1 <=? n + n) :~: 'True predSucc _ = Witness ``` resulted in the following compile-time error: ``` Can't find interface-file declaration for type constructor or class equational-reasoning-0.4.0.0:Proof.Propositional.Empty Probable cause: bug in .hi-boot file, or inconsistent .hi file Use -ddump-if-trace to get an idea of which file caused the error ``` The probem is, Empty class is provided by separate existing package [^2], but is once defined in hidden module and re-exported from exposed from exposed module. If I expose the module where Empty is originally defined and change the module name passed to lookupModule appropriately, then the first code becomes working as expected. So the question: is there any way to retrieve TyCon information defined in hidden module but exported? [^1]: https://github.com/konn/ghc-typelits-presburger/ [^2]: https://github.com/konn/equational-reasoning-in-haskell -- Hiromi ISHII konn.jinro@gmail.com Doctoral program in Mathematics, University of Tsukuba