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 -- NB 1: we can't just unify the type variable with the type
184 -- because the type might not be a tau-type, and we aren't
185 -- allowed to instantiate an ordinary type variable with
188 -- NB 2: can we short-cut to an error case?
189 -- when the arg/res is not a tau-type?
190 -- NO! e.g. f :: ((forall a. a->a) -> Int) -> Int
192 -- is perfectly fine!
194 tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv)
195 = getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
197 Just ty -> tc_sub exp_sty exp_ty ty ty
198 Nothing -> imitateFun tv exp_sty `thenNF_Tc` \ (act_arg, act_res) ->
199 tcSub_fun exp_arg exp_res act_arg act_res
201 tc_sub _ (TyVarTy tv) act_sty act_ty@(FunTy act_arg act_res)
202 = getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
204 Just ty -> tc_sub ty ty act_sty act_ty
205 Nothing -> imitateFun tv act_sty `thenNF_Tc` \ (exp_arg, exp_res) ->
206 tcSub_fun exp_arg exp_res act_arg act_res
208 -----------------------------------
210 -- If none of the above match, we revert to the plain unifier
211 tc_sub exp_sty expected_ty act_sty actual_ty
212 = uTys exp_sty expected_ty act_sty actual_ty `thenTc_`
213 returnTc (idCoercion, emptyLIE)
216 %************************************************************************
218 \subsection{Functions}
220 %************************************************************************
223 tcSub_fun exp_arg exp_res act_arg act_res
224 = tcSub act_arg exp_arg `thenTc` \ (co_fn_arg, lie1) ->
225 tcSub exp_res act_res `thenTc` \ (co_fn_res, lie2) ->
226 tcGetUnique `thenNF_Tc` \ uniq ->
228 -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
229 -- co_fn_res :: HsExpr act_res -> HsExpr exp_res
230 -- co_fn :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
231 arg_id = mkSysLocal SLIT("sub") uniq exp_arg
232 coercion | isIdCoercion co_fn_arg,
233 isIdCoercion co_fn_res = idCoercion
234 | otherwise = mkCoercion co_fn
236 co_fn e = DictLam [arg_id]
237 (co_fn_res <$> (HsApp e (co_fn_arg <$> (HsVar arg_id))))
238 -- Slight hack; using a "DictLam" to get an ordinary simple lambda
239 -- HsVar arg_id :: HsExpr exp_arg
240 -- co_fn_arg $it :: HsExpr act_arg
241 -- HsApp e $it :: HsExpr act_res
242 -- co_fn_res $it :: HsExpr exp_res
244 returnTc (coercion, lie1 `plusLIE` lie2)
246 imitateFun :: TcTyVar -> TcType -> NF_TcM (TcType, TcType)
248 = ASSERT( not (isHoleTyVar tv) )
249 -- NB: tv is an *ordinary* tyvar and so are the new ones
251 -- Check that tv isn't a type-signature type variable
252 -- (This would be found later in checkSigTyVars, but
253 -- we get a better error message if we do it here.)
254 checkTcM (not (isSkolemTyVar tv))
255 (failWithTcM (unifyWithSigErr tv ty)) `thenTc_`
257 newTyVarTy openTypeKind `thenNF_Tc` \ arg ->
258 newTyVarTy openTypeKind `thenNF_Tc` \ res ->
259 putTcTyVar tv (mkFunTy arg res) `thenNF_Tc_`
260 returnNF_Tc (arg,res)
264 %************************************************************************
266 \subsection{Generalisation}
268 %************************************************************************
271 tcGen :: TcSigmaType -- expected_ty
272 -> (TcPhiType -> TcM (result, LIE)) -- spec_ty
273 -> TcM (ExprCoFn, result, LIE)
274 -- The expression has type: spec_ty -> expected_ty
276 tcGen expected_ty thing_inside -- We expect expected_ty to be a forall-type
277 -- If not, the call is a no-op
278 = tcInstType expected_ty `thenNF_Tc` \ (forall_tvs, theta, phi_ty) ->
280 -- Type-check the arg and unify with poly type
281 thing_inside phi_ty `thenTc` \ (result, lie) ->
283 -- Check that the "forall_tvs" havn't been constrained
284 -- The interesting bit here is that we must include the free variables
285 -- of the expected_ty. Here's an example:
286 -- runST (newVar True)
287 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
288 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
289 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
290 -- So now s' isn't unconstrained because it's linked to a.
291 -- Conclusion: include the free vars of the expected_ty in the
292 -- list of "free vars" for the signature check.
294 tcExtendGlobalTyVars free_tvs $
295 tcAddErrCtxtM (sigCtxt forall_tvs theta phi_ty) $
297 newDicts SignatureOrigin theta `thenNF_Tc` \ dicts ->
298 tcSimplifyCheck sig_msg forall_tvs dicts lie `thenTc` \ (free_lie, inst_binds) ->
299 checkSigTyVars forall_tvs free_tvs `thenTc` \ zonked_tvs ->
302 -- This HsLet binds any Insts which came out of the simplification.
303 -- It's a bit out of place here, but using AbsBind involves inventing
304 -- a couple of new names which seems worse.
305 dict_ids = map instToId dicts
306 co_fn e = TyLam zonked_tvs (DictLam dict_ids (mkHsLet inst_binds e))
308 returnTc (mkCoercion co_fn, result, free_lie)
310 free_tvs = tyVarsOfType expected_ty
311 sig_msg = ptext SLIT("When generalising the type of an expression")
316 %************************************************************************
318 \subsection{Coercion functions}
320 %************************************************************************
323 type Coercion a = Maybe (a -> a)
324 -- Nothing => identity fn
326 type ExprCoFn = Coercion TypecheckedHsExpr
327 type PatCoFn = Coercion TcPat
329 (<.>) :: Coercion a -> Coercion a -> Coercion a -- Composition
330 Nothing <.> Nothing = Nothing
331 Nothing <.> Just f = Just f
332 Just f <.> Nothing = Just f
333 Just f1 <.> Just f2 = Just (f1 . f2)
335 (<$>) :: Coercion a -> a -> a
339 mkCoercion :: (a -> a) -> Coercion a
340 mkCoercion f = Just f
342 idCoercion :: Coercion a
345 isIdCoercion :: Coercion a -> Bool
346 isIdCoercion = isNothing
349 %************************************************************************
351 \subsection[Unify-exported]{Exported unification functions}
353 %************************************************************************
355 The exported functions are all defined as versions of some
356 non-exported generic functions.
358 Unify two @TauType@s. Dead straightforward.
361 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
362 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
363 = -- The unifier should only ever see tau-types
364 -- (no quantification whatsoever)
365 ASSERT2( isTauTy ty1, ppr ty1 )
366 ASSERT2( isTauTy ty2, ppr ty2 )
367 tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
371 @unifyTauTyList@ unifies corresponding elements of two lists of
372 @TauType@s. It uses @uTys@ to do the real work. The lists should be
373 of equal length. We charge down the list explicitly so that we can
374 complain if their lengths differ.
377 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM ()
378 unifyTauTyLists [] [] = returnTc ()
379 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_`
380 unifyTauTyLists tys1 tys2
381 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
384 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
385 all together. It is used, for example, when typechecking explicit
386 lists, when all the elts should be of the same type.
389 unifyTauTyList :: [TcTauType] -> TcM ()
390 unifyTauTyList [] = returnTc ()
391 unifyTauTyList [ty] = returnTc ()
392 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
396 %************************************************************************
398 \subsection[Unify-uTys]{@uTys@: getting down to business}
400 %************************************************************************
402 @uTys@ is the heart of the unifier. Each arg happens twice, because
403 we want to report errors in terms of synomyms if poss. The first of
404 the pair is used in error messages only; it is always the same as the
405 second, except that if the first is a synonym then the second may be a
406 de-synonym'd version. This way we get better error messages.
408 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
411 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
412 -- ty1 is the *expected* type
414 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
415 -- ty2 is the *actual* type
418 -- Always expand synonyms (see notes at end)
419 -- (this also throws away FTVs)
420 uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
421 uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
423 -- Ignore usage annotations inside typechecker
424 uTys ps_ty1 (UsageTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
425 uTys ps_ty1 ty1 ps_ty2 (UsageTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
427 -- Variables; go for uVar
428 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
429 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
430 -- "True" means args swapped
433 uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
434 | n1 == n2 = uTys t1 t1 t2 t2
435 uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
436 | c1 == c2 = unifyTauTyLists tys1 tys2
437 uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
438 | tc1 == tc2 = unifyTauTyLists tys1 tys2
440 -- Functions; just check the two parts
441 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
442 = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
444 -- Type constructors must match
445 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
446 | con1 == con2 && equalLength tys1 tys2
447 = unifyTauTyLists tys1 tys2
449 | con1 == openKindCon
450 -- When we are doing kind checking, we might match a kind '?'
451 -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and
452 -- (CCallable Int) and (CCallable Int#) are both OK
453 = unifyOpenTypeKind ps_ty2
455 -- Applications need a bit of care!
456 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
457 -- NB: we've already dealt with type variables and Notes,
458 -- so if one type is an App the other one jolly well better be too
459 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
460 = case tcSplitAppTy_maybe ty2 of
461 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
462 Nothing -> unifyMisMatch ps_ty1 ps_ty2
464 -- Now the same, but the other way round
465 -- Don't swap the types, because the error messages get worse
466 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
467 = case tcSplitAppTy_maybe ty1 of
468 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
469 Nothing -> unifyMisMatch ps_ty1 ps_ty2
471 -- Not expecting for-alls in unification
472 -- ... but the error message from the unifyMisMatch more informative
473 -- than a panic message!
475 -- Anything else fails
476 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
482 If you are tempted to make a short cut on synonyms, as in this
486 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
487 -- NO = if (con1 == con2) then
488 -- NO -- Good news! Same synonym constructors, so we can shortcut
489 -- NO -- by unifying their arguments and ignoring their expansions.
490 -- NO unifyTauTypeLists args1 args2
492 -- NO -- Never mind. Just expand them and try again
496 then THINK AGAIN. Here is the whole story, as detected and reported
497 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
499 Here's a test program that should detect the problem:
503 x = (1 :: Bogus Char) :: Bogus Bool
506 The problem with [the attempted shortcut code] is that
510 is not a sufficient condition to be able to use the shortcut!
511 You also need to know that the type synonym actually USES all
512 its arguments. For example, consider the following type synonym
513 which does not use all its arguments.
518 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
519 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
520 would fail, even though the expanded forms (both \tr{Int}) should
523 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
524 unnecessarily bind \tr{t} to \tr{Char}.
526 ... You could explicitly test for the problem synonyms and mark them
527 somehow as needing expansion, perhaps also issuing a warning to the
532 %************************************************************************
534 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
536 %************************************************************************
538 @uVar@ is called when at least one of the types being unified is a
539 variable. It does {\em not} assume that the variable is a fixed point
540 of the substitution; rather, notice that @uVar@ (defined below) nips
541 back into @uTys@ if it turns out that the variable is already bound.
544 uVar :: Bool -- False => tyvar is the "expected"
545 -- True => ty is the "expected" thing
547 -> TcTauType -> TcTauType -- printing and real versions
550 uVar swapped tv1 ps_ty2 ty2
551 = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2)) `thenNF_Tc_`
552 getTcTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
554 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
555 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
556 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
558 -- Expand synonyms; ignore FTVs
559 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
560 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
563 -- The both-type-variable case
564 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
566 -- Same type variable => no-op
570 -- Distinct type variables
571 -- ASSERT maybe_ty1 /= Just
573 = getTcTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
575 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
579 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
580 putTcTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
584 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
585 putTcTyVar tv1 ps_ty2 `thenNF_Tc_`
590 update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
591 -- Try to get rid of open type variables as soon as poss
593 nicer_to_update_tv2 = isUserTyVar tv1
594 -- Don't unify a signature type variable if poss
595 || isSystemName (varName tv2)
596 -- Try to update sys-y type variables in preference to sig-y ones
598 -- Second one isn't a type variable
599 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
600 = -- Check that tv1 isn't a type-signature type variable
601 checkTcM (not (isSkolemTyVar tv1))
602 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
604 -- Check that the kinds match
605 zonkTcType ps_ty2 `thenNF_Tc` \ ps_ty2' ->
606 checkKinds swapped tv1 ps_ty2' `thenTc_`
609 -- Basically we want to update tv1 := ps_ty2
610 -- because ps_ty2 has type-synonym info, which improves later error messages
615 -- f :: (A a -> a -> ()) -> ()
619 -- x = f (\ x p -> p x)
621 -- In the application (p x), we try to match "t" with "A t". If we go
622 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
623 -- an infinite loop later.
624 -- But we should not reject the program, because A t = ().
625 -- Rather, we should bind t to () (= non_var_ty2).
627 -- That's why we have this two-state occurs-check
628 if not (tv1 `elemVarSet` tyVarsOfType ps_ty2') then
629 putTcTyVar tv1 ps_ty2' `thenNF_Tc_`
632 zonkTcType non_var_ty2 `thenNF_Tc` \ non_var_ty2' ->
633 if not (tv1 `elemVarSet` tyVarsOfType non_var_ty2') then
634 -- This branch rarely succeeds, except in strange cases
635 -- like that in the example above
636 putTcTyVar tv1 non_var_ty2' `thenNF_Tc_`
639 failWithTcM (unifyOccurCheck tv1 ps_ty2')
642 checkKinds swapped tv1 ty2
643 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
644 -- ty2 has been zonked at this stage
646 | tk1 `eqKind` liftedTypeKind && tk2 `eqKind` unliftedTypeKind
647 -- Check that we don't unify a lifted type variable with an
648 -- unlifted type: e.g. (id 3#) is illegal
649 = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
653 = -- Check that we aren't losing boxity info (shouldn't happen)
654 WARN (not (tk2 `hasMoreBoxityInfo` tk1),
655 (ppr tv1 <+> ppr tk1) $$ (ppr ty2 <+> ppr tk2))
658 (k1,k2) | swapped = (tk2,tk1)
659 | otherwise = (tk1,tk2)
665 %************************************************************************
667 \subsection[Unify-fun]{@unifyFunTy@}
669 %************************************************************************
671 @subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
672 creation of type variables.
674 * subFunTy is used when we might be faced with a "hole" type variable,
675 in which case we should create two new holes.
677 * unifyFunTy is used when we expect to encounter only "ordinary"
678 type variables, so we should create new ordinary type variables
681 subFunTy :: TcSigmaType -- Fail if ty isn't a function type
682 -> TcM (TcType, TcType) -- otherwise return arg and result types
683 subFunTy ty@(TyVarTy tyvar)
685 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
687 Just ty -> subFunTy ty
688 Nothing | isHoleTyVar tyvar
689 -> newHoleTyVarTy `thenNF_Tc` \ arg ->
690 newHoleTyVarTy `thenNF_Tc` \ res ->
691 putTcTyVar tyvar (mkFunTy arg res) `thenNF_Tc_`
694 -> unify_fun_ty_help ty
697 = case tcSplitFunTy_maybe ty of
698 Just arg_and_res -> returnTc arg_and_res
699 Nothing -> unify_fun_ty_help ty
702 unifyFunTy :: TcPhiType -- Fail if ty isn't a function type
703 -> TcM (TcType, TcType) -- otherwise return arg and result types
705 unifyFunTy ty@(TyVarTy tyvar)
706 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
708 Just ty' -> unifyFunTy ty'
709 Nothing -> unify_fun_ty_help ty
712 = case tcSplitFunTy_maybe ty of
713 Just arg_and_res -> returnTc arg_and_res
714 Nothing -> unify_fun_ty_help ty
716 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
717 = newTyVarTy openTypeKind `thenNF_Tc` \ arg ->
718 newTyVarTy openTypeKind `thenNF_Tc` \ res ->
719 unifyTauTy ty (mkFunTy arg res) `thenTc_`
724 unifyListTy :: TcType -- expected list type
725 -> TcM TcType -- list element type
727 unifyListTy ty@(TyVarTy tyvar)
728 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
730 Just ty' -> unifyListTy ty'
731 other -> unify_list_ty_help ty
734 = case tcSplitTyConApp_maybe ty of
735 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
736 other -> unify_list_ty_help ty
738 unify_list_ty_help ty -- Revert to ordinary unification
739 = newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty ->
740 unifyTauTy ty (mkListTy elt_ty) `thenTc_`
745 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
746 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
747 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
749 Just ty' -> unifyTupleTy boxity arity ty'
750 other -> unify_tuple_ty_help boxity arity ty
752 unifyTupleTy boxity arity ty
753 = case tcSplitTyConApp_maybe ty of
754 Just (tycon, arg_tys)
756 && tyConArity tycon == arity
757 && tupleTyConBoxity tycon == boxity
759 other -> unify_tuple_ty_help boxity arity ty
761 unify_tuple_ty_help boxity arity ty
762 = newTyVarTys arity kind `thenNF_Tc` \ arg_tys ->
763 unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenTc_`
766 kind | isBoxed boxity = liftedTypeKind
767 | otherwise = openTypeKind
771 %************************************************************************
773 \subsection{Kind unification}
775 %************************************************************************
778 unifyKind :: TcKind -- Expected
782 = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
785 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
786 unifyKinds [] [] = returnTc ()
787 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_`
789 unifyKinds _ _ = panic "unifyKinds: length mis-match"
793 unifyOpenTypeKind :: TcKind -> TcM ()
794 -- Ensures that the argument kind is of the form (Type bx)
795 -- for some boxity bx
797 unifyOpenTypeKind ty@(TyVarTy tyvar)
798 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
800 Just ty' -> unifyOpenTypeKind ty'
801 other -> unify_open_kind_help ty
804 | isTypeKind ty = returnTc ()
805 | otherwise = unify_open_kind_help ty
807 unify_open_kind_help ty -- Revert to ordinary unification
808 = newBoxityVar `thenNF_Tc` \ boxity ->
809 unifyKind ty (mkTyConApp typeCon [boxity])
813 %************************************************************************
815 \subsection[Unify-context]{Errors and contexts}
817 %************************************************************************
823 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
824 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
825 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
826 returnNF_Tc (err ty1' ty2')
831 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
832 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
835 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
837 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
838 -- tv1 is zonked already
839 = zonkTcType ty2 `thenNF_Tc` \ ty2' ->
840 returnNF_Tc (err ty2')
842 err ty2 = (env2, ptext SLIT("When matching types") <+>
843 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
845 (pp_expected, pp_actual) | swapped = (pp2, pp1)
846 | otherwise = (pp1, pp2)
847 (env1, tv1') = tidyOpenTyVar tidy_env tv1
848 (env2, ty2') = tidyOpenType env1 ty2
852 unifyMisMatch ty1 ty2
853 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
854 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
856 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
857 msg = hang (ptext SLIT("Couldn't match"))
858 4 (sep [quotes (ppr tidy_ty1),
859 ptext SLIT("against"),
860 quotes (ppr tidy_ty2)])
862 failWithTcM (env, msg)
864 unifyWithSigErr tyvar ty
865 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
866 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
868 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
869 (env2, tidy_ty) = tidyOpenType env1 ty
871 unifyOccurCheck tyvar ty
872 = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
873 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
875 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
876 (env2, tidy_ty) = tidyOpenType env1 ty
881 %************************************************************************
883 \subsection{Checking signature type variables}
885 %************************************************************************
887 @checkSigTyVars@ is used after the type in a type signature has been unified with
888 the actual type found. It then checks that the type variables of the type signature
890 (a) Still all type variables
891 eg matching signature [a] against inferred type [(p,q)]
892 [then a will be unified to a non-type variable]
894 (b) Still all distinct
895 eg matching signature [(a,b)] against inferred type [(p,p)]
896 [then a and b will be unified together]
898 (c) Not mentioned in the environment
899 eg the signature for f in this:
905 Here, f is forced to be monorphic by the free occurence of x.
907 (d) Not (unified with another type variable that is) in scope.
908 eg f x :: (r->r) = (\y->y) :: forall a. a->r
909 when checking the expression type signature, we find that
910 even though there is nothing in scope whose type mentions r,
911 nevertheless the type signature for the expression isn't right.
913 Another example is in a class or instance declaration:
915 op :: forall b. a -> b
917 Here, b gets unified with a
919 Before doing this, the substitution is applied to the signature type variable.
921 We used to have the notion of a "DontBind" type variable, which would
922 only be bound to itself or nothing. Then points (a) and (b) were
923 self-checking. But it gave rise to bogus consequential error messages.
926 f = (*) -- Monomorphic
931 Here, we get a complaint when checking the type signature for g,
932 that g isn't polymorphic enough; but then we get another one when
933 dealing with the (Num x) context arising from f's definition;
934 we try to unify x with Int (to default it), but find that x has already
935 been unified with the DontBind variable "a" from g's signature.
936 This is really a problem with side-effecting unification; we'd like to
937 undo g's effects when its type signature fails, but unification is done
938 by side effect, so we can't (easily).
940 So we revert to ordinary type variables for signatures, and try to
941 give a helpful message in checkSigTyVars.
944 checkSigTyVars :: [TcTyVar] -- Universally-quantified type variables in the signature
945 -> TcTyVarSet -- Tyvars that are free in the type signature
946 -- Not necessarily zonked
947 -- These should *already* be in the free-in-env set,
948 -- and are used here only to improve the error message
949 -> TcM [TcTyVar] -- Zonked signature type variables
951 checkSigTyVars [] free = returnTc []
952 checkSigTyVars sig_tyvars free_tyvars
953 = zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys ->
954 tcGetGlobalTyVars `thenNF_Tc` \ globals ->
956 checkTcM (allDistinctTyVars sig_tys globals)
957 (complain sig_tys globals) `thenTc_`
959 returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
962 complain sig_tys globals
963 = -- "check" checks each sig tyvar in turn
965 (env2, emptyVarEnv, [])
966 (tidy_tvs `zip` tidy_tys) `thenNF_Tc` \ (env3, _, msgs) ->
968 failWithTcM (env3, main_msg $$ vcat msgs)
970 (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tyvars
971 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
973 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
975 check (tidy_env, acc, msgs) (sig_tyvar,ty)
976 -- sig_tyvar is from the signature;
977 -- ty is what you get if you zonk sig_tyvar and then tidy it
979 -- acc maps a zonked type variable back to a signature type variable
980 = case tcGetTyVar_maybe ty of {
981 Nothing -> -- Error (a)!
982 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
986 case lookupVarEnv acc tv of {
987 Just sig_tyvar' -> -- Error (b)!
988 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
990 thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
994 if tv `elemVarSet` globals -- Error (c) or (d)! Type variable escapes
995 -- The least comprehensible, so put it last
997 -- a) get the local TcIds and TyVars from the environment,
998 -- and pass them to find_globals (they might have tv free)
999 -- b) similarly, find any free_tyvars that mention tv
1000 then tcGetEnv `thenNF_Tc` \ ve ->
1001 find_globals tv tidy_env (tcLEnvElts ve) `thenNF_Tc` \ (tidy_env1, globs) ->
1002 find_frees tv tidy_env1 [] (varSetElems free_tyvars) `thenNF_Tc` \ (tidy_env2, frees) ->
1003 returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
1006 returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
1009 -----------------------
1010 -- find_globals looks at the value environment and finds values
1011 -- whose types mention the offending type variable. It has to be
1012 -- careful to zonk the Id's type first, so it has to be in the monad.
1013 -- We must be careful to pass it a zonked type variable, too.
1018 -> NF_TcM (TidyEnv, [SDoc])
1020 find_globals tv tidy_env things
1021 = go tidy_env [] things
1023 go tidy_env acc [] = returnNF_Tc (tidy_env, acc)
1024 go tidy_env acc (thing : things)
1025 = find_thing ignore_it tidy_env thing `thenNF_Tc` \ (tidy_env1, maybe_doc) ->
1027 Just d -> go tidy_env1 (d:acc) things
1028 Nothing -> go tidy_env1 acc things
1030 ignore_it ty = not (tv `elemVarSet` tyVarsOfType ty)
1032 -----------------------
1033 find_thing ignore_it tidy_env (ATcId id)
1034 = zonkTcType (idType id) `thenNF_Tc` \ id_ty ->
1035 if ignore_it id_ty then
1036 returnNF_Tc (tidy_env, Nothing)
1038 (tidy_env', tidy_ty) = tidyOpenType tidy_env id_ty
1039 msg = sep [ppr id <+> dcolon <+> ppr tidy_ty,
1040 nest 2 (parens (ptext SLIT("bound at") <+>
1041 ppr (getSrcLoc id)))]
1043 returnNF_Tc (tidy_env', Just msg)
1045 find_thing ignore_it tidy_env (ATyVar tv)
1046 = zonkTcTyVar tv `thenNF_Tc` \ tv_ty ->
1047 if ignore_it tv_ty then
1048 returnNF_Tc (tidy_env, Nothing)
1050 (tidy_env1, tv1) = tidyOpenTyVar tidy_env tv
1051 (tidy_env2, tidy_ty) = tidyOpenType tidy_env1 tv_ty
1052 msg = sep [ptext SLIT("Type variable") <+> quotes (ppr tv1) <+> eq_stuff, nest 2 bound_at]
1054 eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty
1055 | otherwise = equals <+> ppr tv_ty
1056 -- It's ok to use Type.getTyVar_maybe because ty is zonked by now
1058 bound_at = tyVarBindingInfo tv
1060 returnNF_Tc (tidy_env2, Just msg)
1062 -----------------------
1063 find_frees tv tidy_env acc []
1064 = returnNF_Tc (tidy_env, acc)
1065 find_frees tv tidy_env acc (ftv:ftvs)
1066 = zonkTcTyVar ftv `thenNF_Tc` \ ty ->
1067 if tv `elemVarSet` tyVarsOfType ty then
1069 (tidy_env', ftv') = tidyOpenTyVar tidy_env ftv
1071 find_frees tv tidy_env' (ftv':acc) ftvs
1073 find_frees tv tidy_env acc ftvs
1076 escape_msg sig_tv tv globs frees
1077 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
1078 if not (null globs) then
1079 vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"),
1080 nest 2 (vcat globs)]
1081 else if not (null frees) then
1082 vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
1083 nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
1086 empty -- Sigh. It's really hard to give a good error message
1087 -- all the time. One bad case is an existential pattern match
1089 is_are | isSingleton frees = ptext SLIT("is")
1090 | otherwise = ptext SLIT("are")
1091 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
1092 | otherwise = ptext SLIT("It")
1094 vcat_first :: Int -> [SDoc] -> SDoc
1095 vcat_first n [] = empty
1096 vcat_first 0 (x:xs) = text "...others omitted..."
1097 vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
1100 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
1101 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
1104 These two context are used with checkSigTyVars
1107 sigCtxt :: [TcTyVar] -> TcThetaType -> TcTauType
1108 -> TidyEnv -> NF_TcM (TidyEnv, Message)
1109 sigCtxt sig_tyvars sig_theta sig_tau tidy_env
1110 = zonkTcType sig_tau `thenNF_Tc` \ actual_tau ->
1112 (env1, tidy_sig_tyvars) = tidyOpenTyVars tidy_env sig_tyvars
1113 (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
1114 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1115 msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
1116 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
1119 returnNF_Tc (env3, msg)
1121 sigPatCtxt bound_tvs bound_ids tidy_env
1122 = returnNF_Tc (env1,
1123 sep [ptext SLIT("When checking a pattern that binds"),
1124 nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
1126 show_ids = filter is_interesting bound_ids
1127 is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
1129 (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
1130 ppr_id id ty = ppr id <+> dcolon <+> ppr ty
1131 -- Don't zonk the types so we get the separate, un-unified versions