RE: Question about correct GHC-API use for type checking (or zonking, or tidying)
Well, my tcLocalBinds seems to have a different type then yours (this is from
my copy of 7.6.3 and it's the same in the HEAD that I just synced):
tcLocalBinds :: HsLocalBinds Name - TcM thing - TcM (HsLocalBinds TcId, thing)
If I want to get a GblEnv out, I can use getGblEnv, but doing this:
mkId :: Maybe FreeVars - LHsExpr Name - Name - TcM Id
mkId fvs expr@(L l _) nm = do
((binds', gbl_env),lie) - captureConstraints $ tcLocalBinds binds getGblEnv
setGblEnv gbl_env (tcLookupId nm)
where
binds= HsValBinds $ ValBindsOut [(NonRecursive, unitBag fixbnd)] []
the_bind = mkTopFunBind (L l nm) [mkMatch [] expr emptyLocalBinds]
fixbnd = L l $ maybe the_bind (\vs - the_bind { bind_fvs = vs }) fvs
fails on the tcLookupId with a GHC internal error complaining that my name is
not in scope during type checking, but it passed the renamer.
Ph.
From: Simon Peyton-Jones [mailto:simo...@microsoft.com]
Sent: dinsdag 10 september 2013 14:19
To: Holzenspies, P.K.F. (EWI)
Cc: glasgow-haskell-users@haskell.org
Subject: RE: Question about correct GHC-API use for type checking (or zonking,
or tidying)
What goes wrong if you follow my suggestion below?
tcLocalBinds takes a set of bindings, such as x=e
and returns a GblEnv whose type envt is extended with a binding for x with its
generalised type.
This type wil indeed be closed, unless the current environment (in which
tcLocalBinds runs) has bindings with open types. Which in your case it probably
doesn't.
I feel that I am not being helpful but I'm not sure how to help more.
S
From: Philip K.F. Hölzenspies [mailto:p.k.f.holzensp...@utwente.nl]
Sent: 04 September 2013 21:25
To: Simon Peyton-Jones
Cc: glasgow-haskell-users@haskell.orgmailto:glasgow-haskell-users@haskell.org
Subject: Re: Question about correct GHC-API use for type checking (or zonking,
or tidying)
Ah, this is good to know. What I really would like is a function:
mkId :: Name - LHsExpr Name - TcM Id
where that Id is something I can store in my own monad (IA). The meaning of
this, is indeed let name = expression as a top-level binding. The
behaviour should actually be the same as that statement at the ghci-prompt. My
IA monad implements liftTcM as something that invokes a TcM-monad, i.e.
liftTcM :: TcM b - IA b
liftTcM thing_inside = do
hsc_env - getSession
stored_ids - getStoredIds :: IA [Id]-- this is the list of all Ids
made through mkId mentioned above
ioMsgMaybe . initTcPrintErrors hsc_env iNTERACTIVE $
setInteractiveContext hsc_env (hsc_IC hsc_env) $
tcExtendGlobalValEnv stored_ids $ -- or tcExtendIdEnv??
thing_inside
In the example you give below, I'm curious which thing_inside you give to
tcLocalBinds to get you the correct global environment. Also, if I do what you
suggest, i.e.
poly_id - setGblEnv gbl_env (tcLookupId the_id_name)
is that poly_id self contained, in the sense that I can put it in a new
instantiation as shown above?
Regards,
Philip
[cid:image001.jpg@01CEAEDB.407DA510]
Simon Peyton-Jonesmailto:simo...@microsoft.com
September 4, 2013 6:00 PM
The id you are getting is a monomorphic id, with a type like a-a, not the
polymorphic forall a. a-a. You don't want to go round arbitrarily creating a
new Id with the same unique but a different type. I have no idea what would
happen then.
It's hard for me to understand just what you code is trying to do. I think you
are making bindig
it = some expr
and then you want the type of it. Maybe something like
(binds', gbl_env) - tcLocalBinds (..your bindin..)
poly_id - setGblEnv gbl_env (tcLooupId the_id_name)
But I'm not totally sure.
S
inline: image001.jpg___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Question about correct GHC-API use for type checking (or zonking, or tidying)
The id you are getting is a monomorphic id, with a type like a-a, not the polymorphic forall a. a-a. You don't want to go round arbitrarily creating a new Id with the same unique but a different type. I have no idea what would happen then. It's hard for me to understand just what you code is trying to do. I think you are making bindig it = some expr and then you want the type of it. Maybe something like (binds', gbl_env) - tcLocalBinds (..your bindin..) poly_id - setGblEnv gbl_env (tcLooupId the_id_name) But I'm not totally sure. S From: p.k.f.holzensp...@utwente.nl [mailto:p.k.f.holzensp...@utwente.nl] Sent: 03 September 2013 14:18 To: Simon Peyton-Jones; glasgow-haskell-users@haskell.org Subject: RE: Question about correct GHC-API use for type checking (or zonking, or tidying) Dear Simon, et al, I had a chance to try it now. The strange thing is that when I use the lines: zonked_id - TcMType.zonkId id say $ zonked idType: ++ pp (idType zonked_id) that is still some unresolved type variable (i.e. prints as b_i). Since I already have the intended target-type (considering the code by which it is produced), is it safe to do what TcMType.zonkId does and manually set it? In other words, I now do this: zonked_ty - zonkTcType all_expr_ty return (setIdType id zonked_ty) Will this bite me later? Regards, Philip From: Simon Peyton-Jones [mailto:simo...@microsoft.com] Sent: maandag 2 september 2013 13:34 To: Holzenspies, P.K.F. (EWI); glasgow-haskell-users@haskell.orgmailto:glasgow-haskell-users@haskell.org Subject: RE: Question about correct GHC-API use for type checking (or zonking, or tidying) Does this mean that for the idType to come out correctly I should also zonk (AND BIND) the Id-value I return? Yes, zonk the type and grab the type that comes back. S From: p.k.f.holzensp...@utwente.nlmailto:p.k.f.holzensp...@utwente.nl [mailto:p.k.f.holzensp...@utwente.nl] Sent: 30 August 2013 17:49 To: Simon Peyton-Jones; glasgow-haskell-users@haskell.orgmailto:glasgow-haskell-users@haskell.org Subject: Re: Question about correct GHC-API use for type checking (or zonking, or tidying) I feel so unbelievably ignorant now. I thought with all the IORefs in the type checking process that zonking did this in these refs. Somehow I started thinking that some of these remained in SDocs, not thinking showSDoc is pure and results in a String, which holds no IORefs. Does this mean that for the idType to come out correctly I should also zonk (AND BIND) the Id-value I return? Ph. Sent from Samsung Mobile Original message From: Simon Peyton-Jones simo...@microsoft.commailto:simo...@microsoft.com Date: 30/08/2013 18:25 (GMT+01:00) To: Holzenspies, P.K.F. (EWI) p.k.f.holzensp...@utwente.nlmailto:p.k.f.holzensp...@utwente.nl,glasgow-haskell-users@haskell.org Subject: RE: Question about correct GHC-API use for type checking (or zonking, or tidying) 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- | boun...@haskell.orgmailto:boun...@haskell.org] On Behalf Of p.k.f.holzensp...@utwente.nlmailto:p.k.f.holzensp...@utwente.nl | Sent: 29 August 2013 14:42 | To: glasgow-haskell-users@haskell.orgmailto:glasgow-haskell-users@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
RE: Question about correct GHC-API use for type checking (or zonking, or tidying)
Does this mean that for the idType to come out correctly I should also zonk
(AND BIND) the Id-value I return?
Yes, zonk the type and grab the type that comes back.
S
From: p.k.f.holzensp...@utwente.nl [mailto:p.k.f.holzensp...@utwente.nl]
Sent: 30 August 2013 17:49
To: Simon Peyton-Jones; glasgow-haskell-users@haskell.org
Subject: Re: Question about correct GHC-API use for type checking (or zonking,
or tidying)
I feel so unbelievably ignorant now. I thought with all the IORefs in the type
checking process that zonking did this in these refs. Somehow I started
thinking that some of these remained in SDocs, not thinking showSDoc is pure
and results in a String, which holds no IORefs.
Does this mean that for the idType to come out correctly I should also zonk
(AND BIND) the Id-value I return?
Ph.
Sent from Samsung Mobile
Original message
From: Simon Peyton-Jones simo...@microsoft.commailto:simo...@microsoft.com
Date: 30/08/2013 18:25 (GMT+01:00)
To: Holzenspies, P.K.F. (EWI)
p.k.f.holzensp...@utwente.nlmailto:p.k.f.holzensp...@utwente.nl,glasgow-haskell-users@haskell.org
Subject: RE: Question about correct GHC-API use for type checking (or zonking,
or tidying)
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-
| boun...@haskell.orgmailto:boun...@haskell.org] On Behalf Of
p.k.f.holzensp...@utwente.nlmailto:p.k.f.holzensp...@utwente.nl
| Sent: 29 August 2013 14:42
| To:
glasgow-haskell-users@haskell.orgmailto:glasgow-haskell-users@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 - xfile:///\\x%20-%3e%20x:
|
|
| 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 -}
|
Re: Question about correct GHC-API use for type checking (or zonking, or tidying)
I feel so unbelievably ignorant now. I thought with all the IORefs in the type
checking process that zonking did this in these refs. Somehow I started
thinking that some of these remained in SDocs, not thinking showSDoc is pure
and results in a String, which holds no IORefs.
Does this mean that for the idType to come out correctly I should also zonk
(AND BIND) the Id-value I return?
Ph.
Sent from Samsung Mobile
Original message
From: Simon Peyton-Jones simo...@microsoft.com
Date: 30/08/2013 18:25 (GMT+01:00)
To: Holzenspies, P.K.F. (EWI)
p.k.f.holzensp...@utwente.nl,glasgow-haskell-users@haskell.org
Subject: RE: Question about correct GHC-API use for type checking (or zonking,
or tidying)
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-
| boun...@haskell.org] On Behalf Of p.k.f.holzensp...@utwente.nl
| Sent: 29 August 2013 14:42
| To: glasgow-haskell-users@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:
RE: Question about correct GHC-API use for type checking (or zonking, or tidying)
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-
| boun...@haskell.org] On Behalf Of p.k.f.holzensp...@utwente.nl
| Sent: 29 August 2013 14:42
| To: glasgow-haskell-users@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
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@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
