FunDeps.hs 24.9 KB
Newer Older
Austin Seipp's avatar
Austin Seipp committed
1 2 3 4
{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 2000

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"
Austin Seipp's avatar
Austin Seipp committed
9
-}
10

11 12
{-# LANGUAGE CPP #-}

13
module FunDeps (
14
        FunDepEqn(..), pprEquation,
15 16
        improveFromInstEnv, improveFromAnother,
        checkInstCoverage, checkFunDeps,
17
        pprFundeps
18
    ) where
19 20 21

#include "HsVersions.h"

22 23 24
import Name
import Var
import Class
batterseapower's avatar
batterseapower committed
25
import Type
26
import TcType( transSuperClasses )
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

36
import Pair             ( Pair(..) )
37
import Data.List        ( nubBy )
38
import Data.Maybe
39 40
import Data.Foldable    ( fold )

Austin Seipp's avatar
Austin Seipp committed
41 42 43
{-
************************************************************************
*                                                                      *
44
\subsection{Generate equations from functional dependencies}
Austin Seipp's avatar
Austin Seipp committed
45 46
*                                                                      *
************************************************************************
47 48


49 50 51
Each functional dependency with one variable in the RHS is responsible
for generating a single equality. For instance:
     class C a b | a -> b
52
The constraints ([Wanted] C Int Bool) and [Wanted] C Int alpha
53 54 55 56 57 58
will generate the folloing FunDepEqn
     FDEqn { fd_qtvs = []
           , fd_eqs  = [Pair Bool alpha]
           , fd_pred1 = C Int Bool
           , fd_pred2 = C Int alpha
           , 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 62 63 64
     class C a b c | a -> b c
     [Wanted] C Int alpha alpha
     [Wanted] C Int Bool beta
Will generate:
65 66 67 68 69
     FDEqn { fd_qtvs = []
           , fd_eqs  = [Pair Bool alpha, Pair alpha beta]
           , fd_pred1 = C Int Bool
           , fd_pred2 = C Int alpha
           , fd_loc = ... }
70

71 72
INVARIANT: Corresponding types aren't already equal
That is, there exists at least one non-identity equality in FDEqs.
73 74 75 76 77 78 79 80

Assume:
       class C a b c | a -> b c
       instance C Int x x
And:   [Wanted] C Int Bool alpha
We will /match/ the LHS of fundep equations, producing a matching substitution
and create equations for the RHS sides. In our last example we'd have generated:
      ({x}, [fd1,fd2])
81
where
82 83 84
       fd1 = FDEq 1 Bool x
       fd2 = FDEq 2 alpha x
To ``execute'' the equation, make fresh type variable for each tyvar in the set,
85 86
instantiate the two types with these fresh variables, and then unify or generate
a new constraint. In the above example we would generate a new unification
87 88 89 90 91
variable 'beta' for x and produce the following constraints:
     [Wanted] (Bool ~ beta)
     [Wanted] (alpha ~ beta)

Notice the subtle difference between the above class declaration and:
92 93 94 95 96
       class C a b c | a -> b, a -> c
where we would generate:
      ({x},[fd1]),({x},[fd2])
This means that the template variable would be instantiated to different
unification variables when producing the FD constraints.
97 98

Finally, the position parameters will help us rewrite the wanted constraint ``on the spot''
Austin Seipp's avatar
Austin Seipp committed
99
-}
100

101 102 103 104
data FunDepEqn loc
  = FDEqn { fd_qtvs :: [TyVar]   -- Instantiate these type and kind vars
                                 --   to fresh unification vars,
                                 -- Non-empty only for FunDepEqns arising from instance decls
105

106
          , fd_eqs  :: [Pair Type]  -- Make these pairs of types equal
107 108
          , fd_pred1 :: PredType    -- The FunDepEqn arose from
          , fd_pred2 :: PredType    --  combining these two constraints
109
          , fd_loc :: loc  }
110

Austin Seipp's avatar
Austin Seipp committed
111
{-
112 113
Given a bunch of predicates that must hold, such as

114
        C Int t1, C Int t2, C Bool t3, ?x::t4, ?x::t5
115 116 117 118

improve figures out what extra equations must hold.
For example, if we have

119
        class C a b | a->b where ...
120 121 122

then improve will return

123
        [(t1,t2), (t4,t5)]
124 125 126 127 128 129

NOTA BENE:

  * improve does not iterate.  It's possible that when we make
    t1=t2, for example, that will in turn trigger a new equation.
    This would happen if we also had
130
        C t1 t7, C t2 t8
131 132 133 134 135 136 137
    If t1=t2, we also get t7=t8.

    improve does *not* do this extra step.  It relies on the caller
    doing so.

  * The equations unify types that are not already equal.  So there
    is no effect iff the result of improve is empty
Austin Seipp's avatar
Austin Seipp committed
138
-}
139

Simon Peyton Jones's avatar
Simon Peyton Jones committed
140
instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
141
-- (instFD fd tvs tys) returns fd instantiated with (tvs -> tys)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
142 143 144 145 146 147
instFD (ls,rs) tvs tys
  = (map lookup ls, map lookup rs)
  where
    env       = zipVarEnv tvs tys
    lookup tv = lookupVarEnv_NF env tv

148
zipAndComputeFDEqs :: (Type -> Type -> Bool) -- Discard this FDEq if true
149 150 151 152 153
                   -> [Type] -> [Type]
                   -> [Pair Type]
-- 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)
154
 | discard ty1 ty2 = zipAndComputeFDEqs discard tys1 tys2
155
 | otherwise       = Pair ty1 ty2 : zipAndComputeFDEqs discard tys1 tys2
156
zipAndComputeFDEqs _ _ _ = []
157 158 159

-- Improve a class constraint from another class constraint
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
160 161
improveFromAnother :: loc
                   -> PredType -- Template item (usually given, or inert)
162
                   -> PredType -- Workitem [that can be improved]
163
                   -> [FunDepEqn loc]
164 165
-- Post: FDEqs always oriented from the other to the workitem
--       Equations have empty quantified variables
166
improveFromAnother loc pred1 pred2
167 168
  | Just (cls1, tys1) <- getClassPredTys_maybe pred1
  , Just (cls2, tys2) <- getClassPredTys_maybe pred2
169
  , cls1 == cls2
170
  = [ FDEqn { fd_qtvs = [], fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2, fd_loc = loc }
171 172
    | let (cls_tvs, cls_fds) = classTvsFds cls1
    , fd <- cls_fds
173 174
    , let (ltys1, rs1) = instFD fd cls_tvs tys1
          (ltys2, rs2) = instFD fd cls_tvs tys2
175
    , eqTypes ltys1 ltys2               -- The LHSs match
176
    , let eqs = zipAndComputeFDEqs eqType rs1 rs2
177 178
    , not (null eqs) ]

179
improveFromAnother _ _ _ = []
180 181 182 183


-- Improve a class constraint from instance declarations
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
184

185
pprEquation :: FunDepEqn a -> SDoc
186
pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs })
187 188
  = vcat [text "forall" <+> braces (pprWithCommas ppr qtvs),
          nest 2 (vcat [ ppr t1 <+> text "~" <+> ppr t2
189
                       | Pair t1 t2 <- pairs])]
190

191
improveFromInstEnv :: InstEnvs
192
                   -> (PredType -> SrcSpan -> loc)
193
                   -> PredType
194 195
                   -> [FunDepEqn loc] -- Needs to be a FunDepEqn because
                                      -- of quantified variables
196
-- Post: Equations oriented from the template (matching instance) to the workitem!
197
improveFromInstEnv _inst_env _ pred
198 199
  | not (isClassPred pred)
  = panic "improveFromInstEnv: not a class predicate"
200
improveFromInstEnv inst_env mk_loc pred
201
  | Just (cls, tys) <- getClassPredTys_maybe pred
batterseapower's avatar
batterseapower committed
202 203 204
  , let (cls_tvs, cls_fds) = classTvsFds cls
        instances          = classInstances inst_env cls
        rough_tcs          = roughMatchTcs tys
205
  = [ FDEqn { fd_qtvs = meta_tvs, fd_eqs = eqs
206 207
            , fd_pred1 = p_inst, fd_pred2 = pred
            , fd_loc = mk_loc p_inst (getSrcSpan (is_dfun ispec)) }
208 209
    | fd <- cls_fds             -- Iterate through the fundeps first,
                                -- because there often are none!
210
    , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
211 212 213 214
                -- Trim the rough_tcs based on the head of the fundep.
                -- Remember that instanceCantMatch treats both argumnents
                -- symmetrically, so it's ok to trim the rough_tcs,
                -- rather than trimming each inst_tcs in turn
215
    , ispec <- instances
216 217
    , (meta_tvs, eqs) <- improveClsFD cls_tvs fd ispec
                                      tys trimmed_tcs -- NB: orientation
218
    , let p_inst = mkClassPred cls (is_tys ispec)
219
    ]
220
improveFromInstEnv _ _ _ = []
221

222

223 224 225 226
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
227

228 229 230
improveClsFD clas_tvs fd
             (ClsInst { is_tvs = qtvs, is_tys = tys_inst, is_tcs = rough_tcs_inst })
             tys_actual rough_tcs_actual
231

232 233
-- Compare instance      {a,b}    C sx sp sy sq
--         with wanted     [W] C tx tp ty tq
Simon Peyton Jones's avatar
Simon Peyton Jones committed
234 235 236
--         for fundep (x,y -> p,q)  from class  (C x p y q)
-- If (sx,sy) unifies with (tx,ty), take the subst S

237
-- 'qtvs' are the quantified type variables, the ones which an be instantiated
238
-- to make the types match.  For example, given
239 240
--      class C a b | a->b where ...
--      instance C (Maybe x) (Tree x) where ..
241
--
242
-- and a wanted constraint of form (C (Maybe t1) t2),
243 244
-- then we will call checkClsFD with
--
245 246
--      is_qtvs = {x}, is_tys = [Maybe x,  Tree x]
--                     tys_actual = [Maybe t1, t2]
247 248
--
-- We can instantiate x to t1, and then we want to force
249
--      (Tree x) [t1/x]  ~   t2
250 251

  | instanceCantMatch rough_tcs_inst rough_tcs_actual
252
  = []          -- Filter out ones that can't possibly match,
253 254

  | otherwise
255
  = ASSERT2( length tys_inst == length tys_actual     &&
256 257
             length tys_inst == length clas_tvs
            , ppr tys_inst <+> ppr tys_actual )
258

Richard Eisenberg's avatar
Richard Eisenberg committed
259
    case tcMatchTyKis ltys1 ltys2 of
260
        Nothing  -> []
Richard Eisenberg's avatar
Richard Eisenberg committed
261
        Just subst | isJust (tcMatchTyKisX subst rtys1 rtys2)
262 263 264 265 266 267
                        -- 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
                        -- In making this check we must taking account of the fact that any
                        -- qtvs that aren't already instantiated can be instantiated to anything
                        -- at all
268
                        -- NB: We can't do this 'is-useful-equation' check element-wise
269 270 271 272 273
                        --     because of:
                        --           class C a b c | a -> b c
                        --           instance C Int x x
                        --           [Wanted] C Int alpha Int
                        -- We would get that  x -> alpha  (isJust) and x -> Int (isJust)
274 275
                        -- so we would produce no FDs, which is clearly wrong.
                  -> []
276

277 278 279
                  | null fdeqs
                  -> []

280
                  | otherwise
281
                  -> [(meta_tvs, fdeqs)]
282 283 284 285 286 287
                        -- We could avoid this substTy stuff by producing the eqn
                        -- (qtvs, ls1++rs1, ls2++rs2)
                        -- which will re-do the ls1/ls2 unification when the equation is
                        -- executed.  What we're doing instead is recording the partial
                        -- work of the ls1/ls2 unification leaving a smaller unification problem
                  where
288
                    rtys1' = map (substTyUnchecked subst) rtys1
289

290
                    fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' rtys2
291 292 293
                        -- Don't discard anything!
                        -- We could discard equal types but it's an overkill to call
                        -- eqType again, since we know for sure that /at least one/
294 295
                        -- equation in there is useful)

296
                    meta_tvs = [ setVarType tv (substTyUnchecked subst (varType tv))
297
                               | tv <- qtvs, tv `notElemTCvSubst` subst ]
298 299 300 301 302 303 304 305
                        -- meta_tvs are the quantified type variables
                        -- that have not been substituted out
                        --
                        -- Eg.  class C a b | a -> b
                        --      instance C Int [y]
                        -- Given constraint C Int z
                        -- we generate the equation
                        --      ({y}, [y], z)
306 307 308 309 310 311 312 313
                        --
                        -- But note (a) we get them from the dfun_id, so they are *in order*
                        --              because the kind variables may be mentioned in the
                        --              type variabes' kinds
                        --          (b) we must apply 'subst' to the kinds, in case we have
                        --              matched out a kind variable, but not a type variable
                        --              whose kind mentions that kind variable!
                        --          Trac #6015, #6068
314
  where
315 316
    (ltys1, rtys1) = instFD fd clas_tvs tys_inst
    (ltys2, rtys2) = instFD fd clas_tvs tys_actual
317

Austin Seipp's avatar
Austin Seipp committed
318
{-
319 320
%************************************************************************
%*                                                                      *
Simon Peyton Jones's avatar
Simon Peyton Jones committed
321
        The Coverage condition for instance declarations
Austin Seipp's avatar
Austin Seipp committed
322 323
*                                                                      *
************************************************************************
Simon Peyton Jones's avatar
Simon Peyton Jones committed
324 325 326 327 328 329

Note [Coverage condition]
~~~~~~~~~~~~~~~~~~~~~~~~~
Example
      class C a b | a -> b
      instance theta => C t1 t2
330

Simon Peyton Jones's avatar
Simon Peyton Jones committed
331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351
For the coverage condition, we check
   (normal)    fv(t2) `subset` fv(t1)
   (liberal)   fv(t2) `subset` oclose(fv(t1), theta)

The liberal version  ensures the self-consistency of the instance, but
it does not guarantee termination. Example:

   class Mul a b c | a b -> c where
        (.*.) :: a -> b -> c

   instance Mul Int Int Int where (.*.) = (*)
   instance Mul Int Float Float where x .*. y = fromIntegral x * y
   instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v

In the third instance, it's not the case that fv([c]) `subset` fv(a,[b]).
But it is the case that fv([c]) `subset` oclose( theta, fv(a,[b]) )

But it is a mistake to accept the instance because then this defn:
        f = \ b x y -> if b then x .*. [y] else y
makes instance inference go into a loop, because it requires the constraint
        Mul a [b] b
Austin Seipp's avatar
Austin Seipp committed
352
-}
Simon Peyton Jones's avatar
Simon Peyton Jones committed
353

354
checkInstCoverage :: Bool   -- Be liberal
355
                  -> Class -> [PredType] -> [Type]
356
                  -> Validity
Gabor Greif's avatar
Gabor Greif committed
357
-- "be_liberal" flag says whether to use "liberal" coverage of
358 359 360 361 362
--              See Note [Coverage Condition] below
--
-- Return values
--    Nothing  => no problems
--    Just msg => coverage problem described by msg
363

364
checkInstCoverage be_liberal clas theta inst_taus
365
  = allValid (map fundep_ok fds)
366 367
  where
    (tyvars, fds) = classTvsFds clas
368
    fundep_ok fd
369 370
       | and (isEmptyVarSet <$> undetermined_tvs) = IsValid
       | otherwise                                = NotValid msg
371
       where
372
         (ls,rs) = instFD fd tyvars inst_taus
373 374
         ls_tvs = tyCoVarsOfTypes ls
         rs_tvs = splitVisVarsOfTypes rs
375

376 377 378
         undetermined_tvs | be_liberal = liberal_undet_tvs
                          | otherwise  = conserv_undet_tvs

379 380 381
         closed_ls_tvs = oclose theta ls_tvs
         liberal_undet_tvs = (`minusVarSet` closed_ls_tvs) <$> rs_tvs
         conserv_undet_tvs = (`minusVarSet` ls_tvs)        <$> rs_tvs
382

383
         undet_set = fold undetermined_tvs
384

385 386 387 388 389
         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
390 391 392
                      sep [ text "The"
                            <+> ppWhen be_liberal (text "liberal")
                            <+> text "coverage condition fails in class"
393
                            <+> quotes (ppr clas)
394
                          , nest 2 $ text "for functional dependency:"
395
                            <+> quotes (pprFunDep fd) ]
396
                    , sep [ text "Reason: lhs type"<>plural ls <+> pprQuotedList ls
397 398
                          , nest 2 $
                            (if isSingleton ls
399 400 401
                             then text "does not"
                             else text "do not jointly")
                            <+> text "determine rhs type"<>plural rs
402
                            <+> pprQuotedList rs ]
403
                    , text "Un-determined variable" <> pluralVarSet undet_set <> colon
404
                            <+> pprVarSet undet_set (pprWithCommas ppr)
405
                    , ppWhen (isEmptyVarSet $ pSnd undetermined_tvs) $
406
                      ppSuggestExplicitKinds
407 408
                    , ppWhen (not be_liberal &&
                              and (isEmptyVarSet <$> liberal_undet_tvs)) $
409
                      text "Using UndecidableInstances might help" ]
410

411 412
{- Note [Closing over kinds in coverage]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
413 414 415 416 417 418
Suppose we have a fundep  (a::k) -> b
Then if 'a' is instantiated to (x y), where x:k2->*, y:k2,
then fixing x really fixes k2 as well, and so k2 should be added to
the lhs tyvars in the fundep check.

Example (Trac #8391), using liberal coverage
419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465
      data Foo a = ...  -- Foo :: forall k. k -> *
      class Bar a b | a -> b
      instance Bar a (Foo a)

    In the instance decl, (a:k) does fix (Foo k a), but only if we notice
    that (a:k) fixes k.  Trac #10109 is another example.

Here is a more subtle example, from HList-0.4.0.0 (Trac #10564)

  class HasFieldM (l :: k) r (v :: Maybe *)
        | l r -> v where ...
  class HasFieldM1 (b :: Maybe [*]) (l :: k) r v
        | b l r -> v where ...
  class HMemberM (e1 :: k) (l :: [k]) (r :: Maybe [k])
        | e1 l -> r

  data Label :: k -> *
  type family LabelsOf (a :: [*]) ::  *

  instance (HMemberM (Label {k} (l::k)) (LabelsOf xs) b,
            HasFieldM1 b l (r xs) v)
         => HasFieldM l (r xs) v where

Is the instance OK? Does {l,r,xs} determine v?  Well:

  * From the instance constraint HMemberM (Label k l) (LabelsOf xs) b,
    plus the fundep "| el l -> r" in class HMameberM,
    we get {l,k,xs} -> b

  * Note the 'k'!! We must call closeOverKinds on the seed set
    ls_tvs = {l,r,xs}, BEFORE doing oclose, else the {l,k,xs}->b
    fundep won't fire.  This was the reason for #10564.

  * So starting from seeds {l,r,xs,k} we do oclose to get
    first {l,r,xs,k,b}, via the HMemberM constraint, and then
    {l,r,xs,k,b,v}, via the HasFieldM1 constraint.

  * And that fixes v.

However, we must closeOverKinds whenever augmenting the seed set
in oclose!  Consider Trac #10109:

  data Succ a   -- Succ :: forall k. k -> *
  class Add (a :: k1) (b :: k2) (ab :: k3) | a b -> ab
  instance (Add a b ab) => Add (Succ {k1} (a :: k1))
                               b
                               (Succ {k3} (ab :: k3})
466

467 468 469 470
We start with seed set {a:k1,b:k2} and closeOverKinds to {a,k1,b,k2}.
Now use the fundep to extend to {a,k1,b,k2,ab}.  But we need to
closeOverKinds *again* now to {a,k1,b,k2,ab,k3}, so that we fix all
the variables free in (Succ {k3} ab).
471

472
Bottom line:
473 474
  * closeOverKinds on initial seeds (done automatically
    by tyCoVarsOfTypes in checkInstCoverage)
475
  * and closeOverKinds whenever extending those seeds (in oclose)
476

Simon Peyton Jones's avatar
Simon Peyton Jones committed
477 478 479 480 481 482 483 484 485
Note [The liberal coverage condition]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(oclose preds tvs) closes the set of type variables tvs,
wrt functional dependencies in preds.  The result is a superset
of the argument set.  For example, if we have
        class C a b | a->b where ...
then
        oclose [C (x,y) z, C (x,p) q] {x,y} = {x,y,z}
because if we know x and y then that fixes z.
486

Simon Peyton Jones's avatar
Simon Peyton Jones committed
487 488 489 490
We also use equality predicates in the predicates; if we have an
assumption `t1 ~ t2`, then we use the fact that if we know `t1` we
also know `t2` and the other way.
  eg    oclose [C (x,y) z, a ~ x] {a,y} = {a,y,z,x}
491

Austin Seipp's avatar
Austin Seipp committed
492
oclose is used (only) when checking the coverage condition for
Simon Peyton Jones's avatar
Simon Peyton Jones committed
493
an instance declaration
Austin Seipp's avatar
Austin Seipp committed
494
-}
495

496
oclose :: [PredType] -> TyCoVarSet -> TyCoVarSet
Simon Peyton Jones's avatar
Simon Peyton Jones committed
497 498 499
-- See Note [The liberal coverage condition]
oclose preds fixed_tvs
  | null tv_fds = fixed_tvs -- Fast escape hatch for common case.
500
  | otherwise   = fixVarSet extend fixed_tvs
Simon Peyton Jones's avatar
Simon Peyton Jones committed
501
  where
502 503 504
    extend fixed_tvs = foldl add fixed_tvs tv_fds
       where
          add fixed_tvs (ls,rs)
505
            | ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` closeOverKinds rs
506
            | otherwise                = fixed_tvs
507
            -- closeOverKinds: see Note [Closing over kinds in coverage]
508

509 510
    tv_fds  :: [(TyCoVarSet,TyCoVarSet)]
    tv_fds  = [ (tyCoVarsOfTypes ls, tyCoVarsOfTypes rs)
511
              | pred <- preds
512 513 514
              , pred' <- pred : transSuperClasses pred
                   -- Look for fundeps in superclasses too
              , (ls, rs) <- determined pred' ]
515

Simon Peyton Jones's avatar
Simon Peyton Jones committed
516 517 518
    determined :: PredType -> [([Type],[Type])]
    determined pred
       = case classifyPredType pred of
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
519
            EqPred NomEq t1 t2 -> [([t1],[t2]), ([t2],[t1])]
520 521 522
            ClassPred cls tys  -> [ instFD fd cls_tvs tys
                                  | let (cls_tvs, cls_fds) = classTvsFds cls
                                  , fd <- cls_fds ]
523
            _ -> []
524

Austin Seipp's avatar
Austin Seipp committed
525 526 527
{-
************************************************************************
*                                                                      *
528
        Check that a new instance decl is OK wrt fundeps
Austin Seipp's avatar
Austin Seipp committed
529 530
*                                                                      *
************************************************************************
531 532

Here is the bad case:
533 534 535
        class C a b | a->b where ...
        instance C Int Bool where ...
        instance C Int Char where ...
536 537 538 539

The point is that a->b, so Int in the first parameter must uniquely
determine the second.  In general, given the same class decl, and given

540 541
        instance C s1 s2 where ...
        instance C t1 t2 where ...
542 543 544 545

Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).

Matters are a little more complicated if there are free variables in
546
the s2/t2.
547

548 549 550
        class D a b c | a -> b
        instance D a b => D [(a,a)] [b] Int
        instance D a b => D [a]     [b] Bool
551 552 553

The instance decls don't overlap, because the third parameter keeps
them separate.  But we want to make sure that given any constraint
554
        D s1 s2 s3
555
if s1 matches
556 557 558 559 560 561 562 563 564 565 566 567

Note [Bogus consistency check]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In checkFunDeps we check that a new ClsInst is consistent with all the
ClsInsts in the environment.

The bogus aspect is discussed in Trac #10675. Currenty it if the two
types are *contradicatory*, using (isNothing . tcUnifyTys).  But all
the papers say we should check if the two types are *equal* thus
   not (substTys subst rtys1 `eqTypes` substTys subst rtys2)
For now I'm leaving the bogus form because that's the way it has
been for years.
Austin Seipp's avatar
Austin Seipp committed
568
-}
569

570 571
checkFunDeps :: InstEnvs -> ClsInst -> [ClsInst]
-- The Consistency Check.
Edward Z. Yang's avatar
Edward Z. Yang committed
572
-- Check whether adding DFunId would break functional-dependency constraints
573
-- Used only for instance decls defined in the module being compiled
574 575 576 577 578 579 580
-- Returns a list of the ClsInst in InstEnvs that are inconsistent
-- with the proposed new ClsInst
checkFunDeps inst_envs (ClsInst { is_tvs = qtvs1, is_cls = cls
                                , is_tys = tys1, is_tcs = rough_tcs1 })
  | null fds
  = []
  | otherwise
581
  = nubBy eq_inst $
582 583 584
    [ ispec | ispec <- cls_insts
            , fd    <- fds
            , is_inconsistent fd ispec ]
585
  where
586 587 588 589 590 591 592 593
    cls_insts      = classInstances inst_envs cls
    (cls_tvs, fds) = classTvsFds cls
    qtv_set1       = mkVarSet qtvs1

    is_inconsistent fd (ClsInst { is_tvs = qtvs2, is_tys = tys2, is_tcs = rough_tcs2 })
      | instanceCantMatch trimmed_tcs rough_tcs2
      = False
      | otherwise
Richard Eisenberg's avatar
Richard Eisenberg committed
594
      = case tcUnifyTyKis bind_fn ltys1 ltys2 of
595 596 597 598
          Nothing         -> False
          Just subst
            -> isNothing $   -- Bogus legacy test (Trac #10675)
                             -- See Note [Bogus consistency check]
Richard Eisenberg's avatar
Richard Eisenberg committed
599
               tcUnifyTyKis bind_fn (substTysUnchecked subst rtys1) (substTysUnchecked subst rtys2)
600 601 602 603 604 605 606 607 608 609

      where
        trimmed_tcs    = trimRoughMatchTcs cls_tvs fd rough_tcs1
        (ltys1, rtys1) = instFD fd cls_tvs tys1
        (ltys2, rtys2) = instFD fd cls_tvs tys2
        qtv_set2       = mkVarSet qtvs2
        bind_fn tv | tv `elemVarSet` qtv_set1 = BindMe
                   | tv `elemVarSet` qtv_set2 = BindMe
                   | otherwise                = Skolem

610
    eq_inst i1 i2 = instanceDFunId i1 == instanceDFunId i2
611 612 613 614 615 616
        -- An 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
        --      instance C Int Char Char
        -- The second instance conflicts with the first by *both* fundeps
617 618 619

trimRoughMatchTcs :: [TyVar] -> FunDep TyVar -> [Maybe Name] -> [Maybe Name]
-- Computing rough_tcs for a particular fundep
620
--     class C a b c | a -> b where ...
621
-- For each instance .... => C ta tb tc
622
-- we want to match only on the type ta; so our
623
-- rough-match thing must similarly be filtered.
624
-- Hence, we Nothing-ise the tb and tc types right here
625 626
--
-- Result list is same length as input list, just with more Nothings
627
trimRoughMatchTcs clas_tvs (ltvs, _) mb_tcs
628 629
  = zipWith select clas_tvs mb_tcs
  where
630 631
    select clas_tv mb_tc | clas_tv `elem` ltvs = mb_tc
                         | otherwise           = Nothing