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 <[email protected]> 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:[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
