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