[Haskell-cafe] Is there any way in GHC plugin to refer exposed but defined in a hidden module?

[Hiromi ISHII]

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....@gmail.com
Doctoral program in Mathematics,
University of Tsukuba