Yet another major refactoring of the constraint solver
[ghc.git] / compiler / typecheck / TcUnify.lhs
1 %
2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 %
5
6 Type subsumption and unification
7
8 \begin{code}
9 {-# OPTIONS -fno-warn-tabs #-}
10 -- The above warning supression flag is a temporary kludge.
11 -- While working on this module you are encouraged to remove it and
12 -- detab the module (please do the detabbing in a separate patch). See
13 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
14 -- for details
15
16 module TcUnify (
17   -- Full-blown subsumption
18   tcWrapResult, tcSubType, tcGen, 
19   checkConstraints, newImplication, 
20
21   -- Various unifications
22   unifyType, unifyTypeList, unifyTheta, unifyKind, unifyKindEq,
23
24   --------------------------------
25   -- Holes
26   tcInfer,
27   matchExpectedListTy,
28   matchExpectedPArrTy,
29   matchExpectedTyConApp,
30   matchExpectedAppTy, 
31   matchExpectedFunTys,
32   matchExpectedFunKind,
33   wrapFunResCoercion,
34
35   --------------------------------
36   -- Errors
37   mkKindErrorCtxt
38
39   ) where
40
41 #include "HsVersions.h"
42
43 import HsSyn
44 import TypeRep
45 import TcMType
46 import TcIface
47 import TcRnMonad
48 import TcType
49 import Type
50 import TcEvidence
51 import Name ( isSystemName )
52 import Inst
53 import Kind
54 import TyCon
55 import TysWiredIn
56 import Var
57 import VarSet
58 import VarEnv
59 import ErrUtils
60 import DynFlags
61 import BasicTypes
62 import Maybes ( allMaybes )
63 import Util
64 import Outputable
65 import FastString
66
67 import Control.Monad
68 \end{code}
69
70
71 %************************************************************************
72 %*                                                                      *
73              matchExpected functions
74 %*                                                                      *
75 %************************************************************************
76
77 Note [Herald for matchExpectedFunTys]
78 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
79 The 'herald' always looks like:
80    "The equation(s) for 'f' have"
81    "The abstraction (\x.e) takes"
82    "The section (+ x) expects"
83    "The function 'f' is applied to"
84
85 This is used to construct a message of form
86
87    The abstraction `\Just 1 -> ...' takes two arguments
88    but its type `Maybe a -> a' has only one
89
90    The equation(s) for `f' have two arguments
91    but its type `Maybe a -> a' has only one
92
93    The section `(f 3)' requires 'f' to take two arguments
94    but its type `Int -> Int' has only one
95
96    The function 'f' is applied to two arguments
97    but its type `Int -> Int' has only one
98
99 Note [matchExpectedFunTys]
100 ~~~~~~~~~~~~~~~~~~~~~~~~~~
101 matchExpectedFunTys checks that an (Expected rho) has the form
102 of an n-ary function.  It passes the decomposed type to the
103 thing_inside, and returns a wrapper to coerce between the two types
104
105 It's used wherever a language construct must have a functional type,
106 namely:
107         A lambda expression
108         A function definition
109      An operator section
110
111 This is not (currently) where deep skolemisation occurs;
112 matchExpectedFunTys does not skolmise nested foralls in the 
113 expected type, becuase it expects that to have been done already
114
115
116 \begin{code}
117 matchExpectedFunTys :: SDoc     -- See Note [Herald for matchExpectedFunTys]
118                     -> Arity
119                     -> TcRhoType 
120                     -> TcM (TcCoercion, [TcSigmaType], TcRhoType)
121
122 -- If    matchExpectFunTys n ty = (co, [t1,..,tn], ty_r)
123 -- then  co : ty ~ (t1 -> ... -> tn -> ty_r)
124 --
125 -- Does not allocate unnecessary meta variables: if the input already is 
126 -- a function, we just take it apart.  Not only is this efficient, 
127 -- it's important for higher rank: the argument might be of form
128 --              (forall a. ty) -> other
129 -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
130 -- hide the forall inside a meta-variable
131
132 matchExpectedFunTys herald arity orig_ty 
133   = go arity orig_ty
134   where
135     -- If     go n ty = (co, [t1,..,tn], ty_r)
136     -- then   co : ty ~ t1 -> .. -> tn -> ty_r
137
138     go n_req ty
139       | n_req == 0 = return (mkTcReflCo ty, [], ty)
140
141     go n_req ty
142       | Just ty' <- tcView ty = go n_req ty'
143
144     go n_req (FunTy arg_ty res_ty)
145       | not (isPredTy arg_ty)
146       = do { (co, tys, ty_r) <- go (n_req-1) res_ty
147            ; return (mkTcFunCo (mkTcReflCo arg_ty) co, arg_ty:tys, ty_r) }
148
149     go n_req ty@(TyVarTy tv)
150       | ASSERT( isTcTyVar tv) isMetaTyVar tv
151       = do { cts <- readMetaTyVar tv
152            ; case cts of
153                Indirect ty' -> go n_req ty'
154                Flexi        -> defer n_req ty }
155
156        -- In all other cases we bale out into ordinary unification
157     go n_req ty = defer n_req ty
158
159     ------------
160     defer n_req fun_ty 
161       = addErrCtxtM mk_ctxt $
162         do { arg_tys <- newFlexiTyVarTys n_req argTypeKind
163            ; res_ty  <- newFlexiTyVarTy openTypeKind
164            ; co   <- unifyType fun_ty (mkFunTys arg_tys res_ty)
165            ; return (co, arg_tys, res_ty) }
166
167     ------------
168     mk_ctxt :: TidyEnv -> TcM (TidyEnv, MsgDoc)
169     mk_ctxt env = do { orig_ty1 <- zonkTcType orig_ty
170                      ; let (env', orig_ty2) = tidyOpenType env orig_ty1
171                            (args, _) = tcSplitFunTys orig_ty2
172                            n_actual = length args
173                      ; return (env', mk_msg orig_ty2 n_actual) }
174
175     mk_msg ty n_args
176       = herald <+> speakNOf arity (ptext (sLit "argument")) <> comma $$ 
177         sep [ptext (sLit "but its type") <+> quotes (pprType ty), 
178              if n_args == 0 then ptext (sLit "has none") 
179              else ptext (sLit "has only") <+> speakN n_args]
180 \end{code}
181
182
183 \begin{code}
184 ----------------------
185 matchExpectedListTy :: TcRhoType -> TcM (TcCoercion, TcRhoType)
186 -- Special case for lists
187 matchExpectedListTy exp_ty
188  = do { (co, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty
189       ; return (co, elt_ty) }
190
191 ----------------------
192 matchExpectedPArrTy :: TcRhoType -> TcM (TcCoercion, TcRhoType)
193 -- Special case for parrs
194 matchExpectedPArrTy exp_ty
195   = do { (co, [elt_ty]) <- matchExpectedTyConApp parrTyCon exp_ty
196        ; return (co, elt_ty) }
197
198 ----------------------
199 matchExpectedTyConApp :: TyCon                -- T :: forall kv1 ... kvm. k1 -> ... -> kn -> *
200                       -> TcRhoType            -- orig_ty
201                       -> TcM (TcCoercion,      -- T k1 k2 k3 a b c ~ orig_ty
202                               [TcSigmaType])  -- Element types, k1 k2 k3 a b c
203                               
204 -- It's used for wired-in tycons, so we call checkWiredInTyCon
205 -- Precondition: never called with FunTyCon
206 -- Precondition: input type :: *
207
208 matchExpectedTyConApp tc orig_ty
209   = do  { checkWiredInTyCon tc
210         ; go (tyConArity tc) orig_ty [] }
211   where
212     go :: Int -> TcRhoType -> [TcSigmaType] -> TcM (TcCoercion, [TcSigmaType])
213     -- If     go n ty tys = (co, [t1..tn] ++ tys)
214     -- then   co : T t1..tn ~ ty
215
216     go n_req ty tys
217       | Just ty' <- tcView ty = go n_req ty' tys
218
219     go n_req ty@(TyVarTy tv) tys
220       | ASSERT( isTcTyVar tv) isMetaTyVar tv
221       = do { cts <- readMetaTyVar tv
222            ; case cts of
223                Indirect ty -> go n_req ty tys
224                Flexi       -> defer n_req ty tys }
225
226     go n_req ty@(TyConApp tycon args) tys
227       | tc == tycon
228       = ASSERT( n_req == length args)   -- ty::*
229         return (mkTcReflCo ty, args ++ tys)
230
231     go n_req (AppTy fun arg) tys
232       | n_req > 0
233       = do { (co, args) <- go (n_req - 1) fun (arg : tys) 
234            ; return (mkTcAppCo co (mkTcReflCo arg), args) }
235
236     go n_req ty tys = defer n_req ty tys
237
238     ----------
239     defer n_req ty tys
240       = do { kappa_tys <- mapM (const newMetaKindVar) kvs
241            ; let arg_kinds' = map (substKiWith kvs kappa_tys) arg_kinds
242            ; tau_tys <- mapM newFlexiTyVarTy arg_kinds'
243            ; co <- unifyType (mkTyConApp tc (kappa_tys ++ tau_tys)) ty
244            ; return (co, kappa_tys ++ tau_tys ++ tys) }
245       where
246         (kvs, body) = splitForAllTys (tyConKind tc)
247         (arg_kinds, _) = splitKindFunTysN (n_req - length kvs) body
248
249 ----------------------
250 matchExpectedAppTy :: TcRhoType                         -- orig_ty
251                    -> TcM (TcCoercion,                   -- m a ~ orig_ty
252                            (TcSigmaType, TcSigmaType))  -- Returns m, a
253 -- If the incoming type is a mutable type variable of kind k, then
254 -- matchExpectedAppTy returns a new type variable (m: * -> k); note the *.
255
256 matchExpectedAppTy orig_ty
257   = go orig_ty
258   where
259     go ty
260       | Just ty' <- tcView ty = go ty'
261
262       | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
263       = return (mkTcReflCo orig_ty, (fun_ty, arg_ty))
264
265     go (TyVarTy tv)
266       | ASSERT( isTcTyVar tv) isMetaTyVar tv
267       = do { cts <- readMetaTyVar tv
268            ; case cts of
269                Indirect ty -> go ty
270                Flexi       -> defer }
271
272     go _ = defer
273
274     -- Defer splitting by generating an equality constraint
275     defer = do { ty1 <- newFlexiTyVarTy kind1
276                ; ty2 <- newFlexiTyVarTy kind2
277                ; co <- unifyType (mkAppTy ty1 ty2) orig_ty
278                ; return (co, (ty1, ty2)) }
279
280     orig_kind = typeKind orig_ty
281     kind1 = mkArrowKind liftedTypeKind (defaultKind orig_kind)
282     kind2 = liftedTypeKind    -- m :: * -> k
283                               -- arg type :: *
284         -- The defaultKind is a bit smelly.  If you remove it,
285         -- try compiling        f x = do { x }
286         -- and you'll get a kind mis-match.  It smells, but
287         -- not enough to lose sleep over.
288 \end{code}
289
290
291 %************************************************************************
292 %*                                                                      *
293                 Subsumption checking
294 %*                                                                      *
295 %************************************************************************
296
297 All the tcSub calls have the form
298                 tcSub actual_ty expected_ty
299 which checks
300                 actual_ty <= expected_ty
301
302 That is, that a value of type actual_ty is acceptable in
303 a place expecting a value of type expected_ty.
304
305 It returns a coercion function
306         co_fn :: actual_ty ~ expected_ty
307 which takes an HsExpr of type actual_ty into one of type
308 expected_ty.
309
310 \begin{code}
311 tcSubType :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
312 -- Check that ty_actual is more polymorphic than ty_expected
313 -- Both arguments might be polytypes, so we must instantiate and skolemise
314 -- Returns a wrapper of shape   ty_actual ~ ty_expected
315 tcSubType origin ctxt ty_actual ty_expected
316   | isSigmaTy ty_actual
317   = do { (sk_wrap, inst_wrap) 
318             <- tcGen ctxt ty_expected $ \ _ sk_rho -> do
319             { (in_wrap, in_rho) <- deeplyInstantiate origin ty_actual
320             ; cow <- unifyType in_rho sk_rho
321             ; return (coToHsWrapper cow <.> in_wrap) }
322        ; return (sk_wrap <.> inst_wrap) }
323
324   | otherwise   -- Urgh!  It seems deeply weird to have equality
325                 -- when actual is not a polytype, and it makes a big 
326                 -- difference e.g. tcfail104
327   = do { cow <- unifyType ty_actual ty_expected
328        ; return (coToHsWrapper cow) }
329   
330 tcInfer :: (TcType -> TcM a) -> TcM (a, TcType)
331 tcInfer tc_infer = do { ty  <- newFlexiTyVarTy openTypeKind
332                       ; res <- tc_infer ty
333                       ; return (res, ty) }
334
335 -----------------
336 tcWrapResult :: HsExpr TcId -> TcRhoType -> TcRhoType -> TcM (HsExpr TcId)
337 tcWrapResult expr actual_ty res_ty
338   = do { cow <- unifyType actual_ty res_ty
339                 -- Both types are deeply skolemised
340        ; return (mkHsWrapCo cow expr) }
341
342 -----------------------------------
343 wrapFunResCoercion
344         :: [TcType]     -- Type of args
345         -> HsWrapper    -- HsExpr a -> HsExpr b
346         -> TcM HsWrapper        -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
347 wrapFunResCoercion arg_tys co_fn_res
348   | isIdHsWrapper co_fn_res
349   = return idHsWrapper
350   | null arg_tys
351   = return co_fn_res
352   | otherwise
353   = do  { arg_ids <- newSysLocalIds (fsLit "sub") arg_tys
354         ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpEvVarApps arg_ids) }
355 \end{code}
356
357
358
359 %************************************************************************
360 %*                                                                      *
361 \subsection{Generalisation}
362 %*                                                                      *
363 %************************************************************************
364
365 \begin{code}
366 tcGen :: UserTypeCtxt -> TcType
367       -> ([TcTyVar] -> TcRhoType -> TcM result)
368       -> TcM (HsWrapper, result)
369         -- The expression has type: spec_ty -> expected_ty
370
371 tcGen ctxt expected_ty thing_inside
372    -- We expect expected_ty to be a forall-type
373    -- If not, the call is a no-op
374   = do  { traceTc "tcGen" empty
375         ; (wrap, tvs', given, rho') <- deeplySkolemise expected_ty
376
377         ; when debugIsOn $
378               traceTc "tcGen" $ vcat [
379                            text "expected_ty" <+> ppr expected_ty,
380                            text "inst ty" <+> ppr tvs' <+> ppr rho' ]
381
382         -- Generally we must check that the "forall_tvs" havn't been constrained
383         -- The interesting bit here is that we must include the free variables
384         -- of the expected_ty.  Here's an example:
385         --       runST (newVar True)
386         -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
387         -- for (newVar True), with s fresh.  Then we unify with the runST's arg type
388         -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
389         -- So now s' isn't unconstrained because it's linked to a.
390         -- 
391         -- However [Oct 10] now that the untouchables are a range of 
392         -- TcTyVars, all this is handled automatically with no need for
393         -- extra faffing around
394
395         -- Use the *instantiated* type in the SkolemInfo
396         -- so that the names of displayed type variables line up
397         ; let skol_info = SigSkol ctxt (mkPiTypes given rho')
398
399         ; (ev_binds, result) <- checkConstraints skol_info tvs' given $
400                                 thing_inside tvs' rho'
401
402         ; return (wrap <.> mkWpLet ev_binds, result) }
403           -- The ev_binds returned by checkConstraints is very
404           -- often empty, in which case mkWpLet is a no-op
405
406 checkConstraints :: SkolemInfo
407                  -> [TcTyVar]           -- Skolems
408                  -> [EvVar]             -- Given
409                  -> TcM result
410                  -> TcM (TcEvBinds, result)
411
412 checkConstraints skol_info skol_tvs given thing_inside
413   | null skol_tvs && null given
414   = do { res <- thing_inside; return (emptyTcEvBinds, res) }
415       -- Just for efficiency.  We check every function argument with
416       -- tcPolyExpr, which uses tcGen and hence checkConstraints.
417
418   | otherwise
419   = newImplication skol_info skol_tvs given thing_inside
420
421 newImplication :: SkolemInfo -> [TcTyVar]
422                -> [EvVar] -> TcM result
423                -> TcM (TcEvBinds, result)
424 newImplication skol_info skol_tvs given thing_inside
425   = ASSERT2( all isTcTyVar skol_tvs, ppr skol_tvs )
426     ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
427     do { ((result, untch), wanted) <- captureConstraints  $ 
428                                       captureUntouchables $
429                                       thing_inside
430
431        ; if isEmptyWC wanted && not (hasEqualities given)
432             -- Optimisation : if there are no wanteds, and the givens
433             -- are sufficiently simple, don't generate an implication
434             -- at all.  Reason for the hasEqualities test:
435             -- we don't want to lose the "inaccessible alternative"
436             -- error check
437          then 
438             return (emptyTcEvBinds, result)
439          else do
440        { ev_binds_var <- newTcEvBinds
441        ; lcl_env <- getLclTypeEnv
442        ; loc <- getCtLoc skol_info
443        ; emitImplication $ Implic { ic_untch = untch
444                                   , ic_env = lcl_env
445                                   , ic_skols = skol_tvs
446                                   , ic_given = given
447                                   , ic_wanted = wanted
448                                   , ic_insol  = insolubleWC wanted
449                                   , ic_binds = ev_binds_var
450                                   , ic_loc = loc }
451
452        ; return (TcEvBinds ev_binds_var, result) } }
453 \end{code}
454
455 %************************************************************************
456 %*                                                                      *
457                 Boxy unification
458 %*                                                                      *
459 %************************************************************************
460
461 The exported functions are all defined as versions of some
462 non-exported generic functions.
463
464 \begin{code}
465 unifyType :: TcTauType -> TcTauType -> TcM TcCoercion
466 -- Actual and expected types
467 -- Returns a coercion : ty1 ~ ty2
468 unifyType ty1 ty2 = uType [] ty1 ty2
469
470 ---------------
471 unifyPred :: PredType -> PredType -> TcM TcCoercion
472 -- Actual and expected types
473 unifyPred = unifyType
474
475 ---------------
476 unifyTheta :: TcThetaType -> TcThetaType -> TcM [TcCoercion]
477 -- Actual and expected types
478 unifyTheta theta1 theta2
479   = do  { checkTc (equalLength theta1 theta2)
480                   (vcat [ptext (sLit "Contexts differ in length"),
481                          nest 2 $ parens $ ptext (sLit "Use -XRelaxedPolyRec to allow this")])
482         ; zipWithM unifyPred theta1 theta2 }
483 \end{code}
484
485 @unifyTypeList@ takes a single list of @TauType@s and unifies them
486 all together.  It is used, for example, when typechecking explicit
487 lists, when all the elts should be of the same type.
488
489 \begin{code}
490 unifyTypeList :: [TcTauType] -> TcM ()
491 unifyTypeList []                 = return ()
492 unifyTypeList [_]                = return ()
493 unifyTypeList (ty1:tys@(ty2:_)) = do { _ <- unifyType ty1 ty2
494                                      ; unifyTypeList tys }
495 \end{code}
496
497 %************************************************************************
498 %*                                                                      *
499                  uType and friends                                                                      
500 %*                                                                      *
501 %************************************************************************
502
503 uType is the heart of the unifier.  Each arg occurs twice, because
504 we want to report errors in terms of synomyms if possible.  The first of
505 the pair is used in error messages only; it is always the same as the
506 second, except that if the first is a synonym then the second may be a
507 de-synonym'd version.  This way we get better error messages.
508
509 \begin{code}
510 data SwapFlag 
511   = NotSwapped  -- Args are: actual,   expected
512   | IsSwapped   -- Args are: expected, actual
513
514 instance Outputable SwapFlag where
515   ppr IsSwapped  = ptext (sLit "Is-swapped")
516   ppr NotSwapped = ptext (sLit "Not-swapped")
517
518 unSwap :: SwapFlag -> (a->a->b) -> a -> a -> b
519 unSwap NotSwapped f a b = f a b
520 unSwap IsSwapped  f a b = f b a
521
522 ------------
523 uType, uType_np, uType_defer
524   :: [EqOrigin]
525   -> TcType    -- ty1 is the *actual* type
526   -> TcType    -- ty2 is the *expected* type
527   -> TcM TcCoercion
528
529 --------------
530 -- It is always safe to defer unification to the main constraint solver
531 -- See Note [Deferred unification]
532 uType_defer items ty1 ty2
533   = ASSERT( not (null items) )
534     do { eqv <- newEq ty1 ty2
535        ; loc <- getCtLoc (TypeEqOrigin (last items))
536        ; let ctev = Wanted { ctev_wloc = loc, ctev_evar = eqv
537                            , ctev_pred = mkTcEqPred ty1 ty2 }
538        ; emitFlat $ mkNonCanonical ctev 
539
540        -- Error trace only
541        -- NB. do *not* call mkErrInfo unless tracing is on, because
542        -- it is hugely expensive (#5631)
543        ; ifDOptM Opt_D_dump_tc_trace $ do
544             { ctxt <- getErrCtxt
545             ; doc <- mkErrInfo emptyTidyEnv ctxt
546             ; traceTc "utype_defer" (vcat [ppr eqv, ppr ty1,
547                                            ppr ty2, ppr items, doc])
548             }
549        ; return (mkTcCoVarCo eqv) }
550
551 --------------
552 -- Push a new item on the origin stack (the most common case)
553 uType origin ty1 ty2  -- Push a new item on the origin stack
554   = uType_np (pushOrigin ty1 ty2 origin) ty1 ty2
555
556 --------------
557 -- unify_np (short for "no push" on the origin stack) does the work
558 uType_np origin orig_ty1 orig_ty2
559   = do { traceTc "u_tys " $ vcat 
560               [ sep [ ppr orig_ty1, text "~", ppr orig_ty2]
561               , ppr origin]
562        ; co <- go orig_ty1 orig_ty2
563        ; if isTcReflCo co
564             then traceTc "u_tys yields no coercion" empty
565             else traceTc "u_tys yields coercion:" (ppr co)
566        ; return co }
567   where
568     go :: TcType -> TcType -> TcM TcCoercion
569         -- The arguments to 'go' are always semantically identical 
570         -- to orig_ty{1,2} except for looking through type synonyms
571
572         -- Variables; go for uVar
573         -- Note that we pass in *original* (before synonym expansion), 
574         -- so that type variables tend to get filled in with 
575         -- the most informative version of the type
576     go (TyVarTy tv1) ty2 
577       = do { lookup_res <- lookupTcTyVar tv1
578            ; case lookup_res of
579                Filled ty1   -> go ty1 ty2
580                Unfilled ds1 -> uUnfilledVar origin NotSwapped tv1 ds1 ty2 }
581     go ty1 (TyVarTy tv2) 
582       = do { lookup_res <- lookupTcTyVar tv2
583            ; case lookup_res of
584                Filled ty2   -> go ty1 ty2
585                Unfilled ds2 -> uUnfilledVar origin IsSwapped tv2 ds2 ty1 }
586
587         -- See Note [Expanding synonyms during unification]
588         --
589         -- Also NB that we recurse to 'go' so that we don't push a
590         -- new item on the origin stack. As a result if we have
591         --   type Foo = Int
592         -- and we try to unify  Foo ~ Bool
593         -- we'll end up saying "can't match Foo with Bool"
594         -- rather than "can't match "Int with Bool".  See Trac #4535.
595     go ty1 ty2
596       | Just ty1' <- tcView ty1 = go ty1' ty2
597       | Just ty2' <- tcView ty2 = go ty1  ty2'
598              
599         -- Functions (or predicate functions) just check the two parts
600     go (FunTy fun1 arg1) (FunTy fun2 arg2)
601       = do { co_l <- uType origin fun1 fun2
602            ; co_r <- uType origin arg1 arg2
603            ; return $ mkTcFunCo co_l co_r }
604
605         -- Always defer if a type synonym family (type function)
606         -- is involved.  (Data families behave rigidly.)
607     go ty1@(TyConApp tc1 _) ty2
608       | isSynFamilyTyCon tc1 = uType_defer origin ty1 ty2   
609     go ty1 ty2@(TyConApp tc2 _)
610       | isSynFamilyTyCon tc2 = uType_defer origin ty1 ty2   
611
612     go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
613       -- See Note [Mismatched type lists and application decomposition]
614       | tc1 == tc2, length tys1 == length tys2
615       = do { cos <- zipWithM (uType origin) tys1 tys2
616            ; return $ mkTcTyConAppCo tc1 cos }
617
618     go (LitTy m) ty@(LitTy n)
619       | m == n
620       = return $ mkTcReflCo ty
621
622         -- See Note [Care with type applications]
623         -- Do not decompose FunTy against App; 
624         -- it's often a type error, so leave it for the constraint solver
625     go (AppTy s1 t1) (AppTy s2 t2)
626       = go_app s1 t1 s2 t2
627
628     go (AppTy s1 t1) (TyConApp tc2 ts2)
629       | Just (ts2', t2') <- snocView ts2
630       = ASSERT( isDecomposableTyCon tc2 ) 
631         go_app s1 t1 (TyConApp tc2 ts2') t2'
632
633     go (TyConApp tc1 ts1) (AppTy s2 t2) 
634       | Just (ts1', t1') <- snocView ts1
635       = ASSERT( isDecomposableTyCon tc1 ) 
636         go_app (TyConApp tc1 ts1') t1' s2 t2 
637
638     go ty1 ty2
639       | tcIsForAllTy ty1 || tcIsForAllTy ty2 
640       = unifySigmaTy origin ty1 ty2
641
642         -- Anything else fails
643     go ty1 ty2 = uType_defer origin ty1 ty2 -- failWithMisMatch origin
644
645     ------------------
646     go_app s1 t1 s2 t2
647       = do { co_s <- uType_np origin s1 s2  -- See Note [Unifying AppTy]
648            ; co_t <- uType origin t1 t2        
649            ; return $ mkTcAppCo co_s co_t }
650
651 unifySigmaTy :: [EqOrigin] -> TcType -> TcType -> TcM TcCoercion
652 unifySigmaTy origin ty1 ty2
653   = do { let (tvs1, body1) = tcSplitForAllTys ty1
654              (tvs2, body2) = tcSplitForAllTys ty2
655
656        ; defer_or_continue (not (equalLength tvs1 tvs2)) $ do {
657          (subst1, skol_tvs) <- tcInstSkolTyVars tvs1
658                   -- Get location from monad, not from tvs1
659        ; let tys      = mkTyVarTys skol_tvs
660              phi1     = Type.substTy subst1                   body1
661              phi2     = Type.substTy (zipTopTvSubst tvs2 tys) body2
662              skol_info = UnifyForAllSkol skol_tvs phi1
663
664        ; (ev_binds, co) <- checkConstraints skol_info skol_tvs [] $
665                            uType origin phi1 phi2
666
667        ; return (foldr mkTcForAllCo (TcLetCo ev_binds co) skol_tvs) } }
668   where
669     defer_or_continue True  _ = uType_defer origin ty1 ty2
670     defer_or_continue False m = m
671 \end{code}
672
673 Note [Care with type applications]
674 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
675 Note: type applications need a bit of care!
676 They can match FunTy and TyConApp, so use splitAppTy_maybe
677 NB: we've already dealt with type variables and Notes,
678 so if one type is an App the other one jolly well better be too
679
680 Note [Unifying AppTy]
681 ~~~~~~~~~~~~~~~~~~~~~
682 Consider unifying  (m Int) ~ (IO Int) where m is a unification variable 
683 that is now bound to (say) (Bool ->).  Then we want to report 
684      "Can't unify (Bool -> Int) with (IO Int)
685 and not 
686      "Can't unify ((->) Bool) with IO"
687 That is why we use the "_np" variant of uType, which does not alter the error
688 message.
689
690 Note [Mismatched type lists and application decomposition]
691 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
692 When we find two TyConApps, you might think that the argument lists 
693 are guaranteed equal length.  But they aren't. Consider matching
694         w (T x) ~ Foo (T x y)
695 We do match (w ~ Foo) first, but in some circumstances we simply create
696 a deferred constraint; and then go ahead and match (T x ~ T x y).
697 This came up in Trac #3950.
698
699 So either 
700    (a) either we must check for identical argument kinds 
701        when decomposing applications,
702   
703    (b) or we must be prepared for ill-kinded unification sub-problems
704
705 Currently we adopt (b) since it seems more robust -- no need to maintain
706 a global invariant.
707
708 Note [Expanding synonyms during unification]
709 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
710 We expand synonyms during unification, but:
711  * We expand *after* the variable case so that we tend to unify
712    variables with un-expanded type synonym. This just makes it
713    more likely that the inferred types will mention type synonyms
714    understandable to the user
715
716  * We expand *before* the TyConApp case.  For example, if we have
717       type Phantom a = Int
718    and are unifying
719       Phantom Int ~ Phantom Char
720    it is *wrong* to unify Int and Char.
721
722 Note [Deferred Unification]
723 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
724 We may encounter a unification ty1 ~ ty2 that cannot be performed syntactically,
725 and yet its consistency is undetermined. Previously, there was no way to still
726 make it consistent. So a mismatch error was issued.
727
728 Now these unfications are deferred until constraint simplification, where type
729 family instances and given equations may (or may not) establish the consistency.
730 Deferred unifications are of the form
731                 F ... ~ ...
732 or              x ~ ...
733 where F is a type function and x is a type variable.
734 E.g.
735         id :: x ~ y => x -> y
736         id e = e
737
738 involves the unfication x = y. It is deferred until we bring into account the
739 context x ~ y to establish that it holds.
740
741 If available, we defer original types (rather than those where closed type
742 synonyms have already been expanded via tcCoreView).  This is, as usual, to
743 improve error messages.
744
745
746 %************************************************************************
747 %*                                                                      *
748                  uVar and friends
749 %*                                                                      *
750 %************************************************************************
751
752 @uVar@ is called when at least one of the types being unified is a
753 variable.  It does {\em not} assume that the variable is a fixed point
754 of the substitution; rather, notice that @uVar@ (defined below) nips
755 back into @uTys@ if it turns out that the variable is already bound.
756
757 \begin{code}
758 uUnfilledVar :: [EqOrigin]
759              -> SwapFlag
760              -> TcTyVar -> TcTyVarDetails       -- Tyvar 1
761              -> TcTauType                       -- Type 2
762              -> TcM TcCoercion
763 -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
764 --            It might be a skolem, or untouchable, or meta
765
766 uUnfilledVar origin swapped tv1 details1 (TyVarTy tv2)
767   | tv1 == tv2  -- Same type variable => no-op
768   = return (mkTcReflCo (mkTyVarTy tv1))
769
770   | otherwise  -- Distinct type variables
771   = do  { lookup2 <- lookupTcTyVar tv2
772         ; case lookup2 of
773             Filled ty2'       -> uUnfilledVar origin swapped tv1 details1 ty2' 
774             Unfilled details2 -> uUnfilledVars origin swapped tv1 details1 tv2 details2
775         }
776
777 uUnfilledVar origin swapped tv1 details1 non_var_ty2  -- ty2 is not a type variable
778   = case details1 of
779       MetaTv TauTv ref1 
780         -> do { mb_ty2' <- checkTauTvUpdate tv1 non_var_ty2
781               ; case mb_ty2' of
782                   Nothing   -> do { traceTc "Occ/kind defer" (ppr tv1); defer }
783                   Just ty2' -> updateMeta tv1 ref1 ty2'
784               }
785
786       _other -> do { traceTc "Skolem defer" (ppr tv1); defer }  -- Skolems of all sorts
787   where
788     defer | Just ty2' <- tcView non_var_ty2     -- Note [Avoid deferring]
789                                                 -- non_var_ty2 isn't expanded yet
790           = uUnfilledVar origin swapped tv1 details1 ty2'
791           | otherwise
792           = unSwap swapped (uType_defer origin) (mkTyVarTy tv1) non_var_ty2
793           -- Occurs check or an untouchable: just defer
794           -- NB: occurs check isn't necessarily fatal: 
795           --     eg tv1 occured in type family parameter
796
797 ----------------
798 uUnfilledVars :: [EqOrigin]
799               -> SwapFlag
800               -> TcTyVar -> TcTyVarDetails      -- Tyvar 1
801               -> TcTyVar -> TcTyVarDetails      -- Tyvar 2
802               -> TcM TcCoercion
803 -- Invarant: The type variables are distinct,
804 --           Neither is filled in yet
805
806 uUnfilledVars origin swapped tv1 details1 tv2 details2
807   = do { traceTc "uUnfilledVars" (    text "trying to unify" <+> ppr k1
808                                   <+> text "with"            <+> ppr k2)
809        ; let ctxt = mkKindErrorCtxt ty1 ty2 k1 k2
810        ; sub_kind <- addErrCtxtM ctxt $ unifyKind k1 k2
811
812        ; case (sub_kind, details1, details2) of
813            -- k1 < k2, so update tv2
814            (LT, _, MetaTv _ ref2) -> updateMeta tv2 ref2 ty1
815
816            -- k2 < k1, so update tv1
817            (GT, MetaTv _ ref1, _) -> updateMeta tv1 ref1 ty2
818
819            -- k1 = k2, so we are free to update either way
820            (EQ, MetaTv i1 ref1, MetaTv i2 ref2)
821                 | nicer_to_update_tv1 i1 i2 -> updateMeta tv1 ref1 ty2
822                 | otherwise                 -> updateMeta tv2 ref2 ty1
823            (EQ, MetaTv _ ref1, _) -> updateMeta tv1 ref1 ty2
824            (EQ, _, MetaTv _ ref2) -> updateMeta tv2 ref2 ty1
825
826            -- Can't do it in-place, so defer
827            -- This happens for skolems of all sorts
828            (_, _, _) -> unSwap swapped (uType_defer origin) ty1 ty2 } 
829   where
830     k1       = tyVarKind tv1
831     k2       = tyVarKind tv2
832     ty1      = mkTyVarTy tv1
833     ty2      = mkTyVarTy tv2
834
835     nicer_to_update_tv1 _     SigTv = True
836     nicer_to_update_tv1 SigTv _     = False
837     nicer_to_update_tv1 _         _ = isSystemName (Var.varName tv1)
838         -- Try not to update SigTvs; and try to update sys-y type
839         -- variables in preference to ones gotten (say) by
840         -- instantiating a polymorphic function with a user-written
841         -- type sig
842
843 ----------------
844 checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
845 --    (checkTauTvUpdate tv ty)
846 -- We are about to update the TauTv tv with ty.
847 -- Check (a) that tv doesn't occur in ty (occurs check)
848 --       (b) that kind(ty) is a sub-kind of kind(tv)
849 --       (c) that ty does not contain any type families, see Note [Type family sharing]
850 -- 
851 -- We have two possible outcomes:
852 -- (1) Return the type to update the type variable with, 
853 --        [we know the update is ok]
854 -- (2) Return Nothing,
855 --        [the update might be dodgy]
856 --
857 -- Note that "Nothing" does not mean "definite error".  For example
858 --   type family F a
859 --   type instance F Int = Int
860 -- consider
861 --   a ~ F a
862 -- This is perfectly reasonable, if we later get a ~ Int.  For now, though,
863 -- we return Nothing, leaving it to the later constraint simplifier to
864 -- sort matters out.
865
866 checkTauTvUpdate tv ty
867   = do { ty' <- zonkTcType ty
868        ; let k2 = typeKind ty'
869        ; k1 <- zonkTcKind (tyVarKind tv)
870        ; let ctxt = mkKindErrorCtxt (mkTyVarTy tv) ty' k1 k2
871        ; sub_k <- addErrCtxtM ctxt $
872                   unifyKind (tyVarKind tv) (typeKind ty')
873
874        ; case sub_k of
875            LT -> return Nothing
876            _  -> return (ok ty') }
877   where 
878     ok :: TcType -> Maybe TcType 
879     -- Checks that tv does not occur in the arg type
880     -- expanding type synonyms where necessary to make this so
881     -- eg type Phantom a = Bool
882     --     ok (tv -> Int)         = Nothing
883     --     ok (x -> Int)          = Just (x -> Int)
884     --     ok (Phantom tv -> Int) = Just (Bool -> Int)
885     ok (TyVarTy tv') | not (tv == tv') = Just (TyVarTy tv') 
886     ok this_ty@(TyConApp tc tys) 
887       | not (isSynFamilyTyCon tc), Just tys' <- allMaybes (map ok tys) 
888       = Just (TyConApp tc tys') 
889       | isSynTyCon tc, Just ty_expanded <- tcView this_ty
890       = ok ty_expanded -- See Note [Type synonyms and the occur check] 
891     ok ty@(LitTy {}) = Just ty
892     ok (FunTy arg res) | Just arg' <- ok arg, Just res' <- ok res
893                        = Just (FunTy arg' res') 
894     ok (AppTy fun arg) | Just fun' <- ok fun, Just arg' <- ok arg 
895                        = Just (AppTy fun' arg') 
896     ok (ForAllTy tv1 ty1) | Just ty1' <- ok ty1 = Just (ForAllTy tv1 ty1') 
897     -- Fall-through 
898     ok _ty = Nothing 
899 \end{code}
900
901 Note [Avoid deferring]
902 ~~~~~~~~~~~~~~~~~~~~~~
903 We try to avoid creating deferred constraints only for efficiency.
904 Example (Trac #4917)
905        a ~ Const a b
906 where type Const a b = a.  We can solve this immediately, even when
907 'a' is a skolem, just by expanding the synonym.
908
909 Note [Type synonyms and the occur check]
910 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
911 Generally speaking we try to update a variable with type synonyms not
912 expanded, which improves later error messages, unless looking
913 inside a type synonym may help resolve a spurious occurs check
914 error. Consider:
915           type A a = ()
916
917           f :: (A a -> a -> ()) -> ()
918           f = \ _ -> ()
919
920           x :: ()
921           x = f (\ x p -> p x)
922
923 We will eventually get a constraint of the form t ~ A t. The ok function above will 
924 properly expand the type (A t) to just (), which is ok to be unified with t. If we had
925 unified with the original type A t, we would lead the type checker into an infinite loop. 
926
927 Hence, if the occurs check fails for a type synonym application, then (and *only* then), 
928 the ok function expands the synonym to detect opportunities for occurs check success using
929 the underlying definition of the type synonym. 
930
931 The same applies later on in the constraint interaction code; see TcInteract, 
932 function @occ_check_ok@. 
933
934
935 Note [Type family sharing]
936 ~~~~~~~~~~~~~~ 
937 We must avoid eagerly unifying type variables to types that contain function symbols, 
938 because this may lead to loss of sharing, and in turn, in very poor performance of the
939 constraint simplifier. Assume that we have a wanted constraint: 
940
941   m1 ~ [F m2], 
942   m2 ~ [F m3], 
943   m3 ~ [F m4], 
944   D m1, 
945   D m2, 
946   D m3 
947
948 where D is some type class. If we eagerly unify m1 := [F m2], m2 := [F m3], m3 := [F m2], 
949 then, after zonking, our constraint simplifier will be faced with the following wanted 
950 constraint: 
951
952   D [F [F [F m4]]], 
953   D [F [F m4]], 
954   D [F m4] 
955
956 which has to be flattened by the constraint solver. However, because the sharing is lost, 
957 an polynomially larger number of flatten skolems will be created and the constraint sets 
958 we are working with will be polynomially larger. 
959
960 Instead, if we defer the unifications m1 := [F m2], etc. we will only be generating three 
961 flatten skolems, which is the maximum possible sharing arising from the original constraint. 
962
963 \begin{code}
964 data LookupTyVarResult  -- The result of a lookupTcTyVar call
965   = Unfilled TcTyVarDetails     -- SkolemTv or virgin MetaTv
966   | Filled   TcType
967
968 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
969 lookupTcTyVar tyvar 
970   | MetaTv _ ref <- details
971   = do { meta_details <- readMutVar ref
972        ; case meta_details of
973            Indirect ty -> return (Filled ty)
974            Flexi -> do { is_untch <- isUntouchable tyvar
975                        ; let    -- Note [Unifying untouchables]
976                              ret_details | is_untch  = vanillaSkolemTv
977                                          | otherwise = details
978                        ; return (Unfilled ret_details) } }
979   | otherwise
980   = return (Unfilled details)
981   where
982     details = ASSERT2( isTcTyVar tyvar, ppr tyvar )
983               tcTyVarDetails tyvar
984
985 updateMeta :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM TcCoercion
986 updateMeta tv1 ref1 ty2
987   = do { writeMetaTyVarRef tv1 ref1 ty2
988        ; return (mkTcReflCo ty2) }
989 \end{code}
990
991 Note [Unifying untouchables]
992 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
993 We treat an untouchable type variable as if it was a skolem.  That
994 ensures it won't unify with anything.  It's a slight had, because
995 we return a made-up TcTyVarDetails, but I think it works smoothly.
996
997
998 %************************************************************************
999 %*                                                                      *
1000         Errors and contexts
1001 %*                                                                      *
1002 %************************************************************************
1003
1004 \begin{code}
1005 pushOrigin :: TcType -> TcType -> [EqOrigin] -> [EqOrigin]
1006 pushOrigin ty_act ty_exp origin
1007   = UnifyOrigin { uo_actual = ty_act, uo_expected = ty_exp } : origin
1008 \end{code}
1009
1010
1011 -----------------------------------------
1012         UNUSED FOR NOW
1013 -----------------------------------------
1014
1015 ----------------
1016 ----------------
1017 -- If an error happens we try to figure out whether the function
1018 -- function has been given too many or too few arguments, and say so.
1019 addSubCtxt :: InstOrigin -> TcType -> TcType -> TcM a -> TcM a
1020 addSubCtxt orig actual_res_ty expected_res_ty thing_inside
1021   = addErrCtxtM mk_err thing_inside
1022   where
1023     mk_err tidy_env
1024       = do { exp_ty' <- zonkTcType expected_res_ty
1025            ; act_ty' <- zonkTcType actual_res_ty
1026            ; let (env1, exp_ty'') = tidyOpenType tidy_env exp_ty'
1027                  (env2, act_ty'') = tidyOpenType env1     act_ty'
1028                  (exp_args, _)    = tcSplitFunTys exp_ty''
1029                  (act_args, _)    = tcSplitFunTys act_ty''
1030
1031                  len_act_args     = length act_args
1032                  len_exp_args     = length exp_args
1033
1034                  message = case orig of
1035                              OccurrenceOf fun
1036                                   | len_exp_args < len_act_args -> wrongArgsCtxt "too few"  fun
1037                                   | len_exp_args > len_act_args -> wrongArgsCtxt "too many" fun
1038                              _ -> mkExpectedActualMsg act_ty'' exp_ty''
1039            ; return (env2, message) }
1040
1041
1042 %************************************************************************
1043 %*                                                                      *
1044                 Kind unification
1045 %*                                                                      *
1046 %************************************************************************
1047
1048 Unifying kinds is much, much simpler than unifying types.
1049
1050 One small wrinkle is that as far as the user is concerned, types of kind
1051 Constraint should only be allowed to occur where we expect *exactly* that kind.
1052 We SHOULD NOT allow a type of kind fact to appear in a position expecting
1053 one of argTypeKind or openTypeKind.
1054
1055 The situation is different in the core of the compiler, where we are perfectly
1056 happy to have types of kind Constraint on either end of an arrow.
1057
1058 \begin{code}
1059 matchExpectedFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
1060 -- Like unifyFunTy, but does not fail; instead just returns Nothing
1061
1062 matchExpectedFunKind (TyVarTy kvar) = do
1063     maybe_kind <- readMetaTyVar kvar
1064     case maybe_kind of
1065       Indirect fun_kind -> matchExpectedFunKind fun_kind
1066       Flexi ->
1067           do { arg_kind <- newMetaKindVar
1068              ; res_kind <- newMetaKindVar
1069              ; writeMetaTyVar kvar (mkArrowKind arg_kind res_kind)
1070              ; return (Just (arg_kind,res_kind)) }
1071
1072 matchExpectedFunKind (FunTy arg_kind res_kind) = return (Just (arg_kind,res_kind))
1073 matchExpectedFunKind _                         = return Nothing
1074
1075 -----------------  
1076 unifyKind :: TcKind           -- k1 (actual)
1077           -> TcKind           -- k2 (expected)
1078           -> TcM Ordering     -- Returns the relation between the kinds
1079                               -- LT <=> k1 is a sub-kind of k2
1080
1081 -- unifyKind deals with the top-level sub-kinding story
1082 -- but recurses into the simpler unifyKindEq for any sub-terms
1083 -- The sub-kinding stuff only applies at top level
1084
1085 unifyKind (TyVarTy kv1) k2 = uKVar False unifyKind EQ kv1 k2
1086 unifyKind k1 (TyVarTy kv2) = uKVar True  unifyKind EQ kv2 k1
1087
1088 unifyKind k1 k2       -- See Note [Expanding synonyms during unification]
1089   | Just k1' <- tcView k1 = unifyKind k1' k2
1090   | Just k2' <- tcView k2 = unifyKind k1  k2'
1091
1092 unifyKind k1@(TyConApp kc1 []) k2@(TyConApp kc2 [])
1093   | kc1 == kc2               = return EQ
1094   | kc1 `tcIsSubKindCon` kc2 = return LT
1095   | kc2 `tcIsSubKindCon` kc1 = return GT
1096   | otherwise                = unifyKindMisMatch k1 k2
1097
1098 unifyKind k1 k2 = do { unifyKindEq k1 k2; return EQ }
1099   -- In all other cases, let unifyKindEq do the work
1100
1101 uKVar :: Bool -> (TcKind -> TcKind -> TcM a) -> a
1102       -> MetaKindVar -> TcKind -> TcM a
1103 uKVar isFlipped unify_kind eq_res kv1 k2
1104   | isTcTyVar kv1, isMetaTyVar kv1       -- See Note [Unifying kind variables]
1105   = do  { mb_k1 <- readMetaTyVar kv1
1106         ; case mb_k1 of
1107             Flexi -> do { uUnboundKVar kv1 k2; return eq_res }
1108             Indirect k1 -> if isFlipped then unify_kind k2 k1
1109                                         else unify_kind k1 k2 }
1110   | TyVarTy kv2 <- k2, kv1 == kv2 
1111   = return eq_res
1112
1113   | TyVarTy kv2 <- k2, isTcTyVar kv2, isMetaTyVar kv2
1114   = uKVar (not isFlipped) unify_kind eq_res kv2 (TyVarTy kv1)
1115
1116   | otherwise = if isFlipped 
1117                 then unifyKindMisMatch k2 (TyVarTy kv1)
1118                 else unifyKindMisMatch (TyVarTy kv1) k2
1119
1120 {- Note [Unifying kind variables]
1121 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1122 Rather hackily, kind variables can be TyVars not just TcTyVars.
1123 Main reason is in 
1124    data instance T (D (x :: k)) = ...con-decls...
1125 Here we bring into scope a kind variable 'k', and use it in the 
1126 con-decls.  BUT the con-decls will be finished and frozen, and
1127 are not amenable to subsequent substitution, so it makes sense
1128 to have the *final* kind-variable (a KindVar, not a TcKindVar) in 
1129 scope.  So at least during kind unification we can encounter a
1130 KindVar. 
1131
1132 Hence the isTcTyVar tests before using isMetaTyVar.
1133 -}
1134
1135 ---------------------------
1136 unifyKindEq :: TcKind -> TcKind -> TcM ()
1137 unifyKindEq (TyVarTy kv1) k2 = uKVar False unifyKindEq () kv1 k2
1138 unifyKindEq k1 (TyVarTy kv2) = uKVar True  unifyKindEq () kv2 k1
1139
1140 unifyKindEq (FunTy a1 r1) (FunTy a2 r2)
1141   = do { unifyKindEq a1 a2; unifyKindEq r1 r2 }
1142   
1143 unifyKindEq (TyConApp kc1 k1s) (TyConApp kc2 k2s)
1144   | kc1 == kc2
1145   = ASSERT (length k1s == length k2s)
1146        -- Should succeed since the kind constructors are the same, 
1147        -- and the kinds are sort-checked, thus fully applied
1148     zipWithM_ unifyKindEq k1s k2s
1149
1150 unifyKindEq k1 k2 = unifyKindMisMatch k1 k2
1151
1152 ----------------
1153 uUnboundKVar :: MetaKindVar -> TcKind -> TcM ()
1154 uUnboundKVar kv1 k2@(TyVarTy kv2)
1155   | kv1 == kv2 = return ()
1156   | isTcTyVar kv2, isMetaTyVar kv2   -- Distinct kind variables
1157   = do  { mb_k2 <- readMetaTyVar kv2
1158         ; case mb_k2 of
1159             Indirect k2 -> uUnboundKVar kv1 k2
1160             Flexi -> writeMetaTyVar kv1 k2 }
1161   | otherwise = writeMetaTyVar kv1 k2
1162
1163 uUnboundKVar kv1 non_var_k2
1164   = do  { k2' <- zonkTcKind non_var_k2
1165         ; kindOccurCheck kv1 k2'
1166         ; let k2'' = defaultKind k2'
1167                 -- MetaKindVars must be bound only to simple kinds
1168         ; writeMetaTyVar kv1 k2'' }
1169
1170 ----------------
1171 kindOccurCheck :: TyVar -> Type -> TcM ()
1172 kindOccurCheck kv1 k2   -- k2 is zonked
1173   = if elemVarSet kv1 (tyVarsOfType k2)
1174     then failWithTc (kindOccurCheckErr kv1 k2)
1175     else return ()
1176
1177 mkKindErrorCtxt :: Type -> Type -> Kind -> Kind -> TidyEnv -> TcM (TidyEnv, SDoc)
1178 mkKindErrorCtxt ty1 ty2 k1 k2 env0
1179   = let (env1, ty1') = tidyOpenType env0 ty1
1180         (env2, ty2') = tidyOpenType env1 ty2
1181         (env3, k1' ) = tidyOpenKind env2 k1
1182         (env4, k2' ) = tidyOpenKind env3 k2
1183     in do ty1 <- zonkTcType ty1'
1184           ty2 <- zonkTcType ty2'
1185           k1  <- zonkTcKind k1'
1186           k2  <- zonkTcKind k2'
1187           return (env4, 
1188                   vcat [ ptext (sLit "Kind incompatibility when matching types:")
1189                        , nest 2 (vcat [ ppr ty1 <+> dcolon <+> ppr k1
1190                                       , ppr ty2 <+> dcolon <+> ppr k2 ]) ])
1191
1192 unifyKindMisMatch :: TcKind -> TcKind -> TcM a
1193 unifyKindMisMatch ki1 ki2 = do
1194     ki1' <- zonkTcKind ki1
1195     ki2' <- zonkTcKind ki2
1196     let msg = hang (ptext (sLit "Couldn't match kind"))
1197               2 (sep [quotes (ppr ki1'),
1198                       ptext (sLit "against"),
1199                       quotes (ppr ki2')])
1200     failWithTc msg
1201
1202 ----------------
1203 kindOccurCheckErr :: Var -> Type -> SDoc
1204 kindOccurCheckErr tyvar ty
1205   = hang (ptext (sLit "Occurs check: cannot construct the infinite kind:"))
1206        2 (sep [ppr tyvar, char '=', ppr ty])
1207 \end{code}