tcInferRho
Simon Peyton Jones
simonpj at microsoft.com
Tue Jul 22 13:39:59 UTC 2014
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 implicitlyinstantiated ones that must not be hidden.
One possibility, pioneered by QML (http://research.microsoft.com/enus/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: ghcdevs at haskell.org
 Subject: Re: tcInferRho

 Ah  it's all clear to me now.

 To summarize: a TauTv *can* become a polytype, 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 tautype,
 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 inplace 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: ghcdevs 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
 >  nontau 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 ddumptctrace dpprdebug, 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 polytype. 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 foralls). 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 perhapssignificant 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 higherrank
 >  >  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 ghcdevs
mailing list