compiler/typecheck/FunDeps.hs

   1 {-
   2 (c) The University of Glasgow 2006
   3 (c) The GRASP/AQUA Project, Glasgow University, 2000
   4
   5
   6 FunDeps - functional dependencies
   7
   8 It's better to read it as: "if we know these, then we're going to know these"
   9 -}
  10
  11 {-# LANGUAGE CPP #-}
  12
  13 module FunDeps (
  14         FunDepEqn(..), pprEquation,
  15         improveFromInstEnv, improveFromAnother,
  16         checkInstCoverage, checkFunDeps,
  17         pprFundeps
  18     ) where
  19
  20 #include "HsVersions.h"
  21
  22 import Name
  23 import Var
  24 import Class
  25 import Type
  26 import TcType( immSuperClasses )
  27 import Unify
  28 import InstEnv
  29 import VarSet
  30 import VarEnv
  31 import Outputable
  32 import ErrUtils( Validity(..), allValid )
  33 import SrcLoc
  34 import Util
  35 import FastString
  36
  37 import Pair             ( Pair(..) )
  38 import Data.List        ( nubBy )
  39 import Data.Maybe       ( isJust )
  40
  41 {-
  42 ************************************************************************
  43 *                                                                      *
  44 \subsection{Generate equations from functional dependencies}
  45 *                                                                      *
  46 ************************************************************************
  47
  48
  49 Each functional dependency with one variable in the RHS is responsible
  50 for generating a single equality. For instance:
  51      class C a b | a -> b
  52 The constraints ([Wanted] C Int Bool) and [Wanted] C Int alpha
  53 will generate the folloing FunDepEqn
  54      FDEqn { fd_qtvs = []
  55            , fd_eqs  = [Pair Bool alpha]
  56            , fd_pred1 = C Int Bool
  57            , fd_pred2 = C Int alpha
  58            , fd_loc = ... }
  59 However notice that a functional dependency may have more than one variable
  60 in the RHS which will create more than one pair of types in fd_eqs. Example:
  61      class C a b c | a -> b c
  62      [Wanted] C Int alpha alpha
  63      [Wanted] C Int Bool beta
  64 Will generate:
  65      FDEqn { fd_qtvs = []
  66            , fd_eqs  = [Pair Bool alpha, Pair alpha beta]
  67            , fd_pred1 = C Int Bool
  68            , fd_pred2 = C Int alpha
  69            , fd_loc = ... }
  70
  71 INVARIANT: Corresponding types aren't already equal
  72 That is, there exists at least one non-identity equality in FDEqs.
  73
  74 Assume:
  75        class C a b c | a -> b c
  76        instance C Int x x
  77 And:   [Wanted] C Int Bool alpha
  78 We will /match/ the LHS of fundep equations, producing a matching substitution
  79 and create equations for the RHS sides. In our last example we'd have generated:
  80       ({x}, [fd1,fd2])
  81 where
  82        fd1 = FDEq 1 Bool x
  83        fd2 = FDEq 2 alpha x
  84 To ``execute'' the equation, make fresh type variable for each tyvar in the set,
  85 instantiate the two types with these fresh variables, and then unify or generate
  86 a new constraint. In the above example we would generate a new unification
  87 variable 'beta' for x and produce the following constraints:
  88      [Wanted] (Bool ~ beta)
  89      [Wanted] (alpha ~ beta)
  90
  91 Notice the subtle difference between the above class declaration and:
  92        class C a b c | a -> b, a -> c
  93 where we would generate:
  94       ({x},[fd1]),({x},[fd2])
  95 This means that the template variable would be instantiated to different
  96 unification variables when producing the FD constraints.
  97
  98 Finally, the position parameters will help us rewrite the wanted constraint ``on the spot''
  99 -}
 100
 101 data FunDepEqn loc
 102   = FDEqn { fd_qtvs :: [TyVar]   -- Instantiate these type and kind vars
 103                                  --   to fresh unification vars,
 104                                  -- Non-empty only for FunDepEqns arising from instance decls
 105
 106           , fd_eqs  :: [Pair Type]  -- Make these pairs of types equal
 107           , fd_pred1 :: PredType    -- The FunDepEqn arose from
 108           , fd_pred2 :: PredType    --  combining these two constraints
 109           , fd_loc :: loc  }
 110
 111 {-
 112 Given a bunch of predicates that must hold, such as
 113
 114         C Int t1, C Int t2, C Bool t3, ?x::t4, ?x::t5
 115
 116 improve figures out what extra equations must hold.
 117 For example, if we have
 118
 119         class C a b | a->b where ...
 120
 121 then improve will return
 122
 123         [(t1,t2), (t4,t5)]
 124
 125 NOTA BENE:
 126
 127   * improve does not iterate.  It's possible that when we make
 128     t1=t2, for example, that will in turn trigger a new equation.
 129     This would happen if we also had
 130         C t1 t7, C t2 t8
 131     If t1=t2, we also get t7=t8.
 132
 133     improve does *not* do this extra step.  It relies on the caller
 134     doing so.
 135
 136   * The equations unify types that are not already equal.  So there
 137     is no effect iff the result of improve is empty
 138 -}
 139
 140 instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
 141 -- (instFD fd tvs tys) returns fd instantiated with (tvs -> tys)
 142 instFD (ls,rs) tvs tys
 143   = (map lookup ls, map lookup rs)
 144   where
 145     env       = zipVarEnv tvs tys
 146     lookup tv = lookupVarEnv_NF env tv
 147
 148 zipAndComputeFDEqs :: (Type -> Type -> Bool) -- Discard this FDEq if true
 149                    -> [Type] -> [Type]
 150                    -> [Pair Type]
 151 -- Create a list of (Type,Type) pairs from two lists of types,
 152 -- making sure that the types are not already equal
 153 zipAndComputeFDEqs discard (ty1:tys1) (ty2:tys2)
 154  | discard ty1 ty2 = zipAndComputeFDEqs discard tys1 tys2
 155  | otherwise       = Pair ty1 ty2 : zipAndComputeFDEqs discard tys1 tys2
 156 zipAndComputeFDEqs _ _ _ = []
 157
 158 -- Improve a class constraint from another class constraint
 159 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 160 improveFromAnother :: loc
 161                    -> PredType -- Template item (usually given, or inert)
 162                    -> PredType -- Workitem [that can be improved]
 163                    -> [FunDepEqn loc]
 164 -- Post: FDEqs always oriented from the other to the workitem
 165 --       Equations have empty quantified variables
 166 improveFromAnother loc pred1 pred2
 167   | Just (cls1, tys1) <- getClassPredTys_maybe pred1
 168   , Just (cls2, tys2) <- getClassPredTys_maybe pred2
 169   , tys1 `lengthAtLeast` 2 && cls1 == cls2
 170   = [ FDEqn { fd_qtvs = [], fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2, fd_loc = loc }
 171     | let (cls_tvs, cls_fds) = classTvsFds cls1
 172     , fd <- cls_fds
 173     , let (ltys1, rs1) = instFD fd cls_tvs tys1
 174           (ltys2, rs2) = instFD fd cls_tvs tys2
 175     , eqTypes ltys1 ltys2               -- The LHSs match
 176     , let eqs = zipAndComputeFDEqs eqType rs1 rs2
 177     , not (null eqs) ]
 178
 179 improveFromAnother _ _ _ = []
 180
 181
 182 -- Improve a class constraint from instance declarations
 183 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 184
 185 pprEquation :: FunDepEqn a -> SDoc
 186 pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs })
 187   = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr qtvs),
 188           nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2
 189                        | Pair t1 t2 <- pairs])]
 190
 191 improveFromInstEnv :: InstEnvs
 192                    -> (PredType -> SrcSpan -> loc)
 193                    -> PredType
 194                    -> [FunDepEqn loc] -- Needs to be a FunDepEqn because
 195                                       -- of quantified variables
 196 -- Post: Equations oriented from the template (matching instance) to the workitem!
 197 improveFromInstEnv _inst_env _ pred
 198   | not (isClassPred pred)
 199   = panic "improveFromInstEnv: not a class predicate"
 200 improveFromInstEnv inst_env mk_loc pred
 201   | Just (cls, tys) <- getClassPredTys_maybe pred
 202   , tys `lengthAtLeast` 2
 203   , let (cls_tvs, cls_fds) = classTvsFds cls
 204         instances          = classInstances inst_env cls
 205         rough_tcs          = roughMatchTcs tys
 206   = [ FDEqn { fd_qtvs = meta_tvs, fd_eqs = eqs
 207             , fd_pred1 = p_inst, fd_pred2 = pred
 208             , fd_loc = mk_loc p_inst (getSrcSpan (is_dfun ispec)) }
 209     | fd <- cls_fds             -- Iterate through the fundeps first,
 210                                 -- because there often are none!
 211     , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
 212                 -- Trim the rough_tcs based on the head of the fundep.
 213                 -- Remember that instanceCantMatch treats both argumnents
 214                 -- symmetrically, so it's ok to trim the rough_tcs,
 215                 -- rather than trimming each inst_tcs in turn
 216     , ispec <- instances
 217     , (meta_tvs, eqs) <- checkClsFD fd cls_tvs ispec
 218                                     emptyVarSet tys trimmed_tcs -- NB: orientation
 219     , let p_inst = mkClassPred cls (is_tys ispec)
 220     ]
 221 improveFromInstEnv _ _ _ = []
 222
 223
 224 checkClsFD :: FunDep TyVar -> [TyVar]             -- One functional dependency from the class
 225            -> ClsInst                             -- An instance template
 226            -> TyVarSet -> [Type] -> [Maybe Name]  -- Arguments of this (C tys) predicate
 227                                                   -- TyVarSet are extra tyvars that can be instantiated
 228            -> [([TyVar], [Pair Type])]
 229
 230 checkClsFD fd clas_tvs
 231            (ClsInst { is_tvs = qtvs, is_tys = tys_inst, is_tcs = rough_tcs_inst })
 232            extra_qtvs tys_actual rough_tcs_actual
 233
 234 -- 'qtvs' are the quantified type variables, the ones which an be instantiated
 235 -- to make the types match.  For example, given
 236 --      class C a b | a->b where ...
 237 --      instance C (Maybe x) (Tree x) where ..
 238 --
 239 -- and an Inst of form (C (Maybe t1) t2),
 240 -- then we will call checkClsFD with
 241 --
 242 --      is_qtvs = {x}, is_tys = [Maybe x,  Tree x]
 243 --                     tys_actual = [Maybe t1, t2]
 244 --
 245 -- We can instantiate x to t1, and then we want to force
 246 --      (Tree x) [t1/x]  ~   t2
 247 --
 248 -- This function is also used when matching two Insts (rather than an Inst
 249 -- against an instance decl. In that case, qtvs is empty, and we are doing
 250 -- an equality check
 251 --
 252 -- This function is also used by InstEnv.badFunDeps, which needs to *unify*
 253 -- For the one-sided matching case, the qtvs are just from the template,
 254 -- so we get matching
 255
 256   | instanceCantMatch rough_tcs_inst rough_tcs_actual
 257   = []          -- Filter out ones that can't possibly match,
 258
 259   | otherwise
 260   = ASSERT2( length tys_inst == length tys_actual     &&
 261              length tys_inst == length clas_tvs
 262             , ppr tys_inst <+> ppr tys_actual )
 263
 264     case tcUnifyTys bind_fn ltys1 ltys2 of
 265         Nothing  -> []
 266         Just subst | isJust (tcUnifyTys bind_fn rtys1' rtys2')
 267                         -- Don't include any equations that already hold.
 268                         -- Reason: then we know if any actual improvement has happened,
 269                         --         in which case we need to iterate the solver
 270                         -- In making this check we must taking account of the fact that any
 271                         -- qtvs that aren't already instantiated can be instantiated to anything
 272                         -- at all
 273                         -- NB: We can't do this 'is-useful-equation' check element-wise
 274                         --     because of:
 275                         --           class C a b c | a -> b c
 276                         --           instance C Int x x
 277                         --           [Wanted] C Int alpha Int
 278                         -- We would get that  x -> alpha  (isJust) and x -> Int (isJust)
 279                         -- so we would produce no FDs, which is clearly wrong.
 280                   -> []
 281
 282                   | null fdeqs
 283                   -> []
 284
 285                   | otherwise
 286                   -> [(meta_tvs, fdeqs)]
 287                         -- We could avoid this substTy stuff by producing the eqn
 288                         -- (qtvs, ls1++rs1, ls2++rs2)
 289                         -- which will re-do the ls1/ls2 unification when the equation is
 290                         -- executed.  What we're doing instead is recording the partial
 291                         -- work of the ls1/ls2 unification leaving a smaller unification problem
 292                   where
 293                     rtys1' = map (substTy subst) rtys1
 294                     rtys2' = map (substTy subst) rtys2
 295
 296                     fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' rtys2'
 297                         -- Don't discard anything!
 298                         -- We could discard equal types but it's an overkill to call
 299                         -- eqType again, since we know for sure that /at least one/
 300                         -- equation in there is useful)
 301
 302                     meta_tvs = [ setVarType tv (substTy subst (varType tv))
 303                                | tv <- qtvs, tv `notElemTvSubst` subst ]
 304                         -- meta_tvs are the quantified type variables
 305                         -- that have not been substituted out
 306                         --
 307                         -- Eg.  class C a b | a -> b
 308                         --      instance C Int [y]
 309                         -- Given constraint C Int z
 310                         -- we generate the equation
 311                         --      ({y}, [y], z)
 312                         --
 313                         -- But note (a) we get them from the dfun_id, so they are *in order*
 314                         --              because the kind variables may be mentioned in the
 315                         --              type variabes' kinds
 316                         --          (b) we must apply 'subst' to the kinds, in case we have
 317                         --              matched out a kind variable, but not a type variable
 318                         --              whose kind mentions that kind variable!
 319                         --          Trac #6015, #6068
 320   where
 321     qtv_set = mkVarSet qtvs
 322     bind_fn tv | tv `elemVarSet` qtv_set    = BindMe
 323                | tv `elemVarSet` extra_qtvs = BindMe
 324                | otherwise                  = Skolem
 325
 326     (ltys1, rtys1) = instFD fd clas_tvs tys_inst
 327     (ltys2, rtys2) = instFD fd clas_tvs tys_actual
 328
 329 {-
 330 ************************************************************************
 331 *                                                                      *
 332         The Coverage condition for instance declarations
 333 *                                                                      *
 334 ************************************************************************
 335
 336 Note [Coverage condition]
 337 ~~~~~~~~~~~~~~~~~~~~~~~~~
 338 Example
 339       class C a b | a -> b
 340       instance theta => C t1 t2
 341
 342 For the coverage condition, we check
 343    (normal)    fv(t2) `subset` fv(t1)
 344    (liberal)   fv(t2) `subset` oclose(fv(t1), theta)
 345
 346 The liberal version  ensures the self-consistency of the instance, but
 347 it does not guarantee termination. Example:
 348
 349    class Mul a b c | a b -> c where
 350         (.*.) :: a -> b -> c
 351
 352    instance Mul Int Int Int where (.*.) = (*)
 353    instance Mul Int Float Float where x .*. y = fromIntegral x * y
 354    instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v
 355
 356 In the third instance, it's not the case that fv([c]) `subset` fv(a,[b]).
 357 But it is the case that fv([c]) `subset` oclose( theta, fv(a,[b]) )
 358
 359 But it is a mistake to accept the instance because then this defn:
 360         f = \ b x y -> if b then x .*. [y] else y
 361 makes instance inference go into a loop, because it requires the constraint
 362         Mul a [b] b
 363 -}
 364
 365 checkInstCoverage :: Bool   -- Be liberal
 366                   -> Class -> [PredType] -> [Type]
 367                   -> Validity
 368 -- "be_liberal" flag says whether to use "liberal" coverage of
 369 --              See Note [Coverage Condition] below
 370 --
 371 -- Return values
 372 --    Nothing  => no problems
 373 --    Just msg => coverage problem described by msg
 374
 375 checkInstCoverage be_liberal clas theta inst_taus
 376   = allValid (map fundep_ok fds)
 377   where
 378     (tyvars, fds) = classTvsFds clas
 379     fundep_ok fd
 380        | isEmptyVarSet undetermined_tvs = IsValid
 381        | otherwise                      = NotValid msg
 382        where
 383          (ls,rs) = instFD fd tyvars inst_taus
 384          ls_tvs = tyVarsOfTypes ls
 385          rs_tvs = tyVarsOfTypes rs
 386
 387          undetermined_tvs | be_liberal = liberal_undet_tvs
 388                           | otherwise  = conserv_undet_tvs
 389
 390          liberal_undet_tvs = rs_tvs `minusVarSet`oclose theta (closeOverKinds ls_tvs)
 391          conserv_undet_tvs = rs_tvs `minusVarSet` closeOverKinds ls_tvs
 392             -- closeOverKinds: see Note [Closing over kinds in coverage]
 393
 394          undet_list = varSetElemsKvsFirst undetermined_tvs
 395
 396          msg = vcat [ -- text "ls_tvs" <+> ppr ls_tvs
 397                       -- , text "closed ls_tvs" <+> ppr (closeOverKinds ls_tvs)
 398                       -- , text "theta" <+> ppr theta
 399                       -- , text "oclose" <+> ppr (oclose theta (closeOverKinds ls_tvs))
 400                       -- , text "rs_tvs" <+> ppr rs_tvs
 401                       sep [ ptext (sLit "The")
 402                             <+> ppWhen be_liberal (ptext (sLit "liberal"))
 403                             <+> ptext (sLit "coverage condition fails in class")
 404                             <+> quotes (ppr clas)
 405                           , nest 2 $ ptext (sLit "for functional dependency:")
 406                             <+> quotes (pprFunDep fd) ]
 407                     , sep [ ptext (sLit "Reason: lhs type")<>plural ls <+> pprQuotedList ls
 408                           , nest 2 $
 409                             (if isSingleton ls
 410                              then ptext (sLit "does not")
 411                              else ptext (sLit "do not jointly"))
 412                             <+> ptext (sLit "determine rhs type")<>plural rs
 413                             <+> pprQuotedList rs ]
 414                     , ptext (sLit "Un-determined variable") <> plural undet_list <> colon
 415                             <+> pprWithCommas ppr undet_list
 416                     , ppWhen (all isKindVar undet_list) $
 417                       ptext (sLit "(Use -fprint-explicit-kinds to see the kind variables in the types)")
 418                     , ppWhen (not be_liberal && isEmptyVarSet liberal_undet_tvs) $
 419                       ptext (sLit "Using UndecidableInstances might help") ]
 420
 421 {- Note [Closing over kinds in coverage]
 422 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 423 Suppose we have a fundep  (a::k) -> b
 424 Then if 'a' is instantiated to (x y), where x:k2->*, y:k2,
 425 then fixing x really fixes k2 as well, and so k2 should be added to
 426 the lhs tyvars in the fundep check.
 427
 428 Example (Trac #8391), using liberal coverage
 429       data Foo a = ...  -- Foo :: forall k. k -> *
 430       class Bar a b | a -> b
 431       instance Bar a (Foo a)
 432
 433     In the instance decl, (a:k) does fix (Foo k a), but only if we notice
 434     that (a:k) fixes k.  Trac #10109 is another example.
 435
 436 Here is a more subtle example, from HList-0.4.0.0 (Trac #10564)
 437
 438   class HasFieldM (l :: k) r (v :: Maybe *)
 439         | l r -> v where ...
 440   class HasFieldM1 (b :: Maybe [*]) (l :: k) r v
 441         | b l r -> v where ...
 442   class HMemberM (e1 :: k) (l :: [k]) (r :: Maybe [k])
 443         | e1 l -> r
 444
 445   data Label :: k -> *
 446   type family LabelsOf (a :: [*]) ::  *
 447
 448   instance (HMemberM (Label {k} (l::k)) (LabelsOf xs) b,
 449             HasFieldM1 b l (r xs) v)
 450          => HasFieldM l (r xs) v where
 451
 452 Is the instance OK? Does {l,r,xs} determine v?  Well:
 453
 454   * From the instance constraint HMemberM (Label k l) (LabelsOf xs) b,
 455     plus the fundep "| el l -> r" in class HMameberM,
 456     we get {l,k,xs} -> b
 457
 458   * Note the 'k'!! We must call closeOverKinds on the seed set
 459     ls_tvs = {l,r,xs}, BEFORE doing oclose, else the {l,k,xs}->b
 460     fundep won't fire.  This was the reason for #10564.
 461
 462   * So starting from seeds {l,r,xs,k} we do oclose to get
 463     first {l,r,xs,k,b}, via the HMemberM constraint, and then
 464     {l,r,xs,k,b,v}, via the HasFieldM1 constraint.
 465
 466   * And that fixes v.
 467
 468 However, we must closeOverKinds whenever augmenting the seed set
 469 in oclose!  Consider Trac #10109:
 470
 471   data Succ a   -- Succ :: forall k. k -> *
 472   class Add (a :: k1) (b :: k2) (ab :: k3) | a b -> ab
 473   instance (Add a b ab) => Add (Succ {k1} (a :: k1))
 474                                b
 475                                (Succ {k3} (ab :: k3})
 476
 477 We start with seed set {a:k1,b:k2} and closeOverKinds to {a,k1,b,k2}.
 478 Now use the fundep to extend to {a,k1,b,k2,ab}.  But we need to
 479 closeOverKinds *again* now to {a,k1,b,k2,ab,k3}, so that we fix all
 480 the variables free in (Succ {k3} ab).
 481
 482 Bottom line:
 483   * closeOverKinds on initial seeds (in checkInstCoverage)
 484   * and closeOverKinds whenever extending those seeds (in oclose)
 485
 486 Note [The liberal coverage condition]
 487 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 488 (oclose preds tvs) closes the set of type variables tvs,
 489 wrt functional dependencies in preds.  The result is a superset
 490 of the argument set.  For example, if we have
 491         class C a b | a->b where ...
 492 then
 493         oclose [C (x,y) z, C (x,p) q] {x,y} = {x,y,z}
 494 because if we know x and y then that fixes z.
 495
 496 We also use equality predicates in the predicates; if we have an
 497 assumption `t1 ~ t2`, then we use the fact that if we know `t1` we
 498 also know `t2` and the other way.
 499   eg    oclose [C (x,y) z, a ~ x] {a,y} = {a,y,z,x}
 500
 501 oclose is used (only) when checking the coverage condition for
 502 an instance declaration
 503 -}
 504
 505 oclose :: [PredType] -> TyVarSet -> TyVarSet
 506 -- See Note [The liberal coverage condition]
 507 oclose preds fixed_tvs
 508   | null tv_fds = fixed_tvs -- Fast escape hatch for common case.
 509   | otherwise   = fixVarSet extend fixed_tvs
 510   where
 511     extend fixed_tvs = foldl add fixed_tvs tv_fds
 512        where
 513           add fixed_tvs (ls,rs)
 514             | ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` closeOverKinds rs
 515             | otherwise                = fixed_tvs
 516             -- closeOverKinds: see Note [Closing over kinds in coverage]
 517
 518     tv_fds  :: [(TyVarSet,TyVarSet)]
 519     tv_fds  = [ (tyVarsOfTypes ls, tyVarsOfTypes rs)
 520               | pred <- preds
 521               , (ls, rs) <- determined pred ]
 522
 523     determined :: PredType -> [([Type],[Type])]
 524     determined pred
 525        = case classifyPredType pred of
 526             EqPred NomEq t1 t2 -> [([t1],[t2]), ([t2],[t1])]
 527             ClassPred cls tys -> local_fds ++ concatMap determined superclasses
 528               where
 529                local_fds = [ instFD fd cls_tvs tys
 530                            | fd <- cls_fds ]
 531                (cls_tvs, cls_fds) = classTvsFds cls
 532                superclasses = immSuperClasses cls tys
 533             _ -> []
 534
 535 {-
 536 ************************************************************************
 537 *                                                                      *
 538         Check that a new instance decl is OK wrt fundeps
 539 *                                                                      *
 540 ************************************************************************
 541
 542 Here is the bad case:
 543         class C a b | a->b where ...
 544         instance C Int Bool where ...
 545         instance C Int Char where ...
 546
 547 The point is that a->b, so Int in the first parameter must uniquely
 548 determine the second.  In general, given the same class decl, and given
 549
 550         instance C s1 s2 where ...
 551         instance C t1 t2 where ...
 552
 553 Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
 554
 555 Matters are a little more complicated if there are free variables in
 556 the s2/t2.
 557
 558         class D a b c | a -> b
 559         instance D a b => D [(a,a)] [b] Int
 560         instance D a b => D [a]     [b] Bool
 561
 562 The instance decls don't overlap, because the third parameter keeps
 563 them separate.  But we want to make sure that given any constraint
 564         D s1 s2 s3
 565 if s1 matches
 566 -}
 567
 568 checkFunDeps :: InstEnvs -> ClsInst
 569              -> Maybe [ClsInst] -- Nothing  <=> ok
 570                                 -- Just dfs <=> conflict with dfs
 571 -- Check whether adding DFunId would break functional-dependency constraints
 572 -- Used only for instance decls defined in the module being compiled
 573 checkFunDeps inst_envs ispec
 574   | null bad_fundeps = Nothing
 575   | otherwise        = Just bad_fundeps
 576   where
 577     (ins_tvs, clas, ins_tys) = instanceHead ispec
 578     ins_tv_set   = mkVarSet ins_tvs
 579     cls_inst_env = classInstances inst_envs clas
 580     bad_fundeps  = badFunDeps cls_inst_env clas ins_tv_set ins_tys
 581
 582 badFunDeps :: [ClsInst] -> Class
 583            -> TyVarSet -> [Type]        -- Proposed new instance type
 584            -> [ClsInst]
 585 badFunDeps cls_insts clas ins_tv_set ins_tys
 586   = nubBy eq_inst $
 587     [ ispec | fd <- fds,        -- fds is often empty, so do this first!
 588               let trimmed_tcs = trimRoughMatchTcs clas_tvs fd rough_tcs,
 589               ispec <- cls_insts,
 590               notNull (checkClsFD fd clas_tvs ispec ins_tv_set ins_tys trimmed_tcs)
 591     ]
 592   where
 593     (clas_tvs, fds) = classTvsFds clas
 594     rough_tcs = roughMatchTcs ins_tys
 595     eq_inst i1 i2 = instanceDFunId i1 == instanceDFunId i2
 596         -- An single instance may appear twice in the un-nubbed conflict list
 597         -- because it may conflict with more than one fundep.  E.g.
 598         --      class C a b c | a -> b, a -> c
 599         --      instance C Int Bool Bool
 600         --      instance C Int Char Char
 601         -- The second instance conflicts with the first by *both* fundeps
 602
 603 trimRoughMatchTcs :: [TyVar] -> FunDep TyVar -> [Maybe Name] -> [Maybe Name]
 604 -- Computing rough_tcs for a particular fundep
 605 --     class C a b c | a -> b where ...
 606 -- For each instance .... => C ta tb tc
 607 -- we want to match only on the type ta; so our
 608 -- rough-match thing must similarly be filtered.
 609 -- Hence, we Nothing-ise the tb and tc types right here
 610 trimRoughMatchTcs clas_tvs (ltvs, _) mb_tcs
 611   = zipWith select clas_tvs mb_tcs
 612   where
 613     select clas_tv mb_tc | clas_tv `elem` ltvs = mb_tc
 614                          | otherwise           = Nothing