tcInferRho
Richard Eisenberg
eir at cis.upenn.edu
Tue Jul 22 13:26:36 UTC 2014
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
> | > | >
> | >
> | >
>
>
More information about the ghc-devs
mailing list