Fix Trac #5048: location on AbsBinds

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

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index ec6adc8..eecfb27 100644 (file)
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -82,11 +82,11 @@ simplifyDeriv :: CtOrigin
 -- Simplify 'wanted' as much as possibles
 -- Fail if not possible
 simplifyDeriv orig tvs theta 
 -- 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
+  = 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

@@ -111,6 +111,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

@@ -743,13 +768,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 +958,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 +982,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)])