add -fsimpleopt-before-flatten

[ghc-hetmet.git] / compiler / typecheck / TcSimplify.lhs

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index ec6adc8..cf41372 100644 (file)
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -49,7 +49,7 @@ simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
 -- but when there is nothing to quantify we don't wrap
 -- in a degenerate implication, so we do that here instead
 simplifyTop wanteds 
 -- but when there is nothing to quantify we don't wrap
 -- in a degenerate implication, so we do that here instead
 simplifyTop wanteds 

-  = simplifyCheck SimplCheck wanteds
+  = simplifyCheck (SimplCheck (ptext (sLit "top level"))) wanteds

 
 ------------------
 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
 
 ------------------
 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)

@@ -61,7 +61,8 @@ simplifyDefault :: ThetaType  -- Wanted; has no type variables in it
                 -> TcM ()      -- Succeeds iff the constraint is soluble
 simplifyDefault theta
   = do { wanted <- newFlatWanteds DefaultOrigin theta
                 -> TcM ()      -- Succeeds iff the constraint is soluble
 simplifyDefault theta
   = do { wanted <- newFlatWanteds DefaultOrigin theta

-       ; _ignored_ev_binds <- simplifyCheck SimplCheck (mkFlatWC wanted)
+       ; _ignored_ev_binds <- simplifyCheck (SimplCheck (ptext (sLit "defaults"))) 
+                                            (mkFlatWC wanted)

        ; return () }
 \end{code}
 
        ; return () }
 \end{code}
 

@@ -75,27 +76,29 @@ simplifyDefault theta
 
 \begin{code}
 simplifyDeriv :: CtOrigin
 
 \begin{code}
 simplifyDeriv :: CtOrigin

-               -> [TyVar]      
-               -> ThetaType            -- Wanted
-               -> TcM ThetaType        -- Needed
+              -> PredType
+             -> [TyVar]        
+             -> ThetaType              -- Wanted
+             -> TcM ThetaType  -- Needed

 -- Given  instance (wanted) => C inst_ty 
 -- Simplify 'wanted' as much as possibles
 -- Fail if not possible
 -- Given  instance (wanted) => C inst_ty 
 -- Simplify 'wanted' as much as possibles
 -- Fail if not possible

-simplifyDeriv orig tvs theta 
-  = do { tvs_skols <- tcInstSuperSkolTyVars tvs -- Skolemize
-                          -- One reason is that the constraint solving machinery
-                  -- expects *TcTyVars* not TyVars.  Another is that
-                  -- when looking up instances we don't want overlap
-                  -- of type variables
+simplifyDeriv orig pred tvs theta 
+  = do { tvs_skols <- tcInstSkolTyVars tvs -- Skolemize
+               -- The constraint solving machinery 
+               -- expects *TcTyVars* not TyVars.  
+               -- We use *non-overlappable* (vanilla) skolems
+               -- See Note [Overlap and deriving]

 
        ; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
              subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
 
        ; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
              subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs

+            doc = parens $ ptext (sLit "deriving") <+> parens (ppr pred)

 
        ; wanted <- newFlatWanteds orig (substTheta skol_subst theta)
 
        ; traceTc "simplifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
        ; (residual_wanted, _binds)
 
        ; wanted <- newFlatWanteds orig (substTheta skol_subst theta)
 
        ; traceTc "simplifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
        ; (residual_wanted, _binds)

-             <- runTcS SimplInfer NoUntouchables $
+             <- runTcS (SimplInfer doc) NoUntouchables $

                 solveWanteds emptyInert (mkFlatWC wanted)
 
        ; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted)
                 solveWanteds emptyInert (mkFlatWC wanted)
 
        ; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted)

@@ -111,6 +114,31 @@ simplifyDeriv orig tvs theta
        ; return (substTheta subst_skol min_theta) }
 \end{code}
 
        ; return (substTheta subst_skol min_theta) }
 \end{code}
 

+Note [Overlap and deriving]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider some overlapping instances:
+  data Show a => Show [a] where ..
+  data Show [Char] where ...
+
+Now a data type with deriving:
+  data T a = MkT [a] deriving( Show )
+
+We want to get the derived instance
+  instance Show [a] => Show (T a) where...
+and NOT
+  instance Show a => Show (T a) where...
+so that the (Show (T Char)) instance does the Right Thing
+
+It's very like the situation when we're inferring the type
+of a function
+   f x = show [x]
+and we want to infer
+   f :: Show [a] => a -> String
+
+BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
+             the context for the derived instance. 
+            Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
+

 Note [Exotic derived instance contexts]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In a 'derived' instance declaration, we *infer* the context.  It's a
 Note [Exotic derived instance contexts]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In a 'derived' instance declaration, we *infer* the context.  It's a

@@ -222,7 +250,7 @@ simplifyInfer top_lvl apply_mr name_taus wanteds
             -- Step 2 
                    -- Now simplify the possibly-bound constraints
        ; (simpl_results, tc_binds0)
             -- Step 2 
                    -- Now simplify the possibly-bound constraints
        ; (simpl_results, tc_binds0)

-           <- runTcS SimplInfer NoUntouchables $
+           <- runTcS (SimplInfer (ppr (map fst name_taus))) NoUntouchables $

               simplifyWithApprox (zonked_wanteds { wc_flat = perhaps_bound })
 
        ; when (insolubleWC simpl_results)  -- Fail fast if there is an insoluble constraint
               simplifyWithApprox (zonked_wanteds { wc_flat = perhaps_bound })
 
        ; when (insolubleWC simpl_results)  -- Fail fast if there is an insoluble constraint

@@ -522,7 +550,7 @@ simplifyRule name tv_bndrs lhs_wanted rhs_wanted
                 -- variables; hence *no untouchables*
 
        ; (lhs_results, lhs_binds)
                 -- variables; hence *no untouchables*
 
        ; (lhs_results, lhs_binds)

-              <- runTcS SimplRuleLhs untch $
+              <- runTcS (SimplRuleLhs name) untch $

                  solveWanteds emptyInert zonked_lhs
 
        ; traceTc "simplifyRule" $
                  solveWanteds emptyInert zonked_lhs
 
        ; traceTc "simplifyRule" $

@@ -564,7 +592,8 @@ simplifyRule name tv_bndrs lhs_wanted rhs_wanted
 
             -- Hence the rather painful ad-hoc treatement here
        ; rhs_binds_var@(EvBindsVar evb_ref _)  <- newTcEvBinds
 
             -- Hence the rather painful ad-hoc treatement here
        ; rhs_binds_var@(EvBindsVar evb_ref _)  <- newTcEvBinds

-       ; rhs_binds1 <- simplifyCheck SimplCheck $
+       ; let doc = ptext (sLit "rhs of rule") <+> doubleQuotes (ftext name)
+       ; rhs_binds1 <- simplifyCheck (SimplCheck doc) $

             WC { wc_flat = emptyBag
                , wc_insol = emptyBag
                , wc_impl = unitBag $
             WC { wc_flat = emptyBag
                , wc_insol = emptyBag
                , wc_impl = unitBag $

@@ -743,13 +772,14 @@ solveNestedImplications just_given_inert unsolved_cans implics
   | otherwise 
   = do {  -- See Note [Preparing inert set for implications]
          -- Push the unsolved wanteds inwards, but as givens
   | otherwise 
   = do {  -- See Note [Preparing inert set for implications]
          -- Push the unsolved wanteds inwards, but as givens

-         traceTcS "solveWanteds: preparing inerts for implications {"  empty
-     
-       ; let pushed_givens    = givensFromWanteds unsolved_cans
+         let pushed_givens    = givensFromWanteds unsolved_cans

              tcs_untouchables = filterVarSet isFlexiTcsTv $
                                 tyVarsOfEvVarXs pushed_givens
              -- See Note [Extra TcsTv untouchables]
 
              tcs_untouchables = filterVarSet isFlexiTcsTv $
                                 tyVarsOfEvVarXs pushed_givens
              -- See Note [Extra TcsTv untouchables]
 

+       ; traceTcS "solveWanteds: preparing inerts for implications {"  
+                  (vcat [ppr tcs_untouchables, ppr pushed_givens])
+     

        ; (_, inert_for_implics) <- solveInteract just_given_inert pushed_givens
 
        ; traceTcS "solveWanteds: } now doing nested implications {" $
        ; (_, inert_for_implics) <- solveInteract just_given_inert pushed_givens
 
        ; traceTcS "solveWanteds: } now doing nested implications {" $

@@ -932,10 +962,10 @@ NB: A consequence is that every simplifier-generated TcsTv variable
     constraints. In effect, by floating an equality out of the
     implication we are committing to have it solved in the outside.
 
     constraints. In effect, by floating an equality out of the
     implication we are committing to have it solved in the outside.
 

-NB: A consequence is that every simplifier-generated TcsTv variable that gets floated out 
-    of an implication becomes now untouchable next time we go inside that implication to 
-    solve any residual constraints. In effect, by floating an equality out of the implication 
-    we are committing to have it solved in the outside. 
+Note [Float Equalities out of Implications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
+We want to float equalities out of vanilla existentials, but *not* out 
+of GADT pattern matches. 

 
 
 \begin{code}
 
 
 \begin{code}

@@ -956,7 +986,7 @@ solveCTyFunEqs cts
 
       ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
   where
 
       ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
   where

-    solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setWantedCoBind cv ty
+    solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setCoBind cv ty

 
 ------------
 type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])
 
 ------------
 type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])