[GHC] #8995: When generalising, use levels rather than global tyvars

[GHC]

#8995: When generalising, use levels rather than global tyvars
-------------------------------------+------------------------------------
        Reporter:  simonpj           |            Owner:
            Type:  bug               |           Status:  new
        Priority:  normal            |        Milestone:
       Component:  Compiler          |          Version:  7.8.2
      Resolution:                    |         Keywords:
Operating System:  Unknown/Multiple  |     Architecture:  Unknown/Multiple
 Type of failure:  None/Unknown      |       Difficulty:  Unknown
       Test Case:                    |       Blocked By:
        Blocking:                    |  Related Tickets:
-------------------------------------+------------------------------------

Comment (by remy):

 Hi Simon,

 Oleg pointed me to your implementation issue in case I could help...

 I do not understand all the details because I do not know the internals of
 GHC, but I do believe that you only need one notion of ranks.

 However, I am a bit confused by your description.  First, because GHC does
 not generalizes unanotated local let-binding, then you should not have to
 play with ranks around (unnanotaed) let-bindings or perhaps the case you
 are
 describing is that of annotated local-let bindings.  So below, I'll asume
 that you do generalize then as in ML, and I'll describe how ranks can work
 for ML (formally, you can see [1], which has later be generalized by
 typing
 constraints [2]).

 You say that you want to increase the rank on RHS of a Let-bindings, but I
 do not see why. Or is it a typo and you meant LHS?

 In ML, we increase the rank on LHS of a let-bindings, because this is the
 type that we will have to generalize.  So when generalizing we just have
 to
 pick variables of higher-rank (i.e. those introduced during the type
 checking of the LHS that haven't be downgraded during resolution of the
 constraint). More precisely, "let x = a1 in a2" is typechecked at rank n
 as follows:

 1) typecheck a1 at rank (n+1): this generates constraint C with fresh
    variables/nodes introduced at rank (n+1).

 2) solve the fresh part of the constraint (that at rank n+1); this may
    downgrade some fresh nodes to rank n or lower.

 3) generalize nodes that remain at rank (n+1); this returns a type scheme
 S.

 4) typecheck a2 at rank n in the environment extended with x : S.

 In particular, I do not understand why you would increase the level when
 typechecking the RHS. You just return to the level n at which the whole
 let-biding is being typechecked.

 In step 2, variables may be downgraded to lower ranks in two cases:

 1) when they have to be unified with a type of a lower rank (either one
 that
    has to be of a lower rank, e.g. a type variable introduced at a lower
    rank,

 2) when they are equal to a term whose variables are all of lower rank.

 My understanding is that Step 2 is what you describe as one of the
 problem.

 Steps 1) and 2) can also be explained in term of typing constraints as
 presented in [2]. At generalization points it is useful to remove useless
 quantifications (which would be correct but unnecessarily copy too much of
 the type scheme). This is done by rule C-LetApp (p. 32) that transforms a
 constraints:

         let x : forall (Xs, Ys | C1) T in C2
 into
         exists (Ys) let x : forall (Xs | C1) T in C2

 provided "Ys" are disjoint from "ftv (C2)" and "exists (Xs) C1
 _dertermines_
 Ys".  Here, turning "all (Ys)" into "exist (YS)" amounts to decreasing the
 rank of "Ys". The definition of "determines" is semantical at this point,
 but we later give syntactic sufficient conditions in the case of equality
 constraints (lemma 1.8.7 on page 82) which, as explained on p. 83,
 includes
 the two cases corresponding the ones above:

 1) a variable X may be moved to Ys when it is dominated by a node of lower
    rank (a free variable exists (Xs) C1).

 2) a variable X may be moved to Ys when all variables it dominates are
    already in Ys.

 So it does not harm at all to keep delayed constraints in type schemes,
 but
 1) the generic part of the constraint should be simplified, so as to
 ensure
 that the (generic part of the) type scheme is solvable and 2) delayed
 constraints must be (carefully) taken into account at generalisation time
 to
 avoid generalizing too many type variables (those that are "determined"
 from
 the context)

 I hope I haven't completely misunderstood your problem...

         Didier

 [1] http://hal.inria.fr/docs/00/07/70/06/PS/RR-1766.ps)

 [2] ATTAPL, the essence of ML. (Page numbers refers to the online draft
     version http://cristal.inria.fr/attapl/preversion.ps.gz)

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8995#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler