Moved canonicalisation inside solveInteract
[ghc-hetmet.git] / compiler / typecheck / TcSimplify.lhs
index f6b9ed2..b312d09 100644 (file)
@@ -10,7 +10,6 @@ module TcSimplify(
 import HsSyn          
 import TcRnMonad
 import TcErrors
-import TcCanonical
 import TcMType
 import TcType 
 import TcSMonad 
@@ -33,6 +32,7 @@ import BasicTypes     ( RuleName )
 import Data.List       ( partition )
 import Outputable
 import FastString
+import Control.Monad    ( unless )
 \end{code}
 
 
@@ -440,8 +440,7 @@ over implicit parameters. See the predicate isFreeWhenInferring.
 ***********************************************************************************
 
 When constructing evidence for superclasses in an instance declaration, 
-  * we MUST have the "self" dictionary available, but
-  * we must NOT have its superclasses derived from "self"
+  * we MUST have the "self" dictionary available
 
 Moreover, we must *completely* solve the constraints right now,
 not wrap them in an implication constraint to solve later.  Why?
@@ -461,25 +460,85 @@ Now, if there is some *other* top-level constraint solved
 looking like
        foo :: Ord [Int]
         foo = scsel dCInt
-we must not solve the (Ord [Int]) wanted from foo!!
+we must not solve the (Ord [Int]) wanted from foo!
+
+Note [Dependencies in self dictionaries] 
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Moreover, notice that when solving for a superclass, we record the dependency of 
+self on the superclass. This is because this dependency is not evident in the 
+EvBind of the self dictionary, which only involves a call to a DFun. Example: 
+
+class A a => C a 
+instance B a => C a 
+
+When we check the instance declaration, we pass in a self dictionary that is merely
+     self = dfun b
+But we will be asked to solve that from: 
+   [Given] d : B a 
+   [Derived] self : C a 
+We can show: 
+   [Wanted] sc : A a
+The problem is that self *depends* on the sc variable, but that is not apparent in 
+the binding self = dfun b. So we record the extra dependency, using the evidence bind: 
+   EvBind self (EvDFunApp dfun [b] [b,sc])
+It is these dependencies that are the ''true'' dependencies in an EvDFunApp, and those 
+that we must chase in function isGoodRecEv (in TcSMonad) 
 
 \begin{code}
-simplifySuperClass :: EvVar    -- The "self" dictionary
-                  -> WantedConstraints
-                  -> TcM ()
-simplifySuperClass self wanteds
-  = do { wanteds <- mapBagM zonkWanted wanteds
-       ; loc <- getCtLoc NoScSkol
-       ; ((unsolved_flats,unsolved_impls), frozen_errors, ev_binds)
+simplifySuperClass :: [TyVar]
+                   -> [EvVar]          -- givens
+                   -> EvVar            -- the superclass we must solve for
+                   -> EvBind           -- the 'self' evidence bind 
+                   -> TcM TcEvBinds
+-- Post:  
+--   ev_binds <- simplifySuperClasses tvs inst_givens sc_dict self_ev_bind
+-- Then: 
+--    1) ev_binds already contains self_ev_bind
+--    2) if successful then ev_binds contains binding for
+--       the wanted superclass, sc_dict
+simplifySuperClass tvs inst_givens sc_dict (EvBind self_dict self_ev)
+  = do { giv_loc      <- getCtLoc InstSkol  -- For the inst_givens
+       ; want_loc     <- getCtLoc ScOrigin  -- As wanted/derived (for the superclass and self)
+       ; lcl_env      <- getLclTypeEnv
+
+       -- Record the dependency of self_dict to sc_dict, see Note [Dependencies in self dictionaries]
+       ; let wanted = unitBag $ WcEvVar $ WantedEvVar sc_dict want_loc
+             self_ev_with_dep
+               = case self_ev of 
+                   EvDFunApp df tys insts deps -> EvDFunApp df tys insts (sc_dict:deps)
+                   _ -> panic "Self-dictionary not EvDFunApp!"
+
+       -- And solve for it
+       ; ((unsolved_flats, unsolved_implics), frozen_errors, ev_binds)
              <- runTcS SimplCheck NoUntouchables $
-               do { can_self <- canGivens loc [self]
-                  ; let inert = foldlBag updInertSet emptyInert can_self
-                    -- No need for solveInteract; we know it's inert
-
-                  ; solveWanteds inert wanteds }
-
-       ; ASSERT2( isEmptyBag ev_binds, ppr ev_binds )
-         reportUnsolved (unsolved_flats,unsolved_impls) frozen_errors }
+                do {   -- Record a binding for self_dict that *depends on sc_dict*
+                       -- And canonicalise self_dict (which adds its superclasses)
+                       -- with a Derived origin, which in turn triggers the
+                       -- goodRecEv recursive-evidence check
+                   ; setEvBind self_dict self_ev_with_dep
+                       -- The rest is just like solveImplication
+                   ; let cts = mapBag (\d -> (Given giv_loc, d)) (listToBag inst_givens)
+                                          `snocBag` (Derived want_loc DerSelf, self_dict)
+                   ; inert           <- solveInteract emptyInert cts
+                                        
+                   ; solveWanteds inert wanted }
+
+       -- For error reporting, conjure up a fake implication,
+       -- so that we get decent error messages
+       ; let implic = Implic { ic_untch  = NoUntouchables
+                             , ic_env    = lcl_env
+                             , ic_skols  = mkVarSet tvs
+                             , ic_given  = inst_givens
+                             , ic_wanted = mapBag WcEvVar unsolved_flats
+                             , ic_scoped = panic "super1"
+                             , ic_binds  = panic "super2"
+                             , ic_loc    = giv_loc }
+        ; ASSERT (isEmptyBag unsolved_implics) -- Impossible to have any implications!
+          unless (isEmptyBag unsolved_flats) $
+          reportUnsolved (emptyBag, unitBag implic) frozen_errors
+
+        ; return (EvBinds ev_binds) }
 \end{code}
 
 
@@ -644,12 +703,11 @@ solveWanteds :: InertSet        -- Given
 -- out of one or more of the implications 
 solveWanteds inert wanteds
   = do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds
-       ; can_flats <- canWanteds $ bagToList flat_wanteds
        ; traceTcS "solveWanteds {" $
                  vcat [ text "wanteds =" <+> ppr wanteds
                       , text "inert =" <+> ppr inert ]
        ; (unsolved_flats, unsolved_implics) 
-               <- simpl_loop 1 inert can_flats implic_wanteds
+               <- simpl_loop 1 inert flat_wanteds implic_wanteds
        ; bb <- getTcEvBindsBag
        ; tb <- getTcSTyBindsMap
        ; traceTcS "solveWanteds }" $
@@ -665,63 +723,66 @@ solveWanteds inert wanteds
   where
     simpl_loop :: Int 
                -> InertSet 
-               -> CanonicalCts -- May inlude givens (in the recursive call)
+               -> Bag WantedEvVar
                -> Bag Implication
                -> TcS (CanonicalCts, Bag Implication)
-    simpl_loop n inert can_ws implics
+    simpl_loop n inert work_items implics
       | n>10
-      = trace "solveWanteds: loop" $   -- Always bleat
+      = trace "solveWanteds: loop" $                   -- Always bleat
         do { traceTcS "solveWanteds: loop" (ppr inert)  -- Bleat more informatively
-           ; return (can_ws, implics) }
+
+             -- We don't want to call the canonicalizer on those wanted ev vars
+             -- so try one last time to solveInteract them 
+           ; inert1 <- solveInteract inert $ 
+                       mapBag (\(WantedEvVar ev wloc) -> (Wanted wloc, ev)) work_items
+           ; let (_, unsolved_cans) = extractUnsolved inert1
+           ; return (unsolved_cans, implics) }
 
       | otherwise
       = do { traceTcS "solveWanteds: simpl_loop start {" $
                  vcat [ text "n =" <+> ppr n
-                      , text "can_ws =" <+> ppr can_ws
+                      , text "work_items =" <+> ppr work_items
                       , text "implics =" <+> ppr implics
                       , text "inert =" <+> ppr inert ]
-           ; inert1 <- solveInteract inert can_ws
-           ; let (inert2, unsolved_flats) = extractUnsolved inert1
+           ; inert1 <- solveInteract inert $ 
+                       mapBag (\(WantedEvVar ev wloc) -> (Wanted wloc,ev)) work_items
+           ; let (inert2, unsolved_cans) = extractUnsolved inert1
+                 unsolved_wevvars 
+                     = mapBag (\ct -> WantedEvVar (cc_id ct) (getWantedLoc ct)) unsolved_cans
 
            -- NB: Importantly, inerts2 may contain *more* givens than inert 
            -- because of having solved equalities from can_ws 
            ; traceTcS "solveWanteds: done flats"  $
                  vcat [ text "inerts =" <+> ppr inert2
-                      , text "unsolved =" <+> ppr unsolved_flats ]
+                      , text "unsolved =" <+> ppr unsolved_cans ]
 
                 -- Go inside each implication
            ; (implic_eqs, unsolved_implics) 
-               <- solveNestedImplications inert2 unsolved_flats implics
+               <- solveNestedImplications inert2 unsolved_wevvars implics
 
                 -- Apply defaulting rules if and only if there
                -- no floated equalities.  If there are, they may
                -- solve the remaining wanteds, so don't do defaulting.
            ; final_eqs <- if not (isEmptyBag implic_eqs)
                          then return implic_eqs
-                          else applyDefaultingRules inert2 unsolved_flats
-                                     
-               -- default_eqs are *givens*, so simpl_loop may 
-               -- recurse with givens in the argument
+                          else applyDefaultingRules inert2 unsolved_cans
 
            ; traceTcS "solveWanteds: simpl_loop end }" $
                  vcat [ text "final_eqs =" <+> ppr final_eqs
-                      , text "unsolved_flats =" <+> ppr unsolved_flats
+                      , text "unsolved_flats =" <+> ppr unsolved_cans
                       , text "unsolved_implics =" <+> ppr unsolved_implics ]
 
            ; if isEmptyBag final_eqs then
-                 return (unsolved_flats, unsolved_implics)
+                 return (unsolved_cans, unsolved_implics)
              else 
-                 do { can_final_eqs <- canWanteds (Bag.bagToList final_eqs)
-                       -- final eqs is *just* a bunch of WantedEvVars
-                    ; simpl_loop (n+1) inert2 
-                          (can_final_eqs `andCCan` unsolved_flats) unsolved_implics 
+                 simpl_loop (n+1) inert2 -- final_eqs are just some WantedEvVars
+                            (final_eqs `unionBags` unsolved_wevvars) unsolved_implics
                        -- Important: reiterate with inert2, not plainly inert
                        -- because inert2 may contain more givens, as the result of solving
-                       -- some wanteds in the incoming can_ws 
-                     }       
+                       -- some wanteds in the incoming can_ws
            }
 
-solveNestedImplications :: InertSet -> CanonicalCts -> Bag Implication
+solveNestedImplications :: InertSet -> Bag WantedEvVar -> Bag Implication
                         -> TcS (Bag WantedEvVar, Bag Implication)
 solveNestedImplications inerts unsolved implics
   | isEmptyBag implics
@@ -775,8 +836,10 @@ solveImplication tcs_untouchables inert
     do { traceTcS "solveImplication {" (ppr imp) 
 
          -- Solve flat givens
-       ; can_givens  <- canGivens loc givens
-       ; given_inert <- solveInteract inert can_givens
+--       ; can_givens  <- canGivens loc givens
+--       ; let given_fl = Given loc
+       ; given_inert <- solveInteract inert $ 
+                        mapBag (\c -> (Given loc,c)) (listToBag givens)
 
          -- Simplify the wanteds
        ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
@@ -1035,7 +1098,7 @@ Basic plan behind applyDefaulting rules:
 
 \begin{code}
 applyDefaultingRules :: InertSet
-                     -> CanonicalCts          -- All wanteds
+                     -> CanonicalCts        -- All wanteds
                      -> TcS (Bag WantedEvVar)  -- All wanteds again!  
 -- Return some *extra* givens, which express the 
 -- type-class-default choice
@@ -1151,16 +1214,12 @@ disambigGroup (default_ty:default_tys) inert group
   = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
        ; let ct_loc = get_ct_loc (cc_flavor the_ct) 
        ; ev <- TcSMonad.newWantedCoVar (mkTyVarTy the_tv) default_ty
-       ; let wanted_eq = CTyEqCan { cc_id = ev
-                                  , cc_flavor = Wanted ct_loc
-                                  , cc_tyvar  = the_tv 
-                                  , cc_rhs    = default_ty }
        ; success <- tryTcS $ 
-                   do { final_inert <- solveInteract inert(listToBag $ wanted_eq:wanteds)
-                      ; let (_, unsolved) = extractUnsolved final_inert                                    
-                       ; errs <- getTcSErrorsBag 
+                   do { final_inert <- solveInteract inert $
+                                        consBag (Wanted ct_loc, ev) wanted_to_solve
+                      ; let (_, unsolved) = extractUnsolved final_inert                         
+                       ; errs <- getTcSErrorsBag
                       ; return (isEmptyBag unsolved && isEmptyBag errs) }
-
        ; case success of
            True  ->  -- Success: record the type variable binding, and return
                     do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
@@ -1171,8 +1230,10 @@ disambigGroup (default_ty:default_tys) inert group
                        ; disambigGroup default_tys inert group } }
   where
     ((the_ct,the_tv):_) = group
-    wanteds = map fst group
-    wanted_ev_vars = map deCanonicaliseWanted wanteds
+    wanteds             = map fst group
+    wanted_ev_vars      = map deCanonicaliseWanted wanteds
+    wanted_to_solve     = listToBag $ 
+                          map (\(WantedEvVar ev wloc) -> (Wanted wloc,ev)) wanted_ev_vars
 
     get_ct_loc (Wanted l) = l
     get_ct_loc _ = panic "Asked  to disambiguate given or derived!"