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 \begin{code} 11 module FunDeps ( 12 Equation, pprEquation, 13 oclose, grow, improveOne, 14 checkInstCoverage, checkFunDeps, 15 pprFundeps 16 ) where 17 18 #include "HsVersions.h" 19 20 import Name 21 import Var 22 import Class 23 import TcGadt 24 import TcType 25 import InstEnv 26 import VarSet 27 import VarEnv 28 import Outputable 29 import Util 30 import Data.Maybe ( isJust ) 31 \end{code} 32 33 34 %************************************************************************ 35 %* * 36 \subsection{Close type variables} 37 %* * 38 %************************************************************************ 39 40 oclose(vs,C) The result of extending the set of tyvars vs 41 using the functional dependencies from C 42 43 grow(vs,C) The result of extend the set of tyvars vs 44 using all conceivable links from C. 45 46 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e} 47 Then grow(vs,C) = {a,b,c} 48 49 Note that grow(vs,C) `superset` grow(vs,simplify(C)) 50 That is, simplfication can only shrink the result of grow. 51 52 Notice that 53 oclose is conservative v `elem` oclose(vs,C) 54 one way: => v is definitely fixed by vs 55 56 grow is conservative if v might be fixed by vs 57 the other way: => v `elem` grow(vs,C) 58 59 ---------------------------------------------------------- 60 (oclose preds tvs) closes the set of type variables tvs, 61 wrt functional dependencies in preds. The result is a superset 62 of the argument set. For example, if we have 63 class C a b | a->b where ... 64 then 65 oclose [C (x,y) z, C (x,p) q] {x,y} = {x,y,z} 66 because if we know x and y then that fixes z. 67 68 oclose is used (only) when generalising a type T; see extensive 69 notes in TcSimplify. 70 71 Note [Important subtlety in oclose] 72 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 73 Consider (oclose (C Int t) {}), where class C a b | a->b 74 Then, since a->b, 't' is fully determined by Int, and the 75 uniform thing is to return {t}. 76 77 However, consider 78 class D a b c | b->c 79 f x = e -- Generates constraint (D s Int t) 80 -- \x.e has type s->s 81 Then, if (oclose (D s Int t) {}) = {t}, we'll make the function 82 monomorphic in 't', thus 83 f :: forall s. D s Int t => s -> s 84 85 But if this function is never called, t will never be instantiated; 86 the functional dependencies that fix t may well be instance decls in 87 some importing module. But the top-level defaulting of unconstrained 88 type variales will fix t=GHC.Prim.Any, and that's simply a bug. 89 90 Conclusion: oclose only returns a type variable as "fixed" if it 91 depends on at least one type variable in the input fixed_tvs. 92 93 Remember, it's always sound for oclose to return a smaller set. 94 95 \begin{code} 96 oclose :: [PredType] -> TyVarSet -> TyVarSet 97 -- entered 14,369 timesoclose preds fixed_tvs 98 | null tv_fds = fixed_tvs -- Fast escape hatch for common case 99 | isEmptyVarSet fixed_tvs = emptyVarSet -- Note [Important subtlety in oclose] 100 | otherwise = loop fixed_tvs 101 where 102 loop fixed_tvs 103 | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs 104 | otherwise = loop new_fixed_tvs 105 where 106 new_fixed_tvs = foldl extend fixed_tvs tv_fds 107 108 extend fixed_tvs (ls,rs) 109 | not (isEmptyVarSet ls) -- Note [Important subtlety in oclose] 110 , ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` rs 111 | otherwise = fixed_tvs 112 113 tv_fds :: [(TyVarSet,TyVarSet)] 114 -- In our example, tv_fds will be [ ({x,y}, {z}), ({x,p},{q}) ] 115 -- Meaning "knowing x,y fixes z, knowing x,p fixes q" 116 tv_fds = [ (tyVarsOfTypes xs, tyVarsOfTypes ys) 117 | ClassP cls tys <- preds, -- Ignore implicit params 118 let (cls_tvs, cls_fds) = classTvsFds cls, 119 fd <- cls_fds, 120 let (xs,ys) = instFD fd cls_tvs tys 121 ] 122 \end{code} 123 124 Note [Growing the tau-tvs using constraints] 125 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 126 (grow preds tvs) is the result of extend the set of tyvars tvs 127 using all conceivable links from pred 128 129 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e} 130 Then grow precs tvs = {a,b,c} 131 132 All the type variables from an implicit parameter are added, whether or 133 not they are mentioned in tvs; see Note [Implicit parameters and ambiguity] 134 in TcSimplify. 135 136 See also Note [Ambiguity] in TcSimplify 137 138 \begin{code} 139 grow :: [PredType] -> TyVarSet -> TyVarSet 140 -- entered 14,634 timesgrow preds fixed_tvs 141 | null preds = real_fixed_tvs 142 | otherwise = loop real_fixed_tvs 143 where 144 -- Add the implicit parameters; 145 -- see Note [Implicit parameters and ambiguity] in TcSimplify 146 real_fixed_tvs = foldr unionVarSet fixed_tvs ip_tvs 147 148 loop fixed_tvs 149 | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs 150 | otherwise = loop new_fixed_tvs 151 where 152 new_fixed_tvs = foldl extend fixed_tvs non_ip_tvs 153 154 extend fixed_tvs pred_tvs 155 | fixed_tvs `intersectsVarSet` pred_tvs = fixed_tvs `unionVarSet` pred_tvs 156 | otherwise = fixed_tvs 157 158 (ip_tvs, non_ip_tvs) = partitionWith get_ip preds 159 get_ip (IParam _ ty) = Left (tyVarsOfType ty) 160 get_ip other = Right (tyVarsOfPred other) 161 \end{code} 162 163 %************************************************************************ 164 %* * 165 \subsection{Generate equations from functional dependencies} 166 %* * 167 %************************************************************************ 168 169 170 \begin{code} 171 type Equation = (TyVarSet, [(Type, Type)]) 172 -- These pairs of types should be equal, for some 173 -- substitution of the tyvars in the tyvar set 174 -- INVARIANT: corresponding types aren't already equal 175 176 -- It's important that we have a *list* of pairs of types. Consider 177 -- class C a b c | a -> b c where ... 178 -- instance C Int x x where ... 179 -- Then, given the constraint (C Int Bool v) we should improve v to Bool, 180 -- via the equation ({x}, [(Bool,x), (v,x)]) 181 -- This would not happen if the class had looked like 182 -- class C a b c | a -> b, a -> c 183 184 -- To "execute" the equation, make fresh type variable for each tyvar in the set, 185 -- instantiate the two types with these fresh variables, and then unify. 186 -- 187 -- For example, ({a,b}, (a,Int,b), (Int,z,Bool)) 188 -- We unify z with Int, but since a and b are quantified we do nothing to them 189 -- We usually act on an equation by instantiating the quantified type varaibles 190 -- to fresh type variables, and then calling the standard unifier. 191 192 -- never enteredpprEquation (qtvs, pairs) 193 = vcat [ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)), 194 nest 2 (vcat [ ppr t1 <+> ptext SLIT(":=:") <+> ppr t2 | (t1,t2) <- pairs])] 195 \end{code} 196 197 Given a bunch of predicates that must hold, such as 198 199 C Int t1, C Int t2, C Bool t3, ?x::t4, ?x::t5 200 201 improve figures out what extra equations must hold. 202 For example, if we have 203 204 class C a b | a->b where ... 205 206 then improve will return 207 208 [(t1,t2), (t4,t5)] 209 210 NOTA BENE: 211 212 * improve does not iterate. It's possible that when we make 213 t1=t2, for example, that will in turn trigger a new equation. 214 This would happen if we also had 215 C t1 t7, C t2 t8 216 If t1=t2, we also get t7=t8. 217 218 improve does *not* do this extra step. It relies on the caller 219 doing so. 220 221 * The equations unify types that are not already equal. So there 222 is no effect iff the result of improve is empty 223 224 225 226 \begin{code} 227 type Pred_Loc = (PredType, SDoc) -- SDoc says where the Pred comes from 228 229 improveOne :: (Class -> [Instance]) -- Gives instances for given class 230 -> Pred_Loc -- Do improvement triggered by this 231 -> [Pred_Loc] -- Current constraints 232 -> [(Equation,Pred_Loc,Pred_Loc)] -- Derived equalities that must also hold 233 -- (NB the above INVARIANT for type Equation) 234 -- The Pred_Locs explain which two predicates were 235 -- combined (for error messages) 236 -- Just do improvement triggered by a single, distinguised predicate 237 238 -- entered 382,662 timesimproveOne inst_env pred@(IParam ip ty, _) preds 239 = [ ((emptyVarSet, [(ty,ty2)]), pred, p2) 240 | p2@(IParam ip2 ty2, _) <- preds 241 , ip==ip2 242 , not (ty `tcEqType` ty2)] 243 244 improveOne inst_env pred@(ClassP cls tys, _) preds 245 | tys `lengthAtLeast` 2 246 = instance_eqns ++ pairwise_eqns 247 -- NB: we put the instance equations first. This biases the 248 -- order so that we first improve individual constraints against the 249 -- instances (which are perhaps in a library and less likely to be 250 -- wrong; and THEN perform the pairwise checks. 251 -- The other way round, it's possible for the pairwise check to succeed 252 -- and cause a subsequent, misleading failure of one of the pair with an 253 -- instance declaration. See tcfail143.hs for an example 254 where 255 (cls_tvs, cls_fds) = classTvsFds cls 256 instances = inst_env cls 257 rough_tcs = roughMatchTcs tys 258 259 -- NOTE that we iterate over the fds first; they are typically 260 -- empty, which aborts the rest of the loop. 261 pairwise_eqns :: [(Equation,Pred_Loc,Pred_Loc)] 262 pairwise_eqns -- This group comes from pairwise comparison 263 = [ (eqn, pred, p2) 264 | fd <- cls_fds 265 , p2@(ClassP cls2 tys2, _) <- preds 266 , cls == cls2 267 , eqn <- checkClsFD emptyVarSet fd cls_tvs tys tys2 268 ] 269 270 instance_eqns :: [(Equation,Pred_Loc,Pred_Loc)] 271 instance_eqns -- This group comes from comparing with instance decls 272 = [ (eqn, p_inst, pred) 273 | fd <- cls_fds -- Iterate through the fundeps first, 274 -- because there often are none! 275 , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs 276 -- Trim the rough_tcs based on the head of the fundep. 277 -- Remember that instanceCantMatch treats both argumnents 278 -- symmetrically, so it's ok to trim the rough_tcs, 279 -- rather than trimming each inst_tcs in turn 280 , ispec@(Instance { is_tvs = qtvs, is_tys = tys_inst, 281 is_tcs = inst_tcs }) <- instances 282 , not (instanceCantMatch inst_tcs trimmed_tcs) 283 , eqn <- checkClsFD qtvs fd cls_tvs tys_inst tys 284 , let p_inst = (mkClassPred cls tys_inst, 285 ptext SLIT("arising from the instance declaration at") 286 <+> ppr (getSrcLoc ispec)) 287 ] 288 289 improveOne inst_env eq_pred preds 290 = [] 291 292 293 checkClsFD :: TyVarSet -- Quantified type variables; see note below 294 -> FunDep TyVar -> [TyVar] -- One functional dependency from the class 295 -> [Type] -> [Type] 296 -> [Equation] 297 298 -- entered 11,756 timescheckClsFD qtvs fd clas_tvs tys1 tys2 299 -- 'qtvs' are the quantified type variables, the ones which an be instantiated 300 -- to make the types match. For example, given 301 -- class C a b | a->b where ... 302 -- instance C (Maybe x) (Tree x) where .. 303 -- 304 -- and an Inst of form (C (Maybe t1) t2), 305 -- then we will call checkClsFD with 306 -- 307 -- qtvs = {x}, tys1 = [Maybe x, Tree x] 308 -- tys2 = [Maybe t1, t2] 309 -- 310 -- We can instantiate x to t1, and then we want to force 311 -- (Tree x) [t1/x] :=: t2 312 -- 313 -- This function is also used when matching two Insts (rather than an Inst 314 -- against an instance decl. In that case, qtvs is empty, and we are doing 315 -- an equality check 316 -- 317 -- This function is also used by InstEnv.badFunDeps, which needs to *unify* 318 -- For the one-sided matching case, the qtvs are just from the template, 319 -- so we get matching 320 -- 321 = ASSERT2( length tys1 == length tys2 && 322 length tys1 == length clas_tvs 323 , ppr tys1 <+> ppr tys2 ) 324 325 case tcUnifyTys bind_fn ls1 ls2 of 326 Nothing -> [] 327 Just subst | isJust (tcUnifyTys bind_fn rs1' rs2') 328 -- Don't include any equations that already hold. 329 -- Reason: then we know if any actual improvement has happened, 330 -- in which case we need to iterate the solver 331 -- In making this check we must taking account of the fact that any 332 -- qtvs that aren't already instantiated can be instantiated to anything 333 -- at all 334 -> [] 335 336 | otherwise -- Aha! A useful equation 337 -> [ (qtvs', zip rs1' rs2')] 338 -- We could avoid this substTy stuff by producing the eqn 339 -- (qtvs, ls1++rs1, ls2++rs2) 340 -- which will re-do the ls1/ls2 unification when the equation is 341 -- executed. What we're doing instead is recording the partial 342 -- work of the ls1/ls2 unification leaving a smaller unification problem 343 where 344 rs1' = substTys subst rs1 345 rs2' = substTys subst rs2 346 qtvs' = filterVarSet (`notElemTvSubst` subst) qtvs 347 -- qtvs' are the quantified type variables 348 -- that have not been substituted out 349 -- 350 -- Eg. class C a b | a -> b 351 -- instance C Int [y] 352 -- Given constraint C Int z 353 -- we generate the equation 354 -- ({y}, [y], z) 355 where 356 bind_fn tv | tv `elemVarSet` qtvs = BindMe 357 | otherwise = Skolem 358 359 (ls1, rs1) = instFD fd clas_tvs tys1 360 (ls2, rs2) = instFD fd clas_tvs tys2 361 362 instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type 363 -- entered 23,682 timesinstFD (ls,rs) tvs tys 364 = (map lookup ls, map lookup rs) 365 where 366 env = zipVarEnv tvs tys 367 lookup tv = lookupVarEnv_NF env tv 368 \end{code} 369 370 \begin{code} 371 checkInstCoverage :: Class -> [Type] -> Bool 372 -- Check that the Coverage Condition is obeyed in an instance decl 373 -- For example, if we have 374 -- class theta => C a b | a -> b 375 -- instance C t1 t2 376 -- Then we require fv(t2) `subset` fv(t1) 377 -- See Note [Coverage Condition] below 378 379 -- entered 2826 timescheckInstCoverage clas inst_taus 380 = all fundep_ok fds 381 where 382 (tyvars, fds) = classTvsFds clas 383 fundep_ok fd = tyVarsOfTypes rs `subVarSet` tyVarsOfTypes ls 384 where 385 (ls,rs) = instFD fd tyvars inst_taus 386 \end{code} 387 388 Note [Coverage condition] 389 ~~~~~~~~~~~~~~~~~~~~~~~~~ 390 For the coverage condition, we used to require only that 391 fv(t2) `subset` oclose(fv(t1), theta) 392 393 Example: 394 class Mul a b c | a b -> c where 395 (.*.) :: a -> b -> c 396 397 instance Mul Int Int Int where (.*.) = (*) 398 instance Mul Int Float Float where x .*. y = fromIntegral x * y 399 instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v 400 401 In the third instance, it's not the case that fv([c]) `subset` fv(a,[b]). 402 But it is the case that fv([c]) `subset` oclose( theta, fv(a,[b]) ) 403 404 But it is a mistake to accept the instance because then this defn: 405 f = \ b x y -> if b then x .*. [y] else y 406 makes instance inference go into a loop, because it requires the constraint 407 Mul a [b] b 408 409 410 %************************************************************************ 411 %* * 412 Check that a new instance decl is OK wrt fundeps 413 %* * 414 %************************************************************************ 415 416 Here is the bad case: 417 class C a b | a->b where ... 418 instance C Int Bool where ... 419 instance C Int Char where ... 420 421 The point is that a->b, so Int in the first parameter must uniquely 422 determine the second. In general, given the same class decl, and given 423 424 instance C s1 s2 where ... 425 instance C t1 t2 where ... 426 427 Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2). 428 429 Matters are a little more complicated if there are free variables in 430 the s2/t2. 431 432 class D a b c | a -> b 433 instance D a b => D [(a,a)] [b] Int 434 instance D a b => D [a] [b] Bool 435 436 The instance decls don't overlap, because the third parameter keeps 437 them separate. But we want to make sure that given any constraint 438 D s1 s2 s3 439 if s1 matches 440 441 442 \begin{code} 443 checkFunDeps :: (InstEnv, InstEnv) -> Instance 444 -> Maybe [Instance] -- Nothing <=> ok 445 -- Just dfs <=> conflict with dfs 446 -- Check wheher adding DFunId would break functional-dependency constraints 447 -- Used only for instance decls defined in the module being compiled 448 -- entered 8512 timescheckFunDeps inst_envs ispec 449 | null bad_fundeps = Nothing 450 | otherwise = Just bad_fundeps 451 where 452 (ins_tvs, _, clas, ins_tys) = instanceHead ispec 453 ins_tv_set = mkVarSet ins_tvs 454 cls_inst_env = classInstances inst_envs clas 455 bad_fundeps = badFunDeps cls_inst_env clas ins_tv_set ins_tys 456 457 badFunDeps :: [Instance] -> Class 458 -> TyVarSet -> [Type] -- Proposed new instance type 459 -> [Instance] 460 -- entered 8512 timesbadFunDeps cls_insts clas ins_tv_set ins_tys 461 = [ ispec | fd <- fds, -- fds is often empty 462 let trimmed_tcs = trimRoughMatchTcs clas_tvs fd rough_tcs, 463 ispec@(Instance { is_tcs = inst_tcs, is_tvs = tvs, 464 is_tys = tys }) <- cls_insts, 465 -- Filter out ones that can't possibly match, 466 -- based on the head of the fundep 467 not (instanceCantMatch inst_tcs trimmed_tcs), 468 notNull (checkClsFD (tvs `unionVarSet` ins_tv_set) 469 fd clas_tvs tys ins_tys) 470 ] 471 where 472 (clas_tvs, fds) = classTvsFds clas 473 rough_tcs = roughMatchTcs ins_tys 474 475 trimRoughMatchTcs :: [TyVar] -> FunDep TyVar -> [Maybe Name] -> [Maybe Name] 476 -- Computing rough_tcs for a particular fundep 477 -- class C a b c | a -> b where ... 478 -- For each instance .... => C ta tb tc 479 -- we want to match only on the types ta, tc; so our 480 -- rough-match thing must similarly be filtered. 481 -- Hence, we Nothing-ise the tb type right here 482 -- entered 3589 timestrimRoughMatchTcs clas_tvs (_,rtvs) mb_tcs 483 = zipWith select clas_tvs mb_tcs 484 where 485 select clas_tv mb_tc | clas_tv `elem` rtvs = Nothing 486 | otherwise = mb_tc 487 \end{code} 488 489 490