2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section{Type subsumption and unification}
8 -- Full-blown subsumption
9 tcSubOff, tcSubExp, tcGen,
10 checkSigTyVars, checkSigTyVarsWrt, sigCtxt, findGlobals,
12 -- Various unifications
13 unifyTauTy, unifyTauTyList, unifyTauTyLists,
14 unifyKind, unifyKinds, unifyFunKind,
17 --------------------------------
19 Expected(..), newHole, readExpectedType,
20 zapExpectedType, zapExpectedTo, zapExpectedBranches,
21 subFunTys, unifyFunTy,
22 zapToListTy, unifyListTy,
23 zapToPArrTy, unifyPArrTy,
24 zapToTupleTy, unifyTupleTy
28 #include "HsVersions.h"
31 import HsSyn ( HsExpr(..) )
32 import TcHsSyn ( mkHsLet, mkHsDictLam,
33 ExprCoFn, idCoercion, isIdCoercion, mkCoercion, (<.>), (<$>) )
34 import TypeRep ( Type(..), PredType(..), TyNote(..) )
36 import TcRnMonad -- TcType, amongst others
37 import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
38 TcTyVarSet, TcThetaType, TyVarDetails(SigTv),
39 isTauTy, isSigmaTy, mkFunTys, mkTyConApp,
40 tcSplitAppTy_maybe, tcSplitTyConApp_maybe,
41 tcGetTyVar_maybe, tcGetTyVar,
42 mkFunTy, tyVarsOfType, mkPhiTy,
43 typeKind, tcSplitFunTy_maybe, mkForAllTys,
44 isSkolemTyVar, isUserTyVar,
45 tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
46 allDistinctTyVars, pprType )
47 import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind,
48 openTypeKind, liftedTypeKind, mkArrowKind,
49 isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
50 isSubKind, pprKind, splitKindFunTys )
51 import Inst ( newDicts, instToId, tcInstCall )
52 import TcMType ( getTcTyVar, putTcTyVar, tcInstType, newKindVar,
53 newTyVarTy, newTyVarTys, zonkTcKind,
54 zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV,
55 readKindVar,writeKindVar )
56 import TcSimplify ( tcSimplifyCheck )
57 import TysWiredIn ( listTyCon, parrTyCon, tupleTyCon )
58 import TcEnv ( tcGetGlobalTyVars, findGlobals )
59 import TyCon ( TyCon, tyConArity, isTupleTyCon, tupleTyConBoxity )
60 import Id ( Id, mkSysLocal )
61 import Var ( Var, varName, tyVarKind )
62 import VarSet ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems )
64 import Name ( isSystemName )
65 import ErrUtils ( Message )
66 import SrcLoc ( noLoc )
67 import BasicTypes ( Boxity, Arity, isBoxed )
68 import Util ( equalLength, lengthExceeds, notNull )
74 * A hole is always filled in with an ordinary type, not another hole.
76 %************************************************************************
78 \subsection{'hole' type variables}
80 %************************************************************************
83 data Expected ty = Infer (TcRef ty) -- The hole to fill in for type inference
84 | Check ty -- The type to check during type checking
86 newHole :: TcM (TcRef ty)
87 newHole = newMutVar (error "Empty hole in typechecker")
89 readExpectedType :: Expected ty -> TcM ty
90 readExpectedType (Infer hole) = readMutVar hole
91 readExpectedType (Check ty) = returnM ty
93 zapExpectedType :: Expected TcType -> Kind -> TcM TcTauType
94 -- In the inference case, ensure we have a monotype
95 -- (including an unboxed tuple)
96 zapExpectedType (Infer hole) kind
97 = do { ty <- newTyVarTy kind ;
101 zapExpectedType (Check ty) kind
102 | typeKind ty `isSubKind` kind = return ty
103 | otherwise = do { ty1 <- newTyVarTy kind
106 -- The unify is to ensure that 'ty' has the desired kind
107 -- For example, in (case e of r -> b) we push an OpenTypeKind
110 zapExpectedTo :: Expected TcType -> TcTauType -> TcM ()
111 zapExpectedTo (Infer hole) ty2 = writeMutVar hole ty2
112 zapExpectedTo (Check ty1) ty2 = unifyTauTy ty1 ty2
114 zapExpectedBranches :: [a] -> Expected TcType -> TcM (Expected TcType)
115 -- Zap the expected type to a monotype if there is more than one branch
116 zapExpectedBranches branches exp_ty
117 | lengthExceeds branches 1 = zapExpectedType exp_ty openTypeKind `thenM` \ exp_ty' ->
118 return (Check exp_ty')
119 | otherwise = returnM exp_ty
121 instance Outputable ty => Outputable (Expected ty) where
122 ppr (Check ty) = ptext SLIT("Expected type") <+> ppr ty
123 ppr (Infer hole) = ptext SLIT("Inferring type")
127 %************************************************************************
129 \subsection[Unify-fun]{@unifyFunTy@}
131 %************************************************************************
133 @subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
134 creation of type variables.
136 * subFunTy is used when we might be faced with a "hole" type variable,
137 in which case we should create two new holes.
139 * unifyFunTy is used when we expect to encounter only "ordinary"
140 type variables, so we should create new ordinary type variables
144 -> Expected TcRhoType -- Fail if ty isn't a function type
145 -> ([(pat, Expected TcRhoType)] -> Expected TcRhoType -> TcM a)
148 subFunTys pats (Infer hole) thing_inside
149 = -- This is the interesting case
150 mapM new_pat_hole pats `thenM` \ pats_w_holes ->
151 newHole `thenM` \ res_hole ->
154 thing_inside pats_w_holes (Infer res_hole) `thenM` \ answer ->
156 -- Extract the answers
157 mapM read_pat_hole pats_w_holes `thenM` \ arg_tys ->
158 readMutVar res_hole `thenM` \ res_ty ->
160 -- Write the answer into the incoming hole
161 writeMutVar hole (mkFunTys arg_tys res_ty) `thenM_`
163 -- And return the answer
166 new_pat_hole pat = newHole `thenM` \ hole -> return (pat, Infer hole)
167 read_pat_hole (pat, Infer hole) = readMutVar hole
169 subFunTys pats (Check ty) thing_inside
170 = go pats ty `thenM` \ (pats_w_tys, res_ty) ->
171 thing_inside pats_w_tys res_ty
173 go [] ty = return ([], Check ty)
174 go (pat:pats) ty = unifyFunTy ty `thenM` \ (arg,res) ->
175 go pats res `thenM` \ (pats_w_tys, final_res) ->
176 return ((pat, Check arg) : pats_w_tys, final_res)
178 unifyFunTy :: TcRhoType -- Fail if ty isn't a function type
179 -> TcM (TcType, TcType) -- otherwise return arg and result types
181 unifyFunTy ty@(TyVarTy tyvar)
182 = getTcTyVar tyvar `thenM` \ maybe_ty ->
184 Just ty' -> unifyFunTy ty'
185 Nothing -> unify_fun_ty_help ty
188 = case tcSplitFunTy_maybe ty of
189 Just arg_and_res -> returnM arg_and_res
190 Nothing -> unify_fun_ty_help ty
192 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
193 = newTyVarTy argTypeKind `thenM` \ arg ->
194 newTyVarTy openTypeKind `thenM` \ res ->
195 unifyTauTy ty (mkFunTy arg res) `thenM_`
200 ----------------------
201 zapToListTy, zapToPArrTy :: Expected TcType -- expected list type
202 -> TcM TcType -- list element type
203 unifyListTy, unifyPArrTy :: TcType -> TcM TcType
204 zapToListTy = zapToXTy listTyCon
205 unifyListTy = unifyXTy listTyCon
206 zapToPArrTy = zapToXTy parrTyCon
207 unifyPArrTy = unifyXTy parrTyCon
209 ----------------------
210 zapToXTy :: TyCon -- T :: *->*
211 -> Expected TcType -- Expected type (T a)
212 -> TcM TcType -- Element type, a
214 zapToXTy tc (Check ty) = unifyXTy tc ty
215 zapToXTy tc (Infer hole) = do { elt_ty <- newTyVarTy liftedTypeKind ;
216 writeMutVar hole (mkTyConApp tc [elt_ty]) ;
219 ----------------------
220 unifyXTy :: TyCon -> TcType -> TcM TcType
221 unifyXTy tc ty@(TyVarTy tyvar)
222 = getTcTyVar tyvar `thenM` \ maybe_ty ->
224 Just ty' -> unifyXTy tc ty'
225 other -> unify_x_ty_help tc ty
228 = case tcSplitTyConApp_maybe ty of
229 Just (tycon, [arg_ty]) | tycon == tc -> returnM arg_ty
230 other -> unify_x_ty_help tc ty
232 unify_x_ty_help tc ty -- Revert to ordinary unification
233 = newTyVarTy liftedTypeKind `thenM` \ elt_ty ->
234 unifyTauTy ty (mkTyConApp tc [elt_ty]) `thenM_`
239 ----------------------
240 zapToTupleTy :: Boxity -> Arity -> Expected TcType -> TcM [TcType]
241 zapToTupleTy boxity arity (Check ty) = unifyTupleTy boxity arity ty
242 zapToTupleTy boxity arity (Infer hole) = do { (tup_ty, arg_tys) <- new_tuple_ty boxity arity ;
243 writeMutVar hole tup_ty ;
246 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
247 = getTcTyVar tyvar `thenM` \ maybe_ty ->
249 Just ty' -> unifyTupleTy boxity arity ty'
250 other -> unify_tuple_ty_help boxity arity ty
252 unifyTupleTy boxity arity ty
253 = case tcSplitTyConApp_maybe ty of
254 Just (tycon, arg_tys)
256 && tyConArity tycon == arity
257 && tupleTyConBoxity tycon == boxity
259 other -> unify_tuple_ty_help boxity arity ty
261 unify_tuple_ty_help boxity arity ty
262 = new_tuple_ty boxity arity `thenM` \ (tup_ty, arg_tys) ->
263 unifyTauTy ty tup_ty `thenM_`
266 new_tuple_ty boxity arity
267 = newTyVarTys arity kind `thenM` \ arg_tys ->
268 return (mkTyConApp tup_tc arg_tys, arg_tys)
270 tup_tc = tupleTyCon boxity arity
271 kind | isBoxed boxity = liftedTypeKind
272 | otherwise = argTypeKind -- Components of an unboxed tuple
273 -- can be unboxed, but not unboxed tuples
277 %************************************************************************
279 \subsection{Subsumption}
281 %************************************************************************
283 All the tcSub calls have the form
285 tcSub expected_ty offered_ty
287 offered_ty <= expected_ty
289 That is, that a value of type offered_ty is acceptable in
290 a place expecting a value of type expected_ty.
292 It returns a coercion function
293 co_fn :: offered_ty -> expected_ty
294 which takes an HsExpr of type offered_ty into one of type
298 tcSubExp :: Expected TcRhoType -> TcRhoType -> TcM ExprCoFn
299 tcSubOff :: TcSigmaType -> Expected TcSigmaType -> TcM ExprCoFn
302 These two check for holes
305 tcSubExp expected_ty offered_ty
306 = traceTc (text "tcSubExp" <+> (ppr expected_ty $$ ppr offered_ty)) `thenM_`
307 checkHole expected_ty offered_ty tcSub
309 tcSubOff expected_ty offered_ty
310 = checkHole offered_ty expected_ty (\ off exp -> tcSub exp off)
312 -- checkHole looks for a hole in its first arg;
313 -- If so, and it is uninstantiated, it fills in the hole
314 -- with its second arg
315 -- Otherwise it calls thing_inside, passing the two args, looking
316 -- through any instantiated hole
318 checkHole (Infer hole) other_ty thing_inside
319 = do { writeMutVar hole other_ty; return idCoercion }
321 checkHole (Check ty) other_ty thing_inside
322 = thing_inside ty other_ty
325 No holes expected now. Add some error-check context info.
328 tcSub :: TcSigmaType -> TcSigmaType -> TcM ExprCoFn -- Locally used only
329 tcSub expected_ty actual_ty
330 = traceTc (text "tcSub" <+> details) `thenM_`
331 addErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
332 (tc_sub expected_ty expected_ty actual_ty actual_ty)
334 details = vcat [text "Expected:" <+> ppr expected_ty,
335 text "Actual: " <+> ppr actual_ty]
338 tc_sub carries the types before and after expanding type synonyms
341 tc_sub :: TcSigmaType -- expected_ty, before expanding synonyms
342 -> TcSigmaType -- ..and after
343 -> TcSigmaType -- actual_ty, before
344 -> TcSigmaType -- ..and after
347 -----------------------------------
349 tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty act_ty
350 tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty
352 -----------------------------------
353 -- Generalisation case
354 -- actual_ty: d:Eq b => b->b
355 -- expected_ty: forall a. Ord a => a->a
356 -- co_fn e /\a. \d2:Ord a. let d = eqFromOrd d2 in e
358 -- It is essential to do this *before* the specialisation case
359 -- Example: f :: (Eq a => a->a) -> ...
360 -- g :: Ord b => b->b
363 tc_sub exp_sty expected_ty act_sty actual_ty
364 | isSigmaTy expected_ty
365 = tcGen expected_ty (tyVarsOfType actual_ty) (
366 -- It's really important to check for escape wrt the free vars of
367 -- both expected_ty *and* actual_ty
368 \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
369 ) `thenM` \ (gen_fn, co_fn) ->
370 returnM (gen_fn <.> co_fn)
372 -----------------------------------
373 -- Specialisation case:
374 -- actual_ty: forall a. Ord a => a->a
375 -- expected_ty: Int -> Int
376 -- co_fn e = e Int dOrdInt
378 tc_sub exp_sty expected_ty act_sty actual_ty
379 | isSigmaTy actual_ty
380 = tcInstCall Rank2Origin actual_ty `thenM` \ (inst_fn, body_ty) ->
381 tc_sub exp_sty expected_ty body_ty body_ty `thenM` \ co_fn ->
382 returnM (co_fn <.> inst_fn)
384 -----------------------------------
387 tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
388 = tcSub_fun exp_arg exp_res act_arg act_res
390 -----------------------------------
391 -- Type variable meets function: imitate
393 -- NB 1: we can't just unify the type variable with the type
394 -- because the type might not be a tau-type, and we aren't
395 -- allowed to instantiate an ordinary type variable with
398 -- NB 2: can we short-cut to an error case?
399 -- when the arg/res is not a tau-type?
400 -- NO! e.g. f :: ((forall a. a->a) -> Int) -> Int
402 -- is perfectly fine, because we can instantiat f's type to a monotype
404 -- However, we get can get jolly unhelpful error messages.
405 -- e.g. foo = id runST
407 -- Inferred type is less polymorphic than expected
408 -- Quantified type variable `s' escapes
409 -- Expected type: ST s a -> t
410 -- Inferred type: (forall s1. ST s1 a) -> a
411 -- In the first argument of `id', namely `runST'
412 -- In a right-hand side of function `foo': id runST
414 -- I'm not quite sure what to do about this!
416 tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv)
417 = getTcTyVar tv `thenM` \ maybe_ty ->
419 Just ty -> tc_sub exp_sty exp_ty ty ty
420 Nothing -> imitateFun tv exp_sty `thenM` \ (act_arg, act_res) ->
421 tcSub_fun exp_arg exp_res act_arg act_res
423 tc_sub _ (TyVarTy tv) act_sty act_ty@(FunTy act_arg act_res)
424 = getTcTyVar tv `thenM` \ maybe_ty ->
426 Just ty -> tc_sub ty ty act_sty act_ty
427 Nothing -> imitateFun tv act_sty `thenM` \ (exp_arg, exp_res) ->
428 tcSub_fun exp_arg exp_res act_arg act_res
430 -----------------------------------
432 -- If none of the above match, we revert to the plain unifier
433 tc_sub exp_sty expected_ty act_sty actual_ty
434 = uTys exp_sty expected_ty act_sty actual_ty `thenM_`
438 %************************************************************************
440 \subsection{Functions}
442 %************************************************************************
445 tcSub_fun exp_arg exp_res act_arg act_res
446 = tc_sub act_arg act_arg exp_arg exp_arg `thenM` \ co_fn_arg ->
447 tc_sub exp_res exp_res act_res act_res `thenM` \ co_fn_res ->
448 newUnique `thenM` \ uniq ->
450 -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
451 -- co_fn_res :: HsExpr act_res -> HsExpr exp_res
452 -- co_fn :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
453 arg_id = mkSysLocal FSLIT("sub") uniq exp_arg
454 coercion | isIdCoercion co_fn_arg,
455 isIdCoercion co_fn_res = idCoercion
456 | otherwise = mkCoercion co_fn
458 co_fn e = DictLam [arg_id]
459 (noLoc (co_fn_res <$> (HsApp (noLoc e) (noLoc (co_fn_arg <$> HsVar arg_id)))))
460 -- Slight hack; using a "DictLam" to get an ordinary simple lambda
461 -- HsVar arg_id :: HsExpr exp_arg
462 -- co_fn_arg $it :: HsExpr act_arg
463 -- HsApp e $it :: HsExpr act_res
464 -- co_fn_res $it :: HsExpr exp_res
468 imitateFun :: TcTyVar -> TcType -> TcM (TcType, TcType)
470 = -- NB: tv is an *ordinary* tyvar and so are the new ones
472 -- Check that tv isn't a type-signature type variable
473 -- (This would be found later in checkSigTyVars, but
474 -- we get a better error message if we do it here.)
475 checkM (not (isSkolemTyVar tv))
476 (failWithTcM (unifyWithSigErr tv ty)) `thenM_`
478 newTyVarTy argTypeKind `thenM` \ arg ->
479 newTyVarTy openTypeKind `thenM` \ res ->
480 putTcTyVar tv (mkFunTy arg res) `thenM_`
485 %************************************************************************
487 \subsection{Generalisation}
489 %************************************************************************
492 tcGen :: TcSigmaType -- expected_ty
493 -> TcTyVarSet -- Extra tyvars that the universally
494 -- quantified tyvars of expected_ty
495 -- must not be unified
496 -> (TcRhoType -> TcM result) -- spec_ty
497 -> TcM (ExprCoFn, result)
498 -- The expression has type: spec_ty -> expected_ty
500 tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type
501 -- If not, the call is a no-op
502 = tcInstType SigTv expected_ty `thenM` \ (forall_tvs, theta, phi_ty) ->
504 -- Type-check the arg and unify with poly type
505 getLIE (thing_inside phi_ty) `thenM` \ (result, lie) ->
507 -- Check that the "forall_tvs" havn't been constrained
508 -- The interesting bit here is that we must include the free variables
509 -- of the expected_ty. Here's an example:
510 -- runST (newVar True)
511 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
512 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
513 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
514 -- So now s' isn't unconstrained because it's linked to a.
515 -- Conclusion: include the free vars of the expected_ty in the
516 -- list of "free vars" for the signature check.
518 newDicts SignatureOrigin theta `thenM` \ dicts ->
519 tcSimplifyCheck sig_msg forall_tvs dicts lie `thenM` \ inst_binds ->
522 zonkTcTyVars forall_tvs `thenM` \ forall_tys ->
523 traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
524 text "expected_ty" <+> ppr expected_ty,
525 text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr phi_ty,
526 text "free_tvs" <+> ppr free_tvs,
527 text "forall_tys" <+> ppr forall_tys]) `thenM_`
530 checkSigTyVarsWrt free_tvs forall_tvs `thenM` \ zonked_tvs ->
532 traceTc (text "tcGen:done") `thenM_`
535 -- This HsLet binds any Insts which came out of the simplification.
536 -- It's a bit out of place here, but using AbsBind involves inventing
537 -- a couple of new names which seems worse.
538 dict_ids = map instToId dicts
539 co_fn e = TyLam zonked_tvs (mkHsDictLam dict_ids (mkHsLet inst_binds (noLoc e)))
541 returnM (mkCoercion co_fn, result)
543 free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
544 sig_msg = ptext SLIT("expected type of an expression")
549 %************************************************************************
551 \subsection[Unify-exported]{Exported unification functions}
553 %************************************************************************
555 The exported functions are all defined as versions of some
556 non-exported generic functions.
558 Unify two @TauType@s. Dead straightforward.
561 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
562 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
563 = -- The unifier should only ever see tau-types
564 -- (no quantification whatsoever)
565 ASSERT2( isTauTy ty1, ppr ty1 )
566 ASSERT2( isTauTy ty2, ppr ty2 )
567 addErrCtxtM (unifyCtxt "type" ty1 ty2) $
571 @unifyTauTyList@ unifies corresponding elements of two lists of
572 @TauType@s. It uses @uTys@ to do the real work. The lists should be
573 of equal length. We charge down the list explicitly so that we can
574 complain if their lengths differ.
577 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM ()
578 unifyTauTyLists [] [] = returnM ()
579 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenM_`
580 unifyTauTyLists tys1 tys2
581 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
584 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
585 all together. It is used, for example, when typechecking explicit
586 lists, when all the elts should be of the same type.
589 unifyTauTyList :: [TcTauType] -> TcM ()
590 unifyTauTyList [] = returnM ()
591 unifyTauTyList [ty] = returnM ()
592 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenM_`
596 %************************************************************************
598 \subsection[Unify-uTys]{@uTys@: getting down to business}
600 %************************************************************************
602 @uTys@ is the heart of the unifier. Each arg happens twice, because
603 we want to report errors in terms of synomyms if poss. The first of
604 the pair is used in error messages only; it is always the same as the
605 second, except that if the first is a synonym then the second may be a
606 de-synonym'd version. This way we get better error messages.
608 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
611 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
612 -- ty1 is the *expected* type
614 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
615 -- ty2 is the *actual* type
618 -- Always expand synonyms (see notes at end)
619 -- (this also throws away FTVs)
620 uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
621 uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
623 -- Variables; go for uVar
624 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
625 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
626 -- "True" means args swapped
629 uTys _ (PredTy (IParam n1 t1)) _ (PredTy (IParam n2 t2))
630 | n1 == n2 = uTys t1 t1 t2 t2
631 uTys _ (PredTy (ClassP c1 tys1)) _ (PredTy (ClassP c2 tys2))
632 | c1 == c2 = unifyTauTyLists tys1 tys2
634 -- Functions; just check the two parts
635 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
636 = uTys fun1 fun1 fun2 fun2 `thenM_` uTys arg1 arg1 arg2 arg2
638 -- NewType constructors must match
639 uTys _ (NewTcApp tc1 tys1) _ (NewTcApp tc2 tys2)
640 | tc1 == tc2 = unifyTauTyLists tys1 tys2
642 -- Ordinary type constructors must match
643 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
644 | con1 == con2 && equalLength tys1 tys2
645 = unifyTauTyLists tys1 tys2
647 -- Applications need a bit of care!
648 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
649 -- NB: we've already dealt with type variables and Notes,
650 -- so if one type is an App the other one jolly well better be too
651 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
652 = case tcSplitAppTy_maybe ty2 of
653 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenM_` uTys t1 t1 t2 t2
654 Nothing -> unifyMisMatch ps_ty1 ps_ty2
656 -- Now the same, but the other way round
657 -- Don't swap the types, because the error messages get worse
658 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
659 = case tcSplitAppTy_maybe ty1 of
660 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenM_` uTys t1 t1 t2 t2
661 Nothing -> unifyMisMatch ps_ty1 ps_ty2
663 -- Not expecting for-alls in unification
664 -- ... but the error message from the unifyMisMatch more informative
665 -- than a panic message!
667 -- Anything else fails
668 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
674 If you are tempted to make a short cut on synonyms, as in this
678 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
679 -- NO = if (con1 == con2) then
680 -- NO -- Good news! Same synonym constructors, so we can shortcut
681 -- NO -- by unifying their arguments and ignoring their expansions.
682 -- NO unifyTauTypeLists args1 args2
684 -- NO -- Never mind. Just expand them and try again
688 then THINK AGAIN. Here is the whole story, as detected and reported
689 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
691 Here's a test program that should detect the problem:
695 x = (1 :: Bogus Char) :: Bogus Bool
698 The problem with [the attempted shortcut code] is that
702 is not a sufficient condition to be able to use the shortcut!
703 You also need to know that the type synonym actually USES all
704 its arguments. For example, consider the following type synonym
705 which does not use all its arguments.
710 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
711 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
712 would fail, even though the expanded forms (both \tr{Int}) should
715 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
716 unnecessarily bind \tr{t} to \tr{Char}.
718 ... You could explicitly test for the problem synonyms and mark them
719 somehow as needing expansion, perhaps also issuing a warning to the
724 %************************************************************************
726 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
728 %************************************************************************
730 @uVar@ is called when at least one of the types being unified is a
731 variable. It does {\em not} assume that the variable is a fixed point
732 of the substitution; rather, notice that @uVar@ (defined below) nips
733 back into @uTys@ if it turns out that the variable is already bound.
736 uVar :: Bool -- False => tyvar is the "expected"
737 -- True => ty is the "expected" thing
739 -> TcTauType -> TcTauType -- printing and real versions
742 uVar swapped tv1 ps_ty2 ty2
743 = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2)) `thenM_`
744 getTcTyVar tv1 `thenM` \ maybe_ty1 ->
746 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
747 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
748 other -> uUnboundVar swapped tv1 ps_ty2 ty2
750 -- Expand synonyms; ignore FTVs
751 uUnboundVar swapped tv1 ps_ty2 (NoteTy n2 ty2)
752 = uUnboundVar swapped tv1 ps_ty2 ty2
755 -- The both-type-variable case
756 uUnboundVar swapped tv1 ps_ty2 ty2@(TyVarTy tv2)
758 -- Same type variable => no-op
762 -- Distinct type variables
764 = getTcTyVar tv2 `thenM` \ maybe_ty2 ->
766 Just ty2' -> uUnboundVar swapped tv1 ty2' ty2'
769 -- It should always be the case that either k1 <: k2 or k2 <: k1
770 -- Reason: a type variable never gets the kinds (#) or #
772 -> ASSERT2( k1 `isSubKind` k2, (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
773 putTcTyVar tv2 (TyVarTy tv1) `thenM_`
777 -> ASSERT2( k2 `isSubKind` k1, (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
778 putTcTyVar tv1 ps_ty2 `thenM_`
783 update_tv2 = k1 `isSubKind` k2 && (k1 /= k2 || nicer_to_update_tv2)
784 -- Update the variable with least kind info
785 -- See notes on type inference in Kind.lhs
786 -- The "nicer to" part only applies if the two kinds are the same,
787 -- so we can choose which to do.
789 nicer_to_update_tv2 = isUserTyVar tv1
790 -- Don't unify a signature type variable if poss
791 || isSystemName (varName tv2)
792 -- Try to update sys-y type variables in preference to sig-y ones
794 -- Second one isn't a type variable
795 uUnboundVar swapped tv1 ps_ty2 non_var_ty2
796 = -- Check that tv1 isn't a type-signature type variable
797 checkM (not (isSkolemTyVar tv1))
798 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenM_`
800 -- Do the occurs check, and check that we are not
801 -- unifying a type variable with a polytype
802 -- Returns a zonked type ready for the update
803 checkValue tv1 ps_ty2 non_var_ty2 `thenM` \ ty2 ->
805 -- Check that the kinds match
806 checkKinds swapped tv1 ty2 `thenM_`
808 -- Perform the update
809 putTcTyVar tv1 ty2 `thenM_`
814 checkKinds swapped tv1 ty2
815 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
816 -- ty2 has been zonked at this stage, which ensures that
817 -- its kind has as much boxity information visible as possible.
818 | tk2 `isSubKind` tk1 = returnM ()
821 -- Either the kinds aren't compatible
822 -- (can happen if we unify (a b) with (c d))
823 -- or we are unifying a lifted type variable with an
824 -- unlifted type: e.g. (id 3#) is illegal
825 = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
826 unifyKindMisMatch k1 k2
829 (k1,k2) | swapped = (tk2,tk1)
830 | otherwise = (tk1,tk2)
836 checkValue tv1 ps_ty2 non_var_ty2
837 -- Do the occurs check, and check that we are not
838 -- unifying a type variable with a polytype
839 -- Return the type to update the type variable with, or fail
841 -- Basically we want to update tv1 := ps_ty2
842 -- because ps_ty2 has type-synonym info, which improves later error messages
847 -- f :: (A a -> a -> ()) -> ()
851 -- x = f (\ x p -> p x)
853 -- In the application (p x), we try to match "t" with "A t". If we go
854 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
855 -- an infinite loop later.
856 -- But we should not reject the program, because A t = ().
857 -- Rather, we should bind t to () (= non_var_ty2).
859 -- That's why we have this two-state occurs-check
860 = zonkTcType ps_ty2 `thenM` \ ps_ty2' ->
861 case okToUnifyWith tv1 ps_ty2' of {
862 Nothing -> returnM ps_ty2' ; -- Success
865 zonkTcType non_var_ty2 `thenM` \ non_var_ty2' ->
866 case okToUnifyWith tv1 non_var_ty2' of
867 Nothing -> -- This branch rarely succeeds, except in strange cases
868 -- like that in the example above
871 Just problem -> failWithTcM (unifyCheck problem tv1 ps_ty2')
874 data Problem = OccurCheck | NotMonoType
876 okToUnifyWith :: TcTyVar -> TcType -> Maybe Problem
877 -- (okToUnifyWith tv ty) checks whether it's ok to unify
880 -- Just p => not ok, problem p
885 ok (TyVarTy tv') | tv == tv' = Just OccurCheck
886 | otherwise = Nothing
887 ok (AppTy t1 t2) = ok t1 `and` ok t2
888 ok (FunTy t1 t2) = ok t1 `and` ok t2
889 ok (TyConApp _ ts) = oks ts
890 ok (NewTcApp _ ts) = oks ts
891 ok (ForAllTy _ _) = Just NotMonoType
892 ok (PredTy st) = ok_st st
893 ok (NoteTy (FTVNote _) t) = ok t
894 ok (NoteTy (SynNote t1) t2) = ok t1 `and` ok t2
895 -- Type variables may be free in t1 but not t2
896 -- A forall may be in t2 but not t1
898 oks ts = foldr (and . ok) Nothing ts
900 ok_st (ClassP _ ts) = oks ts
901 ok_st (IParam _ t) = ok t
904 Just p `and` m = Just p
908 %************************************************************************
912 %************************************************************************
914 Unifying kinds is much, much simpler than unifying types.
917 unifyKind :: TcKind -- Expected
920 unifyKind LiftedTypeKind LiftedTypeKind = returnM ()
921 unifyKind UnliftedTypeKind UnliftedTypeKind = returnM ()
923 unifyKind OpenTypeKind k2 | isOpenTypeKind k2 = returnM ()
924 unifyKind ArgTypeKind k2 | isArgTypeKind k2 = returnM ()
925 -- Respect sub-kinding
927 unifyKind (FunKind a1 r1) (FunKind a2 r2)
928 = do { unifyKind a2 a1; unifyKind r1 r2 }
929 -- Notice the flip in the argument,
930 -- so that the sub-kinding works right
932 unifyKind (KindVar kv1) k2 = uKVar False kv1 k2
933 unifyKind k1 (KindVar kv2) = uKVar True kv2 k1
934 unifyKind k1 k2 = unifyKindMisMatch k1 k2
936 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
937 unifyKinds [] [] = returnM ()
938 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenM_`
940 unifyKinds _ _ = panic "unifyKinds: length mis-match"
943 uKVar :: Bool -> KindVar -> TcKind -> TcM ()
945 = do { mb_k1 <- readKindVar kv1
947 Nothing -> uUnboundKVar swapped kv1 k2
948 Just k1 | swapped -> unifyKind k2 k1
949 | otherwise -> unifyKind k1 k2 }
952 uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM ()
953 uUnboundKVar swapped kv1 k2@(KindVar kv2)
954 | kv1 == kv2 = returnM ()
955 | otherwise -- Distinct kind variables
956 = do { mb_k2 <- readKindVar kv2
958 Just k2 -> uUnboundKVar swapped kv1 k2
959 Nothing -> writeKindVar kv1 k2 }
961 uUnboundKVar swapped kv1 non_var_k2
962 = do { k2' <- zonkTcKind non_var_k2
963 ; kindOccurCheck kv1 k2'
964 ; k2'' <- kindSimpleKind swapped k2'
965 -- KindVars must be bound only to simple kinds
966 -- Polarities: (kindSimpleKind True ?) succeeds
967 -- returning *, corresponding to unifying
970 ; writeKindVar kv1 k2'' }
973 kindOccurCheck kv1 k2 -- k2 is zonked
974 = checkTc (not_in k2) (kindOccurCheckErr kv1 k2)
976 not_in (KindVar kv2) = kv1 /= kv2
977 not_in (FunKind a2 r2) = not_in a2 && not_in r2
980 kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
981 -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
982 -- If the flag is False, it requires k <: sk
983 -- E.g. kindSimpleKind False ?? = *
984 -- What about (kv -> *) :=: ?? -> *
985 kindSimpleKind orig_swapped orig_kind
986 = go orig_swapped orig_kind
988 go sw (FunKind k1 k2) = do { k1' <- go (not sw) k1
990 ; return (FunKind k1' k2') }
991 go True OpenTypeKind = return liftedTypeKind
992 go True ArgTypeKind = return liftedTypeKind
993 go sw LiftedTypeKind = return liftedTypeKind
994 go sw k@(KindVar _) = return k -- KindVars are always simple
995 go swapped kind = failWithTc (ptext SLIT("Unexpected kind unification failure:")
996 <+> ppr orig_swapped <+> ppr orig_kind)
997 -- I think this can't actually happen
999 -- T v = MkT v v must be a type
1000 -- T v w = MkT (v -> w) v must not be an umboxed tuple
1003 kindOccurCheckErr tyvar ty
1004 = hang (ptext SLIT("Occurs check: cannot construct the infinite kind:"))
1005 2 (sep [ppr tyvar, char '=', ppr ty])
1007 unifyKindMisMatch ty1 ty2
1008 = zonkTcKind ty1 `thenM` \ ty1' ->
1009 zonkTcKind ty2 `thenM` \ ty2' ->
1011 msg = hang (ptext SLIT("Couldn't match kind"))
1012 2 (sep [quotes (ppr ty1'),
1013 ptext SLIT("against"),
1020 unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
1021 -- Like unifyFunTy, but does not fail; instead just returns Nothing
1023 unifyFunKind (KindVar kvar)
1024 = readKindVar kvar `thenM` \ maybe_kind ->
1026 Just fun_kind -> unifyFunKind fun_kind
1027 Nothing -> do { arg_kind <- newKindVar
1028 ; res_kind <- newKindVar
1029 ; writeKindVar kvar (mkArrowKind arg_kind res_kind)
1030 ; returnM (Just (arg_kind,res_kind)) }
1032 unifyFunKind (FunKind arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
1033 unifyFunKind other = returnM Nothing
1036 %************************************************************************
1038 \subsection[Unify-context]{Errors and contexts}
1040 %************************************************************************
1046 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
1047 = zonkTcType ty1 `thenM` \ ty1' ->
1048 zonkTcType ty2 `thenM` \ ty2' ->
1049 returnM (err ty1' ty2')
1051 err ty1 ty2 = (env1,
1054 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
1055 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
1058 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
1060 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
1061 -- tv1 and ty2 are zonked already
1064 msg = (env2, ptext SLIT("When matching types") <+>
1065 sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual])
1067 (pp_expected, pp_actual) | swapped = (pp2, pp1)
1068 | otherwise = (pp1, pp2)
1069 (env1, tv1') = tidyOpenTyVar tidy_env tv1
1070 (env2, ty2') = tidyOpenType env1 ty2
1071 pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1)
1072 pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)
1074 unifyMisMatch ty1 ty2
1075 = zonkTcType ty1 `thenM` \ ty1' ->
1076 zonkTcType ty2 `thenM` \ ty2' ->
1078 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
1079 msg = hang (ptext SLIT("Couldn't match"))
1080 2 (sep [quotes (ppr tidy_ty1),
1081 ptext SLIT("against"),
1082 quotes (ppr tidy_ty2)])
1084 failWithTcM (env, msg)
1087 unifyWithSigErr tyvar ty
1088 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
1089 2 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
1091 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
1092 (env2, tidy_ty) = tidyOpenType env1 ty
1094 unifyCheck problem tyvar ty
1096 2 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
1098 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
1099 (env2, tidy_ty) = tidyOpenType env1 ty
1101 msg = case problem of
1102 OccurCheck -> ptext SLIT("Occurs check: cannot construct the infinite type:")
1103 NotMonoType -> ptext SLIT("Cannot unify a type variable with a type scheme:")
1107 %************************************************************************
1111 %************************************************************************
1113 ---------------------------
1114 -- We would like to get a decent error message from
1115 -- (a) Under-applied type constructors
1116 -- f :: (Maybe, Maybe)
1117 -- (b) Over-applied type constructors
1118 -- f :: Int x -> Int x
1122 checkExpectedKind :: Outputable a => a -> TcKind -> TcKind -> TcM ()
1123 -- A fancy wrapper for 'unifyKind', which tries
1124 -- to give decent error messages.
1125 checkExpectedKind ty act_kind exp_kind
1126 | act_kind `isSubKind` exp_kind -- Short cut for a very common case
1129 = tryTc (unifyKind exp_kind act_kind) `thenM` \ (errs, mb_r) ->
1131 Just _ -> returnM () ; -- Unification succeeded
1134 -- So there's definitely an error
1135 -- Now to find out what sort
1136 zonkTcKind exp_kind `thenM` \ exp_kind ->
1137 zonkTcKind act_kind `thenM` \ act_kind ->
1139 let (exp_as, _) = splitKindFunTys exp_kind
1140 (act_as, _) = splitKindFunTys act_kind
1141 n_exp_as = length exp_as
1142 n_act_as = length act_as
1144 err | n_exp_as < n_act_as -- E.g. [Maybe]
1145 = quotes (ppr ty) <+> ptext SLIT("is not applied to enough type arguments")
1147 -- Now n_exp_as >= n_act_as. In the next two cases,
1148 -- n_exp_as == 0, and hence so is n_act_as
1149 | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
1150 = ptext SLIT("Expecting a lifted type, but") <+> quotes (ppr ty)
1151 <+> ptext SLIT("is unlifted")
1153 | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
1154 = ptext SLIT("Expecting an unlifted type, but") <+> quotes (ppr ty)
1155 <+> ptext SLIT("is lifted")
1157 | otherwise -- E.g. Monad [Int]
1158 = sep [ ptext SLIT("Expecting kind") <+> quotes (pprKind exp_kind) <> comma,
1159 ptext SLIT("but") <+> quotes (ppr ty) <+>
1160 ptext SLIT("has kind") <+> quotes (pprKind act_kind)]
1162 failWithTc (ptext SLIT("Kind error:") <+> err)
1166 %************************************************************************
1168 \subsection{Checking signature type variables}
1170 %************************************************************************
1172 @checkSigTyVars@ is used after the type in a type signature has been unified with
1173 the actual type found. It then checks that the type variables of the type signature
1175 (a) Still all type variables
1176 eg matching signature [a] against inferred type [(p,q)]
1177 [then a will be unified to a non-type variable]
1179 (b) Still all distinct
1180 eg matching signature [(a,b)] against inferred type [(p,p)]
1181 [then a and b will be unified together]
1183 (c) Not mentioned in the environment
1184 eg the signature for f in this:
1190 Here, f is forced to be monorphic by the free occurence of x.
1192 (d) Not (unified with another type variable that is) in scope.
1193 eg f x :: (r->r) = (\y->y) :: forall a. a->r
1194 when checking the expression type signature, we find that
1195 even though there is nothing in scope whose type mentions r,
1196 nevertheless the type signature for the expression isn't right.
1198 Another example is in a class or instance declaration:
1200 op :: forall b. a -> b
1202 Here, b gets unified with a
1204 Before doing this, the substitution is applied to the signature type variable.
1206 We used to have the notion of a "DontBind" type variable, which would
1207 only be bound to itself or nothing. Then points (a) and (b) were
1208 self-checking. But it gave rise to bogus consequential error messages.
1211 f = (*) -- Monomorphic
1213 g :: Num a => a -> a
1216 Here, we get a complaint when checking the type signature for g,
1217 that g isn't polymorphic enough; but then we get another one when
1218 dealing with the (Num x) context arising from f's definition;
1219 we try to unify x with Int (to default it), but find that x has already
1220 been unified with the DontBind variable "a" from g's signature.
1221 This is really a problem with side-effecting unification; we'd like to
1222 undo g's effects when its type signature fails, but unification is done
1223 by side effect, so we can't (easily).
1225 So we revert to ordinary type variables for signatures, and try to
1226 give a helpful message in checkSigTyVars.
1229 checkSigTyVars :: [TcTyVar] -> TcM [TcTyVar]
1230 checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
1232 checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM [TcTyVar]
1233 checkSigTyVarsWrt extra_tvs sig_tvs
1234 = zonkTcTyVarsAndFV (varSetElems extra_tvs) `thenM` \ extra_tvs' ->
1235 check_sig_tyvars extra_tvs' sig_tvs
1238 :: TcTyVarSet -- Global type variables. The universally quantified
1239 -- tyvars should not mention any of these
1240 -- Guaranteed already zonked.
1241 -> [TcTyVar] -- Universally-quantified type variables in the signature
1242 -- Not guaranteed zonked.
1243 -> TcM [TcTyVar] -- Zonked signature type variables
1245 check_sig_tyvars extra_tvs []
1247 check_sig_tyvars extra_tvs sig_tvs
1248 = zonkTcTyVars sig_tvs `thenM` \ sig_tys ->
1249 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
1251 env_tvs = gbl_tvs `unionVarSet` extra_tvs
1253 traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tys,
1254 text "gbl_tvs" <+> ppr gbl_tvs,
1255 text "extra_tvs" <+> ppr extra_tvs])) `thenM_`
1257 checkM (allDistinctTyVars sig_tys env_tvs)
1258 (complain sig_tys env_tvs) `thenM_`
1260 returnM (map (tcGetTyVar "checkSigTyVars") sig_tys)
1263 complain sig_tys globals
1264 = -- "check" checks each sig tyvar in turn
1266 (env2, emptyVarEnv, [])
1267 (tidy_tvs `zip` tidy_tys) `thenM` \ (env3, _, msgs) ->
1269 failWithTcM (env3, main_msg $$ nest 2 (vcat msgs))
1271 (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs
1272 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
1274 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
1276 check (tidy_env, acc, msgs) (sig_tyvar,ty)
1277 -- sig_tyvar is from the signature;
1278 -- ty is what you get if you zonk sig_tyvar and then tidy it
1280 -- acc maps a zonked type variable back to a signature type variable
1281 = case tcGetTyVar_maybe ty of {
1282 Nothing -> -- Error (a)!
1283 returnM (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
1287 case lookupVarEnv acc tv of {
1288 Just sig_tyvar' -> -- Error (b)!
1289 returnM (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
1291 thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
1295 if tv `elemVarSet` globals -- Error (c) or (d)! Type variable escapes
1296 -- The least comprehensible, so put it last
1298 -- get the local TcIds and TyVars from the environment,
1299 -- and pass them to find_globals (they might have tv free)
1300 then findGlobals (unitVarSet tv) tidy_env `thenM` \ (tidy_env1, globs) ->
1301 returnM (tidy_env1, acc, escape_msg sig_tyvar tv globs : msgs)
1304 returnM (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
1310 -----------------------
1311 escape_msg sig_tv tv globs
1312 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
1313 if notNull globs then
1314 vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"),
1315 nest 2 (vcat globs)]
1317 empty -- Sigh. It's really hard to give a good error message
1318 -- all the time. One bad case is an existential pattern match.
1319 -- We rely on the "When..." context to help.
1321 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
1322 | otherwise = ptext SLIT("It")
1325 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
1326 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
1329 These two context are used with checkSigTyVars
1332 sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
1333 -> TidyEnv -> TcM (TidyEnv, Message)
1334 sigCtxt id sig_tvs sig_theta sig_tau tidy_env
1335 = zonkTcType sig_tau `thenM` \ actual_tau ->
1337 (env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs
1338 (env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
1339 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1340 sub_msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
1341 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
1343 msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id),