Re: tcInferRho

Ah -- it's all clear to me now. To summarize: a TauTv *can* become a poly-type, but the solver won't ever discover so. That would seem to contradict

= TauTv -- This MetaTv is an ordinary unification variable -- A TauTv is always filled in with a tau-type, which -- never contains any ForAlls

which appears in the declaration for MetaInfo in TcType. Is that an accurate summary? Thanks for helping to clear this up! Richard On Jul 22, 2014, at 9:19 AM, Simon Peyton Jones wrote:

Indeed.

Unification variables *can* unify with polytypes, as you see.

GHC does "on the fly" unification with in-place update, and only defers to the constraint solver if it can't readily unify on the fly. The squishiness is precisely that for this setting we *must* unify on the fly, so the "it's always ok to defer" rule doesn't hold.

Simon

| -----Original Message----- | From: Richard Eisenberg [mailto:eir@cis.upenn.edu] | Sent: 22 July 2014 13:22 | To: Simon Peyton Jones | Cc: ghc-devs@haskell.org | Subject: Re: tcInferRho | | OK -- that all makes sense. | | But why does it actually work, I wonder? It seems that to get the | behavior that you describe below, and the behavior that we see in | practice, a unification variable *does* have to unify with a non-tau- | type, like (forall a. a -> a) -> Int. But doesn't defer_me in | TcUnify.checkTauTvUpdate prevent such a thing from happening? | | To learn more, I tried compiling this code: | | > f :: Bool -> Bool -> (forall a. a -> a) -> () f = undefined | > | > g = (True `f` False) id | | I use infix application to avoid tcInferRho. | | With -ddump-tc-trace -dppr-debug, I see the following bit: | | > Scratch.hs:18:6: | > u_tys | > untch 0 | > (forall a{tv apE} [sk]. a{tv apE} [sk] -> a{tv apE} [sk]) -> () | > ~ | > t_aHO{tv} [tau[0]] | > a type equality (forall a{tv apE} [sk]. | > a{tv apE} [sk] -> a{tv apE} [sk]) | > -> () | > ~ | > t_aHO{tv} [tau[0]] | > Scratch.hs:18:6: | > writeMetaTyVar | > t_aHO{tv} [tau[0]] := (forall a{tv apE} [sk]. | > a{tv apE} [sk] -> a{tv apE} [sk]) | > -> () | > | | What's very strange to me here is that we see t_aHO, a **tau** type, | being rewritten to a poly-type. I could clearly throw in more printing | statements to see what is going on, but I wanted to check if this looks | strange to you, too. | | Thanks, | Richard | | On Jul 22, 2014, at 6:28 AM, Simon Peyton Jones | wrote: | | > Richard | > | > You are right; there is something squishy here. | > | > The original idea was that a unification variable only stands for a | *monotype* (with no for-alls). But our basic story for the type | inference engine is | > tcExpr :: HsExpr -> TcType -> TcM HsExpr' | > which checks that the expression has the given expected type. To do | inference we pass in a unification variable as the "expected type". | BUT if the expression actually has a type like (forall a. a->a) -> Int, | then the unification variable clearly isn't being unified with a | monotype. There are a couple of places where we must "zonk" the | expected type, after calling tcExpr, to expose the foralls. A major | example is TcExpr.tcInferFun. | > | > I say this is squishy because *in principle* we could replace every | unification with generating an equality constraint, for later solving. | (This does often happen, see TcUnify.uType_defer.) BUT if we generate | an equality constraint, the zonking won't work, and the foralls won't | be exposed early enough. I wish that the story here was more solid. | > | > The original idea of tcInferRho was to have some special cases that | did not rely on this squishy "unify with polytype" story. It had a | number of special cases, perhaps not enough as you observe. But it | does look as if the original goal (which I think was to deal with | function applications) doesn't even use it -- it uses tcInferFun | instead. | > | > So I think you may be right: tcInferRho may not be important. There | is a perhaps-significant efficiency question though: it avoids | allocating an unifying a fresh unification variable each time. | > | > Simon | > | > | -----Original Message----- | > | From: Richard Eisenberg [mailto:eir@cis.upenn.edu] | > | Sent: 18 July 2014 22:00 | > | To: Simon Peyton Jones | > | Subject: Re: tcInferRho | > | | > | I thought as much, but I can't seem to tickle the bug. For example: | > | | > | > {-# LANGUAGE RankNTypes #-} | > | > | > | > f :: Int -> Bool -> (forall a. a -> a) -> Int f = undefined | > | > | > | > x = (3 `f` True) | > | > | > | | > | | > | GHCi tells me that x's type is `x :: (forall a. a -> a) -> Int`, as | > | we would hope. If we were somehow losing the higher-rank | > | polymorphism without tcInferRho, then I would expect something like | > | `(3 `f` True) $ not)` to succeed (or behave bizarrely), but we get | a | > | very sensible type error | > | | > | Couldn't match type 'a' with 'Bool' | > | 'a' is a rigid type variable bound by | > | a type expected by the context: a -> a | > | at /Users/rae/temp/Bug.hs:6:5 | > | Expected type: a -> a | > | Actual type: Bool -> Bool | > | In the second argument of '($)', namely 'not' | > | In the expression: (3 `f` True) $ not | > | | > | So, instead of just adding more cases, I wonder if we can't | *remove* | > | cases, as it seems that the gears turn fine without this function. | > | This continues to surprise me, but it's what the evidence | indicates. | > | Can you make any sense of this? | > | | > | Thanks, | > | Richard | > | | > | | > | On Jul 18, 2014, at 12:49 PM, Simon Peyton Jones | > | | > | wrote: | > | | > | > You're right, its' an omission. The reason for the special case | > | > is | > | described in the comment on tcInferRho. Adding OpApp would be a | > | Good Thing. A bit tiresome because we'd need to pass to tcInferApp | > | the function to use to reconstruct the result HsExpr (currently | > | foldl mkHsApp, in tcInferApp), so that in the OpApp case it'd | > | reconstruct an OpApp. | > | > | > | > Go ahead and do this if you like | > | > | > | > S | > | > | > | > | -----Original Message----- | > | > | From: Richard Eisenberg [mailto:eir@cis.upenn.edu] | > | > | Sent: 17 July 2014 18:48 | > | > | To: Simon Peyton Jones | > | > | Subject: tcInferRho | > | > | | > | > | Hi Simon, | > | > | | > | > | I'm in the process of rejiggering the functions in TcHsType to | > | > | be | > | more | > | > | like those in TcExpr, in order to handle the richer type/kind | > | language | > | > | of my branch. | > | > | | > | > | I have a question about tcInferRho (TcExpr.lhs:115). It calls | > | > | tcInfExpr, which handles three special cases of HsExpr, before | > | > | deferring to tcExpr. The three cases are HsVar, HsPar, and | HsApp. | > | > | What's odd about this is that there are other cases that seem | to | > | belong | > | > | in this group, like OpApp. After all, (x + y) and ((+) x y) | > | > | should behave the same in all circumstances, right? I can't | find | > | > | a way to tickle the omission here, so there may not be a bug, | > | > | but it certainly is a little strange. Can you shed any light? | > | > | | > | > | Thanks! | > | > | Richard | > | > | > | >