tcInferRho

[Simon Peyton Jones]

Yes that comment is a lie!

I would welcome a way to tighten this up.

Unifying with foralls is just fine, provided they behave rigidly like type constructors.  The unifier can even unify two foralls, and generate evidence.  All good. 

BUT foralls are implicitly instantiated, and it is the implicitly-instantiated ones that must not be hidden.

One possibility, pioneered by QML (http://research.microsoft.com/en-us/um/people/crusso/qml/) is to have two kinds of foralls, implicitly instantiated and explicitly instantiated. GHC has been moving in that direction but only fitfully.  That's one reason that the entire ImpredicativeTypes extensions is currently in limbo.

Simon

| -----Original Message-----
| From: Richard Eisenberg [mailto:eir at cis.upenn.edu]
| Sent: 22 July 2014 14:27
| To: Simon Peyton Jones
| Cc: ghc-devs at haskell.org
| Subject: 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 <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
| > | > | >
| > | >
| > | >
| >
| >