Question about correct GHC-API use for type checking (or zonking, or tidying)
p.k.f.holzenspies at utwente.nl
p.k.f.holzenspies at utwente.nl
Thu Aug 29 15:42:03 CEST 2013
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 }
More information about the Glasgow-haskell-users
mailing list