2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section{Type subsumption and unification}
8 -- Full-blown subsumption
9 tcSub, tcGen, subFunTy,
10 checkSigTyVars, sigCtxt, sigPatCtxt,
12 -- Various unifications
13 unifyTauTy, unifyTauTyList, unifyTauTyLists,
14 unifyFunTy, unifyListTy, unifyTupleTy,
15 unifyKind, unifyKinds, unifyOpenTypeKind,
18 Coercion, ExprCoFn, PatCoFn,
19 (<$>), (<.>), mkCoercion,
20 idCoercion, isIdCoercion
24 #include "HsVersions.h"
27 import HsSyn ( HsExpr(..) )
28 import TcHsSyn ( TypecheckedHsExpr, TcPat,
29 mkHsDictApp, mkHsTyApp, mkHsLet )
30 import TypeRep ( Type(..), SourceType(..),
31 openKindCon, typeCon )
33 import TcMonad -- TcType, amongst others
34 import TcType ( TcKind, TcType, TcSigmaType, TcPhiType, TcTyVar, TcTauType,
35 TcTyVarSet, TcThetaType,
37 tcSplitAppTy_maybe, tcSplitTyConApp_maybe,
38 tcGetTyVar_maybe, tcGetTyVar,
39 mkTyConApp, mkTyVarTys, mkFunTy, tyVarsOfType, mkRhoTy,
40 typeKind, tcSplitFunTy_maybe, mkForAllTys,
41 isHoleTyVar, isSkolemTyVar, isUserTyVar, allDistinctTyVars,
42 tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
43 eqKind, openTypeKind, liftedTypeKind, unliftedTypeKind, isTypeKind,
44 hasMoreBoxityInfo, tyVarBindingInfo
46 import qualified Type ( getTyVar_maybe )
47 import Inst ( LIE, emptyLIE, plusLIE, mkLIE,
50 import TcMType ( getTcTyVar, putTcTyVar, tcInstType,
51 newTyVarTy, newTyVarTys, newBoxityVar, newHoleTyVarTy,
52 zonkTcType, zonkTcTyVars, zonkTcTyVar )
53 import TcSimplify ( tcSimplifyCheck )
54 import TysWiredIn ( listTyCon, mkListTy, mkTupleTy )
55 import TcEnv ( TcTyThing(..), tcExtendGlobalTyVars, tcGetGlobalTyVars, tcLEnvElts )
56 import TyCon ( tyConArity, isTupleTyCon, tupleTyConBoxity )
57 import PprType ( pprType )
58 import CoreFVs ( idFreeTyVars )
59 import Id ( mkSysLocal, idType )
60 import Var ( Var, varName, tyVarKind )
61 import VarSet ( elemVarSet, varSetElems )
63 import Name ( isSystemName, getSrcLoc )
64 import ErrUtils ( Message )
65 import BasicTypes ( Boxity, Arity, isBoxed )
66 import Util ( isSingleton, equalLength )
67 import Maybe ( isNothing )
72 %************************************************************************
74 \subsection{Subsumption}
76 %************************************************************************
79 tcSub :: TcSigmaType -- expected_ty; can be a type scheme;
80 -- can be a "hole" type variable
81 -> TcSigmaType -- actual_ty; can be a type scheme
82 -> TcM (ExprCoFn, LIE)
85 (tcSub expected_ty actual_ty) checks that
86 actual_ty <= expected_ty
87 That is, that a value of type actual_ty is acceptable in
88 a place expecting a value of type expected_ty.
90 It returns a coercion function
91 co_fn :: actual_ty -> expected_ty
92 which takes an HsExpr of type actual_ty into one of type
96 tcSub expected_ty actual_ty
97 = traceTc (text "tcSub" <+> details) `thenNF_Tc_`
98 tcAddErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
99 (tc_sub expected_ty expected_ty actual_ty actual_ty)
101 details = vcat [text "Expected:" <+> ppr expected_ty,
102 text "Actual: " <+> ppr actual_ty]
105 tc_sub carries the types before and after expanding type synonyms
108 tc_sub :: TcSigmaType -- expected_ty, before expanding synonyms
109 -> TcSigmaType -- ..and after
110 -> TcSigmaType -- actual_ty, before
111 -> TcSigmaType -- ..and after
112 -> TcM (ExprCoFn, LIE)
114 -----------------------------------
116 tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty act_ty
117 tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty
119 -----------------------------------
120 -- "Hole type variable" case
121 -- Do this case before unwrapping for-alls in the actual_ty
123 tc_sub _ (TyVarTy tv) act_sty act_ty
125 = -- It's a "hole" type variable
126 getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
129 Just ty -> -- Already been assigned
130 tc_sub ty ty act_sty act_ty ;
132 Nothing -> -- Assign it
133 putTcTyVar tv act_sty `thenNF_Tc_`
134 returnTc (idCoercion, emptyLIE)
137 -----------------------------------
138 -- Generalisation case
139 -- actual_ty: d:Eq b => b->b
140 -- expected_ty: forall a. Ord a => a->a
141 -- co_fn e /\a. \d2:Ord a. let d = eqFromOrd d2 in e
143 -- It is essential to do this *before* the specialisation case
144 -- Example: f :: (Eq a => a->a) -> ...
145 -- g :: Ord b => b->b
148 tc_sub exp_sty expected_ty act_sty actual_ty
149 | isSigmaTy expected_ty
150 = tcGen expected_ty (
151 \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
152 ) `thenTc` \ (gen_fn, co_fn, lie) ->
153 returnTc (gen_fn <.> co_fn, lie)
155 -----------------------------------
156 -- Specialisation case:
157 -- actual_ty: forall a. Ord a => a->a
158 -- expected_ty: Int -> Int
159 -- co_fn e = e Int dOrdInt
161 tc_sub exp_sty expected_ty act_sty actual_ty
162 | isSigmaTy actual_ty
163 = tcInstType actual_ty `thenNF_Tc` \ (tvs, theta, body_ty) ->
164 newDicts orig theta `thenNF_Tc` \ dicts ->
166 inst_fn e = mkHsDictApp (mkHsTyApp e (mkTyVarTys tvs))
169 tc_sub exp_sty expected_ty body_ty body_ty `thenTc` \ (co_fn, lie) ->
170 returnTc (co_fn <.> mkCoercion inst_fn, lie `plusLIE` mkLIE dicts)
174 -----------------------------------
177 tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
178 = tcSub_fun exp_arg exp_res act_arg act_res
180 -----------------------------------
181 -- Type variable meets function: imitate
183 -- MARK: can we short-cut to an error case?
184 -- when the arg/res is not a tau-type?
185 -- NO! e.g. f :: ((forall a. a->a) -> Int) -> Int
187 -- is perfectly fine!
189 tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv)
190 = getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
192 Just ty -> tc_sub exp_sty exp_ty ty ty
193 Nothing -> imitateFun tv `thenNF_Tc` \ (act_arg, act_res) ->
194 tcSub_fun exp_arg exp_res act_arg act_res
196 tc_sub _ (TyVarTy tv) act_sty act_ty@(FunTy act_arg act_res)
197 = getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
199 Just ty -> tc_sub ty ty act_sty act_ty
200 Nothing -> imitateFun tv `thenNF_Tc` \ (exp_arg, exp_res) ->
201 tcSub_fun exp_arg exp_res act_arg act_res
203 -----------------------------------
205 -- If none of the above match, we revert to the plain unifier
206 tc_sub exp_sty expected_ty act_sty actual_ty
207 = uTys exp_sty expected_ty act_sty actual_ty `thenTc_`
208 returnTc (idCoercion, emptyLIE)
211 %************************************************************************
213 \subsection{Functions}
215 %************************************************************************
218 tcSub_fun exp_arg exp_res act_arg act_res
219 = tcSub act_arg exp_arg `thenTc` \ (co_fn_arg, lie1) ->
220 tcSub exp_res act_res `thenTc` \ (co_fn_res, lie2) ->
221 tcGetUnique `thenNF_Tc` \ uniq ->
223 -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
224 -- co_fn_res :: HsExpr act_res -> HsExpr exp_res
225 -- co_fn :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
226 arg_id = mkSysLocal SLIT("sub") uniq exp_arg
227 coercion | isIdCoercion co_fn_arg,
228 isIdCoercion co_fn_res = idCoercion
229 | otherwise = mkCoercion co_fn
231 co_fn e = DictLam [arg_id]
232 (co_fn_res <$> (HsApp e (co_fn_arg <$> (HsVar arg_id))))
233 -- Slight hack; using a "DictLam" to get an ordinary simple lambda
234 -- HsVar arg_id :: HsExpr exp_arg
235 -- co_fn_arg $it :: HsExpr act_arg
236 -- HsApp e $it :: HsExpr act_res
237 -- co_fn_res $it :: HsExpr exp_res
239 returnTc (coercion, lie1 `plusLIE` lie2)
241 imitateFun :: TcTyVar -> NF_TcM (TcType, TcType)
243 = ASSERT( not (isHoleTyVar tv) )
244 newTyVarTy openTypeKind `thenNF_Tc` \ arg ->
245 newTyVarTy openTypeKind `thenNF_Tc` \ res ->
246 -- NB: tv is an *ordinary* tyvar and so are the new ones
247 putTcTyVar tv (mkFunTy arg res) `thenNF_Tc_`
248 returnNF_Tc (arg,res)
252 %************************************************************************
254 \subsection{Generalisation}
256 %************************************************************************
259 tcGen :: TcSigmaType -- expected_ty
260 -> (TcPhiType -> TcM (result, LIE)) -- spec_ty
261 -> TcM (ExprCoFn, result, LIE)
262 -- The expression has type: spec_ty -> expected_ty
264 tcGen expected_ty thing_inside -- We expect expected_ty to be a forall-type
265 -- If not, the call is a no-op
266 = tcInstType expected_ty `thenNF_Tc` \ (forall_tvs, theta, phi_ty) ->
268 -- Type-check the arg and unify with poly type
269 thing_inside phi_ty `thenTc` \ (result, lie) ->
271 -- Check that the "forall_tvs" havn't been constrained
272 -- The interesting bit here is that we must include the free variables
273 -- of the expected_ty. Here's an example:
274 -- runST (newVar True)
275 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
276 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
277 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
278 -- So now s' isn't unconstrained because it's linked to a.
279 -- Conclusion: include the free vars of the expected_ty in the
280 -- list of "free vars" for the signature check.
282 tcExtendGlobalTyVars free_tvs $
283 tcAddErrCtxtM (sigCtxt forall_tvs theta phi_ty) $
285 newDicts SignatureOrigin theta `thenNF_Tc` \ dicts ->
286 tcSimplifyCheck sig_msg forall_tvs dicts lie `thenTc` \ (free_lie, inst_binds) ->
287 checkSigTyVars forall_tvs free_tvs `thenTc` \ zonked_tvs ->
290 -- This HsLet binds any Insts which came out of the simplification.
291 -- It's a bit out of place here, but using AbsBind involves inventing
292 -- a couple of new names which seems worse.
293 dict_ids = map instToId dicts
294 co_fn e = TyLam zonked_tvs (DictLam dict_ids (mkHsLet inst_binds e))
296 returnTc (mkCoercion co_fn, result, free_lie)
298 free_tvs = tyVarsOfType expected_ty
299 sig_msg = ptext SLIT("When generalising the type of an expression")
304 %************************************************************************
306 \subsection{Coercion functions}
308 %************************************************************************
311 type Coercion a = Maybe (a -> a)
312 -- Nothing => identity fn
314 type ExprCoFn = Coercion TypecheckedHsExpr
315 type PatCoFn = Coercion TcPat
317 (<.>) :: Coercion a -> Coercion a -> Coercion a -- Composition
318 Nothing <.> Nothing = Nothing
319 Nothing <.> Just f = Just f
320 Just f <.> Nothing = Just f
321 Just f1 <.> Just f2 = Just (f1 . f2)
323 (<$>) :: Coercion a -> a -> a
327 mkCoercion :: (a -> a) -> Coercion a
328 mkCoercion f = Just f
330 idCoercion :: Coercion a
333 isIdCoercion :: Coercion a -> Bool
334 isIdCoercion = isNothing
337 %************************************************************************
339 \subsection[Unify-exported]{Exported unification functions}
341 %************************************************************************
343 The exported functions are all defined as versions of some
344 non-exported generic functions.
346 Unify two @TauType@s. Dead straightforward.
349 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
350 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
351 = -- The unifier should only ever see tau-types
352 -- (no quantification whatsoever)
353 ASSERT2( isTauTy ty1, ppr ty1 )
354 ASSERT2( isTauTy ty2, ppr ty2 )
355 tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
359 @unifyTauTyList@ unifies corresponding elements of two lists of
360 @TauType@s. It uses @uTys@ to do the real work. The lists should be
361 of equal length. We charge down the list explicitly so that we can
362 complain if their lengths differ.
365 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM ()
366 unifyTauTyLists [] [] = returnTc ()
367 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_`
368 unifyTauTyLists tys1 tys2
369 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
372 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
373 all together. It is used, for example, when typechecking explicit
374 lists, when all the elts should be of the same type.
377 unifyTauTyList :: [TcTauType] -> TcM ()
378 unifyTauTyList [] = returnTc ()
379 unifyTauTyList [ty] = returnTc ()
380 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
384 %************************************************************************
386 \subsection[Unify-uTys]{@uTys@: getting down to business}
388 %************************************************************************
390 @uTys@ is the heart of the unifier. Each arg happens twice, because
391 we want to report errors in terms of synomyms if poss. The first of
392 the pair is used in error messages only; it is always the same as the
393 second, except that if the first is a synonym then the second may be a
394 de-synonym'd version. This way we get better error messages.
396 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
399 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
400 -- ty1 is the *expected* type
402 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
403 -- ty2 is the *actual* type
406 -- Always expand synonyms (see notes at end)
407 -- (this also throws away FTVs)
408 uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
409 uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
411 -- Ignore usage annotations inside typechecker
412 uTys ps_ty1 (UsageTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
413 uTys ps_ty1 ty1 ps_ty2 (UsageTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
415 -- Variables; go for uVar
416 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
417 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
418 -- "True" means args swapped
421 uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
422 | n1 == n2 = uTys t1 t1 t2 t2
423 uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
424 | c1 == c2 = unifyTauTyLists tys1 tys2
425 uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
426 | tc1 == tc2 = unifyTauTyLists tys1 tys2
428 -- Functions; just check the two parts
429 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
430 = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
432 -- Type constructors must match
433 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
434 | con1 == con2 && equalLength tys1 tys2
435 = unifyTauTyLists tys1 tys2
437 | con1 == openKindCon
438 -- When we are doing kind checking, we might match a kind '?'
439 -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and
440 -- (CCallable Int) and (CCallable Int#) are both OK
441 = unifyOpenTypeKind ps_ty2
443 -- Applications need a bit of care!
444 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
445 -- NB: we've already dealt with type variables and Notes,
446 -- so if one type is an App the other one jolly well better be too
447 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
448 = case tcSplitAppTy_maybe ty2 of
449 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
450 Nothing -> unifyMisMatch ps_ty1 ps_ty2
452 -- Now the same, but the other way round
453 -- Don't swap the types, because the error messages get worse
454 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
455 = case tcSplitAppTy_maybe ty1 of
456 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
457 Nothing -> unifyMisMatch ps_ty1 ps_ty2
459 -- Not expecting for-alls in unification
460 -- ... but the error message from the unifyMisMatch more informative
461 -- than a panic message!
463 -- Anything else fails
464 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
470 If you are tempted to make a short cut on synonyms, as in this
474 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
475 -- NO = if (con1 == con2) then
476 -- NO -- Good news! Same synonym constructors, so we can shortcut
477 -- NO -- by unifying their arguments and ignoring their expansions.
478 -- NO unifyTauTypeLists args1 args2
480 -- NO -- Never mind. Just expand them and try again
484 then THINK AGAIN. Here is the whole story, as detected and reported
485 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
487 Here's a test program that should detect the problem:
491 x = (1 :: Bogus Char) :: Bogus Bool
494 The problem with [the attempted shortcut code] is that
498 is not a sufficient condition to be able to use the shortcut!
499 You also need to know that the type synonym actually USES all
500 its arguments. For example, consider the following type synonym
501 which does not use all its arguments.
506 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
507 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
508 would fail, even though the expanded forms (both \tr{Int}) should
511 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
512 unnecessarily bind \tr{t} to \tr{Char}.
514 ... You could explicitly test for the problem synonyms and mark them
515 somehow as needing expansion, perhaps also issuing a warning to the
520 %************************************************************************
522 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
524 %************************************************************************
526 @uVar@ is called when at least one of the types being unified is a
527 variable. It does {\em not} assume that the variable is a fixed point
528 of the substitution; rather, notice that @uVar@ (defined below) nips
529 back into @uTys@ if it turns out that the variable is already bound.
532 uVar :: Bool -- False => tyvar is the "expected"
533 -- True => ty is the "expected" thing
535 -> TcTauType -> TcTauType -- printing and real versions
538 uVar swapped tv1 ps_ty2 ty2
539 = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2)) `thenNF_Tc_`
540 getTcTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
542 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
543 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
544 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
546 -- Expand synonyms; ignore FTVs
547 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
548 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
551 -- The both-type-variable case
552 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
554 -- Same type variable => no-op
558 -- Distinct type variables
559 -- ASSERT maybe_ty1 /= Just
561 = getTcTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
563 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
567 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
568 putTcTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
572 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
573 putTcTyVar tv1 ps_ty2 `thenNF_Tc_`
578 update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
579 -- Try to get rid of open type variables as soon as poss
581 nicer_to_update_tv2 = isUserTyVar tv1
582 -- Don't unify a signature type variable if poss
583 || isSystemName (varName tv2)
584 -- Try to update sys-y type variables in preference to sig-y ones
586 -- Second one isn't a type variable
587 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
588 = -- Check that tv1 isn't a type-signature type variable
589 checkTcM (not (isSkolemTyVar tv1))
590 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
592 -- Check that the kinds match
593 zonkTcType ps_ty2 `thenNF_Tc` \ ps_ty2' ->
594 checkKinds swapped tv1 ps_ty2' `thenTc_`
597 -- Basically we want to update tv1 := ps_ty2
598 -- because ps_ty2 has type-synonym info, which improves later error messages
603 -- f :: (A a -> a -> ()) -> ()
607 -- x = f (\ x p -> p x)
609 -- In the application (p x), we try to match "t" with "A t". If we go
610 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
611 -- an infinite loop later.
612 -- But we should not reject the program, because A t = ().
613 -- Rather, we should bind t to () (= non_var_ty2).
615 -- That's why we have this two-state occurs-check
616 if not (tv1 `elemVarSet` tyVarsOfType ps_ty2') then
617 putTcTyVar tv1 ps_ty2' `thenNF_Tc_`
620 zonkTcType non_var_ty2 `thenNF_Tc` \ non_var_ty2' ->
621 if not (tv1 `elemVarSet` tyVarsOfType non_var_ty2') then
622 -- This branch rarely succeeds, except in strange cases
623 -- like that in the example above
624 putTcTyVar tv1 non_var_ty2' `thenNF_Tc_`
627 failWithTcM (unifyOccurCheck tv1 ps_ty2')
630 checkKinds swapped tv1 ty2
631 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
632 -- ty2 has been zonked at this stage
634 | tk1 `eqKind` liftedTypeKind && tk2 `eqKind` unliftedTypeKind
635 -- Check that we don't unify a lifted type variable with an
636 -- unlifted type: e.g. (id 3#) is illegal
637 = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
641 = -- Check that we aren't losing boxity info (shouldn't happen)
642 WARN (not (tk2 `hasMoreBoxityInfo` tk1),
643 (ppr tv1 <+> ppr tk1) $$ (ppr ty2 <+> ppr tk2))
646 (k1,k2) | swapped = (tk2,tk1)
647 | otherwise = (tk1,tk2)
653 %************************************************************************
655 \subsection[Unify-fun]{@unifyFunTy@}
657 %************************************************************************
659 @subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
660 creation of type variables.
662 * subFunTy is used when we might be faced with a "hole" type variable,
663 in which case we should create two new holes.
665 * unifyFunTy is used when we expect to encounter only "ordinary"
666 type variables, so we should create new ordinary type variables
669 subFunTy :: TcSigmaType -- Fail if ty isn't a function type
670 -> TcM (TcType, TcType) -- otherwise return arg and result types
671 subFunTy ty@(TyVarTy tyvar)
673 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
675 Just ty -> subFunTy ty
676 Nothing | isHoleTyVar tyvar
677 -> newHoleTyVarTy `thenNF_Tc` \ arg ->
678 newHoleTyVarTy `thenNF_Tc` \ res ->
679 putTcTyVar tyvar (mkFunTy arg res) `thenNF_Tc_`
682 -> unify_fun_ty_help ty
685 = case tcSplitFunTy_maybe ty of
686 Just arg_and_res -> returnTc arg_and_res
687 Nothing -> unify_fun_ty_help ty
690 unifyFunTy :: TcPhiType -- Fail if ty isn't a function type
691 -> TcM (TcType, TcType) -- otherwise return arg and result types
693 unifyFunTy ty@(TyVarTy tyvar)
694 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
696 Just ty' -> unifyFunTy ty'
697 Nothing -> unify_fun_ty_help ty
700 = case tcSplitFunTy_maybe ty of
701 Just arg_and_res -> returnTc arg_and_res
702 Nothing -> unify_fun_ty_help ty
704 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
705 = newTyVarTy openTypeKind `thenNF_Tc` \ arg ->
706 newTyVarTy openTypeKind `thenNF_Tc` \ res ->
707 unifyTauTy ty (mkFunTy arg res) `thenTc_`
712 unifyListTy :: TcType -- expected list type
713 -> TcM TcType -- list element type
715 unifyListTy ty@(TyVarTy tyvar)
716 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
718 Just ty' -> unifyListTy ty'
719 other -> unify_list_ty_help ty
722 = case tcSplitTyConApp_maybe ty of
723 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
724 other -> unify_list_ty_help ty
726 unify_list_ty_help ty -- Revert to ordinary unification
727 = newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty ->
728 unifyTauTy ty (mkListTy elt_ty) `thenTc_`
733 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
734 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
735 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
737 Just ty' -> unifyTupleTy boxity arity ty'
738 other -> unify_tuple_ty_help boxity arity ty
740 unifyTupleTy boxity arity ty
741 = case tcSplitTyConApp_maybe ty of
742 Just (tycon, arg_tys)
744 && tyConArity tycon == arity
745 && tupleTyConBoxity tycon == boxity
747 other -> unify_tuple_ty_help boxity arity ty
749 unify_tuple_ty_help boxity arity ty
750 = newTyVarTys arity kind `thenNF_Tc` \ arg_tys ->
751 unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenTc_`
754 kind | isBoxed boxity = liftedTypeKind
755 | otherwise = openTypeKind
759 %************************************************************************
761 \subsection{Kind unification}
763 %************************************************************************
766 unifyKind :: TcKind -- Expected
770 = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
773 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
774 unifyKinds [] [] = returnTc ()
775 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_`
777 unifyKinds _ _ = panic "unifyKinds: length mis-match"
781 unifyOpenTypeKind :: TcKind -> TcM ()
782 -- Ensures that the argument kind is of the form (Type bx)
783 -- for some boxity bx
785 unifyOpenTypeKind ty@(TyVarTy tyvar)
786 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
788 Just ty' -> unifyOpenTypeKind ty'
789 other -> unify_open_kind_help ty
792 | isTypeKind ty = returnTc ()
793 | otherwise = unify_open_kind_help ty
795 unify_open_kind_help ty -- Revert to ordinary unification
796 = newBoxityVar `thenNF_Tc` \ boxity ->
797 unifyKind ty (mkTyConApp typeCon [boxity])
801 %************************************************************************
803 \subsection[Unify-context]{Errors and contexts}
805 %************************************************************************
811 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
812 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
813 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
814 returnNF_Tc (err ty1' ty2')
819 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
820 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
823 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
825 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
826 -- tv1 is zonked already
827 = zonkTcType ty2 `thenNF_Tc` \ ty2' ->
828 returnNF_Tc (err ty2')
830 err ty2 = (env2, ptext SLIT("When matching types") <+>
831 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
833 (pp_expected, pp_actual) | swapped = (pp2, pp1)
834 | otherwise = (pp1, pp2)
835 (env1, tv1') = tidyOpenTyVar tidy_env tv1
836 (env2, ty2') = tidyOpenType env1 ty2
840 unifyMisMatch ty1 ty2
841 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
842 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
844 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
845 msg = hang (ptext SLIT("Couldn't match"))
846 4 (sep [quotes (ppr tidy_ty1),
847 ptext SLIT("against"),
848 quotes (ppr tidy_ty2)])
850 failWithTcM (env, msg)
852 unifyWithSigErr tyvar ty
853 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
854 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
856 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
857 (env2, tidy_ty) = tidyOpenType env1 ty
859 unifyOccurCheck tyvar ty
860 = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
861 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
863 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
864 (env2, tidy_ty) = tidyOpenType env1 ty
869 %************************************************************************
871 \subsection{Checking signature type variables}
873 %************************************************************************
875 @checkSigTyVars@ is used after the type in a type signature has been unified with
876 the actual type found. It then checks that the type variables of the type signature
878 (a) Still all type variables
879 eg matching signature [a] against inferred type [(p,q)]
880 [then a will be unified to a non-type variable]
882 (b) Still all distinct
883 eg matching signature [(a,b)] against inferred type [(p,p)]
884 [then a and b will be unified together]
886 (c) Not mentioned in the environment
887 eg the signature for f in this:
893 Here, f is forced to be monorphic by the free occurence of x.
895 (d) Not (unified with another type variable that is) in scope.
896 eg f x :: (r->r) = (\y->y) :: forall a. a->r
897 when checking the expression type signature, we find that
898 even though there is nothing in scope whose type mentions r,
899 nevertheless the type signature for the expression isn't right.
901 Another example is in a class or instance declaration:
903 op :: forall b. a -> b
905 Here, b gets unified with a
907 Before doing this, the substitution is applied to the signature type variable.
909 We used to have the notion of a "DontBind" type variable, which would
910 only be bound to itself or nothing. Then points (a) and (b) were
911 self-checking. But it gave rise to bogus consequential error messages.
914 f = (*) -- Monomorphic
919 Here, we get a complaint when checking the type signature for g,
920 that g isn't polymorphic enough; but then we get another one when
921 dealing with the (Num x) context arising from f's definition;
922 we try to unify x with Int (to default it), but find that x has already
923 been unified with the DontBind variable "a" from g's signature.
924 This is really a problem with side-effecting unification; we'd like to
925 undo g's effects when its type signature fails, but unification is done
926 by side effect, so we can't (easily).
928 So we revert to ordinary type variables for signatures, and try to
929 give a helpful message in checkSigTyVars.
932 checkSigTyVars :: [TcTyVar] -- Universally-quantified type variables in the signature
933 -> TcTyVarSet -- Tyvars that are free in the type signature
934 -- Not necessarily zonked
935 -- These should *already* be in the free-in-env set,
936 -- and are used here only to improve the error message
937 -> TcM [TcTyVar] -- Zonked signature type variables
939 checkSigTyVars [] free = returnTc []
940 checkSigTyVars sig_tyvars free_tyvars
941 = zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys ->
942 tcGetGlobalTyVars `thenNF_Tc` \ globals ->
944 checkTcM (allDistinctTyVars sig_tys globals)
945 (complain sig_tys globals) `thenTc_`
947 returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
950 complain sig_tys globals
951 = -- "check" checks each sig tyvar in turn
953 (env2, emptyVarEnv, [])
954 (tidy_tvs `zip` tidy_tys) `thenNF_Tc` \ (env3, _, msgs) ->
956 failWithTcM (env3, main_msg $$ vcat msgs)
958 (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tyvars
959 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
961 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
963 check (tidy_env, acc, msgs) (sig_tyvar,ty)
964 -- sig_tyvar is from the signature;
965 -- ty is what you get if you zonk sig_tyvar and then tidy it
967 -- acc maps a zonked type variable back to a signature type variable
968 = case tcGetTyVar_maybe ty of {
969 Nothing -> -- Error (a)!
970 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
974 case lookupVarEnv acc tv of {
975 Just sig_tyvar' -> -- Error (b)!
976 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
978 thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
982 if tv `elemVarSet` globals -- Error (c) or (d)! Type variable escapes
983 -- The least comprehensible, so put it last
985 -- a) get the local TcIds and TyVars from the environment,
986 -- and pass them to find_globals (they might have tv free)
987 -- b) similarly, find any free_tyvars that mention tv
988 then tcGetEnv `thenNF_Tc` \ ve ->
989 find_globals tv tidy_env (tcLEnvElts ve) `thenNF_Tc` \ (tidy_env1, globs) ->
990 find_frees tv tidy_env1 [] (varSetElems free_tyvars) `thenNF_Tc` \ (tidy_env2, frees) ->
991 returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
994 returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
997 -----------------------
998 -- find_globals looks at the value environment and finds values
999 -- whose types mention the offending type variable. It has to be
1000 -- careful to zonk the Id's type first, so it has to be in the monad.
1001 -- We must be careful to pass it a zonked type variable, too.
1006 -> NF_TcM (TidyEnv, [SDoc])
1008 find_globals tv tidy_env things
1009 = go tidy_env [] things
1011 go tidy_env acc [] = returnNF_Tc (tidy_env, acc)
1012 go tidy_env acc (thing : things)
1013 = find_thing ignore_it tidy_env thing `thenNF_Tc` \ (tidy_env1, maybe_doc) ->
1015 Just d -> go tidy_env1 (d:acc) things
1016 Nothing -> go tidy_env1 acc things
1018 ignore_it ty = not (tv `elemVarSet` tyVarsOfType ty)
1020 -----------------------
1021 find_thing ignore_it tidy_env (ATcId id)
1022 = zonkTcType (idType id) `thenNF_Tc` \ id_ty ->
1023 if ignore_it id_ty then
1024 returnNF_Tc (tidy_env, Nothing)
1026 (tidy_env', tidy_ty) = tidyOpenType tidy_env id_ty
1027 msg = sep [ppr id <+> dcolon <+> ppr tidy_ty,
1028 nest 2 (parens (ptext SLIT("bound at") <+>
1029 ppr (getSrcLoc id)))]
1031 returnNF_Tc (tidy_env', Just msg)
1033 find_thing ignore_it tidy_env (ATyVar tv)
1034 = zonkTcTyVar tv `thenNF_Tc` \ tv_ty ->
1035 if ignore_it tv_ty then
1036 returnNF_Tc (tidy_env, Nothing)
1038 (tidy_env1, tv1) = tidyOpenTyVar tidy_env tv
1039 (tidy_env2, tidy_ty) = tidyOpenType tidy_env1 tv_ty
1040 msg = sep [ptext SLIT("Type variable") <+> quotes (ppr tv1) <+> eq_stuff, nest 2 bound_at]
1042 eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty
1043 | otherwise = equals <+> ppr tv_ty
1044 -- It's ok to use Type.getTyVar_maybe because ty is zonked by now
1046 bound_at = tyVarBindingInfo tv
1048 returnNF_Tc (tidy_env2, Just msg)
1050 -----------------------
1051 find_frees tv tidy_env acc []
1052 = returnNF_Tc (tidy_env, acc)
1053 find_frees tv tidy_env acc (ftv:ftvs)
1054 = zonkTcTyVar ftv `thenNF_Tc` \ ty ->
1055 if tv `elemVarSet` tyVarsOfType ty then
1057 (tidy_env', ftv') = tidyOpenTyVar tidy_env ftv
1059 find_frees tv tidy_env' (ftv':acc) ftvs
1061 find_frees tv tidy_env acc ftvs
1064 escape_msg sig_tv tv globs frees
1065 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
1066 if not (null globs) then
1067 vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"),
1068 nest 2 (vcat globs)]
1069 else if not (null frees) then
1070 vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
1071 nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
1074 empty -- Sigh. It's really hard to give a good error message
1075 -- all the time. One bad case is an existential pattern match
1077 is_are | isSingleton frees = ptext SLIT("is")
1078 | otherwise = ptext SLIT("are")
1079 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
1080 | otherwise = ptext SLIT("It")
1082 vcat_first :: Int -> [SDoc] -> SDoc
1083 vcat_first n [] = empty
1084 vcat_first 0 (x:xs) = text "...others omitted..."
1085 vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
1088 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
1089 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
1092 These two context are used with checkSigTyVars
1095 sigCtxt :: [TcTyVar] -> TcThetaType -> TcTauType
1096 -> TidyEnv -> NF_TcM (TidyEnv, Message)
1097 sigCtxt sig_tyvars sig_theta sig_tau tidy_env
1098 = zonkTcType sig_tau `thenNF_Tc` \ actual_tau ->
1100 (env1, tidy_sig_tyvars) = tidyOpenTyVars tidy_env sig_tyvars
1101 (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
1102 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1103 msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
1104 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
1107 returnNF_Tc (env3, msg)
1109 sigPatCtxt bound_tvs bound_ids tidy_env
1110 = returnNF_Tc (env1,
1111 sep [ptext SLIT("When checking a pattern that binds"),
1112 nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
1114 show_ids = filter is_interesting bound_ids
1115 is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
1117 (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
1118 ppr_id id ty = ppr id <+> dcolon <+> ppr ty
1119 -- Don't zonk the types so we get the separate, un-unified versions