tcInferRho

[Simon Peyton Jones]

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