tcInferRho

[Richard Eisenberg]

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 <simonpj at microsoft.com> 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 at cis.upenn.edu]
> | Sent: 22 July 2014 13:22
> | To: Simon Peyton Jones
> | Cc: ghc-devs at 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 <simonpj at microsoft.com>
> | 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 at 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
> | > | <simonpj at microsoft.com>
> | > | 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 at 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
> | > | >
> | >
> | >
> 
>