Changes between Version 1 and Version 2 of Commentary/Compiler/TypeNatSolver


Ignore:
Timestamp:
Dec 9, 2012 4:58:13 PM (17 months ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Commentary/Compiler/TypeNatSolver

    v1 v2  
    7474inert set back to the work queue.   We DON'T do this, because it is 
    7575quite inefficient: there is no obvious way to compute which "wanted"s 
    76 might be affected, so we have to restart all of them!. 
     76might be affected, so we have to restart all of them! 
    7777 
    7878The heart of the interaction is the function `interactCt`, which 
     
    9696 
    9797 
     98=== Derived Constraints === 
    9899 
     100"Derived" constraints are facts that are implied by the constraints 
     101in the inert set.  They do not have complete proofs because their 
     102proof may depend on proofs of as yet unsolved "wanted" constraints. 
     103GHC does not associate any proof terms with "derived" constraints. 
     104In the constraint solver, they are mostly used as "hints".  For example, 
     105consider the wanted constraint {{{5 + 3 ~ x}}}, where {{{x}}} is a 
     106free unification variable.  These are the steps we'll take to solve 
     107the constraint: 
     108 
     109{{{ 
     110    Rules: 
     111    Add_def(5,3) : 5 + 3 ~ 8 
     112    Add_fun : forall a b c1 c2. (a + b ~ c1, a + b ~ c2) => c1 ~ c2 
     113 
     114    1. Add [W] C: 5 + 3 ~ x to inert set 
     115    2. Generate new derived: 
     116     [D] Add_fun(C,Add_def) : x ~ 8   (proof discarded) 
     117    3. GHC uses this hint to improve the wanted to [W] C: 5 + 3 ~ 8 
     118    4. Solved: 
     119     [W] C = Add_def(5,3) 
     120}}} 
     121 
     122 
     123 
     124 
     125 
     126 
     127 
     128 
     129 
     130 
     131 
     132 
     133 
     134 
     135 
     136