Fix header locations
[ghc.git] / compiler / typecheck / FunDeps.hs
index ab7e102..c8f0b1d 100644 (file)
@@ -19,12 +19,16 @@ module FunDeps (
 
 #include "HsVersions.h"
 
+import GhcPrelude
+
 import Name
 import Var
 import Class
 import Type
-import TcType( immSuperClasses )
+import TcType( transSuperClasses )
+import CoAxiom( TypeEqn )
 import Unify
+import FamInst( injTyVarsOfTypes )
 import InstEnv
 import VarSet
 import VarEnv
@@ -32,7 +36,6 @@ import Outputable
 import ErrUtils( Validity(..), allValid )
 import SrcLoc
 import Util
-import FastString
 
 import Pair             ( Pair(..) )
 import Data.List        ( nubBy )
@@ -51,7 +54,7 @@ Each functional dependency with one variable in the RHS is responsible
 for generating a single equality. For instance:
      class C a b | a -> b
 The constraints ([Wanted] C Int Bool) and [Wanted] C Int alpha
-will generate the folloing FunDepEqn
+will generate the following FunDepEqn
      FDEqn { fd_qtvs = []
            , fd_eqs  = [Pair Bool alpha]
            , fd_pred1 = C Int Bool
@@ -104,10 +107,10 @@ data FunDepEqn loc
                                  --   to fresh unification vars,
                                  -- Non-empty only for FunDepEqns arising from instance decls
 
-          , fd_eqs  :: [Pair Type]  -- Make these pairs of types equal
-          , fd_pred1 :: PredType    -- The FunDepEqn arose from
-          , fd_pred2 :: PredType    --  combining these two constraints
-          , fd_loc :: loc  }
+          , fd_eqs   :: [TypeEqn]  -- Make these pairs of types equal
+          , fd_pred1 :: PredType   -- The FunDepEqn arose from
+          , fd_pred2 :: PredType   --  combining these two constraints
+          , fd_loc   :: loc  }
 
 {-
 Given a bunch of predicates that must hold, such as
@@ -148,7 +151,7 @@ instFD (ls,rs) tvs tys
 
 zipAndComputeFDEqs :: (Type -> Type -> Bool) -- Discard this FDEq if true
                    -> [Type] -> [Type]
-                   -> [Pair Type]
+                   -> [TypeEqn]
 -- Create a list of (Type,Type) pairs from two lists of types,
 -- making sure that the types are not already equal
 zipAndComputeFDEqs discard (ty1:tys1) (ty2:tys2)
@@ -167,7 +170,7 @@ improveFromAnother :: loc
 improveFromAnother loc pred1 pred2
   | Just (cls1, tys1) <- getClassPredTys_maybe pred1
   , Just (cls2, tys2) <- getClassPredTys_maybe pred2
-  , tys1 `lengthAtLeast` 2 && cls1 == cls2
+  , cls1 == cls2
   = [ FDEqn { fd_qtvs = [], fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2, fd_loc = loc }
     | let (cls_tvs, cls_fds) = classTvsFds cls1
     , fd <- cls_fds
@@ -183,10 +186,13 @@ improveFromAnother _ _ _ = []
 -- Improve a class constraint from instance declarations
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
+instance Outputable (FunDepEqn a) where
+  ppr = pprEquation
+
 pprEquation :: FunDepEqn a -> SDoc
 pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs })
-  = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr qtvs),
-          nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2
+  = vcat [text "forall" <+> braces (pprWithCommas ppr qtvs),
+          nest 2 (vcat [ ppr t1 <+> text "~" <+> ppr t2
                        | Pair t1 t2 <- pairs])]
 
 improveFromInstEnv :: InstEnvs
@@ -195,12 +201,9 @@ improveFromInstEnv :: InstEnvs
                    -> [FunDepEqn loc] -- Needs to be a FunDepEqn because
                                       -- of quantified variables
 -- Post: Equations oriented from the template (matching instance) to the workitem!
-improveFromInstEnv _inst_env _ pred
-  | not (isClassPred pred)
-  = panic "improveFromInstEnv: not a class predicate"
 improveFromInstEnv inst_env mk_loc pred
-  | Just (cls, tys) <- getClassPredTys_maybe pred
-  , tys `lengthAtLeast` 2
+  | Just (cls, tys) <- ASSERT2( isClassPred pred, ppr pred )
+                       getClassPredTys_maybe pred
   , let (cls_tvs, cls_fds) = classTvsFds cls
         instances          = classInstances inst_env cls
         rough_tcs          = roughMatchTcs tys
@@ -211,7 +214,7 @@ improveFromInstEnv inst_env mk_loc pred
                                 -- because there often are none!
     , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
                 -- Trim the rough_tcs based on the head of the fundep.
-                -- Remember that instanceCantMatch treats both argumnents
+                -- Remember that instanceCantMatch treats both arguments
                 -- symmetrically, so it's ok to trim the rough_tcs,
                 -- rather than trimming each inst_tcs in turn
     , ispec <- instances
@@ -225,7 +228,7 @@ improveFromInstEnv _ _ _ = []
 improveClsFD :: [TyVar] -> FunDep TyVar    -- One functional dependency from the class
              -> ClsInst                    -- An instance template
              -> [Type] -> [Maybe Name]     -- Arguments of this (C tys) predicate
-             -> [([TyCoVar], [Pair Type])] -- Empty or singleton
+             -> [([TyCoVar], [TypeEqn])]   -- Empty or singleton
 
 improveClsFD clas_tvs fd
              (ClsInst { is_tvs = qtvs, is_tys = tys_inst, is_tcs = rough_tcs_inst })
@@ -236,7 +239,7 @@ improveClsFD clas_tvs fd
 --         for fundep (x,y -> p,q)  from class  (C x p y q)
 -- If (sx,sy) unifies with (tx,ty), take the subst S
 
--- 'qtvs' are the quantified type variables, the ones which an be instantiated
+-- 'qtvs' are the quantified type variables, the ones which can be instantiated
 -- to make the types match.  For example, given
 --      class C a b | a->b where ...
 --      instance C (Maybe x) (Tree x) where ..
@@ -254,13 +257,13 @@ improveClsFD clas_tvs fd
   = []          -- Filter out ones that can't possibly match,
 
   | otherwise
-  = ASSERT2( length tys_inst == length tys_actual     &&
-             length tys_inst == length clas_tvs
+  = ASSERT2( equalLength tys_inst tys_actual &&
+             equalLength tys_inst clas_tvs
             , ppr tys_inst <+> ppr tys_actual )
 
-    case tcMatchTys qtv_set ltys1 ltys2 of
+    case tcMatchTyKis ltys1 ltys2 of
         Nothing  -> []
-        Just subst | isJust (tcMatchTysX qtv_set subst rtys1 rtys2)
+        Just subst | isJust (tcMatchTyKisX subst rtys1 rtys2)
                         -- Don't include any equations that already hold.
                         -- Reason: then we know if any actual improvement has happened,
                         --         in which case we need to iterate the solver
@@ -287,7 +290,7 @@ improveClsFD clas_tvs fd
                         -- executed.  What we're doing instead is recording the partial
                         -- work of the ls1/ls2 unification leaving a smaller unification problem
                   where
-                    rtys1' = map (substTy subst) rtys1
+                    rtys1' = map (substTyUnchecked subst) rtys1
 
                     fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' rtys2
                         -- Don't discard anything!
@@ -295,7 +298,7 @@ improveClsFD clas_tvs fd
                         -- eqType again, since we know for sure that /at least one/
                         -- equation in there is useful)
 
-                    meta_tvs = [ setVarType tv (substTy subst (varType tv))
+                    meta_tvs = [ setVarType tv (substTyUnchecked subst (varType tv))
                                | tv <- qtvs, tv `notElemTCvSubst` subst ]
                         -- meta_tvs are the quantified type variables
                         -- that have not been substituted out
@@ -314,7 +317,6 @@ improveClsFD clas_tvs fd
                         --              whose kind mentions that kind variable!
                         --          Trac #6015, #6068
   where
-    qtv_set = mkVarSet qtvs
     (ltys1, rtys1) = instFD fd clas_tvs tys_inst
     (ltys2, rtys2) = instFD fd clas_tvs tys_actual
 
@@ -383,33 +385,33 @@ checkInstCoverage be_liberal clas theta inst_taus
          liberal_undet_tvs = (`minusVarSet` closed_ls_tvs) <$> rs_tvs
          conserv_undet_tvs = (`minusVarSet` ls_tvs)        <$> rs_tvs
 
-         undet_list = varSetElemsWellScoped (fold undetermined_tvs)
+         undet_set = fold undetermined_tvs
 
          msg = vcat [ -- text "ls_tvs" <+> ppr ls_tvs
                       -- , text "closed ls_tvs" <+> ppr (closeOverKinds ls_tvs)
                       -- , text "theta" <+> ppr theta
                       -- , text "oclose" <+> ppr (oclose theta (closeOverKinds ls_tvs))
                       -- , text "rs_tvs" <+> ppr rs_tvs
-                      sep [ ptext (sLit "The")
-                            <+> ppWhen be_liberal (ptext (sLit "liberal"))
-                            <+> ptext (sLit "coverage condition fails in class")
+                      sep [ text "The"
+                            <+> ppWhen be_liberal (text "liberal")
+                            <+> text "coverage condition fails in class"
                             <+> quotes (ppr clas)
-                          , nest 2 $ ptext (sLit "for functional dependency:")
+                          , nest 2 $ text "for functional dependency:"
                             <+> quotes (pprFunDep fd) ]
-                    , sep [ ptext (sLit "Reason: lhs type")<>plural ls <+> pprQuotedList ls
+                    , sep [ text "Reason: lhs type"<>plural ls <+> pprQuotedList ls
                           , nest 2 $
                             (if isSingleton ls
-                             then ptext (sLit "does not")
-                             else ptext (sLit "do not jointly"))
-                            <+> ptext (sLit "determine rhs type")<>plural rs
+                             then text "does not"
+                             else text "do not jointly")
+                            <+> text "determine rhs type"<>plural rs
                             <+> pprQuotedList rs ]
-                    , ptext (sLit "Un-determined variable") <> plural undet_list <> colon
-                            <+> pprWithCommas ppr undet_list
+                    , text "Un-determined variable" <> pluralVarSet undet_set <> colon
+                            <+> pprVarSet undet_set (pprWithCommas ppr)
                     , ppWhen (isEmptyVarSet $ pSnd undetermined_tvs) $
-                      ptext (sLit "(Use -fprint-explicit-kinds to see the kind variables in the types)")
+                      ppSuggestExplicitKinds
                     , ppWhen (not be_liberal &&
                               and (isEmptyVarSet <$> liberal_undet_tvs)) $
-                      ptext (sLit "Using UndecidableInstances might help") ]
+                      text "Using UndecidableInstances might help" ]
 
 {- Note [Closing over kinds in coverage]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -494,6 +496,36 @@ also know `t2` and the other way.
 
 oclose is used (only) when checking the coverage condition for
 an instance declaration
+
+Note [Equality superclasses]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have
+  class (a ~ [b]) => C a b
+
+Remember from Note [The equality types story] in TysPrim, that
+  * (a ~~ b) is a superclass of (a ~ b)
+  * (a ~# b) is a superclass of (a ~~ b)
+
+So when oclose expands superclasses we'll get a (a ~# [b]) superclass.
+But that's an EqPred not a ClassPred, and we jolly well do want to
+account for the mutual functional dependencies implied by (t1 ~# t2).
+Hence the EqPred handling in oclose.  See Trac #10778.
+
+Note [Care with type functions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (Trac #12803)
+  class C x y | x -> y
+  type family F a b
+  type family G c d = r | r -> d
+
+Now consider
+  oclose (C (F a b) (G c d)) {a,b}
+
+Knowing {a,b} fixes (F a b) regardless of the injectivity of F.
+But knowing (G c d) fixes only {d}, because G is only injective
+in its second parameter.
+
+Hence the tyCoVarsOfTypes/injTyVarsOfTypes dance in tv_fds.
 -}
 
 oclose :: [PredType] -> TyCoVarSet -> TyCoVarSet
@@ -510,24 +542,25 @@ oclose preds fixed_tvs
             -- closeOverKinds: see Note [Closing over kinds in coverage]
 
     tv_fds  :: [(TyCoVarSet,TyCoVarSet)]
-    tv_fds  = [ (tyCoVarsOfTypes ls, tyCoVarsOfTypes rs)
+    tv_fds  = [ (tyCoVarsOfTypes ls, injTyVarsOfTypes rs)
+                  -- See Note [Care with type functions]
               | pred <- preds
-              , (ls, rs) <- determined pred ]
+              , pred' <- pred : transSuperClasses pred
+                   -- Look for fundeps in superclasses too
+              , (ls, rs) <- determined pred' ]
 
     determined :: PredType -> [([Type],[Type])]
     determined pred
        = case classifyPredType pred of
             EqPred NomEq t1 t2 -> [([t1],[t2]), ([t2],[t1])]
-            ClassPred cls tys -> local_fds ++ concatMap determined superclasses
-              where
-               local_fds = [ instFD fd cls_tvs tys
-                           | fd <- cls_fds ]
-               (cls_tvs, cls_fds) = classTvsFds cls
-               superclasses = immSuperClasses cls tys
+               -- See Note [Equality superclasses]
+            ClassPred cls tys  -> [ instFD fd cls_tvs tys
+                                  | let (cls_tvs, cls_fds) = classTvsFds cls
+                                  , fd <- cls_fds ]
             _ -> []
 
-{-
-************************************************************************
+
+{- *********************************************************************
 *                                                                      *
         Check that a new instance decl is OK wrt fundeps
 *                                                                      *
@@ -595,12 +628,12 @@ checkFunDeps inst_envs (ClsInst { is_tvs = qtvs1, is_cls = cls
       | instanceCantMatch trimmed_tcs rough_tcs2
       = False
       | otherwise
-      = case tcUnifyTys bind_fn ltys1 ltys2 of
+      = case tcUnifyTyKis bind_fn ltys1 ltys2 of
           Nothing         -> False
           Just subst
             -> isNothing $   -- Bogus legacy test (Trac #10675)
                              -- See Note [Bogus consistency check]
-               tcUnifyTys bind_fn (substTys subst rtys1) (substTys subst rtys2)
+               tcUnifyTyKis bind_fn (substTysUnchecked subst rtys1) (substTysUnchecked subst rtys2)
 
       where
         trimmed_tcs    = trimRoughMatchTcs cls_tvs fd rough_tcs1
@@ -612,7 +645,7 @@ checkFunDeps inst_envs (ClsInst { is_tvs = qtvs1, is_cls = cls
                    | otherwise                = Skolem
 
     eq_inst i1 i2 = instanceDFunId i1 == instanceDFunId i2
-        -- An single instance may appear twice in the un-nubbed conflict list
+        -- A single instance may appear twice in the un-nubbed conflict list
         -- because it may conflict with more than one fundep.  E.g.
         --      class C a b c | a -> b, a -> c
         --      instance C Int Bool Bool