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:

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

{-# 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-
      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?


-- 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:
Only members subscribed via the mailman list are allowed to post.

signature.asc (507 bytes) Download Attachment