Comments and white space only
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 14 Apr 2015 08:21:27 +0000 (09:21 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 14 Apr 2015 08:22:04 +0000 (09:22 +0100)
compiler/typecheck/TcFlatten.hs
compiler/typecheck/TcRules.hs

index cd7c3d6..89431f8 100644 (file)
@@ -553,7 +553,7 @@ instance Applicative FlatM where
 
 liftTcS :: TcS a -> FlatM a
 liftTcS thing_inside
-  = FlatM $ const thing_inside 
+  = FlatM $ const thing_inside
 
 emitFlatWork :: Ct -> FlatM ()
 -- See Note [The flattening work list]
@@ -622,7 +622,7 @@ setEqRel new_eq_rel thing_inside
     if new_eq_rel == fe_eq_rel env
     then runFlatM thing_inside env
     else runFlatM thing_inside (env { fe_eq_rel = new_eq_rel })
-    
+
 -- | Change the 'FlattenMode' in a 'FlattenEnv'.
 setMode :: FlattenMode -> FlatM a -> FlatM a
 setMode new_mode thing_inside
index 1684118..084e5de 100644 (file)
@@ -227,11 +227,15 @@ revert to SimplCheck when going under an implication.
 
 ------------------------ So the plan is this -----------------------
 
+* Step 0: typecheck the LHS and RHS to get constraints from each
+
 * Step 1: Simplify the LHS and RHS constraints all together in one bag
           We do this to discover all unification equalities
 
-* Step 2: Zonk the ORIGINAL lhs constraints, and partition them into
-          the ones we will quantify over, and the others
+* Step 2: Zonk the ORIGINAL (unsimplified) lhs constraints, to take
+          advantage of those unifications, and partition them into the
+          ones we will quantify over, and the others
+          See Note [RULE quantification over equalities]
 
 * Step 3: Decide on the type variables to quantify over
 
@@ -251,7 +255,7 @@ From the RULE we get
    lhs-constraints:  T Int ~ alpha
    rhs-constraints:  Bool ~ alpha
 where 'alpha' is the type that connects the two.  If we glom them
-all together, and solve the RHS constraint first, we might solve 
+all together, and solve the RHS constraint first, we might solve
 with alpha := Bool.  But then we'd end up with a RULE like
 
     RULE: f 3 |> (co :: T Int ~ Booo) = True