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,
12 -- Various unifications
13 unifyTauTy, unifyTauTyList, unifyTauTyLists,
14 unifyFunTy, unifyListTy, unifyPArrTy, 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, mkHsLet )
29 import TypeRep ( Type(..), SourceType(..), TyNote(..),
30 openKindCon, typeCon )
32 import TcRnMonad -- TcType, amongst others
33 import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
34 TcTyVarSet, TcThetaType, TyVarDetails(SigTv),
36 tcSplitAppTy_maybe, tcSplitTyConApp_maybe,
37 tcGetTyVar_maybe, tcGetTyVar,
38 mkTyConApp, mkFunTy, tyVarsOfType, mkPhiTy,
39 typeKind, tcSplitFunTy_maybe, mkForAllTys,
40 isHoleTyVar, isSkolemTyVar, isUserTyVar,
41 tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
42 eqKind, openTypeKind, liftedTypeKind, isTypeKind,
43 hasMoreBoxityInfo, tyVarBindingInfo, allDistinctTyVars
45 import qualified Type ( getTyVar_maybe )
46 import Inst ( newDicts, instToId, tcInstCall )
47 import TcMType ( getTcTyVar, putTcTyVar, tcInstType, readHoleResult,
48 newTyVarTy, newTyVarTys, newBoxityVar, newHoleTyVarTy,
49 zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcTyVar )
50 import TcSimplify ( tcSimplifyCheck )
51 import TysWiredIn ( listTyCon, parrTyCon, mkListTy, mkPArrTy, mkTupleTy )
52 import TcEnv ( TcTyThing(..), tcGetGlobalTyVars, getLclEnvElts )
53 import TyCon ( tyConArity, isTupleTyCon, tupleTyConBoxity )
54 import PprType ( pprType )
55 import Id ( Id, mkSysLocal, idType )
56 import Var ( Var, varName, tyVarKind )
57 import VarSet ( emptyVarSet, unionVarSet, elemVarSet, varSetElems )
59 import Name ( isSystemName, getSrcLoc )
60 import ErrUtils ( Message )
61 import BasicTypes ( Boxity, Arity, isBoxed )
62 import Util ( equalLength, notNull )
63 import Maybe ( isNothing )
69 * A hole is always filled in with an ordinary type, not another hole.
71 %************************************************************************
73 \subsection{Subsumption}
75 %************************************************************************
77 All the tcSub calls have the form
79 tcSub expected_ty offered_ty
81 offered_ty <= expected_ty
83 That is, that a value of type offered_ty is acceptable in
84 a place expecting a value of type expected_ty.
86 It returns a coercion function
87 co_fn :: offered_ty -> expected_ty
88 which takes an HsExpr of type offered_ty into one of type
92 type TcHoleType = TcSigmaType -- Either a TcSigmaType,
95 tcSubExp :: TcHoleType -> TcSigmaType -> TcM ExprCoFn
96 tcSubOff :: TcSigmaType -> TcHoleType -> TcM ExprCoFn
97 tcSub :: TcSigmaType -> TcSigmaType -> TcM ExprCoFn
100 These two check for holes
103 tcSubExp expected_ty offered_ty
104 = checkHole expected_ty offered_ty tcSub
106 tcSubOff expected_ty offered_ty
107 = checkHole offered_ty expected_ty (\ off exp -> tcSub exp off)
109 -- checkHole looks for a hole in its first arg;
110 -- If so, and it is uninstantiated, it fills in the hole
111 -- with its second arg
112 -- Otherwise it calls thing_inside, passing the two args, looking
113 -- through any instantiated hole
115 checkHole (TyVarTy tv) other_ty thing_inside
117 = getTcTyVar tv `thenM` \ maybe_ty ->
119 Just ty -> thing_inside ty other_ty
120 Nothing -> putTcTyVar tv other_ty `thenM_`
123 checkHole ty other_ty thing_inside
124 = thing_inside ty other_ty
127 No holes expected now. Add some error-check context info.
130 tcSub expected_ty actual_ty
131 = traceTc (text "tcSub" <+> details) `thenM_`
132 addErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
133 (tc_sub expected_ty expected_ty actual_ty actual_ty)
135 details = vcat [text "Expected:" <+> ppr expected_ty,
136 text "Actual: " <+> ppr actual_ty]
139 tc_sub carries the types before and after expanding type synonyms
142 tc_sub :: TcSigmaType -- expected_ty, before expanding synonyms
143 -> TcSigmaType -- ..and after
144 -> TcSigmaType -- actual_ty, before
145 -> TcSigmaType -- ..and after
148 -----------------------------------
150 tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty act_ty
151 tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty
153 -----------------------------------
154 -- Generalisation case
155 -- actual_ty: d:Eq b => b->b
156 -- expected_ty: forall a. Ord a => a->a
157 -- co_fn e /\a. \d2:Ord a. let d = eqFromOrd d2 in e
159 -- It is essential to do this *before* the specialisation case
160 -- Example: f :: (Eq a => a->a) -> ...
161 -- g :: Ord b => b->b
164 tc_sub exp_sty expected_ty act_sty actual_ty
165 | isSigmaTy expected_ty
166 = tcGen expected_ty (tyVarsOfType actual_ty) (
167 -- It's really important to check for escape wrt the free vars of
168 -- both expected_ty *and* actual_ty
169 \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
170 ) `thenM` \ (gen_fn, co_fn) ->
171 returnM (gen_fn <.> co_fn)
173 -----------------------------------
174 -- Specialisation case:
175 -- actual_ty: forall a. Ord a => a->a
176 -- expected_ty: Int -> Int
177 -- co_fn e = e Int dOrdInt
179 tc_sub exp_sty expected_ty act_sty actual_ty
180 | isSigmaTy actual_ty
181 = tcInstCall Rank2Origin actual_ty `thenM` \ (inst_fn, body_ty) ->
182 tc_sub exp_sty expected_ty body_ty body_ty `thenM` \ co_fn ->
183 returnM (co_fn <.> mkCoercion inst_fn)
185 -----------------------------------
188 tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
189 = tcSub_fun exp_arg exp_res act_arg act_res
191 -----------------------------------
192 -- Type variable meets function: imitate
194 -- NB 1: we can't just unify the type variable with the type
195 -- because the type might not be a tau-type, and we aren't
196 -- allowed to instantiate an ordinary type variable with
199 -- NB 2: can we short-cut to an error case?
200 -- when the arg/res is not a tau-type?
201 -- NO! e.g. f :: ((forall a. a->a) -> Int) -> Int
203 -- is perfectly fine!
205 tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv)
206 = ASSERT( not (isHoleTyVar tv) )
207 getTcTyVar tv `thenM` \ maybe_ty ->
209 Just ty -> tc_sub exp_sty exp_ty ty ty
210 Nothing -> imitateFun tv exp_sty `thenM` \ (act_arg, act_res) ->
211 tcSub_fun exp_arg exp_res act_arg act_res
213 tc_sub _ (TyVarTy tv) act_sty act_ty@(FunTy act_arg act_res)
214 = ASSERT( not (isHoleTyVar tv) )
215 getTcTyVar tv `thenM` \ maybe_ty ->
217 Just ty -> tc_sub ty ty act_sty act_ty
218 Nothing -> imitateFun tv act_sty `thenM` \ (exp_arg, exp_res) ->
219 tcSub_fun exp_arg exp_res act_arg act_res
221 -----------------------------------
223 -- If none of the above match, we revert to the plain unifier
224 tc_sub exp_sty expected_ty act_sty actual_ty
225 = uTys exp_sty expected_ty act_sty actual_ty `thenM_`
229 %************************************************************************
231 \subsection{Functions}
233 %************************************************************************
236 tcSub_fun exp_arg exp_res act_arg act_res
237 = tc_sub act_arg act_arg exp_arg exp_arg `thenM` \ co_fn_arg ->
238 tc_sub exp_res exp_res act_res act_res `thenM` \ co_fn_res ->
239 newUnique `thenM` \ uniq ->
241 -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
242 -- co_fn_res :: HsExpr act_res -> HsExpr exp_res
243 -- co_fn :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
244 arg_id = mkSysLocal FSLIT("sub") uniq exp_arg
245 coercion | isIdCoercion co_fn_arg,
246 isIdCoercion co_fn_res = idCoercion
247 | otherwise = mkCoercion co_fn
249 co_fn e = DictLam [arg_id]
250 (co_fn_res <$> (HsApp e (co_fn_arg <$> (HsVar arg_id))))
251 -- Slight hack; using a "DictLam" to get an ordinary simple lambda
252 -- HsVar arg_id :: HsExpr exp_arg
253 -- co_fn_arg $it :: HsExpr act_arg
254 -- HsApp e $it :: HsExpr act_res
255 -- co_fn_res $it :: HsExpr exp_res
259 imitateFun :: TcTyVar -> TcType -> TcM (TcType, TcType)
261 = ASSERT( not (isHoleTyVar tv) )
262 -- NB: tv is an *ordinary* tyvar and so are the new ones
264 -- Check that tv isn't a type-signature type variable
265 -- (This would be found later in checkSigTyVars, but
266 -- we get a better error message if we do it here.)
267 checkM (not (isSkolemTyVar tv))
268 (failWithTcM (unifyWithSigErr tv ty)) `thenM_`
270 newTyVarTy openTypeKind `thenM` \ arg ->
271 newTyVarTy openTypeKind `thenM` \ res ->
272 putTcTyVar tv (mkFunTy arg res) `thenM_`
277 %************************************************************************
279 \subsection{Generalisation}
281 %************************************************************************
284 tcGen :: TcSigmaType -- expected_ty
285 -> TcTyVarSet -- Extra tyvars that the universally
286 -- quantified tyvars of expected_ty
287 -- must not be unified
288 -> (TcRhoType -> TcM result) -- spec_ty
289 -> TcM (ExprCoFn, result)
290 -- The expression has type: spec_ty -> expected_ty
292 tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type
293 -- If not, the call is a no-op
294 = tcInstType SigTv expected_ty `thenM` \ (forall_tvs, theta, phi_ty) ->
296 -- Type-check the arg and unify with poly type
297 getLIE (thing_inside phi_ty) `thenM` \ (result, lie) ->
299 -- Check that the "forall_tvs" havn't been constrained
300 -- The interesting bit here is that we must include the free variables
301 -- of the expected_ty. Here's an example:
302 -- runST (newVar True)
303 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
304 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
305 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
306 -- So now s' isn't unconstrained because it's linked to a.
307 -- Conclusion: include the free vars of the expected_ty in the
308 -- list of "free vars" for the signature check.
310 newDicts SignatureOrigin theta `thenM` \ dicts ->
311 tcSimplifyCheck sig_msg forall_tvs dicts lie `thenM` \ inst_binds ->
314 zonkTcTyVars forall_tvs `thenM` \ forall_tys ->
315 traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
316 text "expected_ty" <+> ppr expected_ty,
317 text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr phi_ty,
318 text "free_tvs" <+> ppr free_tvs,
319 text "forall_tys" <+> ppr forall_tys]) `thenM_`
322 checkSigTyVarsWrt free_tvs forall_tvs `thenM` \ zonked_tvs ->
324 traceTc (text "tcGen:done") `thenM_`
327 -- This HsLet binds any Insts which came out of the simplification.
328 -- It's a bit out of place here, but using AbsBind involves inventing
329 -- a couple of new names which seems worse.
330 dict_ids = map instToId dicts
331 co_fn e = TyLam zonked_tvs (DictLam dict_ids (mkHsLet inst_binds e))
333 returnM (mkCoercion co_fn, result)
335 free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
336 sig_msg = ptext SLIT("type of an expression")
341 %************************************************************************
343 \subsection{Coercion functions}
345 %************************************************************************
348 type Coercion a = Maybe (a -> a)
349 -- Nothing => identity fn
351 type ExprCoFn = Coercion TypecheckedHsExpr
352 type PatCoFn = Coercion TcPat
354 (<.>) :: Coercion a -> Coercion a -> Coercion a -- Composition
355 Nothing <.> Nothing = Nothing
356 Nothing <.> Just f = Just f
357 Just f <.> Nothing = Just f
358 Just f1 <.> Just f2 = Just (f1 . f2)
360 (<$>) :: Coercion a -> a -> a
364 mkCoercion :: (a -> a) -> Coercion a
365 mkCoercion f = Just f
367 idCoercion :: Coercion a
370 isIdCoercion :: Coercion a -> Bool
371 isIdCoercion = isNothing
374 %************************************************************************
376 \subsection[Unify-exported]{Exported unification functions}
378 %************************************************************************
380 The exported functions are all defined as versions of some
381 non-exported generic functions.
383 Unify two @TauType@s. Dead straightforward.
386 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
387 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
388 = -- The unifier should only ever see tau-types
389 -- (no quantification whatsoever)
390 ASSERT2( isTauTy ty1, ppr ty1 )
391 ASSERT2( isTauTy ty2, ppr ty2 )
392 addErrCtxtM (unifyCtxt "type" ty1 ty2) $
396 @unifyTauTyList@ unifies corresponding elements of two lists of
397 @TauType@s. It uses @uTys@ to do the real work. The lists should be
398 of equal length. We charge down the list explicitly so that we can
399 complain if their lengths differ.
402 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM ()
403 unifyTauTyLists [] [] = returnM ()
404 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenM_`
405 unifyTauTyLists tys1 tys2
406 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
409 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
410 all together. It is used, for example, when typechecking explicit
411 lists, when all the elts should be of the same type.
414 unifyTauTyList :: [TcTauType] -> TcM ()
415 unifyTauTyList [] = returnM ()
416 unifyTauTyList [ty] = returnM ()
417 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenM_`
421 %************************************************************************
423 \subsection[Unify-uTys]{@uTys@: getting down to business}
425 %************************************************************************
427 @uTys@ is the heart of the unifier. Each arg happens twice, because
428 we want to report errors in terms of synomyms if poss. The first of
429 the pair is used in error messages only; it is always the same as the
430 second, except that if the first is a synonym then the second may be a
431 de-synonym'd version. This way we get better error messages.
433 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
436 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
437 -- ty1 is the *expected* type
439 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
440 -- ty2 is the *actual* type
443 -- Always expand synonyms (see notes at end)
444 -- (this also throws away FTVs)
445 uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
446 uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
448 -- Variables; go for uVar
449 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
450 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
451 -- "True" means args swapped
454 uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
455 | n1 == n2 = uTys t1 t1 t2 t2
456 uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
457 | c1 == c2 = unifyTauTyLists tys1 tys2
458 uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
459 | tc1 == tc2 = unifyTauTyLists tys1 tys2
461 -- Functions; just check the two parts
462 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
463 = uTys fun1 fun1 fun2 fun2 `thenM_` uTys arg1 arg1 arg2 arg2
465 -- Type constructors must match
466 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
467 | con1 == con2 && equalLength tys1 tys2
468 = unifyTauTyLists tys1 tys2
470 | con1 == openKindCon
471 -- When we are doing kind checking, we might match a kind '?'
472 -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and
473 -- (CCallable Int) and (CCallable Int#) are both OK
474 = unifyOpenTypeKind ps_ty2
476 -- Applications need a bit of care!
477 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
478 -- NB: we've already dealt with type variables and Notes,
479 -- so if one type is an App the other one jolly well better be too
480 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
481 = case tcSplitAppTy_maybe ty2 of
482 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenM_` uTys t1 t1 t2 t2
483 Nothing -> unifyMisMatch ps_ty1 ps_ty2
485 -- Now the same, but the other way round
486 -- Don't swap the types, because the error messages get worse
487 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
488 = case tcSplitAppTy_maybe ty1 of
489 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenM_` uTys t1 t1 t2 t2
490 Nothing -> unifyMisMatch ps_ty1 ps_ty2
492 -- Not expecting for-alls in unification
493 -- ... but the error message from the unifyMisMatch more informative
494 -- than a panic message!
496 -- Anything else fails
497 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
503 If you are tempted to make a short cut on synonyms, as in this
507 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
508 -- NO = if (con1 == con2) then
509 -- NO -- Good news! Same synonym constructors, so we can shortcut
510 -- NO -- by unifying their arguments and ignoring their expansions.
511 -- NO unifyTauTypeLists args1 args2
513 -- NO -- Never mind. Just expand them and try again
517 then THINK AGAIN. Here is the whole story, as detected and reported
518 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
520 Here's a test program that should detect the problem:
524 x = (1 :: Bogus Char) :: Bogus Bool
527 The problem with [the attempted shortcut code] is that
531 is not a sufficient condition to be able to use the shortcut!
532 You also need to know that the type synonym actually USES all
533 its arguments. For example, consider the following type synonym
534 which does not use all its arguments.
539 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
540 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
541 would fail, even though the expanded forms (both \tr{Int}) should
544 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
545 unnecessarily bind \tr{t} to \tr{Char}.
547 ... You could explicitly test for the problem synonyms and mark them
548 somehow as needing expansion, perhaps also issuing a warning to the
553 %************************************************************************
555 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
557 %************************************************************************
559 @uVar@ is called when at least one of the types being unified is a
560 variable. It does {\em not} assume that the variable is a fixed point
561 of the substitution; rather, notice that @uVar@ (defined below) nips
562 back into @uTys@ if it turns out that the variable is already bound.
565 uVar :: Bool -- False => tyvar is the "expected"
566 -- True => ty is the "expected" thing
568 -> TcTauType -> TcTauType -- printing and real versions
571 uVar swapped tv1 ps_ty2 ty2
572 = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2)) `thenM_`
573 getTcTyVar tv1 `thenM` \ maybe_ty1 ->
575 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
576 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
577 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
579 -- Expand synonyms; ignore FTVs
580 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
581 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
584 -- The both-type-variable case
585 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
587 -- Same type variable => no-op
591 -- Distinct type variables
592 -- ASSERT maybe_ty1 /= Just
594 = getTcTyVar tv2 `thenM` \ maybe_ty2 ->
596 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
600 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
601 putTcTyVar tv2 (TyVarTy tv1) `thenM_`
605 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
606 putTcTyVar tv1 ps_ty2 `thenM_`
611 update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
612 -- Try to get rid of open type variables as soon as poss
614 nicer_to_update_tv2 = isUserTyVar tv1
615 -- Don't unify a signature type variable if poss
616 || isSystemName (varName tv2)
617 -- Try to update sys-y type variables in preference to sig-y ones
619 -- Second one isn't a type variable
620 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
621 = -- Check that tv1 isn't a type-signature type variable
622 checkM (not (isSkolemTyVar tv1))
623 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenM_`
625 -- Do the occurs check, and check that we are not
626 -- unifying a type variable with a polytype
627 -- Returns a zonked type ready for the update
628 checkValue tv1 ps_ty2 non_var_ty2 `thenM` \ ty2 ->
630 -- Check that the kinds match
631 checkKinds swapped tv1 ty2 `thenM_`
633 -- Perform the update
634 putTcTyVar tv1 ty2 `thenM_`
639 checkKinds swapped tv1 ty2
640 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
641 -- ty2 has been zonked at this stage, which ensures that
642 -- its kind has as much boxity information visible as possible.
643 | tk2 `hasMoreBoxityInfo` tk1 = returnM ()
646 -- Either the kinds aren't compatible
647 -- (can happen if we unify (a b) with (c d))
648 -- or we are unifying a lifted type variable with an
649 -- unlifted type: e.g. (id 3#) is illegal
650 = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
654 (k1,k2) | swapped = (tk2,tk1)
655 | otherwise = (tk1,tk2)
661 checkValue tv1 ps_ty2 non_var_ty2
662 -- Do the occurs check, and check that we are not
663 -- unifying a type variable with a polytype
664 -- Return the type to update the type variable with, or fail
666 -- Basically we want to update tv1 := ps_ty2
667 -- because ps_ty2 has type-synonym info, which improves later error messages
672 -- f :: (A a -> a -> ()) -> ()
676 -- x = f (\ x p -> p x)
678 -- In the application (p x), we try to match "t" with "A t". If we go
679 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
680 -- an infinite loop later.
681 -- But we should not reject the program, because A t = ().
682 -- Rather, we should bind t to () (= non_var_ty2).
684 -- That's why we have this two-state occurs-check
685 = zonkTcType ps_ty2 `thenM` \ ps_ty2' ->
686 case okToUnifyWith tv1 ps_ty2' of {
687 Nothing -> returnM ps_ty2' ; -- Success
690 zonkTcType non_var_ty2 `thenM` \ non_var_ty2' ->
691 case okToUnifyWith tv1 non_var_ty2' of
692 Nothing -> -- This branch rarely succeeds, except in strange cases
693 -- like that in the example above
696 Just problem -> failWithTcM (unifyCheck problem tv1 ps_ty2')
699 data Problem = OccurCheck | NotMonoType
701 okToUnifyWith :: TcTyVar -> TcType -> Maybe Problem
702 -- (okToUnifyWith tv ty) checks whether it's ok to unify
705 -- Just p => not ok, problem p
710 ok (TyVarTy tv') | tv == tv' = Just OccurCheck
711 | otherwise = Nothing
712 ok (AppTy t1 t2) = ok t1 `and` ok t2
713 ok (FunTy t1 t2) = ok t1 `and` ok t2
714 ok (TyConApp _ ts) = oks ts
715 ok (ForAllTy _ _) = Just NotMonoType
716 ok (SourceTy st) = ok_st st
717 ok (NoteTy (FTVNote _) t) = ok t
718 ok (NoteTy (SynNote t1) t2) = ok t1 `and` ok t2
719 -- Type variables may be free in t1 but not t2
720 -- A forall may be in t2 but not t1
722 oks ts = foldr (and . ok) Nothing ts
724 ok_st (ClassP _ ts) = oks ts
725 ok_st (IParam _ t) = ok t
726 ok_st (NType _ ts) = oks ts
729 Just p `and` m = Just p
732 %************************************************************************
734 \subsection[Unify-fun]{@unifyFunTy@}
736 %************************************************************************
738 @subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
739 creation of type variables.
741 * subFunTy is used when we might be faced with a "hole" type variable,
742 in which case we should create two new holes.
744 * unifyFunTy is used when we expect to encounter only "ordinary"
745 type variables, so we should create new ordinary type variables
748 subFunTy :: TcHoleType -- Fail if ty isn't a function type
749 -- If it's a hole, make two holes, feed them to...
750 -> (TcHoleType -> TcHoleType -> TcM a) -- the thing inside
751 -> TcM a -- and bind the function type to the hole
753 subFunTy ty@(TyVarTy tyvar) thing_inside
755 = -- This is the interesting case
756 getTcTyVar tyvar `thenM` \ maybe_ty ->
758 Just ty' -> subFunTy ty' thing_inside ;
761 newHoleTyVarTy `thenM` \ arg_ty ->
762 newHoleTyVarTy `thenM` \ res_ty ->
765 thing_inside arg_ty res_ty `thenM` \ answer ->
767 -- Extract the answers
768 readHoleResult arg_ty `thenM` \ arg_ty' ->
769 readHoleResult res_ty `thenM` \ res_ty' ->
771 -- Write the answer into the incoming hole
772 putTcTyVar tyvar (mkFunTy arg_ty' res_ty') `thenM_`
774 -- And return the answer
777 subFunTy ty thing_inside
778 = unifyFunTy ty `thenM` \ (arg,res) ->
782 unifyFunTy :: TcRhoType -- Fail if ty isn't a function type
783 -> TcM (TcType, TcType) -- otherwise return arg and result types
785 unifyFunTy ty@(TyVarTy tyvar)
786 = ASSERT( not (isHoleTyVar tyvar) )
787 getTcTyVar tyvar `thenM` \ maybe_ty ->
789 Just ty' -> unifyFunTy ty'
790 Nothing -> unify_fun_ty_help ty
793 = case tcSplitFunTy_maybe ty of
794 Just arg_and_res -> returnM arg_and_res
795 Nothing -> unify_fun_ty_help ty
797 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
798 = newTyVarTy openTypeKind `thenM` \ arg ->
799 newTyVarTy openTypeKind `thenM` \ res ->
800 unifyTauTy ty (mkFunTy arg res) `thenM_`
805 unifyListTy :: TcType -- expected list type
806 -> TcM TcType -- list element type
808 unifyListTy ty@(TyVarTy tyvar)
809 = getTcTyVar tyvar `thenM` \ maybe_ty ->
811 Just ty' -> unifyListTy ty'
812 other -> unify_list_ty_help ty
815 = case tcSplitTyConApp_maybe ty of
816 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnM arg_ty
817 other -> unify_list_ty_help ty
819 unify_list_ty_help ty -- Revert to ordinary unification
820 = newTyVarTy liftedTypeKind `thenM` \ elt_ty ->
821 unifyTauTy ty (mkListTy elt_ty) `thenM_`
824 -- variant for parallel arrays
826 unifyPArrTy :: TcType -- expected list type
827 -> TcM TcType -- list element type
829 unifyPArrTy ty@(TyVarTy tyvar)
830 = getTcTyVar tyvar `thenM` \ maybe_ty ->
832 Just ty' -> unifyPArrTy ty'
833 _ -> unify_parr_ty_help ty
835 = case tcSplitTyConApp_maybe ty of
836 Just (tycon, [arg_ty]) | tycon == parrTyCon -> returnM arg_ty
837 _ -> unify_parr_ty_help ty
839 unify_parr_ty_help ty -- Revert to ordinary unification
840 = newTyVarTy liftedTypeKind `thenM` \ elt_ty ->
841 unifyTauTy ty (mkPArrTy elt_ty) `thenM_`
846 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
847 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
848 = getTcTyVar tyvar `thenM` \ maybe_ty ->
850 Just ty' -> unifyTupleTy boxity arity ty'
851 other -> unify_tuple_ty_help boxity arity ty
853 unifyTupleTy boxity arity ty
854 = case tcSplitTyConApp_maybe ty of
855 Just (tycon, arg_tys)
857 && tyConArity tycon == arity
858 && tupleTyConBoxity tycon == boxity
860 other -> unify_tuple_ty_help boxity arity ty
862 unify_tuple_ty_help boxity arity ty
863 = newTyVarTys arity kind `thenM` \ arg_tys ->
864 unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenM_`
867 kind | isBoxed boxity = liftedTypeKind
868 | otherwise = openTypeKind
872 %************************************************************************
874 \subsection{Kind unification}
876 %************************************************************************
879 unifyKind :: TcKind -- Expected
883 = addErrCtxtM (unifyCtxt "kind" k1 k2) $
886 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
887 unifyKinds [] [] = returnM ()
888 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenM_`
890 unifyKinds _ _ = panic "unifyKinds: length mis-match"
894 unifyOpenTypeKind :: TcKind -> TcM ()
895 -- Ensures that the argument kind is of the form (Type bx)
896 -- for some boxity bx
898 unifyOpenTypeKind ty@(TyVarTy tyvar)
899 = getTcTyVar tyvar `thenM` \ maybe_ty ->
901 Just ty' -> unifyOpenTypeKind ty'
902 other -> unify_open_kind_help ty
905 | isTypeKind ty = returnM ()
906 | otherwise = unify_open_kind_help ty
908 unify_open_kind_help ty -- Revert to ordinary unification
909 = newBoxityVar `thenM` \ boxity ->
910 unifyKind ty (mkTyConApp typeCon [boxity])
914 %************************************************************************
916 \subsection[Unify-context]{Errors and contexts}
918 %************************************************************************
924 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
925 = zonkTcType ty1 `thenM` \ ty1' ->
926 zonkTcType ty2 `thenM` \ ty2' ->
927 returnM (err ty1' ty2')
932 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
933 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
936 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
938 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
939 -- tv1 is zonked already
940 = zonkTcType ty2 `thenM` \ ty2' ->
943 err ty2 = (env2, ptext SLIT("When matching types") <+>
944 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
946 (pp_expected, pp_actual) | swapped = (pp2, pp1)
947 | otherwise = (pp1, pp2)
948 (env1, tv1') = tidyOpenTyVar tidy_env tv1
949 (env2, ty2') = tidyOpenType env1 ty2
953 unifyMisMatch ty1 ty2
954 = zonkTcType ty1 `thenM` \ ty1' ->
955 zonkTcType ty2 `thenM` \ ty2' ->
957 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
958 msg = hang (ptext SLIT("Couldn't match"))
959 4 (sep [quotes (ppr tidy_ty1),
960 ptext SLIT("against"),
961 quotes (ppr tidy_ty2)])
963 failWithTcM (env, msg)
965 unifyWithSigErr tyvar ty
966 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
967 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
969 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
970 (env2, tidy_ty) = tidyOpenType env1 ty
972 unifyCheck problem tyvar ty
974 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
976 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
977 (env2, tidy_ty) = tidyOpenType env1 ty
979 msg = case problem of
980 OccurCheck -> ptext SLIT("Occurs check: cannot construct the infinite type:")
981 NotMonoType -> ptext SLIT("Cannot unify a type variable with a type scheme:")
986 %************************************************************************
988 \subsection{Checking signature type variables}
990 %************************************************************************
992 @checkSigTyVars@ is used after the type in a type signature has been unified with
993 the actual type found. It then checks that the type variables of the type signature
995 (a) Still all type variables
996 eg matching signature [a] against inferred type [(p,q)]
997 [then a will be unified to a non-type variable]
999 (b) Still all distinct
1000 eg matching signature [(a,b)] against inferred type [(p,p)]
1001 [then a and b will be unified together]
1003 (c) Not mentioned in the environment
1004 eg the signature for f in this:
1010 Here, f is forced to be monorphic by the free occurence of x.
1012 (d) Not (unified with another type variable that is) in scope.
1013 eg f x :: (r->r) = (\y->y) :: forall a. a->r
1014 when checking the expression type signature, we find that
1015 even though there is nothing in scope whose type mentions r,
1016 nevertheless the type signature for the expression isn't right.
1018 Another example is in a class or instance declaration:
1020 op :: forall b. a -> b
1022 Here, b gets unified with a
1024 Before doing this, the substitution is applied to the signature type variable.
1026 We used to have the notion of a "DontBind" type variable, which would
1027 only be bound to itself or nothing. Then points (a) and (b) were
1028 self-checking. But it gave rise to bogus consequential error messages.
1031 f = (*) -- Monomorphic
1033 g :: Num a => a -> a
1036 Here, we get a complaint when checking the type signature for g,
1037 that g isn't polymorphic enough; but then we get another one when
1038 dealing with the (Num x) context arising from f's definition;
1039 we try to unify x with Int (to default it), but find that x has already
1040 been unified with the DontBind variable "a" from g's signature.
1041 This is really a problem with side-effecting unification; we'd like to
1042 undo g's effects when its type signature fails, but unification is done
1043 by side effect, so we can't (easily).
1045 So we revert to ordinary type variables for signatures, and try to
1046 give a helpful message in checkSigTyVars.
1049 checkSigTyVars :: [TcTyVar] -> TcM [TcTyVar]
1050 checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
1052 checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM [TcTyVar]
1053 checkSigTyVarsWrt extra_tvs sig_tvs
1054 = zonkTcTyVarsAndFV (varSetElems extra_tvs) `thenM` \ extra_tvs' ->
1055 check_sig_tyvars extra_tvs' sig_tvs
1058 :: TcTyVarSet -- Global type variables. The universally quantified
1059 -- tyvars should not mention any of these
1060 -- Guaranteed already zonked.
1061 -> [TcTyVar] -- Universally-quantified type variables in the signature
1062 -- Not guaranteed zonked.
1063 -> TcM [TcTyVar] -- Zonked signature type variables
1065 check_sig_tyvars extra_tvs []
1067 check_sig_tyvars extra_tvs sig_tvs
1068 = zonkTcTyVars sig_tvs `thenM` \ sig_tys ->
1069 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
1071 env_tvs = gbl_tvs `unionVarSet` extra_tvs
1073 traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tys,
1074 text "gbl_tvs" <+> ppr gbl_tvs,
1075 text "extra_tvs" <+> ppr extra_tvs])) `thenM_`
1077 checkM (allDistinctTyVars sig_tys env_tvs)
1078 (complain sig_tys env_tvs) `thenM_`
1080 returnM (map (tcGetTyVar "checkSigTyVars") sig_tys)
1083 complain sig_tys globals
1084 = -- "check" checks each sig tyvar in turn
1086 (env2, emptyVarEnv, [])
1087 (tidy_tvs `zip` tidy_tys) `thenM` \ (env3, _, msgs) ->
1089 failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
1091 (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs
1092 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
1094 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
1096 check (tidy_env, acc, msgs) (sig_tyvar,ty)
1097 -- sig_tyvar is from the signature;
1098 -- ty is what you get if you zonk sig_tyvar and then tidy it
1100 -- acc maps a zonked type variable back to a signature type variable
1101 = case tcGetTyVar_maybe ty of {
1102 Nothing -> -- Error (a)!
1103 returnM (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
1107 case lookupVarEnv acc tv of {
1108 Just sig_tyvar' -> -- Error (b)!
1109 returnM (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
1111 thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
1115 if tv `elemVarSet` globals -- Error (c) or (d)! Type variable escapes
1116 -- The least comprehensible, so put it last
1118 -- get the local TcIds and TyVars from the environment,
1119 -- and pass them to find_globals (they might have tv free)
1120 then getLclEnvElts `thenM` \ ve ->
1121 find_globals tv tidy_env ve `thenM` \ (tidy_env1, globs) ->
1122 returnM (tidy_env1, acc, escape_msg sig_tyvar tv globs : msgs)
1125 returnM (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
1131 -----------------------
1132 -- find_globals looks at the value environment and finds values
1133 -- whose types mention the offending type variable. It has to be
1134 -- careful to zonk the Id's type first, so it has to be in the monad.
1135 -- We must be careful to pass it a zonked type variable, too.
1140 -> TcM (TidyEnv, [SDoc])
1142 find_globals tv tidy_env things
1143 = go tidy_env [] things
1145 go tidy_env acc [] = returnM (tidy_env, acc)
1146 go tidy_env acc (thing : things)
1147 = find_thing ignore_it tidy_env thing `thenM` \ (tidy_env1, maybe_doc) ->
1149 Just d -> go tidy_env1 (d:acc) things
1150 Nothing -> go tidy_env1 acc things
1152 ignore_it ty = not (tv `elemVarSet` tyVarsOfType ty)
1154 -----------------------
1155 find_thing ignore_it tidy_env (ATcId id _)
1156 = zonkTcType (idType id) `thenM` \ id_ty ->
1157 if ignore_it id_ty then
1158 returnM (tidy_env, Nothing)
1160 (tidy_env', tidy_ty) = tidyOpenType tidy_env id_ty
1161 msg = sep [ppr id <+> dcolon <+> ppr tidy_ty,
1162 nest 2 (parens (ptext SLIT("bound at") <+>
1163 ppr (getSrcLoc id)))]
1165 returnM (tidy_env', Just msg)
1167 find_thing ignore_it tidy_env (ATyVar tv)
1168 = zonkTcTyVar tv `thenM` \ tv_ty ->
1169 if ignore_it tv_ty then
1170 returnM (tidy_env, Nothing)
1172 (tidy_env1, tv1) = tidyOpenTyVar tidy_env tv
1173 (tidy_env2, tidy_ty) = tidyOpenType tidy_env1 tv_ty
1174 msg = sep [ppr tv1 <+> eq_stuff, nest 2 bound_at]
1176 eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty
1177 | otherwise = equals <+> ppr tv_ty
1178 -- It's ok to use Type.getTyVar_maybe because ty is zonked by now
1180 bound_at = tyVarBindingInfo tv
1182 returnM (tidy_env2, Just msg)
1184 -----------------------
1185 escape_msg sig_tv tv globs
1186 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
1187 if notNull globs then
1188 vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"),
1189 nest 2 (vcat globs)]
1191 empty -- Sigh. It's really hard to give a good error message
1192 -- all the time. One bad case is an existential pattern match.
1193 -- We rely on the "When..." context to help.
1195 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
1196 | otherwise = ptext SLIT("It")
1199 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
1200 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
1203 These two context are used with checkSigTyVars
1206 sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
1207 -> TidyEnv -> TcM (TidyEnv, Message)
1208 sigCtxt id sig_tvs sig_theta sig_tau tidy_env
1209 = zonkTcType sig_tau `thenM` \ actual_tau ->
1211 (env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs
1212 (env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
1213 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1214 sub_msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
1215 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
1217 msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id),