tcInferRho

[Simon Peyton Jones]

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
| > | >
| >
| >