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


Ignore:
Timestamp:
Dec 9, 2012 4:58:13 PM (3 years 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