Robustify lookupFamInstEnv

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

diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs
index 9a369d9..0066d2f 100644 (file)
--- a/compiler/typecheck/TcTyFuns.lhs
+++ b/compiler/typecheck/TcTyFuns.lhs
@@ -69,21 +69,16 @@ tcUnfoldSynFamInst (TyConApp tycon tys)
   | not (isOpenSynTyCon tycon)     -- unfold *only* _synonym_ family instances
   = return Nothing
   | otherwise
   | not (isOpenSynTyCon tycon)     -- unfold *only* _synonym_ family instances
   = return Nothing
   | otherwise

-  = do { -- we only use the indexing arguments for matching, 
-         -- not the additional ones
-       ; maybeFamInst <- tcLookupFamInst tycon idxTys
+  = do { -- The TyCon might be over-saturated, but that's ok for tcLookupFamInst
+       ; maybeFamInst <- tcLookupFamInst tycon tys

        ; case maybeFamInst of
            Nothing                -> return Nothing
        ; case maybeFamInst of
            Nothing                -> return Nothing

-           Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
-                                                   mkTyConApp coe_tc tys')
+           Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys,
+                                                   mkTyConApp coe_tc rep_tys)

              where
              where

-               tys'   = rep_tys ++ restTys

                coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst" 
                                    (tyConFamilyCoercion_maybe rep_tc)
        }
                coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst" 
                                    (tyConFamilyCoercion_maybe rep_tc)
        }

-    where
-        n                = tyConArity tycon
-        (idxTys, restTys) = splitAt n tys

 tcUnfoldSynFamInst _other = return Nothing
 \end{code}
 
 tcUnfoldSynFamInst _other = return Nothing
 \end{code}
 

@@ -231,9 +226,6 @@ tcReduceEqs locals wanteds
 We maintain normalised equalities together with the skolems introduced as
 intermediates during flattening of equalities as well as 
 
 We maintain normalised equalities together with the skolems introduced as
 intermediates during flattening of equalities as well as 
 

-!!!TODO: We probably now can do without the skolem set.  It's not used during
-finalisation in the current code.
-

 \begin{code}
 -- |Configuration of normalised equalities used during solving.
 --
 \begin{code}
 -- |Configuration of normalised equalities used during solving.
 --

@@ -286,7 +278,7 @@ no further propoagation is possible.
 --
 normaliseEqs :: [Inst] -> TcM EqConfig
 normaliseEqs eqs 
 --
 normaliseEqs :: [Inst] -> TcM EqConfig
 normaliseEqs eqs 

-  = do { ASSERTM2( allM isValidWantedEqInst eqs, ppr eqs )
+  = do { ASSERTM2( allM wantedEqInstIsUnsolved eqs, ppr eqs )

        ; traceTc $ ptext (sLit "Entering normaliseEqs")
 
        ; (eqss, skolemss) <- mapAndUnzipM normEqInst eqs
        ; traceTc $ ptext (sLit "Entering normaliseEqs")
 
        ; (eqss, skolemss) <- mapAndUnzipM normEqInst eqs

@@ -352,7 +344,7 @@ finaliseEqsAndDicts (EqConfig { eqs     = eqs
 
          -- Assert that all cotvs of wanted equalities are still unfilled, and
          -- zonk all final insts, to make any improvement visible
 
          -- Assert that all cotvs of wanted equalities are still unfilled, and
          -- zonk all final insts, to make any improvement visible

-       ; ASSERTM2( allM isValidWantedEqInst eqs'', ppr eqs'' )
+       ; ASSERTM2( allM wantedEqInstIsUnsolved eqs'', ppr eqs'' )

        ; zonked_locals  <- zonkInsts locals'
        ; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds')
        ; return (zonked_locals, zonked_wanteds, final_binds, improved)
        ; zonked_locals  <- zonkInsts locals'
        ; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds')
        ; return (zonked_locals, zonked_wanteds, final_binds, improved)

@@ -384,9 +376,6 @@ families.  Moreover, in Forms (2) & (3), the left-hand side may not occur in
 the right-hand side, and the relation x > y is an arbitrary, but total order
 on type variables
 
 the right-hand side, and the relation x > y is an arbitrary, but total order
 on type variables
 

-!!!TODO: We may need to keep track of swapping for error messages (and to
-re-orient on finilisation).
-

 \begin{code}
 data RewriteInst
   = RewriteVar  -- Form (2) above
 \begin{code}
 data RewriteInst
   = RewriteVar  -- Form (2) above

@@ -960,9 +949,6 @@ applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
     -- rule matches => rewrite
   | fam1 == fam2 && tcEqTypes args1 args2 &&
     (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
     -- rule matches => rewrite
   | fam1 == fam2 && tcEqTypes args1 args2 &&
     (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))

--- !!!TODO: tcEqTypes is insufficient as it does not look through type synonyms
--- !!!Check whether anything breaks by making tcEqTypes look through synonyms.
--- !!!Should be ok and we don't want three type equalities.

   = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
        ; eq2' <- deriveEqInst eq2 lhs rhs co2'
        ; liftM Just $ normEqInst eq2'
   = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
        ; eq2' <- deriveEqInst eq2 lhs rhs co2'
        ; liftM Just $ normEqInst eq2'

@@ -1194,16 +1180,26 @@ Return all remaining wanted equalities.  The Boolean result component is True
 if at least one instantiation of a flexible that is *not* a skolem from
 flattening was performed.
 
 if at least one instantiation of a flexible that is *not* a skolem from
 flattening was performed.
 

+We need to instantiate all flexibles that arose as skolems during flattening
+of wanteds before we instantiate any other flexibles. Consider F delta ~
+alpha, F alpha ~ delta, where alpha is a skolem and delta a free flexible. We
+need to produce F (F delta) ~ delta (and not F (F alpha) ~ alpha). Otherwise,
+we may wrongly claim to having performed an improvement, which can lead to
+non-termination of the combined class-family solver.
+

 \begin{code}
 instantiateAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM ([Inst], Bool)
 instantiateAndExtract eqs localsEmpty skolems
   = do { traceTc $ hang (ptext (sLit "instantiateAndExtract:"))
                      4 (ppr eqs $$ ppr skolems)
 \begin{code}
 instantiateAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM ([Inst], Bool)
 instantiateAndExtract eqs localsEmpty skolems
   = do { traceTc $ hang (ptext (sLit "instantiateAndExtract:"))
                      4 (ppr eqs $$ ppr skolems)

-       ; results <- mapM inst wanteds
-       ; let residuals    = [eq | Left eq <- results]
-             only_skolems = and [tv `elemVarSet` skolems | Right tv <- results]
+           -- start by *only* instantiating skolem flexibles from flattening
+       ; unflat_wanteds <- liftM catMaybes $ 
+                             mapM (inst (`elemVarSet` skolems)) wanteds
+           -- only afterwards instantiate free flexibles
+       ; residuals <- liftM catMaybes $ mapM (inst (const True)) unflat_wanteds
+       ; let improvement = length residuals < length unflat_wanteds

        ; residuals' <- mapM rewriteInstToInst residuals
        ; residuals' <- mapM rewriteInstToInst residuals

-       ; return (residuals', not only_skolems)
+       ; return (residuals', improvement)

        }
   where
     wanteds      = filter (isWantedCo . rwi_co) eqs
        }
   where
     wanteds      = filter (isWantedCo . rwi_co) eqs

@@ -1211,9 +1207,9 @@ instantiateAndExtract eqs localsEmpty skolems
                      -- no local equalities or dicts => checking mode
 
         -- co :: alpha ~ t or co :: a ~ alpha
                      -- no local equalities or dicts => checking mode
 
         -- co :: alpha ~ t or co :: a ~ alpha

-    inst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
-      = do { flexi_tv1       <- isFlexible tv1
-           ; maybe_flexi_tv2 <- isFlexibleTy ty2
+    inst mayInst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
+      = do { flexi_tv1       <- isFlexible mayInst tv1
+           ; maybe_flexi_tv2 <- isFlexibleTy mayInst ty2

            ; case (flexi_tv1, maybe_flexi_tv2) of
                (True, _) 
                  -> -- co :: alpha ~ t
            ; case (flexi_tv1, maybe_flexi_tv2) of
                (True, _) 
                  -> -- co :: alpha ~ t

@@ -1221,31 +1217,31 @@ instantiateAndExtract eqs localsEmpty skolems
                (False, Just tv2) 
                  -> -- co :: a ~ alpha                  
                     doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
                (False, Just tv2) 
                  -> -- co :: a ~ alpha                  
                     doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq

-               _ -> return $ Left eq
+               _ -> return $ Just eq

            }
 
         -- co :: F args ~ alpha, and we are in checking mode (ie, no locals)
            }
 
         -- co :: F args ~ alpha, and we are in checking mode (ie, no locals)

-    inst eq@(RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = ty2, 
-                         rwi_co = co})
+    inst mayInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args, 
+                                 rwi_right = ty2, rwi_co = co})

       | Just tv2 <- tcGetTyVar_maybe ty2
       , isMetaTyVar tv2
       | Just tv2 <- tcGetTyVar_maybe ty2
       , isMetaTyVar tv2

-      , checkingMode || tv2 `elemVarSet` skolems
-                        -- !!!TODO: this is too liberal, even if tv2 is in 
+      , mayInst tv2 && (checkingMode || tv2 `elemVarSet` skolems)
+                        -- !!!FIXME: this is too liberal, even if tv2 is in 

                         -- skolems we shouldn't instantiate if tvs occurs 
                         -- in other equalities that may propagate it into the
                         -- environment
       = doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
 
                         -- skolems we shouldn't instantiate if tvs occurs 
                         -- in other equalities that may propagate it into the
                         -- environment
       = doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
 

-    inst eq = return $ Left eq
+    inst _mayInst eq = return $ Just eq

 
     -- tv is a meta var and not filled
 
     -- tv is a meta var and not filled

-    isFlexible tv
-      | isMetaTyVar tv = liftM isFlexi $ readMetaTyVar tv
-      | otherwise      = return False
+    isFlexible mayInst tv
+      | isMetaTyVar tv && mayInst tv = liftM isFlexi $ readMetaTyVar tv
+      | otherwise                    = return False

 
     -- type is a tv that is a meta var and not filled
 
     -- type is a tv that is a meta var and not filled

-    isFlexibleTy ty
-      | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible tv
+    isFlexibleTy mayInst ty
+      | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible mayInst tv

                                             ; if flexi then return $ Just tv 
                                                        else return Nothing
                                             }
                                             ; if flexi then return $ Just tv 
                                                        else return Nothing
                                             }

@@ -1265,7 +1261,7 @@ instantiateAndExtract eqs localsEmpty skolems
                    ptext (sLit "flexible") <+> ppr tv <+>
                    ptext (sLit "already filled with") <+> ppr fill_ty <+>
                    ptext (sLit "meant to fill with") <+> ppr ty
                    ptext (sLit "flexible") <+> ppr tv <+>
                    ptext (sLit "already filled with") <+> ppr fill_ty <+>
                    ptext (sLit "meant to fill with") <+> ppr ty

-               ; return $ Left eq
+               ; return $ Just eq

                }
 
         -- type variable meets type variable
                }
 
         -- type variable meets type variable

@@ -1288,7 +1284,7 @@ instantiateAndExtract eqs localsEmpty skolems
         -- signature skolem meets non-variable type
         -- => cannot update (retain the equality)!
         uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
         -- signature skolem meets non-variable type
         -- => cannot update (retain the equality)!
         uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv

-          = return $ Left eq
+          = return $ Just eq

 
         -- updatable meta variable meets non-variable type
         -- => occurs check, monotype check, and kinds match check, then update
 
         -- updatable meta variable meets non-variable type
         -- => occurs check, monotype check, and kinds match check, then update

@@ -1298,12 +1294,13 @@ instantiateAndExtract eqs localsEmpty skolems
                              
                ; case mb_ty' of
                    Nothing  -> 
                              
                ; case mb_ty' of
                    Nothing  -> 

-                     -- normalisation shouldn't leave families in non_tv_ty
-                     panic "TcTyFuns.uMeta: unexpected synonym family"
+                     -- there may be a family in non_tv_ty due to an unzonked,
+                     -- but updated skolem for a local equality
+                     return $ Just eq

                    Just ty' ->
                      do { checkUpdateMeta swapped tv ref ty'  -- update meta var
                         ; writeMetaTyVar cotv ty'             -- update co var
                    Just ty' ->
                      do { checkUpdateMeta swapped tv ref ty'  -- update meta var
                         ; writeMetaTyVar cotv ty'             -- update co var

-                        ; return $ Right tv
+                        ; return Nothing

                         }
                }
 
                         }
                }
 

@@ -1315,38 +1312,36 @@ instantiateAndExtract eqs localsEmpty skolems
         uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
           = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
                ; writeMetaTyVar cotv (mkTyVarTy tv2)
         uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
           = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
                ; writeMetaTyVar cotv (mkTyVarTy tv2)

-               ; return $ Right tv1
+               ; return Nothing

                }
 
         -- meta variable meets meta variable 
         -- => be clever about which of the two to update 
         --   (from TcUnify.uUnfilledVars minus boxy stuff)
         uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
                }
 
         -- meta variable meets meta variable 
         -- => be clever about which of the two to update 
         --   (from TcUnify.uUnfilledVars minus boxy stuff)
         uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv

-          = do { tv <- case (info1, info2) of
-                         -- Avoid SigTvs if poss
-                         (SigTv _, _      ) | k1_sub_k2 -> update_tv2
-                         (_,       SigTv _) | k2_sub_k1 -> update_tv1
-
-                         (_,   _) | k1_sub_k2 -> if k2_sub_k1 && 
-                                                    nicer_to_update_tv1
-                                                 then update_tv1  -- Same kinds
-                                                 else update_tv2
-                                  | k2_sub_k1 -> update_tv1
-                                  | otherwise -> kind_err >> return tv1
+          = do { case (info1, info2) of
+                   -- Avoid SigTvs if poss
+                   (SigTv _, _      ) | k1_sub_k2 -> update_tv2
+                   (_,       SigTv _) | k2_sub_k1 -> update_tv1
+
+                   (_,   _) | k1_sub_k2 -> if k2_sub_k1 && 
+                                              nicer_to_update_tv1
+                                           then update_tv1  -- Same kinds
+                                           else update_tv2
+                            | k2_sub_k1 -> update_tv1
+                            | otherwise -> kind_err

               -- Update the variable with least kind info
               -- See notes on type inference in Kind.lhs
               -- The "nicer to" part only applies if the two kinds are the same,
               -- so we can choose which to do.
 
                ; writeMetaTyVar cotv (mkTyVarTy tv2)
               -- Update the variable with least kind info
               -- See notes on type inference in Kind.lhs
               -- The "nicer to" part only applies if the two kinds are the same,
               -- so we can choose which to do.
 
                ; writeMetaTyVar cotv (mkTyVarTy tv2)

-               ; return $ Right tv
+               ; return Nothing

                }
           where
                 -- Kinds should be guaranteed ok at this point
             update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
                }
           where
                 -- Kinds should be guaranteed ok at this point
             update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)

-                         >> return tv1

             update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
             update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)

-                         >> return tv2

 
             kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
                        unifyKindMisMatch k1 k2
 
             kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
                        unifyKindMisMatch k1 k2