Skip to content
  • Simon Peyton Jones's avatar
    A collection of type-inference refactorings. · 3f5673f3
    Simon Peyton Jones authored
    This patch does a raft of useful tidy-ups in the type checker.
    I've been meaning to do this for some time, and finally made
    time to do it en route to ICFP.
    
    1. Modify TcType.ExpType to make a distinct data type,
       InferResult for the Infer case, and consequential
       refactoring.
    
    2. Define a new function TcUnify.fillInferResult, to fill in
       an InferResult. It uses TcMType.promoteTcType to promote
       the type to the level of the InferResult.
       See TcMType Note [Promoting a type]
       This refactoring is in preparation for an improvement
       to typechecking pattern bindings, coming next.
    
       I flirted with an elaborate scheme to give better
       higher rank inference, but it was just too complicated.
       See TcMType Note [Promotion and higher rank types]
    
    3. Add to InferResult a new field ir_inst :: Bool to say
       whether or not the type used to fill in the
       InferResult should be deeply instantiated.  See
       TcUnify Note [Deep instantiation of InferResult].
    
    4. Add a TcLevel to SkolemTvs. This will be useful generally
    
        - it's a fast way to see if the type
          variable escapes when floating (not used yet)
    
        - it provides a good consistency check when updating a
          unification variable (TcMType.writeMetaTyVarRef, the
          level_check_ok check)
    
       I originally had another reason (related to the flirting
       in (2), but I left it in because it seems like a step in
       the right direction.
    
    5. Reduce and simplify the plethora of uExpType,
       tcSubType and related functions in TcUnify.  It was
       such an opaque mess and it's still not great, but it's
       better.
    
    6. Simplify the uo_expected field of TypeEqOrigin.  Richard
       had generatlised it to a ExpType, but it was almost always
       a Check type.  Now it's back to being a plain TcType which
       is much, much easier.
    
    7. Improve error messages by refraining from skolemisation when
       it's clear that there's an error: see
       TcUnify Note [Don't skolemise unnecessarily]
    
    8. Type.isPiTy and isForAllTy seem to be missing a coreView check,
       so I added it
    
    9. Kill off tcs_used_tcvs.  Its purpose is to track the
       givens used by wanted constraints.  For dictionaries etc
       we do that via the free vars of the /bindings/ in the
       implication constraint ic_binds.  But for coercions we
       just do update-in-place in the type, rather than
       generating a binding.  So we need something analogous to
       bindings, to track what coercions we have added.
    
       That was the purpose of tcs_used_tcvs.  But it only
       worked for a /single/ iteration, whereas we may have
       multiple iterations of solving an implication.  Look
       at (the old) 'setImplicationStatus'.  If the constraint
       is unsolved, it just drops the used_tvs on the floor.
       If it becomes solved next time round, we'll pick up
       coercions used in that round, but ignore ones used in
       the first round.
    
       There was an outright bug.  Result = (potentialy) bogus
       unused-constraint errors.  Constructing a case where this
       actually happens seems quite trick so I did not do so.
    
       Solution: expand EvBindsVar to include the (free vars of
       the) coercions, so that the coercions are tracked in
       essentially the same way as the bindings.
    
       This turned out to be much simpler.  Less code, more
       correct.
    
    10. Make the ic_binds field in an implication have type
          ic_binds :: EvBindsVar
        instead of (as previously)
           ic_binds :: Maybe EvBindsVar
        This is notably simpler, and faster to use -- less
        testing of the Maybe.  But in the occaional situation
        where we don't have anywhere to put the bindings, the
        belt-and-braces error check is lost.  So I put it back
        as an ASSERT in 'setImplicationStatus' (see the use of
        'termEvidenceAllowed')
    
    All these changes led to quite bit of error message wibbling
    3f5673f3