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

[Simon Peyton-Jones]

Haskell is a *functional* language.  Consider

    say $ "  pre-zonk:  " ++ pp all_expr_ty
    zonkTcType all_expr_ty
    say $ "  post-zonk: " ++ pp all_expr_ty

pp is a pure function; it is given the same input both times, so of course it produces the same output.

If you collect the result of zonkTcType you might have better luck, thus:

    say $ "  pre-zonk:  " ++ pp all_expr_ty
    zonked_expr_ty <- zonkTcType all_expr_ty
    say $ "  post-zonk: " ++ pp zonked_expr_ty

Zonking walks over a type, returning a new type in which unification variables are replaced by the types they unified to.

Hope this helps

Simon

| -----Original Message-----
| From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
| bounces at haskell.org] On Behalf Of p.k.f.holzenspies at utwente.nl
| Sent: 29 August 2013 14:42
| To: glasgow-haskell-users at haskell.org
| Subject: Question about correct GHC-API use for type checking (or
| zonking, or tidying)
| 
| 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 }
| 
| 
| 
| _______________________________________________
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users at haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users