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 | tk2 `hasMoreBoxityInfo` tk1 = returnTc ()
645 -- Either the kinds aren't compatible
646 -- (can happen if we unify (a b) with (c d))
647 -- or we are unifying a lifted type variable with an
648 -- unlifted type: e.g. (id 3#) is illegal
649 = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
653 (k1,k2) | swapped = (tk2,tk1)
654 | otherwise = (tk1,tk2)
660 %************************************************************************
662 \subsection[Unify-fun]{@unifyFunTy@}
664 %************************************************************************
666 @subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
667 creation of type variables.
669 * subFunTy is used when we might be faced with a "hole" type variable,
670 in which case we should create two new holes.
672 * unifyFunTy is used when we expect to encounter only "ordinary"
673 type variables, so we should create new ordinary type variables
676 subFunTy :: TcSigmaType -- Fail if ty isn't a function type
677 -> TcM (TcType, TcType) -- otherwise return arg and result types
678 subFunTy ty@(TyVarTy tyvar)
680 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
682 Just ty -> subFunTy ty
683 Nothing | isHoleTyVar tyvar
684 -> newHoleTyVarTy `thenNF_Tc` \ arg ->
685 newHoleTyVarTy `thenNF_Tc` \ res ->
686 putTcTyVar tyvar (mkFunTy arg res) `thenNF_Tc_`
689 -> unify_fun_ty_help ty
692 = case tcSplitFunTy_maybe ty of
693 Just arg_and_res -> returnTc arg_and_res
694 Nothing -> unify_fun_ty_help ty
697 unifyFunTy :: TcPhiType -- Fail if ty isn't a function type
698 -> TcM (TcType, TcType) -- otherwise return arg and result types
700 unifyFunTy ty@(TyVarTy tyvar)
701 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
703 Just ty' -> unifyFunTy ty'
704 Nothing -> unify_fun_ty_help ty
707 = case tcSplitFunTy_maybe ty of
708 Just arg_and_res -> returnTc arg_and_res
709 Nothing -> unify_fun_ty_help ty
711 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
712 = newTyVarTy openTypeKind `thenNF_Tc` \ arg ->
713 newTyVarTy openTypeKind `thenNF_Tc` \ res ->
714 unifyTauTy ty (mkFunTy arg res) `thenTc_`
719 unifyListTy :: TcType -- expected list type
720 -> TcM TcType -- list element type
722 unifyListTy ty@(TyVarTy tyvar)
723 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
725 Just ty' -> unifyListTy ty'
726 other -> unify_list_ty_help ty
729 = case tcSplitTyConApp_maybe ty of
730 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
731 other -> unify_list_ty_help ty
733 unify_list_ty_help ty -- Revert to ordinary unification
734 = newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty ->
735 unifyTauTy ty (mkListTy elt_ty) `thenTc_`
740 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
741 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
742 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
744 Just ty' -> unifyTupleTy boxity arity ty'
745 other -> unify_tuple_ty_help boxity arity ty
747 unifyTupleTy boxity arity ty
748 = case tcSplitTyConApp_maybe ty of
749 Just (tycon, arg_tys)
751 && tyConArity tycon == arity
752 && tupleTyConBoxity tycon == boxity
754 other -> unify_tuple_ty_help boxity arity ty
756 unify_tuple_ty_help boxity arity ty
757 = newTyVarTys arity kind `thenNF_Tc` \ arg_tys ->
758 unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenTc_`
761 kind | isBoxed boxity = liftedTypeKind
762 | otherwise = openTypeKind
766 %************************************************************************
768 \subsection{Kind unification}
770 %************************************************************************
773 unifyKind :: TcKind -- Expected
777 = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
780 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
781 unifyKinds [] [] = returnTc ()
782 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_`
784 unifyKinds _ _ = panic "unifyKinds: length mis-match"
788 unifyOpenTypeKind :: TcKind -> TcM ()
789 -- Ensures that the argument kind is of the form (Type bx)
790 -- for some boxity bx
792 unifyOpenTypeKind ty@(TyVarTy tyvar)
793 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
795 Just ty' -> unifyOpenTypeKind ty'
796 other -> unify_open_kind_help ty
799 | isTypeKind ty = returnTc ()
800 | otherwise = unify_open_kind_help ty
802 unify_open_kind_help ty -- Revert to ordinary unification
803 = newBoxityVar `thenNF_Tc` \ boxity ->
804 unifyKind ty (mkTyConApp typeCon [boxity])
808 %************************************************************************
810 \subsection[Unify-context]{Errors and contexts}
812 %************************************************************************
818 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
819 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
820 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
821 returnNF_Tc (err ty1' ty2')
826 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
827 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
830 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
832 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
833 -- tv1 is zonked already
834 = zonkTcType ty2 `thenNF_Tc` \ ty2' ->
835 returnNF_Tc (err ty2')
837 err ty2 = (env2, ptext SLIT("When matching types") <+>
838 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
840 (pp_expected, pp_actual) | swapped = (pp2, pp1)
841 | otherwise = (pp1, pp2)
842 (env1, tv1') = tidyOpenTyVar tidy_env tv1
843 (env2, ty2') = tidyOpenType env1 ty2
847 unifyMisMatch ty1 ty2
848 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
849 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
851 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
852 msg = hang (ptext SLIT("Couldn't match"))
853 4 (sep [quotes (ppr tidy_ty1),
854 ptext SLIT("against"),
855 quotes (ppr tidy_ty2)])
857 failWithTcM (env, msg)
859 unifyWithSigErr tyvar ty
860 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
861 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
863 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
864 (env2, tidy_ty) = tidyOpenType env1 ty
866 unifyOccurCheck tyvar ty
867 = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
868 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
870 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
871 (env2, tidy_ty) = tidyOpenType env1 ty
876 %************************************************************************
878 \subsection{Checking signature type variables}
880 %************************************************************************
882 @checkSigTyVars@ is used after the type in a type signature has been unified with
883 the actual type found. It then checks that the type variables of the type signature
885 (a) Still all type variables
886 eg matching signature [a] against inferred type [(p,q)]
887 [then a will be unified to a non-type variable]
889 (b) Still all distinct
890 eg matching signature [(a,b)] against inferred type [(p,p)]
891 [then a and b will be unified together]
893 (c) Not mentioned in the environment
894 eg the signature for f in this:
900 Here, f is forced to be monorphic by the free occurence of x.
902 (d) Not (unified with another type variable that is) in scope.
903 eg f x :: (r->r) = (\y->y) :: forall a. a->r
904 when checking the expression type signature, we find that
905 even though there is nothing in scope whose type mentions r,
906 nevertheless the type signature for the expression isn't right.
908 Another example is in a class or instance declaration:
910 op :: forall b. a -> b
912 Here, b gets unified with a
914 Before doing this, the substitution is applied to the signature type variable.
916 We used to have the notion of a "DontBind" type variable, which would
917 only be bound to itself or nothing. Then points (a) and (b) were
918 self-checking. But it gave rise to bogus consequential error messages.
921 f = (*) -- Monomorphic
926 Here, we get a complaint when checking the type signature for g,
927 that g isn't polymorphic enough; but then we get another one when
928 dealing with the (Num x) context arising from f's definition;
929 we try to unify x with Int (to default it), but find that x has already
930 been unified with the DontBind variable "a" from g's signature.
931 This is really a problem with side-effecting unification; we'd like to
932 undo g's effects when its type signature fails, but unification is done
933 by side effect, so we can't (easily).
935 So we revert to ordinary type variables for signatures, and try to
936 give a helpful message in checkSigTyVars.
939 checkSigTyVars :: [TcTyVar] -- Universally-quantified type variables in the signature
940 -> TcTyVarSet -- Tyvars that are free in the type signature
941 -- Not necessarily zonked
942 -- These should *already* be in the free-in-env set,
943 -- and are used here only to improve the error message
944 -> TcM [TcTyVar] -- Zonked signature type variables
946 checkSigTyVars [] free = returnTc []
947 checkSigTyVars sig_tyvars free_tyvars
948 = zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys ->
949 tcGetGlobalTyVars `thenNF_Tc` \ globals ->
951 checkTcM (allDistinctTyVars sig_tys globals)
952 (complain sig_tys globals) `thenTc_`
954 returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
957 complain sig_tys globals
958 = -- "check" checks each sig tyvar in turn
960 (env2, emptyVarEnv, [])
961 (tidy_tvs `zip` tidy_tys) `thenNF_Tc` \ (env3, _, msgs) ->
963 failWithTcM (env3, main_msg $$ vcat msgs)
965 (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tyvars
966 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
968 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
970 check (tidy_env, acc, msgs) (sig_tyvar,ty)
971 -- sig_tyvar is from the signature;
972 -- ty is what you get if you zonk sig_tyvar and then tidy it
974 -- acc maps a zonked type variable back to a signature type variable
975 = case tcGetTyVar_maybe ty of {
976 Nothing -> -- Error (a)!
977 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
981 case lookupVarEnv acc tv of {
982 Just sig_tyvar' -> -- Error (b)!
983 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
985 thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
989 if tv `elemVarSet` globals -- Error (c) or (d)! Type variable escapes
990 -- The least comprehensible, so put it last
992 -- a) get the local TcIds and TyVars from the environment,
993 -- and pass them to find_globals (they might have tv free)
994 -- b) similarly, find any free_tyvars that mention tv
995 then tcGetEnv `thenNF_Tc` \ ve ->
996 find_globals tv tidy_env (tcLEnvElts ve) `thenNF_Tc` \ (tidy_env1, globs) ->
997 find_frees tv tidy_env1 [] (varSetElems free_tyvars) `thenNF_Tc` \ (tidy_env2, frees) ->
998 returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
1001 returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
1004 -----------------------
1005 -- find_globals looks at the value environment and finds values
1006 -- whose types mention the offending type variable. It has to be
1007 -- careful to zonk the Id's type first, so it has to be in the monad.
1008 -- We must be careful to pass it a zonked type variable, too.
1013 -> NF_TcM (TidyEnv, [SDoc])
1015 find_globals tv tidy_env things
1016 = go tidy_env [] things
1018 go tidy_env acc [] = returnNF_Tc (tidy_env, acc)
1019 go tidy_env acc (thing : things)
1020 = find_thing ignore_it tidy_env thing `thenNF_Tc` \ (tidy_env1, maybe_doc) ->
1022 Just d -> go tidy_env1 (d:acc) things
1023 Nothing -> go tidy_env1 acc things
1025 ignore_it ty = not (tv `elemVarSet` tyVarsOfType ty)
1027 -----------------------
1028 find_thing ignore_it tidy_env (ATcId id)
1029 = zonkTcType (idType id) `thenNF_Tc` \ id_ty ->
1030 if ignore_it id_ty then
1031 returnNF_Tc (tidy_env, Nothing)
1033 (tidy_env', tidy_ty) = tidyOpenType tidy_env id_ty
1034 msg = sep [ppr id <+> dcolon <+> ppr tidy_ty,
1035 nest 2 (parens (ptext SLIT("bound at") <+>
1036 ppr (getSrcLoc id)))]
1038 returnNF_Tc (tidy_env', Just msg)
1040 find_thing ignore_it tidy_env (ATyVar tv)
1041 = zonkTcTyVar tv `thenNF_Tc` \ tv_ty ->
1042 if ignore_it tv_ty then
1043 returnNF_Tc (tidy_env, Nothing)
1045 (tidy_env1, tv1) = tidyOpenTyVar tidy_env tv
1046 (tidy_env2, tidy_ty) = tidyOpenType tidy_env1 tv_ty
1047 msg = sep [ptext SLIT("Type variable") <+> quotes (ppr tv1) <+> eq_stuff, nest 2 bound_at]
1049 eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty
1050 | otherwise = equals <+> ppr tv_ty
1051 -- It's ok to use Type.getTyVar_maybe because ty is zonked by now
1053 bound_at = tyVarBindingInfo tv
1055 returnNF_Tc (tidy_env2, Just msg)
1057 -----------------------
1058 find_frees tv tidy_env acc []
1059 = returnNF_Tc (tidy_env, acc)
1060 find_frees tv tidy_env acc (ftv:ftvs)
1061 = zonkTcTyVar ftv `thenNF_Tc` \ ty ->
1062 if tv `elemVarSet` tyVarsOfType ty then
1064 (tidy_env', ftv') = tidyOpenTyVar tidy_env ftv
1066 find_frees tv tidy_env' (ftv':acc) ftvs
1068 find_frees tv tidy_env acc ftvs
1071 escape_msg sig_tv tv globs frees
1072 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
1073 if not (null globs) then
1074 vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"),
1075 nest 2 (vcat globs)]
1076 else if not (null frees) then
1077 vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
1078 nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
1081 empty -- Sigh. It's really hard to give a good error message
1082 -- all the time. One bad case is an existential pattern match
1084 is_are | isSingleton frees = ptext SLIT("is")
1085 | otherwise = ptext SLIT("are")
1086 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
1087 | otherwise = ptext SLIT("It")
1089 vcat_first :: Int -> [SDoc] -> SDoc
1090 vcat_first n [] = empty
1091 vcat_first 0 (x:xs) = text "...others omitted..."
1092 vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
1095 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
1096 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
1099 These two context are used with checkSigTyVars
1102 sigCtxt :: [TcTyVar] -> TcThetaType -> TcTauType
1103 -> TidyEnv -> NF_TcM (TidyEnv, Message)
1104 sigCtxt sig_tyvars sig_theta sig_tau tidy_env
1105 = zonkTcType sig_tau `thenNF_Tc` \ actual_tau ->
1107 (env1, tidy_sig_tyvars) = tidyOpenTyVars tidy_env sig_tyvars
1108 (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
1109 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1110 msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
1111 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
1114 returnNF_Tc (env3, msg)
1116 sigPatCtxt bound_tvs bound_ids tidy_env
1117 = returnNF_Tc (env1,
1118 sep [ptext SLIT("When checking a pattern that binds"),
1119 nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
1121 show_ids = filter is_interesting bound_ids
1122 is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
1124 (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
1125 ppr_id id ty = ppr id <+> dcolon <+> ppr ty
1126 -- Don't zonk the types so we get the separate, un-unified versions