861b262cf011f45481d7bb37f715443f20aa0628
[ghc.git] / compiler / typecheck / TcCanonical.lhs
1 \begin{code}
2 module TcCanonical(
3     mkCanonical, mkCanonicals, mkCanonicalFEV, canWanteds, canGivens,
4     canOccursCheck, canEq
5  ) where
6
7 #include "HsVersions.h"
8
9 import BasicTypes
10 import Type
11 import TcRnTypes
12
13 import TcType
14 import TcErrors
15 import Coercion
16 import Class
17 import TyCon
18 import TypeRep
19 import Name
20 import Var
21 import Outputable
22 import Control.Monad    ( unless, when, zipWithM, zipWithM_ )
23 import MonadUtils
24 import Control.Applicative ( (<|>) )
25
26 import VarSet
27 import Bag
28
29 import HsBinds
30 import TcSMonad
31 \end{code}
32
33 Note [Canonicalisation]
34 ~~~~~~~~~~~~~~~~~~~~~~~
35 * Converts (Constraint f) _which_does_not_contain_proper_implications_ to CanonicalCts
36 * Unary: treats individual constraints one at a time
37 * Does not do any zonking
38 * Lives in TcS monad so that it can create new skolem variables
39
40
41 %************************************************************************
42 %*                                                                      *
43 %*        Flattening (eliminating all function symbols)                 *
44 %*                                                                      *
45 %************************************************************************
46
47 Note [Flattening]
48 ~~~~~~~~~~~~~~~~~~~~
49   flatten ty  ==>   (xi, cc)
50     where
51       xi has no type functions
52       cc = Auxiliary given (equality) constraints constraining
53            the fresh type variables in xi.  Evidence for these 
54            is always the identity coercion, because internally the
55            fresh flattening skolem variables are actually identified
56            with the types they have been generated to stand in for.
57
58 Note that it is flatten's job to flatten *every type function it sees*.
59 flatten is only called on *arguments* to type functions, by canEqGiven.
60
61 Recall that in comments we use alpha[flat = ty] to represent a
62 flattening skolem variable alpha which has been generated to stand in
63 for ty.
64
65 ----- Example of flattening a constraint: ------
66   flatten (List (F (G Int)))  ==>  (xi, cc)
67     where
68       xi  = List alpha
69       cc  = { G Int ~ beta[flat = G Int],
70               F beta ~ alpha[flat = F beta] }
71 Here
72   * alpha and beta are 'flattening skolem variables'.
73   * All the constraints in cc are 'given', and all their coercion terms 
74     are the identity.
75
76 NB: Flattening Skolems only occur in canonical constraints, which
77 are never zonked, so we don't need to worry about zonking doing
78 accidental unflattening.
79
80 Note that we prefer to leave type synonyms unexpanded when possible,
81 so when the flattener encounters one, it first asks whether its
82 transitive expansion contains any type function applications.  If so,
83 it expands the synonym and proceeds; if not, it simply returns the
84 unexpanded synonym.
85
86 TODO: caching the information about whether transitive synonym
87 expansions contain any type function applications would speed things
88 up a bit; right now we waste a lot of energy traversing the same types
89 multiple times.
90
91 \begin{code}
92 -- Flatten a bunch of types all at once.
93 flattenMany :: CtFlavor -> [Type] -> TcS ([Xi], [Coercion], CanonicalCts)
94 -- Coercions :: Xi ~ Type 
95 flattenMany ctxt tys 
96   = do { (xis, cos, cts_s) <- mapAndUnzip3M (flatten ctxt) tys
97        ; return (xis, cos, andCCans cts_s) }
98
99 -- Flatten a type to get rid of type function applications, returning
100 -- the new type-function-free type, and a collection of new equality
101 -- constraints.  See Note [Flattening] for more detail.
102 flatten :: CtFlavor -> TcType -> TcS (Xi, Coercion, CanonicalCts)
103 -- Postcondition: Coercion :: Xi ~ TcType 
104 flatten ctxt ty 
105   | Just ty' <- tcView ty
106   = do { (xi, co, ccs) <- flatten ctxt ty'
107         -- Preserve type synonyms if possible
108         -- We can tell if ty' is function-free by
109         -- whether there are any floated constraints
110        ; if isEmptyCCan ccs then
111              return (ty, ty, emptyCCan)  
112          else
113              return (xi, co, ccs) }
114
115 flatten _ v@(TyVarTy _)
116   = return (v, v, emptyCCan)
117
118 flatten ctxt (AppTy ty1 ty2)
119   = do { (xi1,co1,c1) <- flatten ctxt ty1
120        ; (xi2,co2,c2) <- flatten ctxt ty2
121        ; return (mkAppTy xi1 xi2, mkAppCoercion co1 co2, c1 `andCCan` c2) }
122
123 flatten ctxt (FunTy ty1 ty2)
124   = do { (xi1,co1,c1) <- flatten ctxt ty1
125        ; (xi2,co2,c2) <- flatten ctxt ty2
126        ; return (mkFunTy xi1 xi2, mkFunCoercion co1 co2, c1 `andCCan` c2) }
127
128 flatten fl (TyConApp tc tys)
129   -- For a normal type constructor or data family application, we just
130   -- recursively flatten the arguments.
131   | not (isSynFamilyTyCon tc)
132     = do { (xis,cos,ccs) <- flattenMany fl tys
133          ; return (mkTyConApp tc xis, mkTyConCoercion tc cos, ccs) }
134
135   -- Otherwise, it's a type function application, and we have to
136   -- flatten it away as well, and generate a new given equality constraint
137   -- between the application and a newly generated flattening skolem variable.
138   | otherwise 
139   = ASSERT( tyConArity tc <= length tys )       -- Type functions are saturated
140       do { (xis, cos, ccs) <- flattenMany fl tys
141          ; let (xi_args, xi_rest)  = splitAt (tyConArity tc) xis
142                (cos_args, cos_rest) = splitAt (tyConArity tc) cos 
143                  -- The type function might be *over* saturated
144                  -- in which case the remaining arguments should
145                  -- be dealt with by AppTys
146                fam_ty = mkTyConApp tc xi_args 
147                fam_co = fam_ty -- identity 
148
149          ; (ret_co, rhs_var, ct) <- 
150              if isGiven fl then
151                do { rhs_var <- newFlattenSkolemTy fam_ty
152                   ; cv <- newGivenCoVar fam_ty rhs_var fam_co
153                   ; let ct = CFunEqCan { cc_id     = cv
154                                        , cc_flavor = fl -- Given
155                                        , cc_fun    = tc 
156                                        , cc_tyargs = xi_args 
157                                        , cc_rhs    = rhs_var }
158                   ; return $ (mkCoVarCoercion cv, rhs_var, ct) }
159              else -- Derived or Wanted: make a new *unification* flatten variable
160                do { rhs_var <- newFlexiTcSTy (typeKind fam_ty)
161                   ; cv <- newWantedCoVar fam_ty rhs_var
162                   ; let ct = CFunEqCan { cc_id = cv
163                                        , cc_flavor = mkWantedFlavor fl
164                                            -- Always Wanted, not Derived
165                                        , cc_fun = tc
166                                        , cc_tyargs = xi_args
167                                        , cc_rhs    = rhs_var }
168                   ; return $ (mkCoVarCoercion cv, rhs_var, ct) }
169
170          ; return ( foldl AppTy rhs_var xi_rest
171                   , foldl AppTy (mkSymCoercion ret_co 
172                                     `mkTransCoercion` mkTyConCoercion tc cos_args) cos_rest
173                   , ccs `extendCCans` ct) }
174
175
176 flatten ctxt (PredTy pred) 
177   = do { (pred', co, ccs) <- flattenPred ctxt pred
178        ; return (PredTy pred', co, ccs) }
179
180 flatten ctxt ty@(ForAllTy {})
181 -- We allow for-alls when, but only when, no type function
182 -- applications inside the forall involve the bound type variables
183 -- TODO: What if it is a (t1 ~ t2) => t3
184 --       Must revisit when the New Coercion API is here! 
185   = do { let (tvs, rho) = splitForAllTys ty
186        ; (rho', co, ccs) <- flatten ctxt rho
187        ; let bad_eqs  = filterBag is_bad ccs
188              is_bad c = tyVarsOfCanonical c `intersectsVarSet` tv_set
189              tv_set   = mkVarSet tvs
190        ; unless (isEmptyBag bad_eqs)
191                 (flattenForAllErrorTcS ctxt ty bad_eqs)
192        ; return (mkForAllTys tvs rho', mkForAllTys tvs co, ccs)  }
193
194 ---------------
195 flattenPred :: CtFlavor -> TcPredType -> TcS (TcPredType, Coercion, CanonicalCts)
196 flattenPred ctxt (ClassP cls tys)
197   = do { (tys', cos, ccs) <- flattenMany ctxt tys
198        ; return (ClassP cls tys', mkClassPPredCo cls cos, ccs) }
199 flattenPred ctxt (IParam nm ty)
200   = do { (ty', co, ccs) <- flatten ctxt ty
201        ; return (IParam nm ty', mkIParamPredCo nm co, ccs) }
202 -- TODO: Handling of coercions between EqPreds must be revisited once the New Coercion API is ready!
203 flattenPred ctxt (EqPred ty1 ty2)
204   = do { (ty1', co1, ccs1) <- flatten ctxt ty1
205        ; (ty2', co2, ccs2) <- flatten ctxt ty2
206        ; return (EqPred ty1' ty2', mkEqPredCo co1 co2, ccs1 `andCCan` ccs2) }
207
208 \end{code}
209
210 %************************************************************************
211 %*                                                                      *
212 %*                Canonicalising given constraints                      *
213 %*                                                                      *
214 %************************************************************************
215
216 \begin{code}
217 canWanteds :: [WantedEvVar] -> TcS CanonicalCts 
218 canWanteds = fmap andCCans . mapM (\(EvVarX ev loc) -> mkCanonical (Wanted loc) ev)
219
220 canGivens :: GivenLoc -> [EvVar] -> TcS CanonicalCts
221 canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc)) givens
222                           ; return (andCCans ccs) }
223
224 mkCanonicals :: CtFlavor -> [EvVar] -> TcS CanonicalCts 
225 mkCanonicals fl vs = fmap andCCans (mapM (mkCanonical fl) vs)
226
227 mkCanonicalFEV :: FlavoredEvVar -> TcS CanonicalCts
228 mkCanonicalFEV (EvVarX ev fl) = mkCanonical fl ev
229
230 mkCanonical :: CtFlavor -> EvVar -> TcS CanonicalCts
231 mkCanonical fl ev = case evVarPred ev of 
232                         ClassP clas tys -> canClass fl ev clas tys 
233                         IParam ip ty    -> canIP    fl ev ip ty
234                         EqPred ty1 ty2  -> canEq    fl ev ty1 ty2 
235                          
236
237 canClass :: CtFlavor -> EvVar -> Class -> [TcType] -> TcS CanonicalCts 
238 canClass fl v cn tys 
239   = do { (xis,cos,ccs) <- flattenMany fl tys  -- cos :: xis ~ tys
240        ; let no_flattening_happened = isEmptyCCan ccs
241              dict_co = mkTyConCoercion (classTyCon cn) cos
242        ; v_new <- if no_flattening_happened then return v
243                   else if isGiven fl        then return v
244                          -- The cos are all identities if fl=Given,
245                          -- hence nothing to do
246                   else do { v' <- newDictVar cn xis  -- D xis
247                           ; when (isWanted fl) $ setDictBind v  (EvCast v' dict_co)
248                           ; when (isGiven fl)  $ setDictBind v' (EvCast v (mkSymCoercion dict_co))
249                                  -- NB: No more setting evidence for derived now 
250                           ; return v' }
251
252        -- Add the superclasses of this one here, See Note [Adding superclasses]. 
253        -- But only if we are not simplifying the LHS of a rule. 
254        ; sctx <- getTcSContext
255        ; sc_cts <- if simplEqsOnly sctx then return emptyCCan 
256                    else newSCWorkFromFlavored v_new fl cn xis
257
258        ; return (sc_cts `andCCan` ccs `extendCCans` CDictCan { cc_id     = v_new
259                                                              , cc_flavor = fl
260                                                              , cc_class  = cn 
261                                                              , cc_tyargs = xis }) }
262 \end{code}
263
264 Note [Adding superclasses]
265 ~~~~~~~~~~~~~~~~~~~~~~~~~~ 
266 Since dictionaries are canonicalized only once in their lifetime, the
267 place to add their superclasses is canonicalisation (The alternative
268 would be to do it during constraint solving, but we'd have to be
269 extremely careful to not repeatedly introduced the same superclass in
270 our worklist). Here is what we do:
271
272 For Givens: 
273        We add all their superclasses as Givens. 
274
275 For Wanteds: 
276        Generally speaking we want to be able to add superclasses of 
277        wanteds for two reasons:
278
279        (1) Oportunities for improvement. Example: 
280                   class (a ~ b) => C a b 
281            Wanted constraint is: C alpha beta 
282            We'd like to simply have C alpha alpha. Similar 
283            situations arise in relation to functional dependencies. 
284            
285        (2) To have minimal constraints to quantify over: 
286            For instance, if our wanted constraint is (Eq a, Ord a) 
287            we'd only like to quantify over Ord a. 
288
289        To deal with (1) above we only add the superclasses of wanteds
290        which may lead to improvement, that is: equality superclasses or 
291        superclasses with functional dependencies. 
292
293        We deal with (2) completely independently in TcSimplify. See 
294        Note [Minimize by SuperClasses] in TcSimplify. 
295
296
297        Moreover, in all cases the extra improvement constraints are 
298        Derived. Derived constraints have an identity (for now), but 
299        we don't do anything with their evidence. For instance they 
300        are never used to rewrite other constraints. 
301
302        See also [New Wanted Superclass Work] in TcInteract. 
303
304
305 For Deriveds: 
306        We do nothing.
307
308 Here's an example that demonstrates why we chose to NOT add
309 superclasses during simplification: [Comes from ticket #4497]
310
311    class Num (RealOf t) => Normed t
312    type family RealOf x
313
314 Assume the generated wanted constraint is: 
315    RealOf e ~ e, Normed e 
316 If we were to be adding the superclasses during simplification we'd get: 
317    Num uf, Normed e, RealOf e ~ e, RealOf e ~ uf 
318 ==> 
319    e ~ uf, Num uf, Normed e, RealOf e ~ e 
320 ==> [Spontaneous solve] 
321    Num uf, Normed uf, RealOf uf ~ uf 
322
323 While looks exactly like our original constraint. If we add the superclass again we'd loop. 
324 By adding superclasses definitely only once, during canonicalisation, this situation can't 
325 happen.
326
327 \begin{code}
328
329 newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS CanonicalCts
330 -- Returns superclasses, see Note [Adding superclasses]
331 newSCWorkFromFlavored ev orig_flavor cls xis 
332   | isDerived orig_flavor 
333   = return emptyCCan  -- Deriveds don't yield more superclasses because we will
334                       -- add them transitively in the case of wanteds. 
335
336   | isGiven orig_flavor 
337   = do { let sc_theta = immSuperClasses cls xis 
338              flavor   = orig_flavor
339        ; sc_vars <- mapM newEvVar sc_theta
340        ; _ <- zipWithM_ setEvBind sc_vars [EvSuperClass ev n | n <- [0..]]
341        ; mkCanonicals flavor sc_vars }
342
343   | isEmptyVarSet (tyVarsOfTypes xis) 
344   = return emptyCCan -- Wanteds with no variables yield no deriveds.
345                      -- See Note [Improvement from Ground Wanteds]
346
347   | otherwise -- Wanted case, just add those SC that can lead to improvement. 
348   = do { let sc_rec_theta = transSuperClasses cls xis 
349              impr_theta   = filter is_improvement_pty sc_rec_theta 
350              Wanted wloc  = orig_flavor
351        ; der_ids <- mapM newDerivedId impr_theta
352        ; mkCanonicals (Derived wloc) der_ids }
353
354
355 is_improvement_pty :: PredType -> Bool 
356 -- Either it's an equality, or has some functional dependency
357 is_improvement_pty (EqPred {})      = True 
358 is_improvement_pty (ClassP cls _ty) = not $ null fundeps
359  where (_,fundeps,_,_,_,_) = classExtraBigSig cls
360 is_improvement_pty _ = False
361
362
363
364
365 canIP :: CtFlavor -> EvVar -> IPName Name -> TcType -> TcS CanonicalCts
366 -- See Note [Canonical implicit parameter constraints] to see why we don't 
367 -- immediately canonicalize (flatten) IP constraints. 
368 canIP fl v nm ty 
369   = return $ singleCCan $ CIPCan { cc_id = v
370                                  , cc_flavor = fl
371                                  , cc_ip_nm = nm
372                                  , cc_ip_ty = ty } 
373
374 -----------------
375 canEq :: CtFlavor -> EvVar -> Type -> Type -> TcS CanonicalCts 
376 canEq fl cv ty1 ty2 
377   | tcEqType ty1 ty2    -- Dealing with equality here avoids
378                         -- later spurious occurs checks for a~a
379   = do { when (isWanted fl) (setWantedCoBind cv ty1)
380        ; return emptyCCan }
381
382 -- If one side is a variable, orient and flatten, 
383 -- WITHOUT expanding type synonyms, so that we tend to 
384 -- substitute a ~ Age rather than a ~ Int when @type Age = Int@
385 canEq fl cv ty1@(TyVarTy {}) ty2 
386   = do { untch <- getUntouchables 
387        ; canEqLeaf untch fl cv (classify ty1) (classify ty2) }
388 canEq fl cv ty1 ty2@(TyVarTy {}) 
389   = do { untch <- getUntouchables 
390        ; canEqLeaf untch fl cv (classify ty1) (classify ty2) }
391       -- NB: don't use VarCls directly because tv1 or tv2 may be scolems!
392
393 canEq fl cv (TyConApp fn tys) ty2 
394   | isSynFamilyTyCon fn, length tys == tyConArity fn
395   = do { untch <- getUntouchables 
396        ; canEqLeaf untch fl cv (FunCls fn tys) (classify ty2) }
397 canEq fl cv ty1 (TyConApp fn tys)
398   | isSynFamilyTyCon fn, length tys == tyConArity fn
399   = do { untch <- getUntouchables 
400        ; canEqLeaf untch fl cv (classify ty1) (FunCls fn tys) }
401
402 canEq fl cv s1 s2
403   | Just (t1a,t1b,t1c) <- splitCoPredTy_maybe s1, 
404     Just (t2a,t2b,t2c) <- splitCoPredTy_maybe s2
405   = do { (v1,v2,v3) 
406              <- if isWanted fl then                   -- Wanted
407                     do { v1 <- newWantedCoVar t1a t2a
408                        ; v2 <- newWantedCoVar t1b t2b 
409                        ; v3 <- newWantedCoVar t1c t2c 
410                        ; let res_co = mkCoPredCo (mkCoVarCoercion v1) 
411                                         (mkCoVarCoercion v2) (mkCoVarCoercion v3)
412                        ; setWantedCoBind cv res_co
413                        ; return (v1,v2,v3) }
414                 else if isGiven fl then               -- Given 
415                          let co_orig = mkCoVarCoercion cv 
416                              coa = mkCsel1Coercion co_orig
417                              cob = mkCsel2Coercion co_orig
418                              coc = mkCselRCoercion co_orig
419                          in do { v1 <- newGivenCoVar t1a t2a coa
420                                ; v2 <- newGivenCoVar t1b t2b cob
421                                ; v3 <- newGivenCoVar t1c t2c coc 
422                                ; return (v1,v2,v3) }
423                 else                                  -- Derived 
424                     do { v1 <- newDerivedId (EqPred t1a t2a)
425                        ; v2 <- newDerivedId (EqPred t1b t2b)
426                        ; v3 <- newDerivedId (EqPred t1c t2c)
427                        ; return (v1,v2,v3) }
428        ; cc1 <- canEq fl v1 t1a t2a 
429        ; cc2 <- canEq fl v2 t1b t2b 
430        ; cc3 <- canEq fl v3 t1c t2c 
431        ; return (cc1 `andCCan` cc2 `andCCan` cc3) }
432
433
434 -- Split up an equality between function types into two equalities.
435 canEq fl cv (FunTy s1 t1) (FunTy s2 t2)
436   = do { (argv, resv) <- 
437              if isWanted fl then 
438                  do { argv <- newWantedCoVar s1 s2 
439                     ; resv <- newWantedCoVar t1 t2 
440                     ; setWantedCoBind cv $ 
441                       mkFunCoercion (mkCoVarCoercion argv) (mkCoVarCoercion resv) 
442                     ; return (argv,resv) } 
443
444              else if isGiven fl then 
445                       let [arg,res] = decomposeCo 2 (mkCoVarCoercion cv) 
446                       in do { argv <- newGivenCoVar s1 s2 arg 
447                             ; resv <- newGivenCoVar t1 t2 res
448                             ; return (argv,resv) } 
449
450              else -- Derived 
451                  do { argv <- newDerivedId (EqPred s1 s2)
452                     ; resv <- newDerivedId (EqPred t1 t2)
453                     ; return (argv,resv) }
454
455        ; cc1 <- canEq fl argv s1 s2 -- inherit original kinds and locations
456        ; cc2 <- canEq fl resv t1 t2
457        ; return (cc1 `andCCan` cc2) }
458
459 canEq fl cv (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2))
460   | n1 == n2
461   = if isWanted fl then 
462         do { v <- newWantedCoVar t1 t2 
463            ; setWantedCoBind cv $ mkIParamPredCo n1 (mkCoVarCoercion cv)
464            ; canEq fl v t1 t2 } 
465     else return emptyCCan -- DV: How to decompose given IP coercions? 
466
467 canEq fl cv (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2))
468   | c1 == c2
469   = if isWanted fl then 
470        do { vs <- zipWithM newWantedCoVar tys1 tys2 
471           ; setWantedCoBind cv $ mkClassPPredCo c1 (map mkCoVarCoercion vs) 
472           ; andCCans <$> zipWith3M (canEq fl) vs tys1 tys2
473           }
474     else return emptyCCan 
475   -- How to decompose given dictionary (and implicit parameter) coercions? 
476   -- You may think that the following is right: 
477   --    let cos = decomposeCo (length tys1) (mkCoVarCoercion cv) 
478   --    in  zipWith3M newGivOrDerCoVar tys1 tys2 cos
479   -- But this assumes that the coercion is a type constructor-based 
480   -- coercion, and not a PredTy (ClassP cn cos) coercion. So we chose
481   -- to not decompose these coercions. We have to get back to this 
482   -- when we clean up the Coercion API.
483
484 canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2)
485   | isAlgTyCon tc1 && isAlgTyCon tc2
486   , tc1 == tc2
487   , length tys1 == length tys2
488   = -- Generate equalities for each of the corresponding arguments
489     do { argsv 
490              <- if isWanted fl then
491                     do { argsv <- zipWithM newWantedCoVar tys1 tys2
492                        ; setWantedCoBind cv $ 
493                          mkTyConCoercion tc1 (map mkCoVarCoercion argsv)
494                        ; return argsv } 
495
496                 else if isGiven fl then 
497                     let cos = decomposeCo (length tys1) (mkCoVarCoercion cv) 
498                     in zipWith3M newGivenCoVar tys1 tys2 cos
499
500                 else -- Derived 
501                     zipWithM (\t1 t2 -> newDerivedId (EqPred t1 t2)) tys1 tys2
502
503        ; andCCans <$> zipWith3M (canEq fl) argsv tys1 tys2 }
504
505 -- See Note [Equality between type applications]
506 --     Note [Care with type applications] in TcUnify
507 canEq fl cv ty1 ty2
508   | Just (s1,t1) <- tcSplitAppTy_maybe ty1
509   , Just (s2,t2) <- tcSplitAppTy_maybe ty2
510     = do { (cv1,cv2) <- 
511              if isWanted fl 
512              then do { cv1 <- newWantedCoVar s1 s2 
513                      ; cv2 <- newWantedCoVar t1 t2 
514                      ; setWantedCoBind cv $ 
515                        mkAppCoercion (mkCoVarCoercion cv1) (mkCoVarCoercion cv2) 
516                      ; return (cv1,cv2) } 
517
518              else if isGiven fl then 
519                     let co1 = mkLeftCoercion  $ mkCoVarCoercion cv 
520                         co2 = mkRightCoercion $ mkCoVarCoercion cv
521                     in do { cv1 <- newGivenCoVar s1 s2 co1 
522                           ; cv2 <- newGivenCoVar t1 t2 co2 
523                           ; return (cv1,cv2) } 
524              else -- Derived
525                  do { cv1 <- newDerivedId (EqPred s1 s2)
526                     ; cv2 <- newDerivedId (EqPred t1 t2)
527                     ; return (cv1,cv2) }
528
529          ; cc1 <- canEq fl cv1 s1 s2 
530          ; cc2 <- canEq fl cv2 t1 t2 
531          ; return (cc1 `andCCan` cc2) } 
532
533 canEq fl cv s1@(ForAllTy {}) s2@(ForAllTy {})
534  | tcIsForAllTy s1, tcIsForAllTy s2, 
535    Wanted {} <- fl 
536  = canEqFailure fl cv
537  | otherwise
538  = do { traceTcS "Ommitting decomposition of given polytype equality" (pprEq s1 s2)
539       ; return emptyCCan }
540
541 -- Finally expand any type synonym applications.
542 canEq fl cv ty1 ty2 | Just ty1' <- tcView ty1 = canEq fl cv ty1' ty2
543 canEq fl cv ty1 ty2 | Just ty2' <- tcView ty2 = canEq fl cv ty1 ty2'
544 canEq fl cv _ _                               = canEqFailure fl cv
545
546 canEqFailure :: CtFlavor -> EvVar -> TcS CanonicalCts
547 canEqFailure fl cv = return (singleCCan (mkFrozenError fl cv))
548 \end{code}
549
550 Note [Equality between type applications]
551 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
552 If we see an equality of the form s1 t1 ~ s2 t2 we can always split
553 it up into s1 ~ s2 /\ t1 ~ t2, since s1 and s2 can't be type
554 functions (type functions use the TyConApp constructor, which never
555 shows up as the LHS of an AppTy).  Other than type functions, types
556 in Haskell are always 
557
558   (1) generative: a b ~ c d implies a ~ c, since different type
559       constructors always generate distinct types
560
561   (2) injective: a b ~ a d implies b ~ d; we never generate the
562       same type from different type arguments.
563
564
565 Note [Canonical ordering for equality constraints]
566 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
567 Implemented as (<+=) below:
568
569   - Type function applications always come before anything else.  
570   - Variables always come before non-variables (other than type
571       function applications).
572
573 Note that we don't need to unfold type synonyms on the RHS to check
574 the ordering; that is, in the rules above it's OK to consider only
575 whether something is *syntactically* a type function application or
576 not.  To illustrate why this is OK, suppose we have an equality of the
577 form 'tv ~ S a b c', where S is a type synonym which expands to a
578 top-level application of the type function F, something like
579
580   type S a b c = F d e
581
582 Then to canonicalize 'tv ~ S a b c' we flatten the RHS, and since S's
583 expansion contains type function applications the flattener will do
584 the expansion and then generate a skolem variable for the type
585 function application, so we end up with something like this:
586
587   tv ~ x
588   F d e ~ x
589
590 where x is the skolem variable.  This is one extra equation than
591 absolutely necessary (we could have gotten away with just 'F d e ~ tv'
592 if we had noticed that S expanded to a top-level type function
593 application and flipped it around in the first place) but this way
594 keeps the code simpler.
595
596 Unlike the OutsideIn(X) draft of May 7, 2010, we do not care about the
597 ordering of tv ~ tv constraints.  There are several reasons why we
598 might:
599
600   (1) In order to be able to extract a substitution that doesn't
601       mention untouchable variables after we are done solving, we might
602       prefer to put touchable variables on the left. However, in and
603       of itself this isn't necessary; we can always re-orient equality
604       constraints at the end if necessary when extracting a substitution.
605
606   (2) To ensure termination we might think it necessary to put
607       variables in lexicographic order. However, this isn't actually 
608       necessary as outlined below.
609
610 While building up an inert set of canonical constraints, we maintain
611 the invariant that the equality constraints in the inert set form an
612 acyclic rewrite system when viewed as L-R rewrite rules.  Moreover,
613 the given constraints form an idempotent substitution (i.e. none of
614 the variables on the LHS occur in any of the RHS's, and type functions
615 never show up in the RHS at all), the wanted constraints also form an
616 idempotent substitution, and finally the LHS of a given constraint
617 never shows up on the RHS of a wanted constraint.  There may, however,
618 be a wanted LHS that shows up in a given RHS, since we do not rewrite
619 given constraints with wanted constraints.
620
621 Suppose we have an inert constraint set
622
623
624   tg_1 ~ xig_1         -- givens
625   tg_2 ~ xig_2
626   ...
627   tw_1 ~ xiw_1         -- wanteds
628   tw_2 ~ xiw_2
629   ...
630
631 where each t_i can be either a type variable or a type function
632 application. Now suppose we take a new canonical equality constraint,
633 t' ~ xi' (note among other things this means t' does not occur in xi')
634 and try to react it with the existing inert set.  We show by induction
635 on the number of t_i which occur in t' ~ xi' that this process will
636 terminate.
637
638 There are several ways t' ~ xi' could react with an existing constraint:
639
640 TODO: finish this proof.  The below was for the case where the entire
641 inert set is an idempotent subustitution...
642
643 (b) We could have t' = t_j for some j.  Then we obtain the new
644     equality xi_j ~ xi'; note that neither xi_j or xi' contain t_j.  We
645     now canonicalize the new equality, which may involve decomposing it
646     into several canonical equalities, and recurse on these.  However,
647     none of the new equalities will contain t_j, so they have fewer
648     occurrences of the t_i than the original equation.
649
650 (a) We could have t_j occurring in xi' for some j, with t' /=
651     t_j. Then we substitute xi_j for t_j in xi' and continue.  However,
652     since none of the t_i occur in xi_j, we have decreased the
653     number of t_i that occur in xi', since we eliminated t_j and did not
654     introduce any new ones.
655
656 \begin{code}
657 data TypeClassifier 
658   = FskCls TcTyVar      -- ^ Flatten skolem 
659   | VarCls TcTyVar      -- ^ Non-flatten-skolem variable 
660   | FunCls TyCon [Type] -- ^ Type function, exactly saturated
661   | OtherCls TcType     -- ^ Neither of the above
662
663 unClassify :: TypeClassifier -> TcType
664 unClassify (VarCls tv)      = TyVarTy tv
665 unClassify (FskCls tv) = TyVarTy tv 
666 unClassify (FunCls fn tys)  = TyConApp fn tys
667 unClassify (OtherCls ty)    = ty
668
669 classify :: TcType -> TypeClassifier
670
671 classify (TyVarTy tv) 
672   | isTcTyVar tv, 
673     FlatSkol {} <- tcTyVarDetails tv = FskCls tv
674   | otherwise                        = VarCls tv
675 classify (TyConApp tc tys) | isSynFamilyTyCon tc
676                            , tyConArity tc == length tys
677                            = FunCls tc tys
678 classify ty                | Just ty' <- tcView ty
679                            = case classify ty' of
680                                OtherCls {} -> OtherCls ty
681                                var_or_fn   -> var_or_fn
682                            | otherwise 
683                            = OtherCls ty
684
685 -- See note [Canonical ordering for equality constraints].
686 reOrient :: CtFlavor -> TypeClassifier -> TypeClassifier -> Bool        
687 -- (t1 `reOrient` t2) responds True 
688 --   iff we should flip to (t2~t1)
689 -- We try to say False if possible, to minimise evidence generation
690 --
691 -- Postcondition: After re-orienting, first arg is not OTherCls
692 reOrient _fl (OtherCls {}) (FunCls {})   = True
693 reOrient _fl (OtherCls {}) (FskCls {})   = True
694 reOrient _fl (OtherCls {}) (VarCls {})   = True
695 reOrient _fl (OtherCls {}) (OtherCls {}) = panic "reOrient"  -- One must be Var/Fun
696
697 reOrient _fl (FunCls {})   (VarCls _tv)  = False  
698   -- But consider the following variation: isGiven fl && isMetaTyVar tv
699
700   -- See Note [No touchables as FunEq RHS] in TcSMonad
701 reOrient _fl (FunCls {}) _                = False             -- Fun/Other on rhs
702
703 reOrient _fl (VarCls {}) (FunCls {})      = True 
704
705 reOrient _fl (VarCls {}) (FskCls {})      = False
706
707 reOrient _fl (VarCls {})  (OtherCls {})   = False
708 reOrient _fl (VarCls tv1)  (VarCls tv2)  
709   | isMetaTyVar tv2 && not (isMetaTyVar tv1) = True 
710   | otherwise                                = False 
711   -- Just for efficiency, see CTyEqCan invariants 
712
713 reOrient _fl (FskCls {}) (VarCls tv2)     = isMetaTyVar tv2 
714   -- Just for efficiency, see CTyEqCan invariants
715
716 reOrient _fl (FskCls {}) (FskCls {})     = False
717 reOrient _fl (FskCls {}) (FunCls {})     = True 
718 reOrient _fl (FskCls {}) (OtherCls {})   = False 
719
720 ------------------
721 canEqLeaf :: TcsUntouchables 
722           -> CtFlavor -> CoVar 
723           -> TypeClassifier -> TypeClassifier -> TcS CanonicalCts 
724 -- Canonicalizing "leaf" equality constraints which cannot be
725 -- decomposed further (ie one of the types is a variable or
726 -- saturated type function application).  
727
728   -- Preconditions: 
729   --    * one of the two arguments is not OtherCls
730   --    * the two types are not equal (looking through synonyms)
731 canEqLeaf _untch fl cv cls1 cls2 
732   | cls1 `re_orient` cls2
733   = do { cv' <- if isWanted fl 
734                 then do { cv' <- newWantedCoVar s2 s1 
735                         ; setWantedCoBind cv $ mkSymCoercion (mkCoVarCoercion cv') 
736                         ; return cv' } 
737                 else if isGiven fl then 
738                          newGivenCoVar s2 s1 (mkSymCoercion (mkCoVarCoercion cv))
739                 else -- Derived
740                     newDerivedId (EqPred s2 s1)
741        ; canEqLeafOriented fl cv' cls2 s1 }
742
743   | otherwise
744   = do { traceTcS "canEqLeaf" (ppr (unClassify cls1) $$ ppr (unClassify cls2))
745        ; canEqLeafOriented fl cv cls1 s2 }
746   where
747     re_orient = reOrient fl 
748     s1 = unClassify cls1  
749     s2 = unClassify cls2  
750
751 ------------------
752 canEqLeafOriented :: CtFlavor -> CoVar 
753                   -> TypeClassifier -> TcType -> TcS CanonicalCts 
754 -- First argument is not OtherCls
755 canEqLeafOriented fl cv cls1@(FunCls fn tys1) s2         -- cv : F tys1
756   | let k1 = kindAppResult (tyConKind fn) tys1,
757     let k2 = typeKind s2, 
758     not (k1 `compatKind` k2) -- Establish the kind invariant for CFunEqCan
759   = canEqFailure fl cv
760     -- Eagerly fails, see Note [Kind errors] in TcInteract
761
762   | otherwise 
763   = ASSERT2( isSynFamilyTyCon fn, ppr (unClassify cls1) )
764     do { (xis1,cos1,ccs1) <- flattenMany fl tys1 -- Flatten type function arguments
765                                                  -- cos1 :: xis1 ~ tys1
766        ; (xi2, co2, ccs2) <- flatten fl s2       -- Flatten entire RHS
767                                                  -- co2  :: xi2 ~ s2
768        ; let ccs = ccs1 `andCCan` ccs2
769              no_flattening_happened = isEmptyCCan ccs
770        ; cv_new <- if no_flattening_happened then return cv
771                    else if isGiven fl        then return cv
772                    else if isWanted fl then 
773                          do { cv' <- newWantedCoVar (unClassify (FunCls fn xis1)) xi2
774                                  -- cv' : F xis ~ xi2
775                             ; let -- fun_co :: F xis1 ~ F tys1
776                                  fun_co = mkTyConCoercion fn cos1
777                                  -- want_co :: F tys1 ~ s2
778                                  want_co = mkSymCoercion fun_co
779                                            `mkTransCoercion` mkCoVarCoercion cv'
780                                            `mkTransCoercion` co2
781                             ; setWantedCoBind cv  want_co
782                             ; return cv' }
783                    else -- Derived 
784                        newDerivedId (EqPred (unClassify (FunCls fn xis1)) xi2)
785
786        ; let final_cc = CFunEqCan { cc_id     = cv_new
787                                   , cc_flavor = fl
788                                   , cc_fun    = fn
789                                   , cc_tyargs = xis1 
790                                   , cc_rhs    = xi2 }
791        ; return $ ccs `extendCCans` final_cc }
792
793 -- Otherwise, we have a variable on the left, so call canEqLeafTyVarLeft
794 canEqLeafOriented fl cv (FskCls tv) s2 
795   = canEqLeafTyVarLeft fl cv tv s2 
796 canEqLeafOriented fl cv (VarCls tv) s2 
797   = canEqLeafTyVarLeft fl cv tv s2 
798 canEqLeafOriented _ cv (OtherCls ty1) ty2 
799   = pprPanic "canEqLeaf" (ppr cv $$ ppr ty1 $$ ppr ty2)
800
801 canEqLeafTyVarLeft :: CtFlavor -> CoVar -> TcTyVar -> TcType -> TcS CanonicalCts
802 -- Establish invariants of CTyEqCans 
803 canEqLeafTyVarLeft fl cv tv s2       -- cv : tv ~ s2
804   | not (k1 `compatKind` k2) -- Establish the kind invariant for CTyEqCan
805   = canEqFailure fl cv
806        -- Eagerly fails, see Note [Kind errors] in TcInteract
807   | otherwise
808   = do { (xi2, co, ccs2) <- flatten fl s2  -- Flatten RHS   co : xi2 ~ s2
809        ; mxi2' <- canOccursCheck fl tv xi2 -- Do an occurs check, and return a possibly
810                                            -- unfolded version of the RHS, if we had to 
811                                            -- unfold any type synonyms to get rid of tv.
812        ; case mxi2' of {
813            Nothing   -> canEqFailure fl cv ;
814            Just xi2' ->
815     do { let no_flattening_happened = isEmptyCCan ccs2
816        ; cv_new <- if no_flattening_happened then return cv
817                    else if isGiven fl        then return cv
818                    else if isWanted fl then 
819                          do { cv' <- newWantedCoVar (mkTyVarTy tv) xi2'  -- cv' : tv ~ xi2
820                             ; setWantedCoBind cv  (mkCoVarCoercion cv' `mkTransCoercion` co)
821                             ; return cv' }
822                    else -- Derived
823                        newDerivedId (EqPred (mkTyVarTy tv) xi2')
824
825        ; return $ ccs2 `extendCCans` CTyEqCan { cc_id     = cv_new
826                                               , cc_flavor = fl
827                                               , cc_tyvar  = tv
828                                               , cc_rhs    = xi2' } } } }
829   where
830     k1 = tyVarKind tv
831     k2 = typeKind s2
832
833 -- See Note [Type synonyms and canonicalization].
834 -- Check whether the given variable occurs in the given type.  We may
835 -- have needed to do some type synonym unfolding in order to get rid
836 -- of the variable, so we also return the unfolded version of the
837 -- type, which is guaranteed to be syntactically free of the given
838 -- type variable.  If the type is already syntactically free of the
839 -- variable, then the same type is returned.
840 --
841 -- Precondition: the two types are not equal (looking though synonyms)
842 canOccursCheck :: CtFlavor -> TcTyVar -> Xi -> TcS (Maybe Xi)
843 canOccursCheck _gw tv xi = return (expandAway tv xi)
844 \end{code}
845
846 @expandAway tv xi@ expands synonyms in xi just enough to get rid of
847 occurrences of tv, if that is possible; otherwise, it returns Nothing.
848 For example, suppose we have
849   type F a b = [a]
850 Then
851   expandAway b (F Int b) = Just [Int]
852 but
853   expandAway a (F a Int) = Nothing
854
855 We don't promise to do the absolute minimum amount of expanding
856 necessary, but we try not to do expansions we don't need to.  We
857 prefer doing inner expansions first.  For example,
858   type F a b = (a, Int, a, [a])
859   type G b   = Char
860 We have
861   expandAway b (F (G b)) = F Char
862 even though we could also expand F to get rid of b.
863
864 \begin{code}
865 expandAway :: TcTyVar -> Xi -> Maybe Xi
866 expandAway tv t@(TyVarTy tv') 
867   | tv == tv' = Nothing
868   | otherwise = Just t
869 expandAway tv xi
870   | not (tv `elemVarSet` tyVarsOfType xi) = Just xi
871 expandAway tv (AppTy ty1 ty2) 
872   = do { ty1' <- expandAway tv ty1
873        ; ty2' <- expandAway tv ty2 
874        ; return (mkAppTy ty1' ty2') }
875 -- mkAppTy <$> expandAway tv ty1 <*> expandAway tv ty2
876 expandAway tv (FunTy ty1 ty2)
877   = do { ty1' <- expandAway tv ty1 
878        ; ty2' <- expandAway tv ty2 
879        ; return (mkFunTy ty1' ty2') } 
880 -- mkFunTy <$> expandAway tv ty1 <*> expandAway tv ty2
881 expandAway tv ty@(ForAllTy {}) 
882   = let (tvs,rho) = splitForAllTys ty
883         tvs_knds  = map tyVarKind tvs 
884     in if tv `elemVarSet` tyVarsOfTypes tvs_knds then 
885        -- Can't expand away the kinds unless we create 
886        -- fresh variables which we don't want to do at this point.
887            Nothing 
888        else do { rho' <- expandAway tv rho
889                ; return (mkForAllTys tvs rho') }
890 expandAway tv (PredTy pred) 
891   = do { pred' <- expandAwayPred tv pred  
892        ; return (PredTy pred') }
893 -- For a type constructor application, first try expanding away the
894 -- offending variable from the arguments.  If that doesn't work, next
895 -- see if the type constructor is a type synonym, and if so, expand
896 -- it and try again.
897 expandAway tv ty@(TyConApp tc tys)
898   = (mkTyConApp tc <$> mapM (expandAway tv) tys) <|> (tcView ty >>= expandAway tv)
899
900 expandAwayPred :: TcTyVar -> TcPredType -> Maybe TcPredType 
901 expandAwayPred tv (ClassP cls tys) 
902   = do { tys' <- mapM (expandAway tv) tys; return (ClassP cls tys') } 
903 expandAwayPred tv (EqPred ty1 ty2)
904   = do { ty1' <- expandAway tv ty1
905        ; ty2' <- expandAway tv ty2 
906        ; return (EqPred ty1' ty2') }
907 expandAwayPred tv (IParam nm ty) 
908   = do { ty' <- expandAway tv ty
909        ; return (IParam nm ty') }
910
911                 
912
913 \end{code}
914
915 Note [Type synonyms and canonicalization]
916 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
917
918 We treat type synonym applications as xi types, that is, they do not
919 count as type function applications.  However, we do need to be a bit
920 careful with type synonyms: like type functions they may not be
921 generative or injective.  However, unlike type functions, they are
922 parametric, so there is no problem in expanding them whenever we see
923 them, since we do not need to know anything about their arguments in
924 order to expand them; this is what justifies not having to treat them
925 as specially as type function applications.  The thing that causes
926 some subtleties is that we prefer to leave type synonym applications
927 *unexpanded* whenever possible, in order to generate better error
928 messages.
929
930 If we encounter an equality constraint with type synonym applications
931 on both sides, or a type synonym application on one side and some sort
932 of type application on the other, we simply must expand out the type
933 synonyms in order to continue decomposing the equality constraint into
934 primitive equality constraints.  For example, suppose we have
935
936   type F a = [Int]
937
938 and we encounter the equality
939
940   F a ~ [b]
941
942 In order to continue we must expand F a into [Int], giving us the
943 equality
944
945   [Int] ~ [b]
946
947 which we can then decompose into the more primitive equality
948 constraint
949
950   Int ~ b.
951
952 However, if we encounter an equality constraint with a type synonym
953 application on one side and a variable on the other side, we should
954 NOT (necessarily) expand the type synonym, since for the purpose of
955 good error messages we want to leave type synonyms unexpanded as much
956 as possible.
957
958 However, there is a subtle point with type synonyms and the occurs
959 check that takes place for equality constraints of the form tv ~ xi.
960 As an example, suppose we have
961
962   type F a = Int
963
964 and we come across the equality constraint
965
966   a ~ F a
967
968 This should not actually fail the occurs check, since expanding out
969 the type synonym results in the legitimate equality constraint a ~
970 Int.  We must actually do this expansion, because unifying a with F a
971 will lead the type checker into infinite loops later.  Put another
972 way, canonical equality constraints should never *syntactically*
973 contain the LHS variable in the RHS type.  However, we don't always
974 need to expand type synonyms when doing an occurs check; for example,
975 the constraint
976
977   a ~ F b
978
979 is obviously fine no matter what F expands to. And in this case we
980 would rather unify a with F b (rather than F b's expansion) in order
981 to get better error messages later.
982
983 So, when doing an occurs check with a type synonym application on the
984 RHS, we use some heuristics to find an expansion of the RHS which does
985 not contain the variable from the LHS.  In particular, given
986
987   a ~ F t1 ... tn
988
989 we first try expanding each of the ti to types which no longer contain
990 a.  If this turns out to be impossible, we next try expanding F
991 itself, and so on.
992
993
994