TcCanonical.lhs 55.1 KB
Newer Older
 simonpj@microsoft.com committed Sep 13, 2010 1 \begin{code}  Ian Lynagh committed Nov 04, 2011 2 3 4 5 6 7 8 {-# OPTIONS -fno-warn-tabs #-} -- The above warning supression flag is a temporary kludge. -- While working on this module you are encouraged to remove it and -- detab the module (please do the detabbing in a separate patch). See -- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces -- for details  simonpj@microsoft.com committed Sep 13, 2010 9 module TcCanonical(  Simon Peyton Jones committed Aug 31, 2012 10  canonicalize, occurCheckExpand, emitWorkNC,  dimitris committed Nov 16, 2011 11  StopOrContinue (..)  simonpj@microsoft.com committed Sep 13, 2010 12 13 14 15 16 17  ) where #include "HsVersions.h" import TcRnTypes import TcType  18 import Type  dreixel committed Nov 11, 2011 19 import Kind  Simon Peyton Jones committed Dec 05, 2011 20 import TcEvidence  simonpj@microsoft.com committed Sep 13, 2010 21 22 23 24 import Class import TyCon import TypeRep import Var  dimitris committed Nov 16, 2011 25 import VarEnv  simonpj@microsoft.com committed Sep 13, 2010 26 import Outputable  Simon Peyton Jones committed Apr 16, 2012 27 import Control.Monad ( when )  simonpj@microsoft.com committed Sep 13, 2010 28 29 import MonadUtils import Control.Applicative ( (<|>) )  Simon Peyton Jones committed Aug 30, 2012 30 import TysWiredIn ( eqTyCon )  simonpj@microsoft.com committed Sep 13, 2010 31 32  import VarSet  simonpj@microsoft.com committed Jan 12, 2011 33 import TcSMonad  simonpj@microsoft.com committed Feb 17, 2011 34 import FastString  simonpj@microsoft.com committed Sep 13, 2010 35   Ian Lynagh committed Jun 05, 2012 36 import Util  Simon Peyton Jones committed Sep 20, 2012 37 import Maybes( catMaybes )  dimitris committed Nov 16, 2011 38 \end{code}  simonpj@microsoft.com committed Sep 13, 2010 39 40 41 42  %************************************************************************ %* *  dimitris committed Nov 16, 2011 43 %* The Canonicaliser *  simonpj@microsoft.com committed Sep 13, 2010 44 45 46 %* * %************************************************************************  dimitris committed Nov 16, 2011 47 48 Note [Canonicalization] ~~~~~~~~~~~~~~~~~~~~~~~  simonpj@microsoft.com committed Sep 13, 2010 49   dimitris committed Nov 16, 2011 50 51 52 53 Canonicalization converts a flat constraint to a canonical form. It is unary (i.e. treats individual constraints one at a time), does not do any zonking, but lives in TcS monad because it needs to create fresh variables (for flattening) and consult the inerts (for efficiency).  simonpj@microsoft.com committed Sep 13, 2010 54   dimitris committed Nov 16, 2011 55 56 57 58 59 The execution plan for canonicalization is the following: 1) Decomposition of equalities happens as necessary until we reach a variable or type family in one side. There is no decomposition step for other forms of constraints.  simonpj@microsoft.com committed Sep 13, 2010 60   dimitris committed Nov 16, 2011 61 62 63 64  2) If, when we decompose, we discover a variable on the head then we look at inert_eqs from the current inert for a substitution for this variable and contine decomposing. Hence we lazily apply the inert substitution if it is needed.  simonpj@microsoft.com committed Sep 13, 2010 65   dimitris committed Nov 16, 2011 66 67  3) If no more decomposition is possible, we deeply apply the substitution from the inert_eqs and continue with flattening.  simonpj@microsoft.com committed Sep 13, 2010 68   dimitris committed Nov 16, 2011 69 70 71 72 73  4) During flattening, we examine whether we have already flattened some function application by looking at all the CTyFunEqs with the same function in the inert set. The reason for deeply applying the inert substitution at step (3) is to maximise our chances of matching an already flattened family application in the inert.  simonpj@microsoft.com committed Sep 13, 2010 74   dimitris committed Nov 16, 2011 75 76 77 78 The net result is that a constraint coming out of the canonicalization phase cannot be rewritten any further from the inerts (but maybe /it/ can rewrite an inert or still interact with an inert in a further phase in the simplifier.  dimitris committed May 17, 2011 79   simonpj@microsoft.com committed Sep 13, 2010 80 \begin{code}  dimitris committed May 18, 2011 81   dimitris committed Nov 16, 2011 82 83 84 85 86 87 88 -- Informative results of canonicalization data StopOrContinue = ContinueWith Ct -- Either no canonicalization happened, or if some did -- happen, it is still safe to just keep going with this -- work item. | Stop -- Some canonicalization happened, extra work is now in -- the TcS WorkList.  simonpj@microsoft.com committed Sep 13, 2010 89   dimitris committed Nov 16, 2011 90 91 92 instance Outputable StopOrContinue where ppr Stop = ptext (sLit "Stop") ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w  simonpj@microsoft.com committed Sep 13, 2010 93 94   dimitris committed Nov 16, 2011 95 96 continueWith :: Ct -> TcS StopOrContinue continueWith = return . ContinueWith  simonpj@microsoft.com committed Sep 13, 2010 97   dimitris committed Nov 16, 2011 98 99 100 101 102 103 104 105 andWhenContinue :: TcS StopOrContinue -> (Ct -> TcS StopOrContinue) -> TcS StopOrContinue andWhenContinue tcs1 tcs2 = do { r <- tcs1 ; case r of Stop -> return Stop ContinueWith ct -> tcs2 ct }  simonpj@microsoft.com committed Sep 13, 2010 106 107 108  \end{code}  dimitris committed Nov 16, 2011 109 110 Note [Caching for canonicals] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~  Simon Peyton Jones committed Feb 16, 2012 111 112 113 114 Our plan with pre-canonicalization is to be able to solve a constraint really fast from existing bindings in TcEvBinds. So one may think that the condition (isCNonCanonical) is not necessary. However consider the following setup:  simonpj@microsoft.com committed Sep 13, 2010 115   dimitris committed Nov 16, 2011 116 117 InertSet = { [W] d1 : Num t } WorkList = { [W] d2 : Num t, [W] c : t ~ Int}  simonpj@microsoft.com committed Sep 13, 2010 118   Simon Peyton Jones committed Feb 16, 2012 119 120 121 122 123 Now, we prioritize equalities, but in our concrete example (should_run/mc17.hs) the first (d2) constraint is dealt with first, because (t ~ Int) is an equality that only later appears in the worklist since it is pulled out from a nested implication constraint. So, let's examine what happens:  dimitris committed Nov 16, 2011 124 125 126 127 128 129 130 131  - We encounter work item (d2 : Num t) - Nothing is yet in EvBinds, so we reach the interaction with inerts and set: d2 := d1 and we discard d2 from the worklist. The inert set remains unaffected.  Simon Peyton Jones committed Feb 16, 2012 132 133 134  - Now the equation ([W] c : t ~ Int) is encountered and kicks-out (d1 : Num t) from the inerts. Then that equation gets spontaneously solved, perhaps. We end up with:  dimitris committed Nov 16, 2011 135 136 137  InertSet : { [G] c : t ~ Int } WorkList : { [W] d1 : Num t}  Simon Peyton Jones committed Feb 16, 2012 138 139  - Now we examine (d1), we observe that there is a binding for (Num t) in the evidence binds and we set:  dimitris committed Nov 16, 2011 140 141 142  d1 := d2 and end up in a loop!  Simon Peyton Jones committed Feb 16, 2012 143 144 145 146 147 148 149 150 Now, the constraints that get kicked out from the inert set are always Canonical, so by restricting the use of the pre-canonicalizer to NonCanonical constraints we eliminate this danger. Moreover, for canonical constraints we already have good caching mechanisms (effectively the interaction solver) and we are interested in reducing things like superclasses of the same non-canonical constraint being generated hence I don't expect us to lose a lot by introducing the (isCNonCanonical) restriction.  dimitris committed Nov 16, 2011 151   Simon Peyton Jones committed Feb 16, 2012 152 153 154 155 156 157 158 A similar situation can arise in TcSimplify, at the end of the solve_wanteds function, where constraints from the inert set are returned as new work -- our substCt ensures however that if they are not rewritten by subst, they remain canonical and hence we will not attempt to solve them from the EvBinds. If on the other hand they did get rewritten and are now non-canonical they will still not match the EvBinds, so we are again good.  simonpj@microsoft.com committed Sep 13, 2010 159   dimitris committed Nov 29, 2011 160 161   dimitris committed Nov 16, 2011 162 \begin{code}  simonpj@microsoft.com committed Sep 13, 2010 163   dimitris committed Nov 16, 2011 164 165 166 167 -- Top-level canonicalization -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ canonicalize :: Ct -> TcS StopOrContinue  Simon Peyton Jones committed Sep 17, 2012 168 canonicalize ct@(CNonCanonical { cc_ev = ev, cc_loc = d })  dimitris committed Nov 16, 2011 169  = do { traceTcS "canonicalize (non-canonical)" (ppr ct)  dimitris committed Nov 28, 2011 170  ; {-# SCC "canEvVar" #-}  Simon Peyton Jones committed Sep 17, 2012 171  canEvNC d ev }  dimitris committed Nov 16, 2011 172   Simon Peyton Jones committed Sep 17, 2012 173 174 canonicalize (CDictCan { cc_loc = d , cc_ev = ev  dimitris committed Nov 16, 2011 175 176  , cc_class = cls , cc_tyargs = xis })  dimitris committed Nov 28, 2011 177  = {-# SCC "canClass" #-}  Simon Peyton Jones committed Sep 17, 2012 178 179 180  canClass d ev cls xis -- Do not add any superclasses canonicalize (CTyEqCan { cc_loc = d , cc_ev = ev  dimitris committed Nov 16, 2011 181 182  , cc_tyvar = tv , cc_rhs = xi })  Simon Peyton Jones committed Sep 20, 2012 183 184  = {-# SCC "canEqLeafTyVarEq" #-} canEqLeafTyVarEq d ev tv xi  dimitris committed Nov 16, 2011 185   Simon Peyton Jones committed Sep 17, 2012 186 187 canonicalize (CFunEqCan { cc_loc = d , cc_ev = ev  dimitris committed Nov 16, 2011 188 189 190  , cc_fun = fn , cc_tyargs = xis1 , cc_rhs = xi2 })  Simon Peyton Jones committed Aug 30, 2012 191  = {-# SCC "canEqLeafFunEq" #-}  Simon Peyton Jones committed Sep 20, 2012 192  canEqLeafFunEq d ev fn xis1 xi2  dimitris committed Nov 16, 2011 193   Simon Peyton Jones committed Sep 17, 2012 194 canonicalize (CIrredEvCan { cc_ev = ev  Simon Peyton Jones committed Sep 17, 2012 195 196 197 198  , cc_loc = d }) = canIrred d ev canonicalize (CHoleCan { cc_ev = ev, cc_loc = d }) = canHole d ev  dimitris committed Nov 16, 2011 199   Simon Peyton Jones committed Sep 17, 2012 200 canEvNC :: CtLoc -> CtEvidence -> TcS StopOrContinue  dimitris committed Dec 22, 2011 201 -- Called only for non-canonical EvVars  Simon Peyton Jones committed Sep 17, 2012 202 203 204 205 206 canEvNC d ev = case classifyPredType (ctEvPred ev) of ClassPred cls tys -> canClassNC d ev cls tys EqPred ty1 ty2 -> canEqNC d ev ty1 ty2 TuplePred tys -> canTuple d ev tys  Simon Peyton Jones committed Sep 17, 2012 207  IrredPred {} -> canIrred d ev  Simon Peyton Jones committed Feb 16, 2012 208 209 210 211 212 213 214 215 216 217 \end{code} %************************************************************************ %* * %* Tuple Canonicalization %* * %************************************************************************ \begin{code}  Simon Peyton Jones committed Sep 17, 2012 218 219 canTuple :: CtLoc -> CtEvidence -> [PredType] -> TcS StopOrContinue canTuple d ev tys  dimitris committed Mar 28, 2012 220 221 222  = do { traceTcS "can_pred" (text "TuplePred!") ; let xcomp = EvTupleMk xdecomp x = zipWith (\_ i -> EvTupleSel x i) tys [0..]  Simon Peyton Jones committed Sep 17, 2012 223  ; ctevs <- xCtFlavor ev tys (XEvTerm xcomp xdecomp)  Simon Peyton Jones committed Aug 30, 2012 224  ; canEvVarsCreated d ctevs }  Simon Peyton Jones committed Feb 16, 2012 225 226 227 228 229 230 231 \end{code} %************************************************************************ %* * %* Class Canonicalization %* * %************************************************************************  dimitris committed Nov 16, 2011 232   Simon Peyton Jones committed Feb 16, 2012 233 234 \begin{code} canClass, canClassNC  Simon Peyton Jones committed Sep 17, 2012 235  :: CtLoc  Simon Peyton Jones committed May 07, 2012 236  -> CtEvidence  Simon Peyton Jones committed Feb 16, 2012 237  -> Class -> [Type] -> TcS StopOrContinue  dimitris committed Nov 16, 2011 238 -- Precondition: EvVar is class evidence  Simon Peyton Jones committed Feb 16, 2012 239 240 241 242 243 244  -- The canClassNC version is used on non-canonical constraints -- and adds superclasses. The plain canClass version is used -- for already-canonical class constraints (but which might have -- been subsituted or somthing), and hence do not need superclasses  Simon Peyton Jones committed Sep 17, 2012 245 246 canClassNC d ev cls tys = canClass d ev cls tys  Simon Peyton Jones committed Feb 16, 2012 247 248  andWhenContinue emitSuperclasses  Simon Peyton Jones committed Sep 17, 2012 249 canClass d ev cls tys  Simon Peyton Jones committed Oct 01, 2012 250  = do { (xis, cos) <- flattenMany d FMFullFlatten (ctEvFlavour ev) tys  Simon Peyton Jones committed Dec 05, 2011 251  ; let co = mkTcTyConAppCo (classTyCon cls) cos  dimitris committed Nov 16, 2011 252  xi = mkClassPred cls xis  Simon Peyton Jones committed Sep 17, 2012 253  ; mb <- rewriteCtFlavor ev xi co  dimitris committed Mar 28, 2012 254  ; case mb of  Simon Peyton Jones committed Oct 01, 2012 255 256 257 258  Nothing -> return Stop Just new_ev -> continueWith $CDictCan { cc_ev = new_ev, cc_loc = d , cc_tyargs = xis, cc_class = cls } }  dimitris committed Mar 28, 2012 259   Simon Peyton Jones committed Feb 16, 2012 260 emitSuperclasses :: Ct -> TcS StopOrContinue  Simon Peyton Jones committed Sep 17, 2012 261 emitSuperclasses ct@(CDictCan { cc_loc = d, cc_ev = ev  Simon Peyton Jones committed Feb 16, 2012 262 263 264  , cc_tyargs = xis_new, cc_class = cls }) -- Add superclasses of this one here, See Note [Adding superclasses]. -- But only if we are not simplifying the LHS of a rule.  Simon Peyton Jones committed Sep 17, 2012 265  = do { newSCWorkFromFlavored d ev cls xis_new  Simon Peyton Jones committed Feb 16, 2012 266 267 268 269 270  -- Arguably we should "seq" the coercions if they are derived, -- as we do below for emit_kind_constraint, to allow errors in -- superclasses to be executed if deferred to runtime! ; continueWith ct } emitSuperclasses _ = panic "emit_superclasses of non-class!"  simonpj@microsoft.com committed Nov 18, 2010 271 272 273 274 275 276 277 278 279 280 281 282 283 284 \end{code} Note [Adding superclasses] ~~~~~~~~~~~~~~~~~~~~~~~~~~ Since dictionaries are canonicalized only once in their lifetime, the place to add their superclasses is canonicalisation (The alternative would be to do it during constraint solving, but we'd have to be extremely careful to not repeatedly introduced the same superclass in our worklist). Here is what we do: For Givens: We add all their superclasses as Givens. For Wanteds:  simonpj@microsoft.com committed Jan 12, 2011 285 286  Generally speaking we want to be able to add superclasses of wanteds for two reasons:  simonpj@microsoft.com committed Nov 18, 2010 287   simonpj@microsoft.com committed Jan 12, 2011 288 289 290 291 292 293 294 295 296  (1) Oportunities for improvement. Example: class (a ~ b) => C a b Wanted constraint is: C alpha beta We'd like to simply have C alpha alpha. Similar situations arise in relation to functional dependencies. (2) To have minimal constraints to quantify over: For instance, if our wanted constraint is (Eq a, Ord a) we'd only like to quantify over Ord a.  simonpj@microsoft.com committed Nov 18, 2010 297   simonpj@microsoft.com committed Jan 12, 2011 298 299 300 301 302 303 304 305 306 307 308 309  To deal with (1) above we only add the superclasses of wanteds which may lead to improvement, that is: equality superclasses or superclasses with functional dependencies. We deal with (2) completely independently in TcSimplify. See Note [Minimize by SuperClasses] in TcSimplify. Moreover, in all cases the extra improvement constraints are Derived. Derived constraints have an identity (for now), but we don't do anything with their evidence. For instance they are never used to rewrite other constraints.  simonpj@microsoft.com committed Nov 18, 2010 310   simonpj@microsoft.com committed Jan 12, 2011 311  See also [New Wanted Superclass Work] in TcInteract.  simonpj@microsoft.com committed Nov 18, 2010 312   simonpj@microsoft.com committed Jan 12, 2011 313 314 315  For Deriveds: We do nothing.  simonpj@microsoft.com committed Nov 18, 2010 316 317 318  Here's an example that demonstrates why we chose to NOT add superclasses during simplification: [Comes from ticket #4497]  dimitris committed May 17, 2011 319   simonpj@microsoft.com committed Nov 18, 2010 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336  class Num (RealOf t) => Normed t type family RealOf x Assume the generated wanted constraint is: RealOf e ~ e, Normed e If we were to be adding the superclasses during simplification we'd get: Num uf, Normed e, RealOf e ~ e, RealOf e ~ uf ==> e ~ uf, Num uf, Normed e, RealOf e ~ e ==> [Spontaneous solve] Num uf, Normed uf, RealOf uf ~ uf While looks exactly like our original constraint. If we add the superclass again we'd loop. By adding superclasses definitely only once, during canonicalisation, this situation can't happen. \begin{code}  Simon Peyton Jones committed Sep 17, 2012 337 newSCWorkFromFlavored :: CtLoc -- Depth  Simon Peyton Jones committed May 07, 2012 338  -> CtEvidence -> Class -> [Xi] -> TcS ()  simonpj@microsoft.com committed Nov 18, 2010 339 -- Returns superclasses, see Note [Adding superclasses]  dimitris committed Mar 28, 2012 340 newSCWorkFromFlavored d flavor cls xis  batterseapower committed Sep 06, 2011 341  | isDerived flavor  dimitris committed Nov 16, 2011 342 343  = return () -- Deriveds don't yield more superclasses because we will -- add them transitively in the case of wanteds.  dimitris committed Mar 28, 2012 344 345 346  | isGiven flavor = do { let sc_theta = immSuperClasses cls xis  dimitris committed Jul 18, 2012 347 348 349  xev_decomp x = zipWith (\_ i -> EvSuperClass x i) sc_theta [0..] xev = XEvTerm { ev_comp = panic "Can't compose for given!" , ev_decomp = xev_decomp }  Simon Peyton Jones committed May 07, 2012 350  ; ctevs <- xCtFlavor flavor sc_theta xev  Simon Peyton Jones committed Aug 30, 2012 351  ; emitWorkNC d ctevs }  dimitris committed May 17, 2011 352 353  | isEmptyVarSet (tyVarsOfTypes xis)  dimitris committed Jul 18, 2012 354  = return () -- Wanteds with no variables yield no deriveds.  dimitris committed Nov 16, 2011 355  -- See Note [Improvement from Ground Wanteds]  simonpj@microsoft.com committed Jan 12, 2011 356   dimitris committed Jul 18, 2012 357  | otherwise -- Wanted case, just add those SC that can lead to improvement.  simonpj@microsoft.com committed Jan 12, 2011 358  = do { let sc_rec_theta = transSuperClasses cls xis  dimitris committed Jul 18, 2012 359 360  impr_theta = filter is_improvement_pty sc_rec_theta ; traceTcS "newSCWork/Derived"$ text "impr_theta =" <+> ppr impr_theta  Simon Peyton Jones committed Sep 17, 2012 361  ; mb_der_evs <- mapM newDerived impr_theta  Simon Peyton Jones committed Aug 30, 2012 362  ; emitWorkNC d (catMaybes mb_der_evs) }  simonpj@microsoft.com committed Jan 12, 2011 363 364 365  is_improvement_pty :: PredType -> Bool -- Either it's an equality, or has some functional dependency  dimitris committed Nov 16, 2011 366 is_improvement_pty ty = go (classifyPredType ty)  batterseapower committed Sep 06, 2011 367 368  where go (EqPred {}) = True  dimitris committed Nov 16, 2011 369 370 371  go (ClassPred cls _tys) = not $null fundeps where (_,fundeps) = classTvsFds cls go (TuplePred ts) = any is_improvement_pty ts  batterseapower committed Sep 06, 2011 372  go (IrredPred {}) = True -- Might have equalities after reduction?  dimitris committed Nov 16, 2011 373 \end{code}  simonpj@microsoft.com committed Jan 12, 2011 374 375   Simon Peyton Jones committed Feb 16, 2012 376 377 378 379 380 381 %************************************************************************ %* * %* Irreducibles canonicalization %* * %************************************************************************  simonpj@microsoft.com committed Jan 12, 2011 382   dimitris committed Nov 16, 2011 383 \begin{code}  Simon Peyton Jones committed Sep 17, 2012 384 canIrred :: CtLoc -> CtEvidence -> TcS StopOrContinue  dimitris committed Nov 16, 2011 385 -- Precondition: ty not a tuple and no other evidence form  Simon Peyton Jones committed Sep 17, 2012 386 387 388 canIrred d ev = do { let ty = ctEvPred ev ; traceTcS "can_pred" (text "IrredPred = " <+> ppr ty)  Simon Peyton Jones committed Sep 18, 2012 389  ; (xi,co) <- flatten d FMFullFlatten (ctEvFlavour ev) ty -- co :: xi ~ ty  dimitris committed Nov 29, 2011 390  ; let no_flattening = xi eqType ty  Simon Peyton Jones committed Sep 17, 2012 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406  -- We can't use isTcReflCo, because even if the coercion is -- Refl, the output type might have had a substitution -- applied to it. For example 'a' might now be 'C b' ; if no_flattening then continueWith$ CIrredEvCan { cc_ev = ev, cc_loc = d } else do { mb <- rewriteCtFlavor ev xi co ; case mb of Just new_ev -> canEvNC d new_ev -- Re-classify and try again Nothing -> return Stop } } -- Found a cached copy canHole :: CtLoc -> CtEvidence -> TcS StopOrContinue canHole d ev = do { let ty = ctEvPred ev  Simon Peyton Jones committed Sep 18, 2012 407  ; (xi,co) <- flatten d FMFullFlatten (ctEvFlavour ev) ty -- co :: xi ~ ty  Simon Peyton Jones committed Sep 17, 2012 408  ; mb <- rewriteCtFlavor ev xi co  dimitris committed Mar 28, 2012 409  ; case mb of  Simon Peyton Jones committed Sep 17, 2012 410 411 412  Just new_ev -> emitInsoluble (CHoleCan { cc_ev = new_ev, cc_loc = d}) Nothing -> return () -- Found a cached copy; won't happen ; return Stop }  dimitris committed Nov 16, 2011 413 \end{code}  simonpj@microsoft.com committed Sep 13, 2010 414   dimitris committed Nov 16, 2011 415 416 417 418 419 420 421 422 423 424 %************************************************************************ %* * %* Flattening (eliminating all function symbols) * %* * %************************************************************************ Note [Flattening] ~~~~~~~~~~~~~~~~~~~~ flatten ty ==> (xi, cc) where  dimitris committed Apr 10, 2012 425 426  xi has no type functions, unless they appear under ForAlls  dimitris committed Nov 16, 2011 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  cc = Auxiliary given (equality) constraints constraining the fresh type variables in xi. Evidence for these is always the identity coercion, because internally the fresh flattening skolem variables are actually identified with the types they have been generated to stand in for. Note that it is flatten's job to flatten *every type function it sees*. flatten is only called on *arguments* to type functions, by canEqGiven. Recall that in comments we use alpha[flat = ty] to represent a flattening skolem variable alpha which has been generated to stand in for ty. ----- Example of flattening a constraint: ------ flatten (List (F (G Int))) ==> (xi, cc) where xi = List alpha cc = { G Int ~ beta[flat = G Int], F beta ~ alpha[flat = F beta] } Here * alpha and beta are 'flattening skolem variables'. * All the constraints in cc are 'given', and all their coercion terms are the identity. NB: Flattening Skolems only occur in canonical constraints, which are never zonked, so we don't need to worry about zonking doing accidental unflattening. Note that we prefer to leave type synonyms unexpanded when possible, so when the flattener encounters one, it first asks whether its transitive expansion contains any type function applications. If so, it expands the synonym and proceeds; if not, it simply returns the unexpanded synonym. \begin{code}  Simon Peyton Jones committed Sep 18, 2012 463 data FlattenMode = FMSubstOnly | FMFullFlatten  dimitris committed Apr 10, 2012 464   dimitris committed Nov 16, 2011 465 -- Flatten a bunch of types all at once.  Simon Peyton Jones committed Sep 17, 2012 466 flattenMany :: CtLoc -> FlattenMode  Simon Peyton Jones committed Sep 18, 2012 467  -> CtFlavour -> [Type] -> TcS ([Xi], [TcCoercion])  dimitris committed Nov 16, 2011 468 -- Coercions :: Xi ~ Type  dimitris committed Nov 28, 2011 469 -- Returns True iff (no flattening happened)  Simon Peyton Jones committed Aug 30, 2012 470 471 472 -- NB: The EvVar inside the 'ctxt :: CtEvidence' is unused, -- we merely want (a) Given/Solved/Derived/Wanted info -- (b) the GivenLoc/WantedLoc for when we create new evidence  dimitris committed Apr 10, 2012 473 flattenMany d f ctxt tys  dimitris committed Nov 28, 2011 474 475  = -- pprTrace "flattenMany" empty $go tys  dimitris committed Nov 29, 2011 476  where go [] = return ([],[])  dimitris committed Apr 10, 2012 477  go (ty:tys) = do { (xi,co) <- flatten d f ctxt ty  dimitris committed Nov 29, 2011 478 479  ; (xis,cos) <- go tys ; return (xi:xis,co:cos) }  dimitris committed Nov 16, 2011 480 481 482 483  -- Flatten a type to get rid of type function applications, returning -- the new type-function-free type, and a collection of new equality -- constraints. See Note [Flattening] for more detail.  Simon Peyton Jones committed Sep 17, 2012 484 flatten :: CtLoc -> FlattenMode  Simon Peyton Jones committed Sep 18, 2012 485  -> CtFlavour -> TcType -> TcS (Xi, TcCoercion)  dimitris committed Nov 16, 2011 486 -- Postcondition: Coercion :: Xi ~ TcType  Simon Peyton Jones committed Sep 17, 2012 487 flatten loc f ctxt ty  dimitris committed Nov 16, 2011 488  | Just ty' <- tcView ty  Simon Peyton Jones committed Sep 17, 2012 489  = do { (xi, co) <- flatten loc f ctxt ty'  dimitris committed Jul 19, 2012 490 491  ; if eqType xi ty then return (ty,co) else return (xi,co) } -- Small tweak for better error messages  dimitris committed Dec 22, 2011 492   dimitris committed Apr 10, 2012 493 flatten _ _ _ xi@(LitTy {}) = return (xi, mkTcReflCo xi)  Iavor S. Diatchki committed Dec 18, 2011 494   Simon Peyton Jones committed Sep 17, 2012 495 496 flatten loc f ctxt (TyVarTy tv) = flattenTyVar loc f ctxt tv  dimitris committed Nov 16, 2011 497   Simon Peyton Jones committed Sep 17, 2012 498 499 500 flatten loc f ctxt (AppTy ty1 ty2) = do { (xi1,co1) <- flatten loc f ctxt ty1 ; (xi2,co2) <- flatten loc f ctxt ty2  Simon Peyton Jones committed Dec 05, 2011 501  ; return (mkAppTy xi1 xi2, mkTcAppCo co1 co2) }  dimitris committed Nov 16, 2011 502   Simon Peyton Jones committed Sep 17, 2012 503 504 505 flatten loc f ctxt (FunTy ty1 ty2) = do { (xi1,co1) <- flatten loc f ctxt ty1 ; (xi2,co2) <- flatten loc f ctxt ty2  Simon Peyton Jones committed Dec 05, 2011 506  ; return (mkFunTy xi1 xi2, mkTcFunCo co1 co2) }  dimitris committed Nov 16, 2011 507   Simon Peyton Jones committed Sep 17, 2012 508 flatten loc f ctxt (TyConApp tc tys)  dimitris committed Nov 16, 2011 509 510 511  -- For a normal type constructor or data family application, we just -- recursively flatten the arguments. | not (isSynFamilyTyCon tc)  Simon Peyton Jones committed Sep 17, 2012 512  = do { (xis,cos) <- flattenMany loc f ctxt tys  Simon Peyton Jones committed Dec 05, 2011 513  ; return (mkTyConApp tc xis, mkTcTyConAppCo tc cos) }  dimitris committed Nov 16, 2011 514 515 516 517 518 519  -- Otherwise, it's a type function application, and we have to -- flatten it away as well, and generate a new given equality constraint -- between the application and a newly generated flattening skolem variable. | otherwise = ASSERT( tyConArity tc <= length tys ) -- Type functions are saturated  Simon Peyton Jones committed Sep 17, 2012 520  do { (xis, cos) <- flattenMany loc f ctxt tys  Simon Peyton Jones committed Aug 28, 2012 521 522  ; let (xi_args, xi_rest) = splitAt (tyConArity tc) xis (cos_args, cos_rest) = splitAt (tyConArity tc) cos  dimitris committed Nov 16, 2011 523 524 525 526  -- The type function might be *over* saturated -- in which case the remaining arguments should -- be dealt with by AppTys fam_ty = mkTyConApp tc xi_args  dimitris committed Mar 28, 2012 527   Simon Peyton Jones committed Aug 28, 2012 528  ; (ret_co, rhs_xi) <-  dimitris committed Apr 10, 2012 529 530  case f of FMSubstOnly ->  Simon Peyton Jones committed Aug 28, 2012 531  return (mkTcReflCo fam_ty, fam_ty)  dimitris committed Apr 10, 2012 532  FMFullFlatten ->  Simon Peyton Jones committed Aug 28, 2012 533 534  do { mb_ct <- lookupFlatEqn fam_ty ; case mb_ct of  dimitris committed Apr 10, 2012 535  Just ct  Simon Peyton Jones committed May 07, 2012 536  | let ctev = cc_ev ct  Simon Peyton Jones committed Sep 18, 2012 537 538  flav = ctEvFlavour ctev , flav canRewrite ctxt  dimitris committed Apr 10, 2012 539 540 541 542 543 544 545 546 547 548  -> -- You may think that we can just return (cc_rhs ct) but not so. -- return (mkTcCoVarCo (ctId ct), cc_rhs ct, []) -- The cached constraint resides in the cache so we have to flatten -- the rhs to make sure we have applied any inert substitution to it. -- Alternatively we could be applying the inert substitution to the -- cache as well when we interact an equality with the inert. -- The design choice is: do we keep the flat cache rewritten or not? -- For now I say we don't keep it fully rewritten. do { traceTcS "flatten/flat-cache hit"$ ppr ct ; let rhs_xi = cc_rhs ct  Simon Peyton Jones committed Sep 18, 2012 549  ; (flat_rhs_xi,co) <- flatten (cc_loc ct) f flav rhs_xi  Simon Peyton Jones committed May 07, 2012 550 551  ; let final_co = evTermCoercion (ctEvTerm ctev) mkTcTransCo mkTcSymCo co  Simon Peyton Jones committed Aug 28, 2012 552  ; return (final_co, flat_rhs_xi) }  dimitris committed Mar 28, 2012 553   Simon Peyton Jones committed Sep 18, 2012 554  _ | Given <- ctxt -- Given: make new flatten skolem  dimitris committed Apr 10, 2012 555  -> do { traceTcS "flatten/flat-cache miss" $empty  Simon Peyton Jones committed Aug 28, 2012 556 557  ; rhs_ty <- newFlattenSkolemTy fam_ty ; let co = mkTcReflCo fam_ty  Simon Peyton Jones committed Sep 17, 2012 558  new_ev = CtGiven { ctev_pred = mkTcEqPred fam_ty rhs_ty  Simon Peyton Jones committed Aug 30, 2012 559  , ctev_evtm = EvCoercion co }  Simon Peyton Jones committed Sep 17, 2012 560  ct = CFunEqCan { cc_ev = new_ev  Simon Peyton Jones committed May 07, 2012 561  , cc_fun = tc  Simon Peyton Jones committed Aug 28, 2012 562 563  , cc_tyargs = xi_args , cc_rhs = rhs_ty  Simon Peyton Jones committed Sep 17, 2012 564  , cc_loc = loc }  Simon Peyton Jones committed Oct 01, 2012 565  ; updWorkListTcS$ extendWorkListFunEq ct  Simon Peyton Jones committed Aug 28, 2012 566 567  ; return (co, rhs_ty) }  dimitris committed Apr 10, 2012 568 569 570  | otherwise -- Wanted or Derived: make new unification variable -> do { traceTcS "flatten/flat-cache miss" $empty ; rhs_xi_var <- newFlexiTcSTy (typeKind fam_ty)  Simon Peyton Jones committed Oct 01, 2012 571 572 573 574 575 576 577 578 579 580  ; ctev <- newWantedEvVarNC (mkTcEqPred fam_ty rhs_xi_var) -- NC (no-cache) version because we've already -- looked in the solved goals an inerts (lookupFlatEqn) ; let ct = CFunEqCan { cc_ev = ctev , cc_fun = tc , cc_tyargs = xi_args , cc_rhs = rhs_xi_var , cc_loc = loc } ; updWorkListTcS$ extendWorkListFunEq ct ; return (evTermCoercion (ctEvTerm ctev), rhs_xi_var) }  dimitris committed Apr 10, 2012 581  }  dimitris committed Mar 28, 2012 582 583 584 585 586 587 588  -- Emit the flat constraints ; return ( mkAppTys rhs_xi xi_rest -- NB mkAppTys: rhs_xi might not be a type variable -- cf Trac #5655 , mkTcAppCos (mkTcSymCo ret_co mkTcTransCo mkTcTyConAppCo tc cos_args) $cos_rest ) }  dimitris committed Nov 16, 2011 589   Simon Peyton Jones committed Sep 17, 2012 590 flatten loc _f ctxt ty@(ForAllTy {})  dimitris committed Nov 16, 2011 591 592 593 -- We allow for-alls when, but only when, no type function -- applications inside the forall involve the bound type variables. = do { let (tvs, rho) = splitForAllTys ty  Simon Peyton Jones committed Sep 17, 2012 594  ; (rho', co) <- flatten loc FMSubstOnly ctxt rho  Simon Peyton Jones committed Aug 28, 2012 595 596  -- Substitute only under a forall -- See Note [Flattening under a forall]  dimitris committed Apr 10, 2012 597  ; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) }  Simon Peyton Jones committed Feb 16, 2012 598 599 \end{code}  Simon Peyton Jones committed Aug 28, 2012 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 Note [Flattening under a forall] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Under a forall, we (a) MUST apply the inert subsitution (b) MUST NOT flatten type family applications Hence FMSubstOnly. For (a) consider c ~ a, a ~ T (forall b. (b, [c]) If we don't apply the c~a substitution to the second constraint we won't see the occurs-check error. For (b) consider (a ~ forall b. F a b), we don't want to flatten to (a ~ forall b.fsk, F a b ~ fsk) because now the 'b' has escaped its scope. We'd have to flatten to (a ~ forall b. fsk b, forall b. F a b ~ fsk b) and we have not begun to think about how to make that work!  Simon Peyton Jones committed Feb 16, 2012 617 \begin{code}  Simon Peyton Jones committed Sep 28, 2012 618 619 620 flattenTyVar, flattenFinalTyVar :: CtLoc -> FlattenMode -> CtFlavour -> TcTyVar -> TcS (Xi, TcCoercion)  Simon Peyton Jones committed Feb 16, 2012 621 -- "Flattening" a type variable means to apply the substitution to it  dimitris committed Aug 29, 2012 622 623 624 -- The substitution is actually the union of the substitution in the TyBinds -- for the unification variables that have been unified already with the inert -- equalities, see Note [Spontaneously solved in TyBinds] in TcInteract.  Simon Peyton Jones committed Sep 17, 2012 625 flattenTyVar loc f ctxt tv  Simon Peyton Jones committed Sep 28, 2012 626 627 628  | not (isTcTyVar tv) -- Happens when flatten under a (forall a. ty) = flattenFinalTyVar loc f ctxt tv -- So ty contains referneces to the non-TcTyVar a | otherwise  Simon Peyton Jones committed Sep 17, 2012 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654  = do { mb_ty <- isFilledMetaTyVar_maybe tv ; case mb_ty of { Just ty -> flatten loc f ctxt ty ; Nothing -> -- Try in ty_binds do { ty_binds <- getTcSTyBindsMap ; case lookupVarEnv ty_binds tv of { Just (_tv,ty) -> flatten loc f ctxt ty ; -- NB: ty_binds coercions are all ReflCo, -- so no need to transitively compose co' with another coercion, -- unlike in 'flatten_from_inerts' Nothing -> -- Try in the inert equalities do { ieqs <- getInertEqs ; let mco = tv_eq_subst ieqs tv -- co : v ~ ty ; case mco of { Just (co,ty) -> do { (ty_final,co') <- flatten loc f ctxt ty ; return (ty_final, co' mkTcTransCo mkTcSymCo co) } ; -- NB recursive call. -- Why? Because inert subst. non-idempotent, Note [Detailed InertCans Invariants] -- In fact, because of flavors, it couldn't possibly be idempotent, -- this is explained in Note [Non-idempotent inert substitution]  Simon Peyton Jones committed Sep 28, 2012 655  Nothing -> flattenFinalTyVar loc f ctxt tv  Simon Peyton Jones committed Sep 17, 2012 656  } } } } } }  dimitris committed Aug 29, 2012 657  where  Simon Peyton Jones committed May 07, 2012 658 659 660  tv_eq_subst subst tv | Just ct <- lookupVarEnv subst tv , let ctev = cc_ev ct  Simon Peyton Jones committed Sep 18, 2012 661  , ctEvFlavour ctev canRewrite ctxt  Simon Peyton Jones committed May 07, 2012 662 663 664 665  = Just (evTermCoercion (ctEvTerm ctev), cc_rhs ct) -- NB: even if ct is Derived we are not going to -- touch the actual coercion so we are fine. | otherwise = Nothing  Simon Peyton Jones committed Sep 28, 2012 666 667 668 669 670 671 672  flattenFinalTyVar loc f ctxt tv = -- Done, but make sure the kind is zonked do { let knd = tyVarKind tv ; (new_knd,_kind_co) <- flatten loc f ctxt knd ; let ty = mkTyVarTy (setVarType tv new_knd) ; return (ty, mkTcReflCo ty) }  Simon Peyton Jones committed Feb 16, 2012 673 674 675 676 677 678 679 680 681 \end{code} Note [Non-idempotent inert substitution] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The inert substitution is not idempotent in the broad sense. It is only idempotent in that it cannot rewrite the RHS of other inert equalities any further. An example of such an inert substitution is:  dimitris committed Mar 28, 2012 682  [G] g1 : ta8 ~ ta4  Simon Peyton Jones committed Feb 16, 2012 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699  [W] g2 : ta4 ~ a5Fj Observe that the wanted cannot rewrite the solved goal, despite the fact that ta4 appears on an RHS of an equality. Now, imagine a constraint: [W] g3: ta8 ~ Int coming in. If we simply apply once the inert substitution we will get: [W] g3_1: ta4 ~ Int and because potentially ta4 is untouchable we will try to insert g3_1 in the inert set, getting a panic since the inert only allows ONE equation per LHS type variable (as it should). For this reason, when we reach to flatten a type variable, we flatten it recursively, so that we can make sure that the inert substitution /is/ fully applied.  dimitris committed Nov 16, 2011 700   dimitris committed Apr 02, 2012 701 Insufficient (non-recursive) rewriting was the reason for #5668.  dimitris committed Nov 16, 2011 702   Simon Peyton Jones committed Feb 16, 2012 703 704 705 706 707 708 709 710  %************************************************************************ %* * %* Equalities %* * %************************************************************************ \begin{code}  Simon Peyton Jones committed Sep 17, 2012 711 712 canEvVarsCreated :: CtLoc -> [CtEvidence] -> TcS StopOrContinue canEvVarsCreated _loc [] = return Stop  Simon Peyton Jones committed Aug 30, 2012 713 714  -- Add all but one to the work list -- and return the first (if any) for futher processing  Simon Peyton Jones committed Sep 17, 2012 715 716 canEvVarsCreated loc (ev : evs) = do { emitWorkNC loc evs; canEvNC loc ev }  Simon Peyton Jones committed Aug 30, 2012 717 718  -- Note the "NC": these are fresh goals, not necessarily canonical  Simon Peyton Jones committed Sep 17, 2012 719 720 emitWorkNC :: CtLoc -> [CtEvidence] -> TcS () emitWorkNC loc evs  Simon Peyton Jones committed Aug 30, 2012 721 722 723  | null evs = return () | otherwise = updWorkListTcS (extendWorkListCts (map mk_nc evs)) where  Simon Peyton Jones committed Sep 17, 2012 724  mk_nc ev = CNonCanonical { cc_ev = ev, cc_loc = loc }  dimitris committed Mar 28, 2012 725   Simon Peyton Jones committed Feb 16, 2012 726 -------------------------  Simon Peyton Jones committed Sep 18, 2012 727 canEqNC, canEq :: CtLoc -> CtEvidence -> Type -> Type -> TcS StopOrContinue  Simon Peyton Jones committed Feb 16, 2012 728   Simon Peyton Jones committed Sep 17, 2012 729 730 canEqNC loc ev ty1 ty2 = canEq loc ev ty1 ty2  Simon Peyton Jones committed Feb 16, 2012 731 732  andWhenContinue emitKindConstraint  Simon Peyton Jones committed Sep 17, 2012 733 canEq _loc ev ty1 ty2  734  | eqType ty1 ty2 -- Dealing with equality here avoids  simonpj@microsoft.com committed Sep 13, 2010 735  -- later spurious occurs checks for a~a  Simon Peyton Jones committed Sep 17, 2012 736 737  = if isWanted ev then setEvBind (ctev_evar ev) (EvCoercion (mkTcReflCo ty1)) >> return Stop  dimitris committed Mar 28, 2012 738 739  else return Stop  simonpj@microsoft.com committed Sep 13, 2010 740   dimitris committed Nov 16, 2011 741 -- If one side is a variable, orient and flatten,  simonpj@microsoft.com committed Sep 13, 2010 742 -- WITHOUT expanding type synonyms, so that we tend to  743 -- substitute a ~ Age rather than a ~ Int when @type Age = Int@  Simon Peyton Jones committed Sep 17, 2012 744 745 746 747 canEq loc ev ty1@(TyVarTy {}) ty2 = canEqLeaf loc ev ty1 ty2 canEq loc ev ty1 ty2@(TyVarTy {}) = canEqLeaf loc ev ty1 ty2  simonpj@microsoft.com committed Sep 13, 2010 748   Simon Peyton Jones committed Jan 12, 2012 749 -- See Note [Naked given applications]  Simon Peyton Jones committed Sep 17, 2012 750 751 752 canEq loc ev ty1 ty2 | Just ty1' <- tcView ty1 = canEq loc ev ty1' ty2 | Just ty2' <- tcView ty2 = canEq loc ev ty1 ty2'  Simon Peyton Jones committed Jan 12, 2012 753   Simon Peyton Jones committed Sep 17, 2012 754 canEq loc ev ty1@(TyConApp fn tys) ty2  755  | isSynFamilyTyCon fn, length tys == tyConArity fn  Simon Peyton Jones committed Sep 17, 2012 756 757  = canEqLeaf loc ev ty1 ty2 canEq loc ev ty1 ty2@(TyConApp fn tys)  758  | isSynFamilyTyCon fn, length tys == tyConArity fn  Simon Peyton Jones committed Sep 17, 2012 759  = canEqLeaf loc ev ty1 ty2  simonpj@microsoft.com committed Nov 12, 2010 760   Simon Peyton Jones committed Sep 17, 2012 761 canEq loc ev ty1 ty2  Simon Peyton Jones committed Jan 12, 2012 762 763 764  | Just (tc1,tys1) <- tcSplitTyConApp_maybe ty1 , Just (tc2,tys2) <- tcSplitTyConApp_maybe ty2 , isDecomposableTyCon tc1 && isDecomposableTyCon tc2  Simon Peyton Jones committed Sep 21, 2012 765  = canDecomposableTyConApp loc ev tc1 tys1 tc2 tys2  Simon Peyton Jones committed Jan 12, 2012 766   Simon Peyton Jones committed Sep 17, 2012 767 canEq loc ev s1@(ForAllTy {}) s2@(ForAllTy {})  dimitris committed Apr 10, 2012 768  | tcIsForAllTy s1, tcIsForAllTy s2  Simon Peyton Jones committed Sep 17, 2012 769  , CtWanted { ctev_evar = orig_ev } <- ev  dimitris committed Apr 10, 2012 770 771 772  = do { let (tvs1,body1) = tcSplitForAllTys s1 (tvs2,body2) = tcSplitForAllTys s2 ; if not (equalLength tvs1 tvs2) then  Simon Peyton Jones committed Sep 18, 2012 773  canEqFailure loc ev s1 s2  dimitris committed Apr 10, 2012 774  else  Simon Peyton Jones committed Sep 17, 2012 775  do { traceTcS "Creating implication for polytype equality"$ ppr ev  dimitris committed Apr 10, 2012 776 777  ; deferTcSForAllEq (loc,orig_ev) (tvs1,body1) (tvs2,body2) ; return Stop } }  Simon Peyton Jones committed Jan 12, 2012 778  | otherwise  dimitris committed Apr 10, 2012 779  = do { traceTcS "Ommitting decomposition of given polytype equality" $ Simon Peyton Jones committed Aug 28, 2012 780  pprEq s1 s2 -- See Note [Do not decompose given polytype equalities]  Simon Peyton Jones committed Jan 12, 2012 781  ; return Stop }  Simon Peyton Jones committed Sep 21, 2012 782 783 784 785 786 787 788 789 790 791 792 793 794 795  -- The last remaining source of success is an application -- e.g. F a b ~ Maybe c where F has arity 1 -- See Note [Equality between type applications] -- Note [Care with type applications] in TcUnify canEq loc ev ty1 ty2 = do { let flav = ctEvFlavour ev ; (s1, co1) <- flatten loc FMSubstOnly flav ty1 ; (s2, co2) <- flatten loc FMSubstOnly flav ty2 ; mb_ct <- rewriteCtFlavor ev (mkTcEqPred s1 s2) (mkHdEqPred s2 co1 co2) ; case mb_ct of Nothing -> return Stop Just new_ev -> last_chance new_ev s1 s2 } where  Simon Peyton Jones committed Sep 28, 2012 796  last_chance ev ty1 ty2  Simon Peyton Jones committed Sep 21, 2012 797 798 799  | Just (tc1,tys1) <- tcSplitTyConApp_maybe ty1 , Just (tc2,tys2) <- tcSplitTyConApp_maybe ty2 , isDecomposableTyCon tc1 && isDecomposableTyCon tc2  Simon Peyton Jones committed Sep 28, 2012 800  = canDecomposableTyConApp loc ev tc1 tys1 tc2 tys2  Simon Peyton Jones committed Sep 21, 2012 801 802 803 804 805 806 807 808 809 810 811  | Just (s1,t1) <- tcSplitAppTy_maybe ty1 , Just (s2,t2) <- tcSplitAppTy_maybe ty2 = do { let xevcomp [x,y] = EvCoercion (mkTcAppCo (evTermCoercion x) (evTermCoercion y)) xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen xevdecomp x = let xco = evTermCoercion x in [EvCoercion (mkTcLRCo CLeft xco), EvCoercion (mkTcLRCo CRight xco)] ; ctevs <- xCtFlavor ev [mkTcEqPred s1 s2, mkTcEqPred t1 t2] (XEvTerm xevcomp xevdecomp) ; canEvVarsCreated loc ctevs } | otherwise  Simon Peyton Jones committed Sep 28, 2012 812  = do { emitInsoluble (CNonCanonical { cc_ev = ev, cc_loc = loc })  Simon Peyton Jones committed Sep 21, 2012 813  ; return Stop }  Simon Peyton Jones committed Jan 12, 2012 814   Simon Peyton Jones committed Feb 16, 2012 815 ------------------------  Simon Peyton Jones committed Sep 21, 2012 816 817 818 819 820 821 822 823 824 825 826 827 828 canDecomposableTyConApp :: CtLoc -> CtEvidence -> TyCon -> [TcType] -> TyCon -> [TcType] -> TcS StopOrContinue canDecomposableTyConApp loc ev tc1 tys1 tc2 tys2 | tc1 /= tc2 || length tys1 /= length tys2 -- Fail straight away for better error messages = canEqFailure loc ev (mkTyConApp tc1 tys1) (mkTyConApp tc2 tys2) | otherwise = do { let xcomp xs = EvCoercion (mkTcTyConAppCo tc1 (map evTermCoercion xs)) xdecomp x = zipWith (\_ i -> EvCoercion$ mkTcNthCo i (evTermCoercion x)) tys1 [0..] xev = XEvTerm xcomp xdecomp ; ctevs <- xCtFlavor ev (zipWith mkTcEqPred tys1 tys2) xev  Simon Peyton Jones committed Sep 17, 2012 829  ; canEvVarsCreated loc ctevs }  Simon Peyton Jones committed May 07, 2012 830   Simon Peyton Jones committed Sep 18, 2012 831 832 833 834 835 836 837 838 839 840 841 canEqFailure :: CtLoc -> CtEvidence -> TcType -> TcType -> TcS StopOrContinue -- See Note [Make sure that insolubles are fully rewritten] canEqFailure loc ev ty1 ty2 = do { let flav = ctEvFlavour ev ; (s1, co1) <- flatten loc FMSubstOnly flav ty1 ; (s2, co2) <- flatten loc FMSubstOnly flav ty2 ; mb_ct <- rewriteCtFlavor ev (mkTcEqPred s1 s2) (mkHdEqPred s2 co1 co2) ; case mb_ct of Just new_ev -> emitInsoluble (CNonCanonical { cc_ev = new_ev, cc_loc = loc }) Nothing -> pprPanic "canEqFailure" (ppr ev $$ppr ty1$$ ppr ty2)  Simon Peyton Jones committed Sep 17, 2012 842  ; return Stop }  dimitris committed Mar 28, 2012 843   Simon Peyton Jones committed Feb 16, 2012 844 845 ------------------------ emitKindConstraint :: Ct -> TcS StopOrContinue  Simon Peyton Jones committed Aug 30, 2012 846 emitKindConstraint ct -- By now ct is canonical  Simon Peyton Jones committed Feb 16, 2012 847  = case ct of  Simon Peyton Jones committed Sep 17, 2012 848 849  CTyEqCan { cc_loc = loc , cc_ev = ev, cc_tyvar = tv  Simon Peyton Jones committed Feb 16, 2012 850  , cc_rhs = ty }  Simon Peyton Jones committed Sep 17, 2012 851  -> emit_kind_constraint loc ev (mkTyVarTy tv) ty  Simon Peyton Jones committed Feb 16, 2012 852   Simon Peyton Jones committed Sep 17, 2012 853 854  CFunEqCan { cc_loc = loc , cc_ev = ev  Simon Peyton Jones committed Feb 16, 2012 855 856  , cc_fun = fn, cc_tyargs = xis1 , cc_rhs = xi2 }  Simon Peyton Jones committed Sep 17, 2012 857  -> emit_kind_constraint loc ev (mkTyConApp fn xis1) xi2  Simon Peyton Jones committed Mar 02, 2012 858   dimitris committed Mar 28, 2012 859  _ -> continueWith ct  Simon Peyton Jones committed Feb 16, 2012 860  where  Simon Peyton Jones committed Sep 28, 2012 861  emit_kind_constraint loc _ev ty1 ty2  Simon Peyton Jones committed Mar 02, 2012 862 863 864  | compatKind k1 k2 -- True when ty1,ty2 are themselves kinds, = continueWith ct -- because then k1, k2 are BOX  Simon Peyton Jones committed Feb 16, 2012 865  | otherwise  Simon Peyton Jones committed Mar 02, 2012 866  = ASSERT( isKind k1 && isKind k2 )  Simon Peyton Jones committed Sep 28, 2012 867 868 869 870 871  do { mw <- newDerived (mkEqPred k1 k2) ; case mw of Nothing -> return () Just kev -> emitWorkNC kind_co_loc [kev] ; continueWith ct }  Simon Peyton Jones committed May 07, 2012 872  where  Simon Peyton Jones committed Feb 16, 2012 873 874  k1 = typeKind ty1 k2 = typeKind ty2  Simon Peyton Jones committed May 07, 2012 875   Simon Peyton Jones committed Feb 16, 2012 876 877  -- Always create a Wanted kind equality even if -- you are decomposing a given constraint.  dimitris committed Mar 28, 2012 878  -- NB: DV finds this reasonable for now. Maybe we have to revisit.  Simon Peyton Jones committed Sep 28, 2012 879  kind_co_loc = setCtLocOrigin loc (KindEqOrigin ty1 ty2 (ctLocOrigin loc))  simonpj@microsoft.com committed Sep 13, 2010 880 881 \end{code}  Simon Peyton Jones committed Sep 18, 2012 882 883 884 885 886 887 888 889 890 891 892 Note [Make sure that insolubles are fully rewritten] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When an equality fails, we still want to rewrite the equality all the way down, so that it accurately reflects (a) the mutable reference substitution in force at start of solving (b) any ty-binds in force at this point in solving See Note [Kick out insolubles] in TcInteract. And if we don't do this there is a bad danger that TcSimplify.applyTyVarDefaulting will find a variable that has in fact been substituted.  Simon Peyton Jones committed Aug 28, 2012 893 894 895 896 897 898 899 Note [Do not decompose given polytype equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider [G] (forall a. t1 ~ forall a. t2). Can we decompose this? No -- what would the evidence look like. So instead we simply discard this given evidence.  Simon Peyton Jones committed Jan 12, 2012 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 Note [Combining insoluble constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ As this point we have an insoluble constraint, like Int~Bool. * If it is Wanted, delete it from the cache, so that subsequent Int~Bool constraints give rise to separate error messages * But if it is Derived, DO NOT delete from cache. A class constraint may get kicked out of the inert set, and then have its functional dependency Derived constraints generated a second time. In that case we don't want to get two (or more) error messages by generating two (or more) insoluble fundep constraints from the same class constraint.  dimitris committed Jun 15, 2011 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 Note [Naked given applications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider: data A a type T a = A a and the given equality: [G] A a ~ T Int We will reach the case canEq where we do a tcSplitAppTy_maybe, but if we dont have the guards (Nothing <- tcView ty1) (Nothing <- tcView ty2) then the given equation is going to fall through and get completely forgotten! What we want instead is this clause to apply only when there is no immediate top-level synonym; if there is one it will be later on unfolded by the later stages of canEq. Test-case is in typecheck/should_compile/GivenTypeSynonym.hs  simonpj@microsoft.com committed Sep 13, 2010 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 Note [Equality between type applications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ If we see an equality of the form s1 t1 ~ s2 t2 we can always split it up into s1 ~ s2 /\ t1 ~ t2, since s1 and s2 can't be type functions (type functions use the TyConApp constructor, which never shows up as the LHS of an AppTy). Other than type functions, types in Haskell are always (1) generative: a b ~ c d implies a ~ c, since different type constructors always generate distinct types (2) injective: a b ~ a d implies b ~ d; we never generate the same type from different type arguments. Note [Canonical ordering for equality constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Implemented as (<+=) below: - Type function applications always come before anything else. - Variables always come before non-variables (other than type function applications). Note that we don't need to unfold type synonyms on the RHS to check the ordering; that is, in the rules above it's OK to consider only whether something is *syntactically* a type function application or not. To illustrate why this is OK, suppose we have an equality of the form 'tv ~ S a b c', where S is a type synonym which expands to a top-level application of the type function F, something like type S a b c = F d e Then to canonicalize 'tv ~ S a b c' we flatten the RHS, and since S's expansion contains type function applications the flattener will do the expansion and then generate a skolem variable for the type function application, so we end up with something like this: tv ~ x F d e ~ x where x is the skolem variable. This is one extra equation than absolutely necessary (we could have gotten away with just 'F d e ~ tv' if we had noticed that S expanded to a top-level type function application and flipped it around in the first place) but this way keeps the code simpler. Unlike the OutsideIn(X) draft of May 7, 2010, we do not care about the ordering of tv ~ tv constraints. There are several reasons why we might: (1) In order to be able to extract a substitution that doesn't mention untouchable variables after we are done solving, we might prefer to put touchable variables on the left. However, in and of itself this isn't necessary; we can always re-orient equality constraints at the end if necessary when extracting a substitution. (2) To ensure termination we might think it necessary to put variables in lexicographic order. However, this isn't actually necessary as outlined below. While building up an inert set of canonical constraints, we maintain the invariant that the equality constraints in the inert set form an acyclic rewrite system when viewed as L-R rewrite rules. Moreover, the given constraints form an idempotent substitution (i.e. none of the variables on the LHS occur in any of the RHS's, and type functions never show up in the RHS at all), the wanted constraints also form an idempotent substitution, and finally the LHS of a given constraint never shows up on the RHS of a wanted constraint. There may, however, be a wanted LHS that shows up in a given RHS, since we do not rewrite given constraints with wanted constraints. Suppose we have an inert constraint set tg_1 ~ xig_1 -- givens tg_2 ~ xig_2 ... tw_1 ~ xiw_1 -- wanteds tw_2 ~ xiw_2 ... where each t_i can be either a type variable or a type function application. Now suppose we take a new canonical equality constraint, t' ~ xi' (note among other things this means t' does not occur in xi') and try to react it with the existing inert set. We show by induction on the number of t_i which occur in t' ~ xi' that this process will terminate. There are several ways t' ~ xi' could react with an existing constraint: TODO: finish this proof. The below was for the case where the entire inert set is an idempotent subustitution... (b) We could have t' = t_j for some j. Then we obtain the new equality xi_j ~ xi'; note that neither xi_j or xi' contain t_j. We now canonicalize the new equality, which may involve decomposing it into several canonical equalities, and recurse on these. However, none of the new equalities will contain t_j, so they have fewer occurrences of the t_i than the original equation. (a) We could have t_j occurring in xi' for some j, with t' /= t_j. Then we substitute xi_j for t_j in xi' and continue. However, since none of the t_i occur in xi_j, we have decreased the number of t_i that occur in xi', since we eliminated t_j and did not introduce any new ones. \begin{code} data TypeClassifier  Simon Peyton Jones committed Aug 28, 2012 1042  = VarCls TcTyVar -- ^ Type variable  Ian Lynagh committed Oct 20, 2010 1043 1044  | FunCls TyCon [Type] -- ^ Type function, exactly saturated | OtherCls TcType -- ^ Neither of the above  simonpj@microsoft.com committed Sep 13, 2010 1045 1046 1047  classify :: TcType -> TypeClassifier  1048   Simon Peyton Jones committed Aug 28, 2012 1049 classify (TyVarTy tv) = ASSERT2( isTcTyVar tv, ppr tv ) VarCls tv  simonpj@microsoft.com committed Sep 13, 2010 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 classify (TyConApp tc tys) | isSynFamilyTyCon tc , tyConArity tc == length tys = FunCls tc tys classify ty | Just ty' <- tcView ty = case classify ty' of OtherCls {} -> OtherCls ty var_or_fn -> var_or_fn | otherwise = OtherCls ty -- See note [Canonical ordering for equality constraints].  Simon Peyton Jones committed May 07, 2012 1061 reOrient :: CtEvidence -> TypeClassifier -> TypeClassifier -> Bool  simonpj@microsoft.com committed Sep 13, 2010 1062 1063 1064 1065 1066 -- (t1 reOrient t2) responds True -- iff we should flip to (t2~t1) -- We try to say False if possible, to minimise evidence generation -- -- Postcondition: After re-orienting, first arg is not OTherCls  Simon Peyton Jones committed Oct 01, 2012 1067 1068 reOrient _ev (OtherCls {}) cls2 = ASSERT( case cls2 of { OtherCls {} -> False; _ -> True } ) True -- One must be Var/Fun  simonpj@microsoft.com committed Feb 11, 2011 1069   Simon Peyton Jones committed Oct 01, 2012 1070 reOrient _ev (FunCls {}) _ = False -- Fun/Other on rhs  Simon Peyton Jones committed Sep 17, 2012 1071  -- But consider the following variation: isGiven ev && isMetaTyVar tv  simonpj@microsoft.com committed Sep 13, 2010 1072  -- See Note [No touchables as FunEq RHS] in TcSMonad  Simon Peyton Jones committed Aug 28, 2012 1073   Simon Peyton Jones committed Oct 01, 2012 1074 1075 reOrient _ev (VarCls {}) (FunCls {}) = True reOrient _ev (VarCls {}) (OtherCls {}) = False  Simon Peyton Jones committed Sep 17, 2012 1076 reOrient _ev (VarCls tv1) (VarCls tv2)  simonpj@microsoft.com committed Nov 12, 2010 1077 1078 1079  | isMetaTyVar tv2 && not (isMetaTyVar tv1) = True | otherwise = False -- Just for efficiency, see CTyEqCan invariants  simonpj@microsoft.com committed Sep 13, 2010 1080 1081  ------------------  dimitris committed Nov 16, 2011 1082   Simon Peyton Jones committed Sep 17, 2012 1083 canEqLeaf :: CtLoc -> CtEvidence  dimitris committed Nov 16, 2011 1084 1085  -> Type -> Type -> TcS StopOrContinue  simonpj@microsoft.com committed Sep 13, 2010 1086 1087 1088 1089 -- Canonicalizing "leaf" equality constraints which cannot be -- decomposed further (ie one of the types is a variable or -- saturated type function application).  dimitris committed Nov 16, 2011