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:[email protected]] | Sent: 22 July 2014 13:22 | To: Simon Peyton Jones | Cc: [email protected] | 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 <[email protected]> | 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:[email protected]] | > | 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 | > | <[email protected]> | > | 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:[email protected]] | > | > | 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 | > | > | > | > _______________________________________________ ghc-devs mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-devs
