2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section{Type subsumption and unification}
8 -- Full-blown subsumption
9 tcSubOff, tcSubExp, tcGen, subFunTy, TcHoleType,
10 checkSigTyVars, checkSigTyVarsWrt, sigCtxt, findGlobals,
12 -- Various unifications
13 unifyTauTy, unifyTauTyList, unifyTauTyLists,
14 unifyFunTy, unifyListTy, unifyPArrTy, unifyTupleTy,
15 unifyKind, unifyKinds, unifyOpenTypeKind, unifyFunKind,
18 Coercion, ExprCoFn, PatCoFn,
19 (<$>), (<.>), mkCoercion,
20 idCoercion, isIdCoercion
24 #include "HsVersions.h"
27 import HsSyn ( HsExpr(..) )
28 import TcHsSyn ( TypecheckedHsExpr, TcPat, mkHsLet )
29 import TypeRep ( Type(..), SourceType(..), TyNote(..), openKindCon )
31 import TcRnMonad -- TcType, amongst others
32 import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
33 TcTyVarSet, TcThetaType, TyVarDetails(SigTv),
35 tcSplitAppTy_maybe, tcSplitTyConApp_maybe,
36 tcGetTyVar_maybe, tcGetTyVar,
37 mkTyConApp, mkFunTy, tyVarsOfType, mkPhiTy,
38 typeKind, tcSplitFunTy_maybe, mkForAllTys,
39 isHoleTyVar, isSkolemTyVar, isUserTyVar,
40 tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
41 eqKind, openTypeKind, liftedTypeKind, isTypeKind, mkArrowKind,
42 hasMoreBoxityInfo, allDistinctTyVars
44 import qualified Type ( getTyVar_maybe )
45 import Inst ( newDicts, instToId, tcInstCall )
46 import TcMType ( getTcTyVar, putTcTyVar, tcInstType, readHoleResult, newKindVar,
47 newTyVarTy, newTyVarTys, newOpenTypeKind, newHoleTyVarTy,
48 zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcTyVar )
49 import TcSimplify ( tcSimplifyCheck )
50 import TysWiredIn ( listTyCon, parrTyCon, mkListTy, mkPArrTy, mkTupleTy )
51 import TcEnv ( TcTyThing(..), tcGetGlobalTyVars, findGlobals )
52 import TyCon ( tyConArity, isTupleTyCon, tupleTyConBoxity )
53 import PprType ( pprType )
54 import Id ( Id, mkSysLocal, idType )
55 import Var ( Var, varName, tyVarKind )
56 import VarSet ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems )
58 import Name ( isSystemName, getSrcLoc )
59 import ErrUtils ( Message )
60 import BasicTypes ( Boxity, Arity, isBoxed )
61 import Util ( equalLength, notNull )
62 import Maybe ( isNothing )
68 * A hole is always filled in with an ordinary type, not another hole.
70 %************************************************************************
72 \subsection{Subsumption}
74 %************************************************************************
76 All the tcSub calls have the form
78 tcSub expected_ty offered_ty
80 offered_ty <= expected_ty
82 That is, that a value of type offered_ty is acceptable in
83 a place expecting a value of type expected_ty.
85 It returns a coercion function
86 co_fn :: offered_ty -> expected_ty
87 which takes an HsExpr of type offered_ty into one of type
91 type TcHoleType = TcSigmaType -- Either a TcSigmaType,
94 tcSubExp :: TcHoleType -> TcSigmaType -> TcM ExprCoFn
95 tcSubOff :: TcSigmaType -> TcHoleType -> TcM ExprCoFn
96 tcSub :: TcSigmaType -> TcSigmaType -> TcM ExprCoFn
99 These two check for holes
102 tcSubExp expected_ty offered_ty
103 = checkHole expected_ty offered_ty tcSub
105 tcSubOff expected_ty offered_ty
106 = checkHole offered_ty expected_ty (\ off exp -> tcSub exp off)
108 -- checkHole looks for a hole in its first arg;
109 -- If so, and it is uninstantiated, it fills in the hole
110 -- with its second arg
111 -- Otherwise it calls thing_inside, passing the two args, looking
112 -- through any instantiated hole
114 checkHole (TyVarTy tv) other_ty thing_inside
116 = getTcTyVar tv `thenM` \ maybe_ty ->
118 Just ty -> thing_inside ty other_ty
119 Nothing -> putTcTyVar tv other_ty `thenM_`
122 checkHole ty other_ty thing_inside
123 = thing_inside ty other_ty
126 No holes expected now. Add some error-check context info.
129 tcSub expected_ty actual_ty
130 = traceTc (text "tcSub" <+> details) `thenM_`
131 addErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
132 (tc_sub expected_ty expected_ty actual_ty actual_ty)
134 details = vcat [text "Expected:" <+> ppr expected_ty,
135 text "Actual: " <+> ppr actual_ty]
138 tc_sub carries the types before and after expanding type synonyms
141 tc_sub :: TcSigmaType -- expected_ty, before expanding synonyms
142 -> TcSigmaType -- ..and after
143 -> TcSigmaType -- actual_ty, before
144 -> TcSigmaType -- ..and after
147 -----------------------------------
149 tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty act_ty
150 tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty
152 -----------------------------------
153 -- Generalisation case
154 -- actual_ty: d:Eq b => b->b
155 -- expected_ty: forall a. Ord a => a->a
156 -- co_fn e /\a. \d2:Ord a. let d = eqFromOrd d2 in e
158 -- It is essential to do this *before* the specialisation case
159 -- Example: f :: (Eq a => a->a) -> ...
160 -- g :: Ord b => b->b
163 tc_sub exp_sty expected_ty act_sty actual_ty
164 | isSigmaTy expected_ty
165 = tcGen expected_ty (tyVarsOfType actual_ty) (
166 -- It's really important to check for escape wrt the free vars of
167 -- both expected_ty *and* actual_ty
168 \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
169 ) `thenM` \ (gen_fn, co_fn) ->
170 returnM (gen_fn <.> co_fn)
172 -----------------------------------
173 -- Specialisation case:
174 -- actual_ty: forall a. Ord a => a->a
175 -- expected_ty: Int -> Int
176 -- co_fn e = e Int dOrdInt
178 tc_sub exp_sty expected_ty act_sty actual_ty
179 | isSigmaTy actual_ty
180 = tcInstCall Rank2Origin actual_ty `thenM` \ (inst_fn, body_ty) ->
181 tc_sub exp_sty expected_ty body_ty body_ty `thenM` \ co_fn ->
182 returnM (co_fn <.> mkCoercion inst_fn)
184 -----------------------------------
187 tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
188 = tcSub_fun exp_arg exp_res act_arg act_res
190 -----------------------------------
191 -- Type variable meets function: imitate
193 -- NB 1: we can't just unify the type variable with the type
194 -- because the type might not be a tau-type, and we aren't
195 -- allowed to instantiate an ordinary type variable with
198 -- NB 2: can we short-cut to an error case?
199 -- when the arg/res is not a tau-type?
200 -- NO! e.g. f :: ((forall a. a->a) -> Int) -> Int
202 -- is perfectly fine!
204 tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv)
205 = ASSERT( not (isHoleTyVar tv) )
206 getTcTyVar tv `thenM` \ maybe_ty ->
208 Just ty -> tc_sub exp_sty exp_ty ty ty
209 Nothing -> imitateFun tv exp_sty `thenM` \ (act_arg, act_res) ->
210 tcSub_fun exp_arg exp_res act_arg act_res
212 tc_sub _ (TyVarTy tv) act_sty act_ty@(FunTy act_arg act_res)
213 = ASSERT( not (isHoleTyVar tv) )
214 getTcTyVar tv `thenM` \ maybe_ty ->
216 Just ty -> tc_sub ty ty act_sty act_ty
217 Nothing -> imitateFun tv act_sty `thenM` \ (exp_arg, exp_res) ->
218 tcSub_fun exp_arg exp_res act_arg act_res
220 -----------------------------------
222 -- If none of the above match, we revert to the plain unifier
223 tc_sub exp_sty expected_ty act_sty actual_ty
224 = uTys exp_sty expected_ty act_sty actual_ty `thenM_`
228 %************************************************************************
230 \subsection{Functions}
232 %************************************************************************
235 tcSub_fun exp_arg exp_res act_arg act_res
236 = tc_sub act_arg act_arg exp_arg exp_arg `thenM` \ co_fn_arg ->
237 tc_sub exp_res exp_res act_res act_res `thenM` \ co_fn_res ->
238 newUnique `thenM` \ uniq ->
240 -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
241 -- co_fn_res :: HsExpr act_res -> HsExpr exp_res
242 -- co_fn :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
243 arg_id = mkSysLocal FSLIT("sub") uniq exp_arg
244 coercion | isIdCoercion co_fn_arg,
245 isIdCoercion co_fn_res = idCoercion
246 | otherwise = mkCoercion co_fn
248 co_fn e = DictLam [arg_id]
249 (co_fn_res <$> (HsApp e (co_fn_arg <$> (HsVar arg_id))))
250 -- Slight hack; using a "DictLam" to get an ordinary simple lambda
251 -- HsVar arg_id :: HsExpr exp_arg
252 -- co_fn_arg $it :: HsExpr act_arg
253 -- HsApp e $it :: HsExpr act_res
254 -- co_fn_res $it :: HsExpr exp_res
258 imitateFun :: TcTyVar -> TcType -> TcM (TcType, TcType)
260 = ASSERT( not (isHoleTyVar tv) )
261 -- NB: tv is an *ordinary* tyvar and so are the new ones
263 -- Check that tv isn't a type-signature type variable
264 -- (This would be found later in checkSigTyVars, but
265 -- we get a better error message if we do it here.)
266 checkM (not (isSkolemTyVar tv))
267 (failWithTcM (unifyWithSigErr tv ty)) `thenM_`
269 newTyVarTy openTypeKind `thenM` \ arg ->
270 newTyVarTy openTypeKind `thenM` \ res ->
271 putTcTyVar tv (mkFunTy arg res) `thenM_`
276 %************************************************************************
278 \subsection{Generalisation}
280 %************************************************************************
283 tcGen :: TcSigmaType -- expected_ty
284 -> TcTyVarSet -- Extra tyvars that the universally
285 -- quantified tyvars of expected_ty
286 -- must not be unified
287 -> (TcRhoType -> TcM result) -- spec_ty
288 -> TcM (ExprCoFn, result)
289 -- The expression has type: spec_ty -> expected_ty
291 tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type
292 -- If not, the call is a no-op
293 = tcInstType SigTv expected_ty `thenM` \ (forall_tvs, theta, phi_ty) ->
295 -- Type-check the arg and unify with poly type
296 getLIE (thing_inside phi_ty) `thenM` \ (result, lie) ->
298 -- Check that the "forall_tvs" havn't been constrained
299 -- The interesting bit here is that we must include the free variables
300 -- of the expected_ty. Here's an example:
301 -- runST (newVar True)
302 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
303 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
304 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
305 -- So now s' isn't unconstrained because it's linked to a.
306 -- Conclusion: include the free vars of the expected_ty in the
307 -- list of "free vars" for the signature check.
309 newDicts SignatureOrigin theta `thenM` \ dicts ->
310 tcSimplifyCheck sig_msg forall_tvs dicts lie `thenM` \ inst_binds ->
313 zonkTcTyVars forall_tvs `thenM` \ forall_tys ->
314 traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
315 text "expected_ty" <+> ppr expected_ty,
316 text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr phi_ty,
317 text "free_tvs" <+> ppr free_tvs,
318 text "forall_tys" <+> ppr forall_tys]) `thenM_`
321 checkSigTyVarsWrt free_tvs forall_tvs `thenM` \ zonked_tvs ->
323 traceTc (text "tcGen:done") `thenM_`
326 -- This HsLet binds any Insts which came out of the simplification.
327 -- It's a bit out of place here, but using AbsBind involves inventing
328 -- a couple of new names which seems worse.
329 dict_ids = map instToId dicts
330 co_fn e = TyLam zonked_tvs (DictLam dict_ids (mkHsLet inst_binds e))
332 returnM (mkCoercion co_fn, result)
334 free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
335 sig_msg = ptext SLIT("type of an expression")
340 %************************************************************************
342 \subsection{Coercion functions}
344 %************************************************************************
347 type Coercion a = Maybe (a -> a)
348 -- Nothing => identity fn
350 type ExprCoFn = Coercion TypecheckedHsExpr
351 type PatCoFn = Coercion TcPat
353 (<.>) :: Coercion a -> Coercion a -> Coercion a -- Composition
354 Nothing <.> Nothing = Nothing
355 Nothing <.> Just f = Just f
356 Just f <.> Nothing = Just f
357 Just f1 <.> Just f2 = Just (f1 . f2)
359 (<$>) :: Coercion a -> a -> a
363 mkCoercion :: (a -> a) -> Coercion a
364 mkCoercion f = Just f
366 idCoercion :: Coercion a
369 isIdCoercion :: Coercion a -> Bool
370 isIdCoercion = isNothing
373 %************************************************************************
375 \subsection[Unify-exported]{Exported unification functions}
377 %************************************************************************
379 The exported functions are all defined as versions of some
380 non-exported generic functions.
382 Unify two @TauType@s. Dead straightforward.
385 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
386 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
387 = -- The unifier should only ever see tau-types
388 -- (no quantification whatsoever)
389 ASSERT2( isTauTy ty1, ppr ty1 )
390 ASSERT2( isTauTy ty2, ppr ty2 )
391 addErrCtxtM (unifyCtxt "type" ty1 ty2) $
395 @unifyTauTyList@ unifies corresponding elements of two lists of
396 @TauType@s. It uses @uTys@ to do the real work. The lists should be
397 of equal length. We charge down the list explicitly so that we can
398 complain if their lengths differ.
401 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM ()
402 unifyTauTyLists [] [] = returnM ()
403 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenM_`
404 unifyTauTyLists tys1 tys2
405 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
408 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
409 all together. It is used, for example, when typechecking explicit
410 lists, when all the elts should be of the same type.
413 unifyTauTyList :: [TcTauType] -> TcM ()
414 unifyTauTyList [] = returnM ()
415 unifyTauTyList [ty] = returnM ()
416 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenM_`
420 %************************************************************************
422 \subsection[Unify-uTys]{@uTys@: getting down to business}
424 %************************************************************************
426 @uTys@ is the heart of the unifier. Each arg happens twice, because
427 we want to report errors in terms of synomyms if poss. The first of
428 the pair is used in error messages only; it is always the same as the
429 second, except that if the first is a synonym then the second may be a
430 de-synonym'd version. This way we get better error messages.
432 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
435 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
436 -- ty1 is the *expected* type
438 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
439 -- ty2 is the *actual* type
442 -- Always expand synonyms (see notes at end)
443 -- (this also throws away FTVs)
444 uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
445 uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
447 -- Variables; go for uVar
448 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
449 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
450 -- "True" means args swapped
453 uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
454 | n1 == n2 = uTys t1 t1 t2 t2
455 uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
456 | c1 == c2 = unifyTauTyLists tys1 tys2
457 uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
458 | tc1 == tc2 = unifyTauTyLists tys1 tys2
460 -- Functions; just check the two parts
461 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
462 = uTys fun1 fun1 fun2 fun2 `thenM_` uTys arg1 arg1 arg2 arg2
464 -- Type constructors must match
465 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
466 | con1 == con2 && equalLength tys1 tys2
467 = unifyTauTyLists tys1 tys2
469 | con1 == openKindCon
470 -- When we are doing kind checking, we might match a kind '?'
471 -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and
472 -- (CCallable Int) and (CCallable Int#) are both OK
473 = unifyOpenTypeKind ps_ty2
475 -- Applications need a bit of care!
476 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
477 -- NB: we've already dealt with type variables and Notes,
478 -- so if one type is an App the other one jolly well better be too
479 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
480 = case tcSplitAppTy_maybe ty2 of
481 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenM_` uTys t1 t1 t2 t2
482 Nothing -> unifyMisMatch ps_ty1 ps_ty2
484 -- Now the same, but the other way round
485 -- Don't swap the types, because the error messages get worse
486 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
487 = case tcSplitAppTy_maybe ty1 of
488 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenM_` uTys t1 t1 t2 t2
489 Nothing -> unifyMisMatch ps_ty1 ps_ty2
491 -- Not expecting for-alls in unification
492 -- ... but the error message from the unifyMisMatch more informative
493 -- than a panic message!
495 -- Anything else fails
496 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
502 If you are tempted to make a short cut on synonyms, as in this
506 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
507 -- NO = if (con1 == con2) then
508 -- NO -- Good news! Same synonym constructors, so we can shortcut
509 -- NO -- by unifying their arguments and ignoring their expansions.
510 -- NO unifyTauTypeLists args1 args2
512 -- NO -- Never mind. Just expand them and try again
516 then THINK AGAIN. Here is the whole story, as detected and reported
517 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
519 Here's a test program that should detect the problem:
523 x = (1 :: Bogus Char) :: Bogus Bool
526 The problem with [the attempted shortcut code] is that
530 is not a sufficient condition to be able to use the shortcut!
531 You also need to know that the type synonym actually USES all
532 its arguments. For example, consider the following type synonym
533 which does not use all its arguments.
538 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
539 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
540 would fail, even though the expanded forms (both \tr{Int}) should
543 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
544 unnecessarily bind \tr{t} to \tr{Char}.
546 ... You could explicitly test for the problem synonyms and mark them
547 somehow as needing expansion, perhaps also issuing a warning to the
552 %************************************************************************
554 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
556 %************************************************************************
558 @uVar@ is called when at least one of the types being unified is a
559 variable. It does {\em not} assume that the variable is a fixed point
560 of the substitution; rather, notice that @uVar@ (defined below) nips
561 back into @uTys@ if it turns out that the variable is already bound.
564 uVar :: Bool -- False => tyvar is the "expected"
565 -- True => ty is the "expected" thing
567 -> TcTauType -> TcTauType -- printing and real versions
570 uVar swapped tv1 ps_ty2 ty2
571 = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2)) `thenM_`
572 getTcTyVar tv1 `thenM` \ maybe_ty1 ->
574 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
575 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
576 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
578 -- Expand synonyms; ignore FTVs
579 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
580 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
583 -- The both-type-variable case
584 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
586 -- Same type variable => no-op
590 -- Distinct type variables
591 -- ASSERT maybe_ty1 /= Just
593 = getTcTyVar tv2 `thenM` \ maybe_ty2 ->
595 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
599 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
600 putTcTyVar tv2 (TyVarTy tv1) `thenM_`
604 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
605 putTcTyVar tv1 ps_ty2 `thenM_`
610 update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
611 -- Try to get rid of open type variables as soon as poss
613 nicer_to_update_tv2 = isUserTyVar tv1
614 -- Don't unify a signature type variable if poss
615 || isSystemName (varName tv2)
616 -- Try to update sys-y type variables in preference to sig-y ones
618 -- Second one isn't a type variable
619 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
620 = -- Check that tv1 isn't a type-signature type variable
621 checkM (not (isSkolemTyVar tv1))
622 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenM_`
624 -- Do the occurs check, and check that we are not
625 -- unifying a type variable with a polytype
626 -- Returns a zonked type ready for the update
627 checkValue tv1 ps_ty2 non_var_ty2 `thenM` \ ty2 ->
629 -- Check that the kinds match
630 checkKinds swapped tv1 ty2 `thenM_`
632 -- Perform the update
633 putTcTyVar tv1 ty2 `thenM_`
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, which ensures that
641 -- its kind has as much boxity information visible as possible.
642 | tk2 `hasMoreBoxityInfo` tk1 = returnM ()
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 = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
653 (k1,k2) | swapped = (tk2,tk1)
654 | otherwise = (tk1,tk2)
660 checkValue tv1 ps_ty2 non_var_ty2
661 -- Do the occurs check, and check that we are not
662 -- unifying a type variable with a polytype
663 -- Return the type to update the type variable with, or fail
665 -- Basically we want to update tv1 := ps_ty2
666 -- because ps_ty2 has type-synonym info, which improves later error messages
671 -- f :: (A a -> a -> ()) -> ()
675 -- x = f (\ x p -> p x)
677 -- In the application (p x), we try to match "t" with "A t". If we go
678 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
679 -- an infinite loop later.
680 -- But we should not reject the program, because A t = ().
681 -- Rather, we should bind t to () (= non_var_ty2).
683 -- That's why we have this two-state occurs-check
684 = zonkTcType ps_ty2 `thenM` \ ps_ty2' ->
685 case okToUnifyWith tv1 ps_ty2' of {
686 Nothing -> returnM ps_ty2' ; -- Success
689 zonkTcType non_var_ty2 `thenM` \ non_var_ty2' ->
690 case okToUnifyWith tv1 non_var_ty2' of
691 Nothing -> -- This branch rarely succeeds, except in strange cases
692 -- like that in the example above
695 Just problem -> failWithTcM (unifyCheck problem tv1 ps_ty2')
698 data Problem = OccurCheck | NotMonoType
700 okToUnifyWith :: TcTyVar -> TcType -> Maybe Problem
701 -- (okToUnifyWith tv ty) checks whether it's ok to unify
704 -- Just p => not ok, problem p
709 ok (TyVarTy tv') | tv == tv' = Just OccurCheck
710 | otherwise = Nothing
711 ok (AppTy t1 t2) = ok t1 `and` ok t2
712 ok (FunTy t1 t2) = ok t1 `and` ok t2
713 ok (TyConApp _ ts) = oks ts
714 ok (ForAllTy _ _) = Just NotMonoType
715 ok (SourceTy st) = ok_st st
716 ok (NoteTy (FTVNote _) t) = ok t
717 ok (NoteTy (SynNote t1) t2) = ok t1 `and` ok t2
718 -- Type variables may be free in t1 but not t2
719 -- A forall may be in t2 but not t1
721 oks ts = foldr (and . ok) Nothing ts
723 ok_st (ClassP _ ts) = oks ts
724 ok_st (IParam _ t) = ok t
725 ok_st (NType _ ts) = oks ts
728 Just p `and` m = Just p
731 %************************************************************************
733 \subsection[Unify-fun]{@unifyFunTy@}
735 %************************************************************************
737 @subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
738 creation of type variables.
740 * subFunTy is used when we might be faced with a "hole" type variable,
741 in which case we should create two new holes.
743 * unifyFunTy is used when we expect to encounter only "ordinary"
744 type variables, so we should create new ordinary type variables
747 subFunTy :: TcHoleType -- Fail if ty isn't a function type
748 -- If it's a hole, make two holes, feed them to...
749 -> (TcHoleType -> TcHoleType -> TcM a) -- the thing inside
750 -> TcM a -- and bind the function type to the hole
752 subFunTy ty@(TyVarTy tyvar) thing_inside
754 = -- This is the interesting case
755 getTcTyVar tyvar `thenM` \ maybe_ty ->
757 Just ty' -> subFunTy ty' thing_inside ;
760 newHoleTyVarTy `thenM` \ arg_ty ->
761 newHoleTyVarTy `thenM` \ res_ty ->
764 thing_inside arg_ty res_ty `thenM` \ answer ->
766 -- Extract the answers
767 readHoleResult arg_ty `thenM` \ arg_ty' ->
768 readHoleResult res_ty `thenM` \ res_ty' ->
770 -- Write the answer into the incoming hole
771 putTcTyVar tyvar (mkFunTy arg_ty' res_ty') `thenM_`
773 -- And return the answer
776 subFunTy ty thing_inside
777 = unifyFunTy ty `thenM` \ (arg,res) ->
781 unifyFunTy :: TcRhoType -- Fail if ty isn't a function type
782 -> TcM (TcType, TcType) -- otherwise return arg and result types
784 unifyFunTy ty@(TyVarTy tyvar)
785 = ASSERT( not (isHoleTyVar tyvar) )
786 getTcTyVar tyvar `thenM` \ maybe_ty ->
788 Just ty' -> unifyFunTy ty'
789 Nothing -> unify_fun_ty_help ty
792 = case tcSplitFunTy_maybe ty of
793 Just arg_and_res -> returnM arg_and_res
794 Nothing -> unify_fun_ty_help ty
796 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
797 = newTyVarTy openTypeKind `thenM` \ arg ->
798 newTyVarTy openTypeKind `thenM` \ res ->
799 unifyTauTy ty (mkFunTy arg res) `thenM_`
804 unifyListTy :: TcType -- expected list type
805 -> TcM TcType -- list element type
807 unifyListTy ty@(TyVarTy tyvar)
808 = getTcTyVar tyvar `thenM` \ maybe_ty ->
810 Just ty' -> unifyListTy ty'
811 other -> unify_list_ty_help ty
814 = case tcSplitTyConApp_maybe ty of
815 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnM arg_ty
816 other -> unify_list_ty_help ty
818 unify_list_ty_help ty -- Revert to ordinary unification
819 = newTyVarTy liftedTypeKind `thenM` \ elt_ty ->
820 unifyTauTy ty (mkListTy elt_ty) `thenM_`
823 -- variant for parallel arrays
825 unifyPArrTy :: TcType -- expected list type
826 -> TcM TcType -- list element type
828 unifyPArrTy ty@(TyVarTy tyvar)
829 = getTcTyVar tyvar `thenM` \ maybe_ty ->
831 Just ty' -> unifyPArrTy ty'
832 _ -> unify_parr_ty_help ty
834 = case tcSplitTyConApp_maybe ty of
835 Just (tycon, [arg_ty]) | tycon == parrTyCon -> returnM arg_ty
836 _ -> unify_parr_ty_help ty
838 unify_parr_ty_help ty -- Revert to ordinary unification
839 = newTyVarTy liftedTypeKind `thenM` \ elt_ty ->
840 unifyTauTy ty (mkPArrTy elt_ty) `thenM_`
845 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
846 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
847 = getTcTyVar tyvar `thenM` \ maybe_ty ->
849 Just ty' -> unifyTupleTy boxity arity ty'
850 other -> unify_tuple_ty_help boxity arity ty
852 unifyTupleTy boxity arity ty
853 = case tcSplitTyConApp_maybe ty of
854 Just (tycon, arg_tys)
856 && tyConArity tycon == arity
857 && tupleTyConBoxity tycon == boxity
859 other -> unify_tuple_ty_help boxity arity ty
861 unify_tuple_ty_help boxity arity ty
862 = newTyVarTys arity kind `thenM` \ arg_tys ->
863 unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenM_`
866 kind | isBoxed boxity = liftedTypeKind
867 | otherwise = openTypeKind
871 %************************************************************************
873 \subsection{Kind unification}
875 %************************************************************************
878 unifyKind :: TcKind -- Expected
881 unifyKind k1 k2 = uTys k1 k1 k2 k2
883 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
884 unifyKinds [] [] = returnM ()
885 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenM_`
887 unifyKinds _ _ = panic "unifyKinds: length mis-match"
891 unifyOpenTypeKind :: TcKind -> TcM ()
892 -- Ensures that the argument kind is of the form (Type bx)
893 -- for some boxity bx
895 unifyOpenTypeKind ty@(TyVarTy tyvar)
896 = getTcTyVar tyvar `thenM` \ maybe_ty ->
898 Just ty' -> unifyOpenTypeKind ty'
899 other -> unify_open_kind_help ty
902 | isTypeKind ty = returnM ()
903 | otherwise = unify_open_kind_help ty
905 unify_open_kind_help ty -- Revert to ordinary unification
906 = newOpenTypeKind `thenM` \ open_kind ->
907 unifyKind ty open_kind
911 unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
912 -- Like unifyFunTy, but does not fail; instead just returns Nothing
914 unifyFunKind (TyVarTy tyvar)
915 = getTcTyVar tyvar `thenM` \ maybe_ty ->
917 Just fun_kind -> unifyFunKind fun_kind
918 Nothing -> newKindVar `thenM` \ arg_kind ->
919 newKindVar `thenM` \ res_kind ->
920 putTcTyVar tyvar (mkArrowKind arg_kind res_kind) `thenM_`
921 returnM (Just (arg_kind,res_kind))
923 unifyFunKind (FunTy arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
924 unifyFunKind (NoteTy _ ty) = unifyFunKind ty
925 unifyFunKind other = returnM Nothing
928 %************************************************************************
930 \subsection[Unify-context]{Errors and contexts}
932 %************************************************************************
938 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
939 = zonkTcType ty1 `thenM` \ ty1' ->
940 zonkTcType ty2 `thenM` \ ty2' ->
941 returnM (err ty1' ty2')
946 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
947 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
950 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
952 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
953 -- tv1 is zonked already
954 = zonkTcType ty2 `thenM` \ ty2' ->
957 err ty2 = (env2, ptext SLIT("When matching types") <+>
958 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
960 (pp_expected, pp_actual) | swapped = (pp2, pp1)
961 | otherwise = (pp1, pp2)
962 (env1, tv1') = tidyOpenTyVar tidy_env tv1
963 (env2, ty2') = tidyOpenType env1 ty2
967 unifyMisMatch ty1 ty2
968 = zonkTcType ty1 `thenM` \ ty1' ->
969 zonkTcType ty2 `thenM` \ ty2' ->
971 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
972 msg = hang (ptext SLIT("Couldn't match"))
973 4 (sep [quotes (ppr tidy_ty1),
974 ptext SLIT("against"),
975 quotes (ppr tidy_ty2)])
977 failWithTcM (env, msg)
979 unifyWithSigErr tyvar ty
980 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
981 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
983 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
984 (env2, tidy_ty) = tidyOpenType env1 ty
986 unifyCheck problem tyvar ty
988 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
990 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
991 (env2, tidy_ty) = tidyOpenType env1 ty
993 msg = case problem of
994 OccurCheck -> ptext SLIT("Occurs check: cannot construct the infinite type:")
995 NotMonoType -> ptext SLIT("Cannot unify a type variable with a type scheme:")
1000 %************************************************************************
1002 \subsection{Checking signature type variables}
1004 %************************************************************************
1006 @checkSigTyVars@ is used after the type in a type signature has been unified with
1007 the actual type found. It then checks that the type variables of the type signature
1009 (a) Still all type variables
1010 eg matching signature [a] against inferred type [(p,q)]
1011 [then a will be unified to a non-type variable]
1013 (b) Still all distinct
1014 eg matching signature [(a,b)] against inferred type [(p,p)]
1015 [then a and b will be unified together]
1017 (c) Not mentioned in the environment
1018 eg the signature for f in this:
1024 Here, f is forced to be monorphic by the free occurence of x.
1026 (d) Not (unified with another type variable that is) in scope.
1027 eg f x :: (r->r) = (\y->y) :: forall a. a->r
1028 when checking the expression type signature, we find that
1029 even though there is nothing in scope whose type mentions r,
1030 nevertheless the type signature for the expression isn't right.
1032 Another example is in a class or instance declaration:
1034 op :: forall b. a -> b
1036 Here, b gets unified with a
1038 Before doing this, the substitution is applied to the signature type variable.
1040 We used to have the notion of a "DontBind" type variable, which would
1041 only be bound to itself or nothing. Then points (a) and (b) were
1042 self-checking. But it gave rise to bogus consequential error messages.
1045 f = (*) -- Monomorphic
1047 g :: Num a => a -> a
1050 Here, we get a complaint when checking the type signature for g,
1051 that g isn't polymorphic enough; but then we get another one when
1052 dealing with the (Num x) context arising from f's definition;
1053 we try to unify x with Int (to default it), but find that x has already
1054 been unified with the DontBind variable "a" from g's signature.
1055 This is really a problem with side-effecting unification; we'd like to
1056 undo g's effects when its type signature fails, but unification is done
1057 by side effect, so we can't (easily).
1059 So we revert to ordinary type variables for signatures, and try to
1060 give a helpful message in checkSigTyVars.
1063 checkSigTyVars :: [TcTyVar] -> TcM [TcTyVar]
1064 checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
1066 checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM [TcTyVar]
1067 checkSigTyVarsWrt extra_tvs sig_tvs
1068 = zonkTcTyVarsAndFV (varSetElems extra_tvs) `thenM` \ extra_tvs' ->
1069 check_sig_tyvars extra_tvs' sig_tvs
1072 :: TcTyVarSet -- Global type variables. The universally quantified
1073 -- tyvars should not mention any of these
1074 -- Guaranteed already zonked.
1075 -> [TcTyVar] -- Universally-quantified type variables in the signature
1076 -- Not guaranteed zonked.
1077 -> TcM [TcTyVar] -- Zonked signature type variables
1079 check_sig_tyvars extra_tvs []
1081 check_sig_tyvars extra_tvs sig_tvs
1082 = zonkTcTyVars sig_tvs `thenM` \ sig_tys ->
1083 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
1085 env_tvs = gbl_tvs `unionVarSet` extra_tvs
1087 traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tys,
1088 text "gbl_tvs" <+> ppr gbl_tvs,
1089 text "extra_tvs" <+> ppr extra_tvs])) `thenM_`
1091 checkM (allDistinctTyVars sig_tys env_tvs)
1092 (complain sig_tys env_tvs) `thenM_`
1094 returnM (map (tcGetTyVar "checkSigTyVars") sig_tys)
1097 complain sig_tys globals
1098 = -- "check" checks each sig tyvar in turn
1100 (env2, emptyVarEnv, [])
1101 (tidy_tvs `zip` tidy_tys) `thenM` \ (env3, _, msgs) ->
1103 failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
1105 (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs
1106 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
1108 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
1110 check (tidy_env, acc, msgs) (sig_tyvar,ty)
1111 -- sig_tyvar is from the signature;
1112 -- ty is what you get if you zonk sig_tyvar and then tidy it
1114 -- acc maps a zonked type variable back to a signature type variable
1115 = case tcGetTyVar_maybe ty of {
1116 Nothing -> -- Error (a)!
1117 returnM (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
1121 case lookupVarEnv acc tv of {
1122 Just sig_tyvar' -> -- Error (b)!
1123 returnM (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
1125 thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
1129 if tv `elemVarSet` globals -- Error (c) or (d)! Type variable escapes
1130 -- The least comprehensible, so put it last
1132 -- get the local TcIds and TyVars from the environment,
1133 -- and pass them to find_globals (they might have tv free)
1134 then findGlobals (unitVarSet tv) tidy_env `thenM` \ (tidy_env1, globs) ->
1135 returnM (tidy_env1, acc, escape_msg sig_tyvar tv globs : msgs)
1138 returnM (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
1144 -----------------------
1145 escape_msg sig_tv tv globs
1146 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
1147 if notNull globs then
1148 vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"),
1149 nest 2 (vcat globs)]
1151 empty -- Sigh. It's really hard to give a good error message
1152 -- all the time. One bad case is an existential pattern match.
1153 -- We rely on the "When..." context to help.
1155 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
1156 | otherwise = ptext SLIT("It")
1159 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
1160 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
1163 These two context are used with checkSigTyVars
1166 sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
1167 -> TidyEnv -> TcM (TidyEnv, Message)
1168 sigCtxt id sig_tvs sig_theta sig_tau tidy_env
1169 = zonkTcType sig_tau `thenM` \ actual_tau ->
1171 (env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs
1172 (env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
1173 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1174 sub_msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
1175 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
1177 msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id),