Question about correct GHC-API use for type checking (or zonking, or tidying)

[p.k.f.holzenspies at utwente.nl]

Dear GHC-ers,

I'm working on building an interactive environment around the composition of expressions. Users can type in (i.e. give strings of) expressions and can then use these expressions to produce other expressions. I'm close to having a working GHC-API binding for this. The resulting types, however, still contain some things I don't quite understand. Any help would be appreciated.

Below, I've included the function exprFromString which should parse, rename and typecheck strings to Id-things and give their type (although, ideally, the idType of said Id-thing should be the same as the type returned). This function lives in the IA (InterActive) monad; a monad that is a GhcMonad and can lift monadic computations in TcM into itself using liftTcM (which uses the initTcPrintErrors and setInteractiveContext functions similarly to TcRnDriver.tcRnExpr).

Near the end of the function, debugging output is produced. This output confuses me slightly. Here is the output for the three inputs "map (+1) [1..10]", "5" and "\\x -> x":


map (+1) [1..10]
  pre-zonk:  forall b. (GHC.Enum.Enum b_i, GHC.Num.Num b_i) => [b_i]
  post-zonk: forall b. (GHC.Enum.Enum b_i, GHC.Num.Num b_i) => [b_i]
  idType:    [b_c]
  tidied:    forall b. (GHC.Enum.Enum b_i, GHC.Num.Num b_i) => [b_i]
5
  pre-zonk:  forall a. GHC.Num.Num a_d => t_c
  post-zonk: forall a. GHC.Num.Num a_d => t_c
  idType:    a_b
  tidied:    forall a. GHC.Num.Num a_d => t_c
\x -> x
  pre-zonk:  forall t. t_e
  post-zonk: forall t. t_e
  idType:    forall t. t -> t
  tidied:    forall t. t_e


The zonking and tidying part of the type-checking process are still a bit unclear to me and I suspect the problems arise there. It looks to me that the type variables in the quantifications are different ones from those in the pi/rho-types. I had expected the types to only contain the variables over which they are quantified, so e.g. in the map-example, I had expected "forall b . (GHC.Enum.Enum b, GHC.Num.Num b) => [b]"

Can anyone explain what I'm missing?

Regards,
Philip





exprFromString :: String -> IA (Id,Type)
exprFromString str = do
  dfs <- getDynFlags
  let pp  = showSDoc dfs . ppr
  pst <- mkPState dfs buf <$> newRealSrcLoc

{- Parse -}
  (loc,rdr_expr) <- case unP parseStmt pst of
    PFailed span err -> throwOneError (mkPlainErrMsg dfs span err)
    POk pst' (Just (L l (ExprStmt rdr_expr _ _ _))) -> do
      logWarningsReportErrors (getMessages pst')
      return (l,rdr_expr)
    POk pst' thing -> throw $ maybe EmptyParse (const NonExpressionParse) thing
  liftTcM $ do
    fresh_it <- freshName loc str

{- Rename -}
    (rn_expr, fvs) <- checkNoErrs $ rnLExpr rdr_expr

{- Typecheck -}
    let binds = mkBinds fresh_it rn_expr fvs

    (((_bnds,((_tc_expr,res_ty),id)),untch),lie) <- captureConstraints . captureUntouchables $
      tcLocalBinds binds ((,) <$> tcInferRho rn_expr <*> tcLookupId fresh_it)
    ((qtvs, dicts, _bool, _evbinds), lie_top) <- captureConstraints $
      simplifyInfer True False [(fresh_it, res_ty)] (untch,lie)

    let all_expr_ty = mkForAllTys qtvs (mkPiTypes dicts res_ty)
    say str
    say $ "  pre-zonk:  " ++ pp all_expr_ty
    zonkTcType all_expr_ty
    say $ "  post-zonk: " ++ pp all_expr_ty
    say $ "  idType:    " ++ pp (idType id)
    say $ "  tidied:    " ++ pp (tidyTopType all_expr_ty)

    return (id,all_expr_ty)
  where
  say = liftIO . putStrLn
  buf = stringToStringBuffer str
  freshName loc str = (\u -> mkInternalName u name loc) <$> newUnique
    where
    name = mkOccNameFS varName $ fsLit $ "it" ++ show (lineOf loc)
    isVarChar c = isAlphaNum c || c == '_' || c == '\''
    lineOf (RealSrcSpan s) = srcSpanStartLine s
    lineOf _ = -1

  mkBinds :: Name -> LHsExpr Name -> FreeVars -> HsLocalBinds Name
  mkBinds nm e@(L l _) fvs = HsValBinds $ ValBindsOut [(NonRecursive, unitBag the_bind)] []
    where
    the_bind = L l (mkTopFunBind (L l nm) [mkMatch [] e emptyLocalBinds]) { bind_fvs = fvs }