ghc/compiler/types/InstEnv.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section[InstEnv]{Utilities for typechecking instance declarations}
   5
   6 The bits common to TcInstDcls and TcDeriv.
   7
   8 \begin{code}
   9 module InstEnv (
  10         DFunId, ClsInstEnv, InstEnv,
  11
  12         emptyInstEnv, extendInstEnv, pprInstEnv,
  13         lookupInstEnv, InstLookupResult(..),
  14         classInstEnv, simpleDFunClassTyCon
  15     ) where
  16
  17 #include "HsVersions.h"
  18
  19 import Class            ( Class, classTvsFds )
  20 import Var              ( TyVar, Id )
  21 import VarSet
  22 import VarEnv
  23 import Maybes           ( MaybeErr(..), returnMaB, failMaB, thenMaB, maybeToBool )
  24 import Name             ( getSrcLoc )
  25 import TcType           ( Type, tcTyConAppTyCon, mkTyVarTy,
  26                           tcSplitDFunTy, tyVarsOfTypes,
  27                           matchTys, unifyTyListsX, allDistinctTyVars
  28                         )
  29 import PprType          ( pprClassPred )
  30 import FunDeps          ( checkClsFD )
  31 import TyCon            ( TyCon )
  32 import Outputable
  33 import UniqFM           ( UniqFM, lookupWithDefaultUFM, addToUFM, emptyUFM, eltsUFM )
  34 import Id               ( idType )
  35 import ErrUtils         ( Message )
  36 import CmdLineOpts
  37 import Util             ( notNull )
  38 \end{code}
  39
  40
  41 %************************************************************************
  42 %*                                                                      *
  43 \subsection{The key types}
  44 %*                                                                      *
  45 %************************************************************************
  46
  47 \begin{code}
  48 type DFunId     = Id
  49
  50 type InstEnv    = UniqFM ClsInstEnv             -- Maps Class to instances for that class
  51
  52 simpleDFunClassTyCon :: DFunId -> (Class, TyCon)
  53 simpleDFunClassTyCon dfun
  54   = (clas, tycon)
  55   where
  56     (_,_,clas,[ty]) = tcSplitDFunTy (idType dfun)
  57     tycon           = tcTyConAppTyCon ty
  58
  59 pprInstEnv :: InstEnv -> SDoc
  60 pprInstEnv env
  61   = vcat [ brackets (pprWithCommas ppr (varSetElems tyvars)) <+>
  62            brackets (pprWithCommas ppr tys) <+> ppr dfun
  63          | cls_inst_env <-  eltsUFM env
  64          , (tyvars, tys, dfun) <- cls_inst_env
  65          ]
  66 \end{code}
  67
  68 %************************************************************************
  69 %*                                                                      *
  70 \subsection{Instance environments: InstEnv and ClsInstEnv}
  71 %*                                                                      *
  72 %************************************************************************
  73
  74 \begin{code}
  75 type ClsInstEnv = [(TyVarSet, [Type], DFunId)]  -- The instances for a particular class
  76         -- INVARIANTs: see notes below
  77
  78 emptyInstEnv :: InstEnv
  79 emptyInstEnv = emptyUFM
  80
  81 classInstEnv :: InstEnv -> Class -> ClsInstEnv
  82 classInstEnv env cls = lookupWithDefaultUFM env [] cls
  83 \end{code}
  84
  85 A @ClsInstEnv@ all the instances of that class.  The @Id@ inside a
  86 ClsInstEnv mapping is the dfun for that instance.
  87
  88 If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
  89
  90         forall a b, C t1 t2 t3  can be constructed by dfun
  91
  92 or, to put it another way, we have
  93
  94         instance (...) => C t1 t2 t3,  witnessed by dfun
  95
  96 There is an important consistency constraint in the elements of a ClsInstEnv:
  97
  98   * [a,b] must be a superset of the free vars of [t1,t2,t3]
  99
 100   * The dfun must itself be quantified over [a,b]
 101
 102   * More specific instances come before less specific ones,
 103     where they overlap
 104
 105 Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
 106         [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
 107 The "a" in the pattern must be one of the forall'd variables in
 108 the dfun type.
 109
 110
 111
 112 Notes on overlapping instances
 113 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 114 In some ClsInstEnvs, overlap is prohibited; that is, no pair of templates unify.
 115
 116 In others, overlap is permitted, but only in such a way that one can make
 117 a unique choice when looking up.  That is, overlap is only permitted if
 118 one template matches the other, or vice versa.  So this is ok:
 119
 120   [a]  [Int]
 121
 122 but this is not
 123
 124   (Int,a)  (b,Int)
 125
 126 If overlap is permitted, the list is kept most specific first, so that
 127 the first lookup is the right choice.
 128
 129
 130 For now we just use association lists.
 131
 132 \subsection{Avoiding a problem with overlapping}
 133
 134 Consider this little program:
 135
 136 \begin{pseudocode}
 137      class C a        where c :: a
 138      class C a => D a where d :: a
 139
 140      instance C Int where c = 17
 141      instance D Int where d = 13
 142
 143      instance C a => C [a] where c = [c]
 144      instance ({- C [a], -} D a) => D [a] where d = c
 145
 146      instance C [Int] where c = [37]
 147
 148      main = print (d :: [Int])
 149 \end{pseudocode}
 150
 151 What do you think `main' prints  (assuming we have overlapping instances, and
 152 all that turned on)?  Well, the instance for `D' at type `[a]' is defined to
 153 be `c' at the same type, and we've got an instance of `C' at `[Int]', so the
 154 answer is `[37]', right? (the generic `C [a]' instance shouldn't apply because
 155 the `C [Int]' instance is more specific).
 156
 157 Ghc-4.04 gives `[37]', while ghc-4.06 gives `[17]', so 4.06 is wrong.  That
 158 was easy ;-)  Let's just consult hugs for good measure.  Wait - if I use old
 159 hugs (pre-September99), I get `[17]', and stranger yet, if I use hugs98, it
 160 doesn't even compile!  What's going on!?
 161
 162 What hugs complains about is the `D [a]' instance decl.
 163
 164 \begin{pseudocode}
 165      ERROR "mj.hs" (line 10): Cannot build superclass instance
 166      *** Instance            : D [a]
 167      *** Context supplied    : D a
 168      *** Required superclass : C [a]
 169 \end{pseudocode}
 170
 171 You might wonder what hugs is complaining about.  It's saying that you
 172 need to add `C [a]' to the context of the `D [a]' instance (as appears
 173 in comments).  But there's that `C [a]' instance decl one line above
 174 that says that I can reduce the need for a `C [a]' instance to the
 175 need for a `C a' instance, and in this case, I already have the
 176 necessary `C a' instance (since we have `D a' explicitly in the
 177 context, and `C' is a superclass of `D').
 178
 179 Unfortunately, the above reasoning indicates a premature commitment to the
 180 generic `C [a]' instance.  I.e., it prematurely rules out the more specific
 181 instance `C [Int]'.  This is the mistake that ghc-4.06 makes.  The fix is to
 182 add the context that hugs suggests (uncomment the `C [a]'), effectively
 183 deferring the decision about which instance to use.
 184
 185 Now, interestingly enough, 4.04 has this same bug, but it's covered up
 186 in this case by a little known `optimization' that was disabled in
 187 4.06.  Ghc-4.04 silently inserts any missing superclass context into
 188 an instance declaration.  In this case, it silently inserts the `C
 189 [a]', and everything happens to work out.
 190
 191 (See `basicTypes/MkId:mkDictFunId' for the code in question.  Search for
 192 `Mark Jones', although Mark claims no credit for the `optimization' in
 193 question, and would rather it stopped being called the `Mark Jones
 194 optimization' ;-)
 195
 196 So, what's the fix?  I think hugs has it right.  Here's why.  Let's try
 197 something else out with ghc-4.04.  Let's add the following line:
 198
 199     d' :: D a => [a]
 200     d' = c
 201
 202 Everyone raise their hand who thinks that `d :: [Int]' should give a
 203 different answer from `d' :: [Int]'.  Well, in ghc-4.04, it does.  The
 204 `optimization' only applies to instance decls, not to regular
 205 bindings, giving inconsistent behavior.
 206
 207 Old hugs had this same bug.  Here's how we fixed it: like GHC, the
 208 list of instances for a given class is ordered, so that more specific
 209 instances come before more generic ones.  For example, the instance
 210 list for C might contain:
 211     ..., C Int, ..., C a, ...
 212 When we go to look for a `C Int' instance we'll get that one first.
 213 But what if we go looking for a `C b' (`b' is unconstrained)?  We'll
 214 pass the `C Int' instance, and keep going.  But if `b' is
 215 unconstrained, then we don't know yet if the more specific instance
 216 will eventually apply.  GHC keeps going, and matches on the generic `C
 217 a'.  The fix is to, at each step, check to see if there's a reverse
 218 match, and if so, abort the search.  This prevents hugs from
 219 prematurely chosing a generic instance when a more specific one
 220 exists.
 221
 222 --Jeff
 223
 224 BUT NOTE [Nov 2001]: we must actually *unify* not reverse-match in
 225 this test.  Suppose the instance envt had
 226     ..., forall a b. C a a b, ..., forall a b c. C a b c, ...
 227 (still most specific first)
 228 Now suppose we are looking for (C x y Int), where x and y are unconstrained.
 229         C x y Int  doesn't match the template {a,b} C a a b
 230 but neither does
 231         C a a b  match the template {x,y} C x y Int
 232 But still x and y might subsequently be unified so they *do* match.
 233
 234 Simple story: unify, don't match.
 235
 236
 237 %************************************************************************
 238 %*                                                                      *
 239 \subsection{Looking up an instance}
 240 %*                                                                      *
 241 %************************************************************************
 242
 243 @lookupInstEnv@ looks up in a @InstEnv@, using a one-way match.  Since
 244 the env is kept ordered, the first match must be the only one.  The
 245 thing we are looking up can have an arbitrary "flexi" part.
 246
 247 \begin{code}
 248 lookupInstEnv :: DynFlags
 249               -> InstEnv                -- The envt
 250               -> Class -> [Type]        -- What we are looking for
 251               -> InstLookupResult
 252
 253 data InstLookupResult
 254   = FoundInst                   -- There is a (template,substitution) pair
 255                                 -- that makes the template match the key,
 256                                 -- and no template is an instance of the key
 257         TyVarSubstEnv Id
 258
 259   | NoMatch Bool        -- Boolean is true iff there is at least one
 260                         -- template that matches the key.
 261                         -- (but there are other template(s) that are
 262                         --  instances of the key, so we don't report
 263                         --  FoundInst)
 264         -- The NoMatch True case happens when we look up
 265         --      Foo [a]
 266         -- in an InstEnv that has entries for
 267         --      Foo [Int]
 268         --      Foo [b]
 269         -- Then which we choose would depend on the way in which 'a'
 270         -- is instantiated.  So we say there is no match, but identify
 271         -- it as ambiguous case in the hope of giving a better error msg.
 272         -- See the notes above from Jeff Lewis
 273
 274 lookupInstEnv dflags env key_cls key_tys
 275   = find (classInstEnv env key_cls)
 276   where
 277     key_vars = tyVarsOfTypes key_tys
 278
 279     find [] = NoMatch False
 280     find ((tpl_tyvars, tpl, dfun_id) : rest)
 281       = case matchTys tpl_tyvars tpl key_tys of
 282           Nothing                 ->
 283                 -- Check whether the things unify, so that
 284                 -- we bale out if a later instantiation of this
 285                 -- predicate might match this instance
 286                 -- [see notes about overlapping instances above]
 287             case unifyTyListsX (key_vars `unionVarSet` tpl_tyvars) key_tys tpl of
 288               Just _ | not (dopt Opt_AllowIncoherentInstances dflags)
 289                      -> NoMatch (any_match rest)
 290                 -- If we allow incoherent instances we don't worry about the
 291                 -- test and just blaze on anyhow.  Requested by John Hughes.
 292               other  -> find rest
 293
 294           Just (subst, leftovers) -> ASSERT( null leftovers )
 295                                      FoundInst subst dfun_id
 296
 297     any_match rest = or [ maybeToBool (matchTys tvs tpl key_tys)
 298                         | (tvs,tpl,_) <- rest
 299                         ]
 300 \end{code}
 301
 302
 303 %************************************************************************
 304 %*                                                                      *
 305 \subsection{Extending an instance environment}
 306 %*                                                                      *
 307 %************************************************************************
 308
 309 @extendInstEnv@ extends a @ClsInstEnv@, checking for overlaps.
 310
 311 A boolean flag controls overlap reporting.
 312
 313 True => overlap is permitted, but only if one template matches the other;
 314         not if they unify but neither is
 315
 316 \begin{code}
 317 extendInstEnv :: DynFlags -> InstEnv -> [DFunId] -> (InstEnv, [Message])
 318   -- Similar, but all we have is the DFuns
 319 extendInstEnv dflags env dfun_ids = foldl (addToInstEnv dflags) (env, []) dfun_ids
 320
 321
 322 addToInstEnv :: DynFlags
 323              -> (InstEnv, [Message])
 324              -> DFunId
 325              -> (InstEnv, [Message])    -- Resulting InstEnv and augmented error messages
 326
 327 addToInstEnv dflags (inst_env, errs) dfun_id
 328         -- Check first that the new instance doesn't
 329         -- conflict with another.  See notes below about fundeps.
 330   | notNull bad_fundeps
 331   = (inst_env, fundep_err : errs)               -- Bad fundeps; report the first only
 332
 333   | otherwise
 334   = case insert_into cls_inst_env of
 335         Failed err        -> (inst_env, err : errs)
 336         Succeeded new_env -> (addToUFM inst_env clas new_env, errs)
 337
 338   where
 339     cls_inst_env = classInstEnv inst_env clas
 340     (ins_tvs, _, clas, ins_tys) = tcSplitDFunTy (idType dfun_id)
 341     bad_fundeps = badFunDeps cls_inst_env clas ins_tv_set ins_tys
 342     fundep_err  = fundepErr dfun_id (head bad_fundeps)
 343
 344     ins_tv_set = mkVarSet ins_tvs
 345     ins_item   = (ins_tv_set, ins_tys, dfun_id)
 346
 347     insert_into [] = returnMaB [ins_item]
 348     insert_into env@(cur_item@(tpl_tvs, tpl_tys, tpl_dfun_id) : rest)
 349       = case unifyTyListsX (ins_tv_set `unionVarSet` tpl_tvs) tpl_tys ins_tys of
 350           Just subst -> insert_unifiable env subst
 351           Nothing    -> carry_on cur_item rest
 352
 353     carry_on cur_item rest = insert_into rest     `thenMaB` \ rest' ->
 354                              returnMaB (cur_item : rest')
 355
 356             -- The two templates unify.  This is acceptable iff
 357             -- (a) -fallow-overlapping-instances is on
 358             -- (b) one is strictly more specific than the other
 359             -- [It's bad if they are identical or incomparable]
 360     insert_unifiable env@(cur_item@(tpl_tvs, tpl_tys, tpl_dfun_id) : rest) subst
 361       |  ins_item_more_specific && cur_item_more_specific
 362       =         -- Duplicates
 363         failMaB (dupInstErr dfun_id tpl_dfun_id)
 364
 365       |  not (dopt Opt_AllowOverlappingInstances dflags)
 366       || not (ins_item_more_specific || cur_item_more_specific)
 367       =         -- Overlap illegal, or the two are incomparable
 368          failMaB (overlapErr dfun_id tpl_dfun_id)
 369
 370       | otherwise
 371       =         -- OK, it's acceptable.  Remaining question is whether
 372                 -- we drop it here or compare it with others
 373         if ins_item_more_specific then
 374                 -- New item is an instance of current item, so drop it here
 375             returnMaB (ins_item : env)
 376         else
 377             carry_on cur_item rest
 378
 379       where
 380         ins_item_more_specific = allVars subst ins_tvs
 381         cur_item_more_specific = allVars subst (varSetElems tpl_tvs)
 382
 383 allVars :: TyVarSubstEnv -> [TyVar] -> Bool
 384 -- True iff all the type vars are mapped to distinct type vars
 385 allVars subst tvs
 386   = allDistinctTyVars (map lookup tvs) emptyVarSet
 387   where
 388     lookup tv = case lookupSubstEnv subst tv of
 389                   Just (DoneTy ty) -> ty
 390                   Nothing          -> mkTyVarTy tv
 391 \end{code}
 392
 393 Functional dependencies
 394 ~~~~~~~~~~~~~~~~~~~~~~~
 395 Here is the bad case:
 396         class C a b | a->b where ...
 397         instance C Int Bool where ...
 398         instance C Int Char where ...
 399
 400 The point is that a->b, so Int in the first parameter must uniquely
 401 determine the second.  In general, given the same class decl, and given
 402
 403         instance C s1 s2 where ...
 404         instance C t1 t2 where ...
 405
 406 Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
 407
 408 Matters are a little more complicated if there are free variables in
 409 the s2/t2.
 410
 411         class D a b c | a -> b
 412         instance D a b => D [(a,a)] [b] Int
 413         instance D a b => D [a]     [b] Bool
 414
 415 The instance decls don't overlap, because the third parameter keeps
 416 them separate.  But we want to make sure that given any constraint
 417         D s1 s2 s3
 418 if s1 matches
 419
 420
 421
 422
 423 \begin{code}
 424 badFunDeps :: ClsInstEnv -> Class
 425            -> TyVarSet -> [Type]        -- Proposed new instance type
 426            -> [DFunId]
 427 badFunDeps cls_inst_env clas ins_tv_set ins_tys
 428   = [ dfun_id | fd <- fds,
 429                (tvs, tys, dfun_id) <- cls_inst_env,
 430                notNull (checkClsFD (tvs `unionVarSet` ins_tv_set) fd clas_tvs tys ins_tys)
 431     ]
 432   where
 433     (clas_tvs, fds) = classTvsFds clas
 434 \end{code}
 435
 436
 437 \begin{code}
 438 dupInstErr dfun1 dfun2 = addInstErr (ptext SLIT("Duplicate instance declarations:"))  dfun1 dfun2
 439 overlapErr dfun1 dfun2 = addInstErr (ptext SLIT("Overlapping instance declarations:")) dfun1 dfun2
 440 fundepErr  dfun1 dfun2 = addInstErr (ptext SLIT("Functional dependencies conflict between instance declarations:"))
 441                                     dfun1 dfun2
 442
 443 addInstErr what dfun1 dfun2
 444  = hang what 2 (ppr_dfun dfun1 $$ ppr_dfun dfun2)
 445   where
 446     ppr_dfun dfun = ppr (getSrcLoc dfun) <> colon <+> pprClassPred clas tys
 447                   where
 448                     (_,_,clas,tys) = tcSplitDFunTy (idType dfun)
 449 \end{code}