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 -- Variables; go for uVar
424 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
425 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
426 -- "True" means args swapped
429 uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
430 | n1 == n2 = uTys t1 t1 t2 t2
431 uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
432 | c1 == c2 = unifyTauTyLists tys1 tys2
433 uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
434 | tc1 == tc2 = unifyTauTyLists tys1 tys2
436 -- Functions; just check the two parts
437 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
438 = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
440 -- Type constructors must match
441 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
442 | con1 == con2 && equalLength tys1 tys2
443 = unifyTauTyLists tys1 tys2
445 | con1 == openKindCon
446 -- When we are doing kind checking, we might match a kind '?'
447 -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and
448 -- (CCallable Int) and (CCallable Int#) are both OK
449 = unifyOpenTypeKind ps_ty2
451 -- Applications need a bit of care!
452 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
453 -- NB: we've already dealt with type variables and Notes,
454 -- so if one type is an App the other one jolly well better be too
455 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
456 = case tcSplitAppTy_maybe ty2 of
457 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
458 Nothing -> unifyMisMatch ps_ty1 ps_ty2
460 -- Now the same, but the other way round
461 -- Don't swap the types, because the error messages get worse
462 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
463 = case tcSplitAppTy_maybe ty1 of
464 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
465 Nothing -> unifyMisMatch ps_ty1 ps_ty2
467 -- Not expecting for-alls in unification
468 -- ... but the error message from the unifyMisMatch more informative
469 -- than a panic message!
471 -- Anything else fails
472 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
478 If you are tempted to make a short cut on synonyms, as in this
482 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
483 -- NO = if (con1 == con2) then
484 -- NO -- Good news! Same synonym constructors, so we can shortcut
485 -- NO -- by unifying their arguments and ignoring their expansions.
486 -- NO unifyTauTypeLists args1 args2
488 -- NO -- Never mind. Just expand them and try again
492 then THINK AGAIN. Here is the whole story, as detected and reported
493 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
495 Here's a test program that should detect the problem:
499 x = (1 :: Bogus Char) :: Bogus Bool
502 The problem with [the attempted shortcut code] is that
506 is not a sufficient condition to be able to use the shortcut!
507 You also need to know that the type synonym actually USES all
508 its arguments. For example, consider the following type synonym
509 which does not use all its arguments.
514 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
515 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
516 would fail, even though the expanded forms (both \tr{Int}) should
519 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
520 unnecessarily bind \tr{t} to \tr{Char}.
522 ... You could explicitly test for the problem synonyms and mark them
523 somehow as needing expansion, perhaps also issuing a warning to the
528 %************************************************************************
530 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
532 %************************************************************************
534 @uVar@ is called when at least one of the types being unified is a
535 variable. It does {\em not} assume that the variable is a fixed point
536 of the substitution; rather, notice that @uVar@ (defined below) nips
537 back into @uTys@ if it turns out that the variable is already bound.
540 uVar :: Bool -- False => tyvar is the "expected"
541 -- True => ty is the "expected" thing
543 -> TcTauType -> TcTauType -- printing and real versions
546 uVar swapped tv1 ps_ty2 ty2
547 = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2)) `thenNF_Tc_`
548 getTcTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
550 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
551 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
552 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
554 -- Expand synonyms; ignore FTVs
555 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
556 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
559 -- The both-type-variable case
560 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
562 -- Same type variable => no-op
566 -- Distinct type variables
567 -- ASSERT maybe_ty1 /= Just
569 = getTcTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
571 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
575 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
576 putTcTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
580 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
581 putTcTyVar tv1 ps_ty2 `thenNF_Tc_`
586 update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
587 -- Try to get rid of open type variables as soon as poss
589 nicer_to_update_tv2 = isUserTyVar tv1
590 -- Don't unify a signature type variable if poss
591 || isSystemName (varName tv2)
592 -- Try to update sys-y type variables in preference to sig-y ones
594 -- Second one isn't a type variable
595 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
596 = -- Check that tv1 isn't a type-signature type variable
597 checkTcM (not (isSkolemTyVar tv1))
598 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
600 -- Check that the kinds match
601 zonkTcType ps_ty2 `thenNF_Tc` \ ps_ty2' ->
602 checkKinds swapped tv1 ps_ty2' `thenTc_`
605 -- Basically we want to update tv1 := ps_ty2
606 -- because ps_ty2 has type-synonym info, which improves later error messages
611 -- f :: (A a -> a -> ()) -> ()
615 -- x = f (\ x p -> p x)
617 -- In the application (p x), we try to match "t" with "A t". If we go
618 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
619 -- an infinite loop later.
620 -- But we should not reject the program, because A t = ().
621 -- Rather, we should bind t to () (= non_var_ty2).
623 -- That's why we have this two-state occurs-check
624 if not (tv1 `elemVarSet` tyVarsOfType ps_ty2') then
625 putTcTyVar tv1 ps_ty2' `thenNF_Tc_`
628 zonkTcType non_var_ty2 `thenNF_Tc` \ non_var_ty2' ->
629 if not (tv1 `elemVarSet` tyVarsOfType non_var_ty2') then
630 -- This branch rarely succeeds, except in strange cases
631 -- like that in the example above
632 putTcTyVar tv1 non_var_ty2' `thenNF_Tc_`
635 failWithTcM (unifyOccurCheck tv1 ps_ty2')
638 checkKinds swapped tv1 ty2
639 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
640 -- ty2 has been zonked at this stage
642 | tk1 `eqKind` liftedTypeKind && tk2 `eqKind` unliftedTypeKind
643 -- Check that we don't unify a lifted type variable with an
644 -- unlifted type: e.g. (id 3#) is illegal
645 = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
649 = -- Check that we aren't losing boxity info (shouldn't happen)
650 WARN (not (tk2 `hasMoreBoxityInfo` tk1),
651 (ppr tv1 <+> ppr tk1) $$ (ppr ty2 <+> ppr tk2))
654 (k1,k2) | swapped = (tk2,tk1)
655 | otherwise = (tk1,tk2)
661 %************************************************************************
663 \subsection[Unify-fun]{@unifyFunTy@}
665 %************************************************************************
667 @subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
668 creation of type variables.
670 * subFunTy is used when we might be faced with a "hole" type variable,
671 in which case we should create two new holes.
673 * unifyFunTy is used when we expect to encounter only "ordinary"
674 type variables, so we should create new ordinary type variables
677 subFunTy :: TcSigmaType -- Fail if ty isn't a function type
678 -> TcM (TcType, TcType) -- otherwise return arg and result types
679 subFunTy ty@(TyVarTy tyvar)
681 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
683 Just ty -> subFunTy ty
684 Nothing | isHoleTyVar tyvar
685 -> newHoleTyVarTy `thenNF_Tc` \ arg ->
686 newHoleTyVarTy `thenNF_Tc` \ res ->
687 putTcTyVar tyvar (mkFunTy arg res) `thenNF_Tc_`
690 -> unify_fun_ty_help ty
693 = case tcSplitFunTy_maybe ty of
694 Just arg_and_res -> returnTc arg_and_res
695 Nothing -> unify_fun_ty_help ty
698 unifyFunTy :: TcPhiType -- Fail if ty isn't a function type
699 -> TcM (TcType, TcType) -- otherwise return arg and result types
701 unifyFunTy ty@(TyVarTy tyvar)
702 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
704 Just ty' -> unifyFunTy ty'
705 Nothing -> unify_fun_ty_help ty
708 = case tcSplitFunTy_maybe ty of
709 Just arg_and_res -> returnTc arg_and_res
710 Nothing -> unify_fun_ty_help ty
712 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
713 = newTyVarTy openTypeKind `thenNF_Tc` \ arg ->
714 newTyVarTy openTypeKind `thenNF_Tc` \ res ->
715 unifyTauTy ty (mkFunTy arg res) `thenTc_`
720 unifyListTy :: TcType -- expected list type
721 -> TcM TcType -- list element type
723 unifyListTy ty@(TyVarTy tyvar)
724 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
726 Just ty' -> unifyListTy ty'
727 other -> unify_list_ty_help ty
730 = case tcSplitTyConApp_maybe ty of
731 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
732 other -> unify_list_ty_help ty
734 unify_list_ty_help ty -- Revert to ordinary unification
735 = newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty ->
736 unifyTauTy ty (mkListTy elt_ty) `thenTc_`
741 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
742 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
743 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
745 Just ty' -> unifyTupleTy boxity arity ty'
746 other -> unify_tuple_ty_help boxity arity ty
748 unifyTupleTy boxity arity ty
749 = case tcSplitTyConApp_maybe ty of
750 Just (tycon, arg_tys)
752 && tyConArity tycon == arity
753 && tupleTyConBoxity tycon == boxity
755 other -> unify_tuple_ty_help boxity arity ty
757 unify_tuple_ty_help boxity arity ty
758 = newTyVarTys arity kind `thenNF_Tc` \ arg_tys ->
759 unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenTc_`
762 kind | isBoxed boxity = liftedTypeKind
763 | otherwise = openTypeKind
767 %************************************************************************
769 \subsection{Kind unification}
771 %************************************************************************
774 unifyKind :: TcKind -- Expected
778 = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
781 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
782 unifyKinds [] [] = returnTc ()
783 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_`
785 unifyKinds _ _ = panic "unifyKinds: length mis-match"
789 unifyOpenTypeKind :: TcKind -> TcM ()
790 -- Ensures that the argument kind is of the form (Type bx)
791 -- for some boxity bx
793 unifyOpenTypeKind ty@(TyVarTy tyvar)
794 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
796 Just ty' -> unifyOpenTypeKind ty'
797 other -> unify_open_kind_help ty
800 | isTypeKind ty = returnTc ()
801 | otherwise = unify_open_kind_help ty
803 unify_open_kind_help ty -- Revert to ordinary unification
804 = newBoxityVar `thenNF_Tc` \ boxity ->
805 unifyKind ty (mkTyConApp typeCon [boxity])
809 %************************************************************************
811 \subsection[Unify-context]{Errors and contexts}
813 %************************************************************************
819 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
820 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
821 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
822 returnNF_Tc (err ty1' ty2')
827 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
828 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
831 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
833 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
834 -- tv1 is zonked already
835 = zonkTcType ty2 `thenNF_Tc` \ ty2' ->
836 returnNF_Tc (err ty2')
838 err ty2 = (env2, ptext SLIT("When matching types") <+>
839 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
841 (pp_expected, pp_actual) | swapped = (pp2, pp1)
842 | otherwise = (pp1, pp2)
843 (env1, tv1') = tidyOpenTyVar tidy_env tv1
844 (env2, ty2') = tidyOpenType env1 ty2
848 unifyMisMatch ty1 ty2
849 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
850 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
852 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
853 msg = hang (ptext SLIT("Couldn't match"))
854 4 (sep [quotes (ppr tidy_ty1),
855 ptext SLIT("against"),
856 quotes (ppr tidy_ty2)])
858 failWithTcM (env, msg)
860 unifyWithSigErr tyvar ty
861 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
862 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
864 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
865 (env2, tidy_ty) = tidyOpenType env1 ty
867 unifyOccurCheck tyvar ty
868 = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
869 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
871 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
872 (env2, tidy_ty) = tidyOpenType env1 ty
877 %************************************************************************
879 \subsection{Checking signature type variables}
881 %************************************************************************
883 @checkSigTyVars@ is used after the type in a type signature has been unified with
884 the actual type found. It then checks that the type variables of the type signature
886 (a) Still all type variables
887 eg matching signature [a] against inferred type [(p,q)]
888 [then a will be unified to a non-type variable]
890 (b) Still all distinct
891 eg matching signature [(a,b)] against inferred type [(p,p)]
892 [then a and b will be unified together]
894 (c) Not mentioned in the environment
895 eg the signature for f in this:
901 Here, f is forced to be monorphic by the free occurence of x.
903 (d) Not (unified with another type variable that is) in scope.
904 eg f x :: (r->r) = (\y->y) :: forall a. a->r
905 when checking the expression type signature, we find that
906 even though there is nothing in scope whose type mentions r,
907 nevertheless the type signature for the expression isn't right.
909 Another example is in a class or instance declaration:
911 op :: forall b. a -> b
913 Here, b gets unified with a
915 Before doing this, the substitution is applied to the signature type variable.
917 We used to have the notion of a "DontBind" type variable, which would
918 only be bound to itself or nothing. Then points (a) and (b) were
919 self-checking. But it gave rise to bogus consequential error messages.
922 f = (*) -- Monomorphic
927 Here, we get a complaint when checking the type signature for g,
928 that g isn't polymorphic enough; but then we get another one when
929 dealing with the (Num x) context arising from f's definition;
930 we try to unify x with Int (to default it), but find that x has already
931 been unified with the DontBind variable "a" from g's signature.
932 This is really a problem with side-effecting unification; we'd like to
933 undo g's effects when its type signature fails, but unification is done
934 by side effect, so we can't (easily).
936 So we revert to ordinary type variables for signatures, and try to
937 give a helpful message in checkSigTyVars.
940 checkSigTyVars :: [TcTyVar] -- Universally-quantified type variables in the signature
941 -> TcTyVarSet -- Tyvars that are free in the type signature
942 -- Not necessarily zonked
943 -- These should *already* be in the free-in-env set,
944 -- and are used here only to improve the error message
945 -> TcM [TcTyVar] -- Zonked signature type variables
947 checkSigTyVars [] free = returnTc []
948 checkSigTyVars sig_tyvars free_tyvars
949 = zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys ->
950 tcGetGlobalTyVars `thenNF_Tc` \ globals ->
952 checkTcM (allDistinctTyVars sig_tys globals)
953 (complain sig_tys globals) `thenTc_`
955 returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
958 complain sig_tys globals
959 = -- "check" checks each sig tyvar in turn
961 (env2, emptyVarEnv, [])
962 (tidy_tvs `zip` tidy_tys) `thenNF_Tc` \ (env3, _, msgs) ->
964 failWithTcM (env3, main_msg $$ vcat msgs)
966 (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tyvars
967 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
969 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
971 check (tidy_env, acc, msgs) (sig_tyvar,ty)
972 -- sig_tyvar is from the signature;
973 -- ty is what you get if you zonk sig_tyvar and then tidy it
975 -- acc maps a zonked type variable back to a signature type variable
976 = case tcGetTyVar_maybe ty of {
977 Nothing -> -- Error (a)!
978 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
982 case lookupVarEnv acc tv of {
983 Just sig_tyvar' -> -- Error (b)!
984 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
986 thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
990 if tv `elemVarSet` globals -- Error (c) or (d)! Type variable escapes
991 -- The least comprehensible, so put it last
993 -- a) get the local TcIds and TyVars from the environment,
994 -- and pass them to find_globals (they might have tv free)
995 -- b) similarly, find any free_tyvars that mention tv
996 then tcGetEnv `thenNF_Tc` \ ve ->
997 find_globals tv tidy_env (tcLEnvElts ve) `thenNF_Tc` \ (tidy_env1, globs) ->
998 find_frees tv tidy_env1 [] (varSetElems free_tyvars) `thenNF_Tc` \ (tidy_env2, frees) ->
999 returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
1002 returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
1005 -----------------------
1006 -- find_globals looks at the value environment and finds values
1007 -- whose types mention the offending type variable. It has to be
1008 -- careful to zonk the Id's type first, so it has to be in the monad.
1009 -- We must be careful to pass it a zonked type variable, too.
1014 -> NF_TcM (TidyEnv, [SDoc])
1016 find_globals tv tidy_env things
1017 = go tidy_env [] things
1019 go tidy_env acc [] = returnNF_Tc (tidy_env, acc)
1020 go tidy_env acc (thing : things)
1021 = find_thing ignore_it tidy_env thing `thenNF_Tc` \ (tidy_env1, maybe_doc) ->
1023 Just d -> go tidy_env1 (d:acc) things
1024 Nothing -> go tidy_env1 acc things
1026 ignore_it ty = not (tv `elemVarSet` tyVarsOfType ty)
1028 -----------------------
1029 find_thing ignore_it tidy_env (ATcId id)
1030 = zonkTcType (idType id) `thenNF_Tc` \ id_ty ->
1031 if ignore_it id_ty then
1032 returnNF_Tc (tidy_env, Nothing)
1034 (tidy_env', tidy_ty) = tidyOpenType tidy_env id_ty
1035 msg = sep [ppr id <+> dcolon <+> ppr tidy_ty,
1036 nest 2 (parens (ptext SLIT("bound at") <+>
1037 ppr (getSrcLoc id)))]
1039 returnNF_Tc (tidy_env', Just msg)
1041 find_thing ignore_it tidy_env (ATyVar tv)
1042 = zonkTcTyVar tv `thenNF_Tc` \ tv_ty ->
1043 if ignore_it tv_ty then
1044 returnNF_Tc (tidy_env, Nothing)
1046 (tidy_env1, tv1) = tidyOpenTyVar tidy_env tv
1047 (tidy_env2, tidy_ty) = tidyOpenType tidy_env1 tv_ty
1048 msg = sep [ptext SLIT("Type variable") <+> quotes (ppr tv1) <+> eq_stuff, nest 2 bound_at]
1050 eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty
1051 | otherwise = equals <+> ppr tv_ty
1052 -- It's ok to use Type.getTyVar_maybe because ty is zonked by now
1054 bound_at = tyVarBindingInfo tv
1056 returnNF_Tc (tidy_env2, Just msg)
1058 -----------------------
1059 find_frees tv tidy_env acc []
1060 = returnNF_Tc (tidy_env, acc)
1061 find_frees tv tidy_env acc (ftv:ftvs)
1062 = zonkTcTyVar ftv `thenNF_Tc` \ ty ->
1063 if tv `elemVarSet` tyVarsOfType ty then
1065 (tidy_env', ftv') = tidyOpenTyVar tidy_env ftv
1067 find_frees tv tidy_env' (ftv':acc) ftvs
1069 find_frees tv tidy_env acc ftvs
1072 escape_msg sig_tv tv globs frees
1073 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
1074 if not (null globs) then
1075 vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"),
1076 nest 2 (vcat globs)]
1077 else if not (null frees) then
1078 vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
1079 nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
1082 empty -- Sigh. It's really hard to give a good error message
1083 -- all the time. One bad case is an existential pattern match
1085 is_are | isSingleton frees = ptext SLIT("is")
1086 | otherwise = ptext SLIT("are")
1087 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
1088 | otherwise = ptext SLIT("It")
1090 vcat_first :: Int -> [SDoc] -> SDoc
1091 vcat_first n [] = empty
1092 vcat_first 0 (x:xs) = text "...others omitted..."
1093 vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
1096 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
1097 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
1100 These two context are used with checkSigTyVars
1103 sigCtxt :: [TcTyVar] -> TcThetaType -> TcTauType
1104 -> TidyEnv -> NF_TcM (TidyEnv, Message)
1105 sigCtxt sig_tyvars sig_theta sig_tau tidy_env
1106 = zonkTcType sig_tau `thenNF_Tc` \ actual_tau ->
1108 (env1, tidy_sig_tyvars) = tidyOpenTyVars tidy_env sig_tyvars
1109 (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
1110 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1111 msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
1112 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
1115 returnNF_Tc (env3, msg)
1117 sigPatCtxt bound_tvs bound_ids tidy_env
1118 = returnNF_Tc (env1,
1119 sep [ptext SLIT("When checking a pattern that binds"),
1120 nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
1122 show_ids = filter is_interesting bound_ids
1123 is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
1125 (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
1126 ppr_id id ty = ppr id <+> dcolon <+> ppr ty
1127 -- Don't zonk the types so we get the separate, un-unified versions