Massive patch for the first months work adding System FC to GHC #34
[ghc-hetmet.git] / compiler / typecheck / TcSimplify.lhs
index 7656198..8f06270 100644 (file)
@@ -9,7 +9,7 @@
 module TcSimplify (
        tcSimplifyInfer, tcSimplifyInferCheck,
        tcSimplifyCheck, tcSimplifyRestricted,
-       tcSimplifyToDicts, tcSimplifyIPs, 
+       tcSimplifyRuleLhs, tcSimplifyIPs, 
        tcSimplifySuperClasses,
        tcSimplifyTop, tcSimplifyInteractive,
        tcSimplifyBracket,
@@ -21,9 +21,9 @@ module TcSimplify (
 #include "HsVersions.h"
 
 import {-# SOURCE #-} TcUnify( unifyType )
-import TypeRep         ( Type(..) )
-import HsSyn           ( HsBind(..), HsExpr(..), LHsExpr, emptyLHsBinds )
-import TcHsSyn         ( mkHsApp, mkHsTyApp, mkHsDictApp )
+import HsSyn           ( HsBind(..), HsExpr(..), LHsExpr, 
+                         ExprCoFn(..), (<.>), nlHsTyApp, emptyLHsBinds )
+import TcHsSyn         ( mkHsApp )
 
 import TcRnMonad
 import Inst            ( lookupInst, LookupInstResult(..),
@@ -32,7 +32,7 @@ import Inst           ( lookupInst, LookupInstResult(..),
                          isMethodFor, isMethod,
                          instToId, tyVarsOfInsts,  cloneDict,
                          ipNamesOfInsts, ipNamesOfInst, dictPred,
-                         fdPredsOfInst,
+                         fdPredsOfInst, mkInstCoFn,
                          newDictsAtLoc, tcInstClassOp,
                          getDictClassTys, isTyVarDict, instLoc,
                          zonkInst, tidyInsts, tidyMoreInsts,
@@ -42,8 +42,7 @@ import Inst           ( lookupInst, LookupInstResult(..),
 import TcEnv           ( tcGetGlobalTyVars, tcLookupId, findGlobals, pprBinders,
                          lclEnvElts, tcMetaTy )
 import InstEnv         ( lookupInstEnv, classInstances, pprInstances )
-import TcMType         ( zonkTcTyVarsAndFV, tcInstTyVars, zonkTcPredType,
-                         checkAmbiguity, checkInstTermination )
+import TcMType         ( zonkTcTyVarsAndFV, tcInstTyVars, zonkTcPredType  )
 import TcType          ( TcTyVar, TcTyVarSet, ThetaType, TcPredType, tidyPred,
                           mkClassPred, isOverloadedTy, mkTyConApp, isSkolemTyVar,
                          mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
@@ -72,8 +71,9 @@ import ListSetOps     ( equivClasses )
 import Util            ( zipEqual, isSingleton )
 import List            ( partition )
 import SrcLoc          ( Located(..) )
-import DynFlags                ( DynFlag(..) )
-import StaticFlags
+import DynFlags                ( DynFlags(ctxtStkDepth), 
+                         DynFlag( Opt_GlasgowExts, Opt_AllowUndecidableInstances, 
+                         Opt_WarnTypeDefaults, Opt_ExtendedDefaultRules ) )
 \end{code}
 
 
@@ -87,6 +87,24 @@ import StaticFlags
        Notes on functional dependencies (a bug)
        --------------------------------------
 
+Consider this:
+
+       class C a b | a -> b
+       class D a b | a -> b
+
+       instance D a b => C a b -- Undecidable 
+                               -- (Not sure if it's crucial to this eg)
+       f :: C a b => a -> Bool
+       f _ = True
+       
+       g :: C a b => a -> Bool
+       g = f
+
+Here f typechecks, but g does not!!  Reason: before doing improvement,
+we reduce the (C a b1) constraint from the call of f to (D a b1).
+
+Here is a more complicated example:
+
 | > class Foo a b | a->b
 | >
 | > class Bar a b | a->b
@@ -258,9 +276,9 @@ any other type variables.
 
 
 
-       --------------------------------------
-               Notes on ambiguity
-       --------------------------------------
+-------------------------------------
+       Note [Ambiguity]
+-------------------------------------
 
 It's very hard to be certain when a type is ambiguous.  Consider
 
@@ -923,7 +941,8 @@ Two more nasty cases are in
 tcSimplifySuperClasses qtvs givens sc_wanteds
   = ASSERT( all isSkolemTyVar qtvs )
     do { (_, frees, binds1) <- tcSimplCheck doc get_qtvs NoSCs givens sc_wanteds
-       ; binds2             <- tc_simplify_top doc False NoSCs frees
+       ; ext_default        <- doptM Opt_ExtendedDefaultRules
+       ; binds2             <- tc_simplify_top doc ext_default NoSCs frees
        ; return (binds1 `unionBags` binds2) }
   where
     get_qtvs = return (mkVarSet qtvs)
@@ -1048,8 +1067,6 @@ tcSimplifyRestricted      -- Used for restricted binding groups
 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        -- Zonk everything in sight
   = mappM zonkInst wanteds                     `thenM` \ wanteds' ->
-    zonkTcTyVarsAndFV (varSetElems tau_tvs)    `thenM` \ tau_tvs' ->
-    tcGetGlobalTyVars                          `thenM` \ gbl_tvs' ->
 
        -- 'reduceMe': Reduce as far as we can.  Don't stop at
        -- dicts; the idea is to get rid of as many type
@@ -1058,25 +1075,30 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        -- immediately, with no constraint on s.
        --
        -- BUT do no improvement!  See Plan D above
+       -- HOWEVER, some unification may take place, if we instantiate
+       --          a method Inst with an equality constraint
     reduceContextWithoutImprovement 
        doc reduceMe wanteds'           `thenM` \ (_frees, _binds, constrained_dicts) ->
 
        -- Next, figure out the tyvars we will quantify over
+    zonkTcTyVarsAndFV (varSetElems tau_tvs)    `thenM` \ tau_tvs' ->
+    tcGetGlobalTyVars                          `thenM` \ gbl_tvs' ->
+    mappM zonkInst constrained_dicts           `thenM` \ constrained_dicts' ->
     let
-       constrained_tvs = tyVarsOfInsts constrained_dicts
-       qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
-                        `minusVarSet` constrained_tvs
+       constrained_tvs' = tyVarsOfInsts constrained_dicts'
+       qtvs' = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
+                        `minusVarSet` constrained_tvs'
     in
     traceTc (text "tcSimplifyRestricted" <+> vcat [
-               pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts,
+               pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts',
                ppr _binds,
-               ppr constrained_tvs, ppr tau_tvs', ppr qtvs ])  `thenM_`
+               ppr constrained_tvs', ppr tau_tvs', ppr qtvs' ])        `thenM_`
 
        -- The first step may have squashed more methods than
        -- necessary, so try again, this time more gently, knowing the exact
        -- set of type variables to quantify over.
        --
-       -- We quantify only over constraints that are captured by qtvs;
+       -- We quantify only over constraints that are captured by qtvs';
        -- these will just be a subset of non-dicts.  This in contrast
        -- to normal inference (using isFreeWhenInferring) in which we quantify over
        -- all *non-inheritable* constraints too.  This implements choice
@@ -1090,7 +1112,7 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        -- expose implicit parameters to the test that follows
     let
        is_nested_group = isNotTopLevel top_lvl
-        try_me inst | isFreeWrtTyVars qtvs inst,
+        try_me inst | isFreeWrtTyVars qtvs' inst,
                      (is_nested_group || isDict inst) = Free
                    | otherwise                        = ReduceMe AddSCs
     in
@@ -1101,20 +1123,20 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        -- See "Notes on implicit parameters, Question 4: top level"
     if is_nested_group then
        extendLIEs frees        `thenM_`
-        returnM (varSetElems qtvs, binds)
+        returnM (varSetElems qtvs', binds)
     else
        let
            (non_ips, bad_ips) = partition isClassDict frees
        in    
        addTopIPErrs bndrs bad_ips      `thenM_`
        extendLIEs non_ips              `thenM_`
-        returnM (varSetElems qtvs, binds)
+        returnM (varSetElems qtvs', binds)
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection{tcSimplifyToDicts}
+               tcSimplifyRuleLhs
 %*                                                                     *
 %************************************************************************
 
@@ -1122,60 +1144,76 @@ On the LHS of transformation rules we only simplify methods and constants,
 getting dictionaries.  We want to keep all of them unsimplified, to serve
 as the available stuff for the RHS of the rule.
 
-The same thing is used for specialise pragmas. Consider
+Example.  Consider the following left-hand side of a rule
+       
+       f (x == y) (y > z) = ...
 
-       f :: Num a => a -> a
-       {-# SPECIALISE f :: Int -> Int #-}
-       f = ...
+If we typecheck this expression we get constraints
 
-The type checker generates a binding like:
+       d1 :: Ord a, d2 :: Eq a
 
-       f_spec = (f :: Int -> Int)
+We do NOT want to "simplify" to the LHS
 
-and we want to end up with
+       forall x::a, y::a, z::a, d1::Ord a.
+         f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
 
-       f_spec = _inline_me_ (f Int dNumInt)
+Instead we want        
 
-But that means that we must simplify the Method for f to (f Int dNumInt)!
-So tcSimplifyToDicts squeezes out all Methods.
+       forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
+         f ((==) d2 x y) ((>) d1 y z) = ...
 
-IMPORTANT NOTE:  we *don't* want to do superclass commoning up.  Consider
+Here is another example:
 
        fromIntegral :: (Integral a, Num b) => a -> b
        {-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
 
-Here, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont*
-want to get
+In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
+we *dont* want to get
 
        forall dIntegralInt.
-       fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
+          fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
 
 because the scsel will mess up RULE matching.  Instead we want
 
        forall dIntegralInt, dNumInt.
-       fromIntegral Int Int dIntegralInt dNumInt = id Int
+         fromIntegral Int Int dIntegralInt dNumInt = id Int
 
-Hence "WithoutSCs"
+Even if we have 
 
-\begin{code}
-tcSimplifyToDicts :: [Inst] -> TcM (TcDictBinds)
-tcSimplifyToDicts wanteds
-  = simpleReduceLoop doc try_me wanteds                `thenM` \ (frees, binds, irreds) ->
-       -- Since try_me doesn't look at types, we don't need to
-       -- do any zonking, so it's safe to call reduceContext directly
-    ASSERT( null frees )
-    extendLIEs irreds          `thenM_`
-    returnM binds
+       g (x == y) (y == z) = ..
 
-  where
-    doc = text "tcSimplifyToDicts"
+where the two dictionaries are *identical*, we do NOT WANT
 
-       -- Reduce methods and lits only; stop as soon as we get a dictionary
-    try_me inst        | isDict inst = KeepDictWithoutSCs      -- See notes above re "WithoutSCs"
-               | otherwise   = ReduceMe NoSCs
-\end{code}
+       forall x::a, y::a, z::a, d1::Eq a
+         f ((==) d1 x y) ((>) d1 y z) = ...
+
+because that will only match if the dict args are (visibly) equal.
+Instead we want to quantify over the dictionaries separately.
 
+In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving
+all dicts unchanged, with absolutely no sharing.  It's simpler to do this
+from scratch, rather than further parameterise simpleReduceLoop etc
 
+\begin{code}
+tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
+tcSimplifyRuleLhs wanteds
+  = go [] emptyBag wanteds
+  where
+    go dicts binds []
+       = return (dicts, binds)
+    go dicts binds (w:ws)
+       | isDict w
+       = go (w:dicts) binds ws
+       | otherwise
+       = do { w' <- zonkInst w  -- So that (3::Int) does not generate a call
+                                -- to fromInteger; this looks fragile to me
+            ; lookup_result <- lookupInst w'
+            ; case lookup_result of
+                GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws)
+                SimpleInst rhs  -> go dicts (addBind binds w rhs) ws
+                NoInstance      -> pprPanic "tcSimplifyRuleLhs" (ppr w)
+         }
+\end{code}
 
 tcSimplifyBracket is used when simplifying the constraints arising from
 a Template Haskell bracket [| ... |].  We want to check that there aren't
@@ -1321,9 +1359,6 @@ data WhatToDo
                        -- but don't produce an error message of any kind.
                        -- It might be quite legitimate such as (Eq a)!
 
- | KeepDictWithoutSCs  -- Return as irreducible; don't add its superclasses
-                       -- Rather specialised: see notes with tcSimplifyToDicts
-
  | DontReduceUnlessConstant    -- Return as irreducible unless it can
                                -- be reduced to a constant in one step
 
@@ -1434,6 +1469,7 @@ extractResults avails wanteds
                   new_binds  = addBind binds w rhs
                   new_avails = addToFM avails w (LinRhss rhss)
 
+       -- get_root is just used for Linear
     get_root irreds frees (Given id _) w = returnM (irreds, frees, id)
     get_root irreds frees Irred               w = cloneDict w  `thenM` \ w' ->
                                           returnM (w':irreds, frees, instToId w')
@@ -1457,10 +1493,6 @@ extractResults avails wanteds
        -- When simplifying with i,f free, we might still notice that
        --   t1=t3; but alas, the binding for t2 (which mentions t1)
        --   will continue to float out!
-       -- (split n i a) returns: n rhss
-       --                        auxiliary bindings
-       --                        1 or 0 insts to add to irreds
-
 
 split :: Int -> TcId -> TcId -> Inst 
       -> TcM (TcDictBinds, [LHsExpr TcId])
@@ -1510,7 +1542,7 @@ split n split_id root_id wanted
                       returnM (L span (VarBind x (mk_app span split_id rhs)),
                                [mk_fs_app span fst_id ty x, mk_fs_app span snd_id ty x])
 
-mk_fs_app span id ty var = L span (HsVar id) `mkHsTyApp` [ty,ty] `mkHsApp` (L span (HsVar var))
+mk_fs_app span id ty var = nlHsTyApp id [ty,ty] `mkHsApp` (L span (HsVar var))
 
 mk_app span id rhs = L span (HsApp (L span (HsVar id)) rhs)
 
@@ -1707,22 +1739,21 @@ I had to produce Y, to produce Y I had to produce Z, and so on.
 
 \begin{code}
 reduceList (n,stack) try_me wanteds state
-  | n > opt_MaxContextReductionDepth
-  = failWithTc (reduceDepthErr n stack)
-
-  | otherwise
-  =
+  = do         { dopts <- getDOpts
 #ifdef DEBUG
-   (if n > 8 then
-       pprTrace "Interesting! Context reduction stack deeper than 8:" 
-               (int n $$ ifPprDebug (nest 2 (pprStack stack)))
-    else (\x->x))
+       ; if n > 8 then
+               dumpTcRn (text "Interesting! Context reduction stack deeper than 8:" 
+                         <+> (int n $$ ifPprDebug (nest 2 (pprStack stack))))
+         else return ()
 #endif
-    go wanteds state
+       ; if n >= ctxtStkDepth dopts then
+           failWithTc (reduceDepthErr n stack)
+         else
+           go wanteds state }
   where
-    go []     state = returnM state
-    go (w:ws) state = reduce (n+1, w:stack) try_me w state     `thenM` \ state' ->
-                     go ws state'
+    go []     state = return state
+    go (w:ws) state = do { state' <- reduce (n+1, w:stack) try_me w state
+                        ; go ws state' }
 
     -- Base case: we're done!
 reduce stack try_me wanted avails
@@ -1737,8 +1768,6 @@ reduce stack try_me wanted avails
   | otherwise
   = case try_me wanted of {
 
-      KeepDictWithoutSCs -> addIrred NoSCs avails wanted
-
     ; DontReduceUnlessConstant ->    -- It's irreducible (or at least should not be reduced)
                                     -- First, see if the inst can be reduced to a constant in one step
        try_simple (addIrred AddSCs)    -- Assume want superclasses
@@ -1895,7 +1924,8 @@ addSCs is_loop avails dict
       | is_given sc_dict          = return avails
       | otherwise                 = addSCs is_loop avails' sc_dict
       where
-       sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
+       sc_sel_rhs = L (instSpan dict) (HsCoerce co_fn (HsVar sc_sel))
+       co_fn      = mkInstCoFn tys [dict]
        avails'    = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
 
     is_given :: Inst -> Bool
@@ -2005,7 +2035,8 @@ It's OK: the final zonking stage should zap y to (), which is fine.
 \begin{code}
 tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
 tcSimplifyTop wanteds
-  = tc_simplify_top doc False {- Not interactive loop -} AddSCs wanteds
+  = do         { ext_default <- doptM Opt_ExtendedDefaultRules
+       ; tc_simplify_top doc ext_default AddSCs wanteds }
   where 
     doc = text "tcSimplifyTop"
 
@@ -2016,7 +2047,7 @@ tcSimplifyInteractive wanteds
 
 -- The TcLclEnv should be valid here, solely to improve
 -- error message generation for the monomorphism restriction
-tc_simplify_top doc is_interactive want_scs wanteds
+tc_simplify_top doc use_extended_defaulting want_scs wanteds
   = do { lcl_env <- getLclEnv
        ; traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env))
 
@@ -2042,13 +2073,13 @@ tc_simplify_top doc is_interactive want_scs wanteds
                =  not (bad_tyvars `intersectsVarSet` tyVarsOfInst (head ds))
                && defaultable_classes (map get_clas ds)
            defaultable_classes clss 
-               | is_interactive = any isInteractiveClass clss
-               | otherwise      = all isStandardClass clss && any isNumericClass clss
+               | use_extended_defaulting = any isInteractiveClass clss
+               | otherwise = all isStandardClass clss && any isNumericClass clss
 
            isInteractiveClass cls = isNumericClass cls
                                  || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
-                       -- In interactive mode, we default Show a to Show ()
-                       -- to avoid graututious errors on "show []"
+                       -- In interactive mode, or with -fextended-default-rules,
+                       -- we default Show a to Show () to avoid graututious errors on "show []"
 
     
                    -- Collect together all the bad guys
@@ -2276,19 +2307,10 @@ tcSimplifyDeriv tc tyvars theta
        rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
                -- This reverse-mapping is a Royal Pain, 
                -- but the result should mention TyVars not TcTyVars
-
-       head_ty = TyConApp tc (map TyVarTy tvs)
     in
    
     addNoInstanceErrs Nothing [] bad_insts             `thenM_`
     mapM_ (addErrTc . badDerivedPred) weird_preds      `thenM_`
-    checkAmbiguity tvs simpl_theta tv_set              `thenM_`
-      -- Check instance termination as for user-declared instances.
-      -- unless we had -fallow-undecidable-instances (which risks
-      -- non-termination in the 'deriving' context-inference fixpoint
-      -- loop).
-    ifM (gla_exts && not undecidable_ok)
-       (checkInstTermination simpl_theta [head_ty])    `thenM_`
     returnM (substTheta rev_env simpl_theta)
   where
     doc    = ptext SLIT("deriving classes for a data type")
@@ -2453,8 +2475,8 @@ addNoInstanceErrs mb_what givens dicts
                                ptext SLIT("to the") <+> what] ]
 
        fix2 | null instance_dicts = []
-            | otherwise           = [ ptext SLIT("add an instance declaration for")
-                                      <+> pprDictsTheta instance_dicts ]
+            | otherwise           = [ sep [ptext SLIT("add an instance declaration for"),
+                                           pprDictsTheta instance_dicts] ]
        instance_dicts = [d | d <- dicts, isClassDict d, not (isTyVarDict d)]
                -- Insts for which it is worth suggesting an adding an instance declaration
                -- Exclude implicit parameters, and tyvar dicts
@@ -2527,7 +2549,7 @@ badDerivedPred pred
 
 reduceDepthErr n stack
   = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
-         ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
+         ptext SLIT("Use -fcontext-stack=N to increase stack size to N"),
          nest 4 (pprStack stack)]
 
 pprStack stack = vcat (map pprInstInFull stack)