I believe that you are asking about type functions. Specifically, I think what you are asking is this:

How can I normalise a type, by rewriting it exhaustively using
the top-level type-function definitions

That is indeed a better formulation of my original question

I think the function TcTyFuns.tcNormaliseFamInst (rather an odd name!) does this. But it's not very helpful to you because it's in the main typechecker monad.

At the moment it is not such a big problem that it is in the typechecker
monad, as we run some parts of our compiler in a GHC Monad, and can thus
initialize a typechecker monad with the function TcRnMonad.initTc.

However, at the moment I can't get to normalise the types as far as I
had hoped. Here is an example of my debug output:

Before normalisation:
Types.Data.Num.Decimal.Literals.D4
Types.Data.Num.Ops.:*: Types.Data.Num.Decimal.Literals.D3

After normalisation:
Types.Data.Num.Decimal.Digits.Dec
  (Types.Data.Num.Decimal.Digits.DecN
   Types.Data.Num.Ops.:. Types.Data.Num.Decimal.Digits.Dec4)
Types.Data.Num.Ops.:*: Types.Data.Num.Decimal.Digits.Dec
                         (Types.Data.Num.Decimal.Digits.DecN
Types.Data.Num.Ops.:. Types.Data.Num.Decimal.Digits.Dec3)

So, currently I can normalize the synonyms D4 and D3, but I can't
normalize the type function :*:. Maybe it has something to do with how I
load the module and its dependencies. Below is the code that I use to
normalize a type-level integer from the tfp library, I hope it's not too
much to read.

normalise_tfp_int :: Type.Type -> Type.Type
normalise_tfp_int ty =
  unsafeRunGhc $ do
    -- Automatically import modules for any fully qualified identifiers
    setDynFlag DynFlags.Opt_ImplicitImportQualified
    let modules = map GHC.mkModuleName ["Types.Data.Num"]
    nty <- normaliseType modules ty
    return nty

normaliseType ::
  [Module.ModuleName]
  -> Type.Type
  -> GHC.Ghc Type.Type
normaliseType modules ty = do
  env <- GHC.getSession
  nty <- HscTypes.ioMsgMaybe $ MonadUtils.liftIO $
    -- Initialize the typechecker monad
    TcRnMonad.initTcPrintErrors env PrelNames.iNTERACTIVE $ do
      mapM importModule modules
      -- Normalize the type
      (_, nty) <- TcTyFuns.tcNormaliseFamInst ty
      return nty
  return nty

importModule :: Module.ModuleName -> TcRnTypes.RnM ()
importModule mod = do
  let reason = Outputable.text "Hardcoded import"
  let pkg = Nothing
  -- Load the interface.
  iface <- LoadIface.loadSrcInterface reason mod False pkg
  let deps = HscTypes.mi_deps iface
  let orphs = HscTypes.dep_orphs deps
  let finsts = HscTypes.dep_finsts deps
  -- Load the dependencies and family instances
  LoadIface.loadOrphanModules orphs False
  LoadIface.loadOrphanModules finsts True


_______________________________________________
Glasgow-haskell-users mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Reply via email to