Skip to content
  • Simon Peyton Jones's avatar
    Allow full constraint solving under a for-all (Trac #5595) · 2e6dcdf7
    Simon Peyton Jones authored
    The main idea is that when we unify
        forall a. t1  ~  forall a. t2
    we get constraints from unifying t1~t2 that mention a.
    We are producing a coercion witnessing the equivalence of
    the for-alls, and inside *that* coercion we need bindings
    for the solved constraints arising from t1~t2.
    
    We didn't have way to do this before.  The big change is
    that here's a new type TcEvidence.TcCoercion, which is
    much like Coercion.Coercion except that there's a slot
    for TcEvBinds in it.
    
    This has a wave of follow-on changes. Not deep but broad.
    
    * New module TcEvidence, which now contains the HsWrapper
      TcEvBinds, EvTerm etc types that used to be in HsBinds
    
    * The typechecker works exclusively in terms of TcCoercion.
    
    * The desugarer converts TcCoercion to Coercion
    
    * The main payload is in TcUnify.unifySigmaTy. This is the
      function that had a gross hack before, but is now beautiful.
    
    * LCoercion is gone!  Hooray.
    
    Many many fiddly changes in conssequence.  But it's nice.
    2e6dcdf7