tcInferRho

[Richard Eisenberg]

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