Big tidy-up of deriving code

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

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 182a7c5..342114b 100644 (file)
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -28,11 +28,10 @@ import Inst
 import TcEnv
 import InstEnv
 import TcGadt
 import TcEnv
 import InstEnv
 import TcGadt

-import TcMType

 import TcType
 import TcType

+import TcMType

 import TcIface
 import Var
 import TcIface
 import Var

-import TyCon

 import Name
 import NameSet
 import Class
 import Name
 import NameSet
 import Class

@@ -657,7 +656,7 @@ tcSimplifyInfer
        :: SDoc
        -> TcTyVarSet           -- fv(T); type vars
        -> [Inst]               -- Wanted
        :: SDoc
        -> TcTyVarSet           -- fv(T); type vars
        -> [Inst]               -- Wanted

-       -> TcM ([TcTyVar],      -- Tyvars to quantify (zonked)
+       -> TcM ([TcTyVar],      -- Tyvars to quantify (zonked and quantified)

                [Inst],         -- Dict Ids that must be bound here (zonked)
                TcDictBinds)    -- Bindings
        -- Any free (escaping) Insts are tossed into the environment
                [Inst],         -- Dict Ids that must be bound here (zonked)
                TcDictBinds)    -- Bindings
        -- Any free (escaping) Insts are tossed into the environment

@@ -848,6 +847,7 @@ bindIrredsR loc qtvs co_vars reft givens irreds
   | otherwise
   = do { let givens' = filter isDict givens
                -- The givens can include methods
   | otherwise
   = do { let givens' = filter isDict givens
                -- The givens can include methods

+               -- See Note [Pruning the givens in an implication constraint]

 
           -- If there are no 'givens', then it's safe to 
           -- partition the 'wanteds' by their qtvs, thereby trimming irreds
 
           -- If there are no 'givens', then it's safe to 
           -- partition the 'wanteds' by their qtvs, thereby trimming irreds

@@ -1171,7 +1171,7 @@ tcSimplifyRestricted      -- Used for restricted binding groups
        -> [Name]               -- Things bound in this group
        -> TcTyVarSet           -- Free in the type of the RHSs
        -> [Inst]               -- Free in the RHSs
        -> [Name]               -- Things bound in this group
        -> TcTyVarSet           -- Free in the type of the RHSs
        -> [Inst]               -- Free in the RHSs

-       -> TcM ([TyVar],        -- Tyvars to quantify (zonked)
+       -> TcM ([TyVar],        -- Tyvars to quantify (zonked and quantified)

                TcDictBinds)    -- Bindings
        -- tcSimpifyRestricted returns no constraints to
        -- quantify over; by definition there are none.
                TcDictBinds)    -- Bindings
        -- tcSimpifyRestricted returns no constraints to
        -- quantify over; by definition there are none.

@@ -1876,6 +1876,20 @@ We can satisfy the (C Int) from the superclass of D, so we don't want
 to float the (C Int) out, even though it mentions no type variable in
 the constraints!
 
 to float the (C Int) out, even though it mentions no type variable in
 the constraints!
 

+Note [Pruning the givens in an implication constraint]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are about to form the implication constraint
+       forall tvs.  Eq a => Ord b
+The (Eq a) cannot contribute to the (Ord b), because it has no access to
+the type variable 'b'.  So we could filter out the (Eq a) from the givens.
+
+Doing so would be a bit tidier, but all the implication constraints get
+simplified away by the optimiser, so it's no great win.   So I don't take
+advantage of that at the moment.
+
+If you do, BE CAREFUL of wobbly type variables.
+
+

 %************************************************************************
 %*                                                                     *
                Avails and AvailHow: the pool of evidence
 %************************************************************************
 %*                                                                     *
                Avails and AvailHow: the pool of evidence

@@ -2330,55 +2344,31 @@ instance declarations.
 
 \begin{code}
 tcSimplifyDeriv :: InstOrigin
 
 \begin{code}
 tcSimplifyDeriv :: InstOrigin

-                -> TyCon

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

+-- Given  instance (wanted) => C inst_ty 
+-- Simplify 'wanted' as much as possible
+-- The inst_ty is needed only for the termination check

 
 

-tcSimplifyDeriv orig tc tyvars theta
-  = tcInstTyVars tyvars                        `thenM` \ (tvs, _, tenv) ->
+tcSimplifyDeriv orig tyvars theta
+  = do { (tvs, _, tenv) <- tcInstTyVars tyvars

        -- The main loop may do unification, and that may crash if 
        -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
        -- ToDo: what if two of them do get unified?
        -- The main loop may do unification, and that may crash if 
        -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
        -- ToDo: what if two of them do get unified?

-    newDictBndrsO orig (substTheta tenv theta) `thenM` \ wanteds ->
-    topCheckLoop doc wanteds                   `thenM` \ (irreds, _) ->
-
-    doptM Opt_GlasgowExts                      `thenM` \ gla_exts ->
-    doptM Opt_AllowUndecidableInstances                `thenM` \ undecidable_ok ->
-    let
-       inst_ty = mkTyConApp tc (mkTyVarTys tvs)
-       (ok_insts, bad_insts) = partition is_ok_inst irreds
-       is_ok_inst inst
-          = isDict inst        -- Exclude implication consraints
-          && (isTyVarClassPred pred || (gla_exts && ok_gla_pred pred))
-          where
-            pred = dictPred inst
-
-       ok_gla_pred pred = null (checkInstTermination [inst_ty] [pred])
-               -- See Note [Deriving context]
-          
-       tv_set = mkVarSet tvs
-       simpl_theta = map dictPred ok_insts
-       weird_preds = [pred | pred <- simpl_theta
-                           , not (tyVarsOfPred pred `subVarSet` tv_set)]  
-
-         -- Check for a bizarre corner case, when the derived instance decl should
-         -- have form  instance C a b => D (T a) where ...
-         -- Note that 'b' isn't a parameter of T.  This gives rise to all sorts
-         -- of problems; in particular, it's hard to compare solutions for
-         -- equality when finding the fixpoint.  So I just rule it out for now.
-       
-       rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
+       ; wanteds <- newDictBndrsO orig (substTheta tenv theta)
+       ; (irreds, _) <- topCheckLoop doc wanteds
+
+       ; let (dicts, non_dicts) = partition isDict irreds
+                                       -- Exclude implication consraints
+       ; addNoInstanceErrs non_dicts   -- I'm not sure if these can really happen
+
+       ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
+             simpl_theta = substTheta rev_env (map dictPred dicts)

                -- This reverse-mapping is a Royal Pain, 
                -- but the result should mention TyVars not TcTyVars
                -- This reverse-mapping is a Royal Pain, 
                -- but the result should mention TyVars not TcTyVars

-    in
-       -- In effect, the bad and wierd insts cover all of the cases that
-       -- would make checkValidInstance fail; if it were called right after tcSimplifyDeriv
-       --   * wierd_preds ensures unambiguous instances (checkAmbiguity in checkValidInstance)
-       --   * ok_gla_pred ensures termination (checkInstTermination in checkValidInstance)
-    addNoInstanceErrs bad_insts                                `thenM_`
-    mapM_ (addErrTc . badDerivedPred) weird_preds      `thenM_`
-    returnM (substTheta rev_env simpl_theta)
+
+       ; return simpl_theta }

   where
     doc = ptext SLIT("deriving classes for a data type")
 \end{code}
   where
     doc = ptext SLIT("deriving classes for a data type")
 \end{code}

@@ -2652,12 +2642,6 @@ warnDefault ups default_ty
                                quotes (ppr default_ty),
                      pprDictsInFull tidy_dicts]
 
                                quotes (ppr default_ty),
                      pprDictsInFull tidy_dicts]
 

--- Used for the ...Thetas variants; all top level
-badDerivedPred pred
-  = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
-         ptext SLIT("type variables that are not data type parameters"),
-         nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
-

 reduceDepthErr n stack
   = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
          ptext SLIT("Use -fcontext-stack=N to increase stack size to N"),
 reduceDepthErr n stack
   = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
          ptext SLIT("Use -fcontext-stack=N to increase stack size to N"),