Is there any way in GHC plugin to refer exposed but defined in a hidden module?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view
|

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
[hidden email]
Doctoral program in Mathematics,
University of Tsukuba


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

signature.asc (507 bytes) Download Attachment