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