2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section{Monadic type operations}
6 This module contains monadic operations over types that contain mutable type variables
10 TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcRhoType, TcTyVarSet,
12 --------------------------------
13 -- Creating new mutable type variables
15 newTyVarTy, -- Kind -> NF_TcM TcType
16 newTyVarTys, -- Int -> Kind -> NF_TcM [TcType]
17 newKindVar, newKindVars, newBoxityVar,
19 --------------------------------
21 tcInstTyVar, tcInstTyVars,
22 tcInstSigVars, tcInstType,
25 --------------------------------
27 unifyTauTy, unifyTauTyList, unifyTauTyLists,
28 unifyFunTy, unifyListTy, unifyTupleTy,
29 unifyKind, unifyKinds, unifyOpenTypeKind,
31 --------------------------------
33 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars,
34 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
35 zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,
39 #include "HsVersions.h"
43 import TypeRep ( Type(..), SourceType(..), Kind, TyNote(..), -- friend
46 import TcType ( tcEqType,
47 tcSplitRhoTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
48 tcSplitTyConApp_maybe, tcSplitFunTy_maybe, tcSplitForAllTys,
49 tcGetTyVar, tcIsTyVarTy,
51 mkAppTy, mkTyVarTy, mkTyVarTys, mkFunTy, mkTyConApp,
53 liftedTypeKind, unliftedTypeKind, openTypeKind, defaultKind, superKind,
54 superBoxity, liftedBoxity, hasMoreBoxityInfo, typeKind,
55 tyVarsOfType, tyVarsOfTypes, tidyOpenType, tidyOpenTypes, tidyTyVar,
58 import Subst ( Subst, mkTopTyVarSubst, substTy )
59 import TyCon ( TyCon, mkPrimTyCon, isTupleTyCon, tyConArity, tupleTyConBoxity )
60 import PrimRep ( PrimRep(VoidRep) )
61 import Var ( TyVar, varName, tyVarKind, tyVarName, isTyVar, mkTyVar,
62 isMutTyVar, isSigTyVar )
65 import TcMonad -- TcType, amongst others
66 import TysWiredIn ( voidTy, listTyCon, mkListTy, mkTupleTy )
68 import Name ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
69 mkLocalName, mkDerivedTyConOcc, isSystemName
72 import BasicTypes ( Boxity, Arity, isBoxed )
73 import Unique ( Uniquable(..) )
74 import SrcLoc ( noSrcLoc )
75 import Util ( nOfThem )
80 %************************************************************************
82 \subsection{New type variables}
84 %************************************************************************
87 newTyVar :: Kind -> NF_TcM TcTyVar
89 = tcGetUnique `thenNF_Tc` \ uniq ->
90 tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind
92 newTyVarTy :: Kind -> NF_TcM TcType
94 = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
95 returnNF_Tc (TyVarTy tc_tyvar)
97 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
98 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
100 newKindVar :: NF_TcM TcKind
102 = tcGetUnique `thenNF_Tc` \ uniq ->
103 tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind `thenNF_Tc` \ kv ->
104 returnNF_Tc (TyVarTy kv)
106 newKindVars :: Int -> NF_TcM [TcKind]
107 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
109 newBoxityVar :: NF_TcM TcKind
111 = tcGetUnique `thenNF_Tc` \ uniq ->
112 tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity `thenNF_Tc` \ kv ->
113 returnNF_Tc (TyVarTy kv)
117 %************************************************************************
119 \subsection{Type instantiation}
121 %************************************************************************
123 I don't understand why this is needed
124 An old comments says "No need for tcSplitForAllTyM because a type
125 variable can't be instantiated to a for-all type"
126 But the same is true of rho types!
129 tcSplitRhoTyM :: TcType -> NF_TcM (TcThetaType, TcType)
133 -- A type variable is never instantiated to a dictionary type,
134 -- so we don't need to do a tcReadVar on the "arg".
135 go syn_t (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
136 Just pair -> go res res (pair:ts)
137 Nothing -> returnNF_Tc (reverse ts, syn_t)
138 go syn_t (NoteTy n t) ts = go syn_t t ts
139 go syn_t (TyVarTy tv) ts = getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
141 Just ty | not (tcIsTyVarTy ty) -> go syn_t ty ts
142 other -> returnNF_Tc (reverse ts, syn_t)
143 go syn_t (UsageTy _ t) ts = go syn_t t ts
144 go syn_t t ts = returnNF_Tc (reverse ts, syn_t)
148 %************************************************************************
150 \subsection{Type instantiation}
152 %************************************************************************
154 Instantiating a bunch of type variables
157 tcInstTyVars :: [TyVar]
158 -> NF_TcM ([TcTyVar], [TcType], Subst)
161 = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
163 tys = mkTyVarTys tc_tyvars
165 returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
166 -- Since the tyvars are freshly made,
167 -- they cannot possibly be captured by
168 -- any existing for-alls. Hence mkTopTyVarSubst
171 = tcGetUnique `thenNF_Tc` \ uniq ->
173 name = setNameUnique (tyVarName tyvar) uniq
174 -- Note that we don't change the print-name
175 -- This won't confuse the type checker but there's a chance
176 -- that two different tyvars will print the same way
177 -- in an error message. -dppr-debug will show up the difference
178 -- Better watch out for this. If worst comes to worst, just
179 -- use mkSysLocalName.
181 tcNewMutTyVar name (tyVarKind tyvar)
183 tcInstSigVars tyvars -- Very similar to tcInstTyVar
184 = tcGetUniques `thenNF_Tc` \ uniqs ->
185 listTc [ ASSERT( not (kind `eqKind` openTypeKind) ) -- Shouldn't happen
186 tcNewSigTyVar name kind
187 | (tyvar, uniq) <- tyvars `zip` uniqs,
188 let name = setNameUnique (tyVarName tyvar) uniq,
189 let kind = tyVarKind tyvar
193 @tcInstType@ instantiates the outer-level for-alls of a TcType with
194 fresh type variables, splits off the dictionary part, and returns the results.
197 tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
199 = case tcSplitForAllTys ty of
200 ([], rho) -> -- There may be overloading but no type variables;
201 -- (?x :: Int) => Int -> Int
203 (theta, tau) = tcSplitRhoTy rho -- Used to be tcSplitRhoTyM
205 returnNF_Tc ([], theta, tau)
207 (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
209 (theta, tau) = tcSplitRhoTy (substTy tenv rho) -- Used to be tcSplitRhoTyM
211 returnNF_Tc (tyvars', theta, tau)
216 %************************************************************************
218 \subsection{Putting and getting mutable type variables}
220 %************************************************************************
223 putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
224 getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
231 | not (isMutTyVar tyvar)
232 = pprTrace "putTcTyVar" (ppr tyvar) $
236 = ASSERT( isMutTyVar tyvar )
237 UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
238 tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
242 Getting is more interesting. The easy thing to do is just to read, thus:
245 getTcTyVar tyvar = tcReadMutTyVar tyvar
248 But it's more fun to short out indirections on the way: If this
249 version returns a TyVar, then that TyVar is unbound. If it returns
250 any other type, then there might be bound TyVars embedded inside it.
252 We return Nothing iff the original box was unbound.
256 | not (isMutTyVar tyvar)
257 = pprTrace "getTcTyVar" (ppr tyvar) $
258 returnNF_Tc (Just (mkTyVarTy tyvar))
261 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
262 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
264 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
265 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
266 returnNF_Tc (Just ty')
268 Nothing -> returnNF_Tc Nothing
270 short_out :: TcType -> NF_TcM TcType
271 short_out ty@(TyVarTy tyvar)
272 | not (isMutTyVar tyvar)
276 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
278 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
279 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
282 other -> returnNF_Tc ty
284 short_out other_ty = returnNF_Tc other_ty
288 %************************************************************************
290 \subsection{Zonking -- the exernal interfaces}
292 %************************************************************************
294 ----------------- Type variables
297 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
298 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
300 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
301 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
302 returnNF_Tc (tyVarsOfTypes tys)
304 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
305 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
307 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
308 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
309 -- Usually this job is done by checkSigTyVars, but in a couple of places
310 -- that is overkill, so we use this simpler chap
311 zonkTcSigTyVars tyvars
312 = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
313 returnNF_Tc (map (tcGetTyVar "zonkTcSigTyVars") tys)
316 ----------------- Types
319 zonkTcType :: TcType -> NF_TcM TcType
320 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
322 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
323 zonkTcTypes tys = mapNF_Tc zonkTcType tys
325 zonkTcClassConstraints cts = mapNF_Tc zonk cts
326 where zonk (clas, tys)
327 = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
328 returnNF_Tc (clas, new_tys)
330 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
331 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
333 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
334 zonkTcPredType (ClassP c ts) =
335 zonkTcTypes ts `thenNF_Tc` \ new_ts ->
336 returnNF_Tc (ClassP c new_ts)
337 zonkTcPredType (IParam n t) =
338 zonkTcType t `thenNF_Tc` \ new_t ->
339 returnNF_Tc (IParam n new_t)
342 ------------------- These ...ToType, ...ToKind versions
343 are used at the end of type checking
346 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
348 = mapNF_Tc zonk_it pairs
350 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
351 returnNF_Tc (name, kind)
353 -- When zonking a kind, we want to
354 -- zonk a *kind* variable to (Type *)
355 -- zonk a *boxity* variable to *
356 zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
357 | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
358 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
360 zonkTcTypeToType :: TcType -> NF_TcM Type
361 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
363 -- Zonk a mutable but unbound type variable to
364 -- Void if it has kind Lifted
366 zonk_unbound_tyvar tv
367 | kind `eqKind` liftedTypeKind || kind `eqKind` openTypeKind
368 = putTcTyVar tv voidTy -- Just to avoid creating a new tycon in
369 -- this vastly common case
371 = putTcTyVar tv (TyConApp (mk_void_tycon tv kind) [])
375 mk_void_tycon tv kind -- Make a new TyCon with the same kind as the
376 -- type variable tv. Same name too, apart from
377 -- making it start with a colon (sigh)
378 -- I dread to think what will happen if this gets out into an
379 -- interface file. Catastrophe likely. Major sigh.
380 = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
381 mkPrimTyCon tc_name kind 0 [] VoidRep
383 tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
385 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
386 -- of a type variable, at the *end* of type checking. It changes
387 -- the *mutable* type variable into an *immutable* one.
389 -- It does this by making an immutable version of tv and binds tv to it.
390 -- Now any bound occurences of the original type variable will get
391 -- zonked to the immutable version.
393 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
394 zonkTcTyVarToTyVar tv
396 -- Make an immutable version, defaulting
397 -- the kind to lifted if necessary
398 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
399 immut_tv_ty = mkTyVarTy immut_tv
401 zap tv = putTcTyVar tv immut_tv_ty
402 -- Bind the mutable version to the immutable one
404 -- If the type variable is mutable, then bind it to immut_tv_ty
405 -- so that all other occurrences of the tyvar will get zapped too
406 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
408 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
414 %************************************************************************
416 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
418 %* For internal use only! *
420 %************************************************************************
423 -- zonkType is used for Kinds as well
425 -- For unbound, mutable tyvars, zonkType uses the function given to it
426 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
427 -- type variable and zonks the kind too
429 zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
430 -- see zonkTcType, and zonkTcTypeToType
433 zonkType unbound_var_fn ty
436 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
437 returnNF_Tc (TyConApp tycon tys')
439 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
440 go ty2 `thenNF_Tc` \ ty2' ->
441 returnNF_Tc (NoteTy (SynNote ty1') ty2')
443 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
445 go (SourceTy p) = go_pred p `thenNF_Tc` \ p' ->
446 returnNF_Tc (SourceTy p')
448 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
449 go res `thenNF_Tc` \ res' ->
450 returnNF_Tc (FunTy arg' res')
452 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
453 go arg `thenNF_Tc` \ arg' ->
454 returnNF_Tc (mkAppTy fun' arg')
456 go (UsageTy u ty) = go u `thenNF_Tc` \ u' ->
457 go ty `thenNF_Tc` \ ty' ->
458 returnNF_Tc (UsageTy u' ty')
460 -- The two interesting cases!
461 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
463 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
464 go ty `thenNF_Tc` \ ty' ->
465 returnNF_Tc (ForAllTy tyvar' ty')
467 go_pred (ClassP c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
468 returnNF_Tc (ClassP c tys')
469 go_pred (NType tc tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
470 returnNF_Tc (NType tc tys')
471 go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' ->
472 returnNF_Tc (IParam n ty')
474 zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
475 -> TcTyVar -> NF_TcM TcType
476 zonkTyVar unbound_var_fn tyvar
477 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
478 -- zonking a forall type, when the bound type variable
479 -- needn't be mutable
480 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
481 returnNF_Tc (TyVarTy tyvar)
484 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
486 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
487 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
492 %************************************************************************
494 \subsection{The Kind variants}
496 %************************************************************************
499 unifyKind :: TcKind -- Expected
503 = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
506 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
507 unifyKinds [] [] = returnTc ()
508 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_`
510 unifyKinds _ _ = panic "unifyKinds: length mis-match"
514 unifyOpenTypeKind :: TcKind -> TcM ()
515 -- Ensures that the argument kind is of the form (Type bx)
516 -- for some boxity bx
518 unifyOpenTypeKind ty@(TyVarTy tyvar)
519 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
521 Just ty' -> unifyOpenTypeKind ty'
522 other -> unify_open_kind_help ty
525 = case tcSplitTyConApp_maybe ty of
526 Just (tycon, [_]) | tycon == typeCon -> returnTc ()
527 other -> unify_open_kind_help ty
529 unify_open_kind_help ty -- Revert to ordinary unification
530 = newBoxityVar `thenNF_Tc` \ boxity ->
531 unifyKind ty (mkTyConApp typeCon [boxity])
535 %************************************************************************
537 \subsection[Unify-exported]{Exported unification functions}
539 %************************************************************************
541 The exported functions are all defined as versions of some
542 non-exported generic functions.
544 Unify two @TauType@s. Dead straightforward.
547 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
548 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
549 = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
553 @unifyTauTyList@ unifies corresponding elements of two lists of
554 @TauType@s. It uses @uTys@ to do the real work. The lists should be
555 of equal length. We charge down the list explicitly so that we can
556 complain if their lengths differ.
559 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM ()
560 unifyTauTyLists [] [] = returnTc ()
561 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_`
562 unifyTauTyLists tys1 tys2
563 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
566 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
567 all together. It is used, for example, when typechecking explicit
568 lists, when all the elts should be of the same type.
571 unifyTauTyList :: [TcTauType] -> TcM ()
572 unifyTauTyList [] = returnTc ()
573 unifyTauTyList [ty] = returnTc ()
574 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
578 %************************************************************************
580 \subsection[Unify-uTys]{@uTys@: getting down to business}
582 %************************************************************************
584 @uTys@ is the heart of the unifier. Each arg happens twice, because
585 we want to report errors in terms of synomyms if poss. The first of
586 the pair is used in error messages only; it is always the same as the
587 second, except that if the first is a synonym then the second may be a
588 de-synonym'd version. This way we get better error messages.
590 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
593 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
594 -- ty1 is the *expected* type
596 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
597 -- ty2 is the *actual* type
600 -- Always expand synonyms (see notes at end)
601 -- (this also throws away FTVs)
602 uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
603 uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
605 -- Ignore usage annotations inside typechecker
606 uTys ps_ty1 (UsageTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
607 uTys ps_ty1 ty1 ps_ty2 (UsageTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
609 -- Variables; go for uVar
610 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
611 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
612 -- "True" means args swapped
615 uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
616 | n1 == n2 = uTys t1 t1 t2 t2
617 uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
618 | c1 == c2 = unifyTauTyLists tys1 tys2
619 uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
620 | tc1 == tc2 = unifyTauTyLists tys1 tys2
622 -- Functions; just check the two parts
623 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
624 = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
626 -- Type constructors must match
627 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
628 | con1 == con2 && length tys1 == length tys2
629 = unifyTauTyLists tys1 tys2
631 | con1 == openKindCon
632 -- When we are doing kind checking, we might match a kind '?'
633 -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and
634 -- (CCallable Int) and (CCallable Int#) are both OK
635 = unifyOpenTypeKind ps_ty2
637 -- Applications need a bit of care!
638 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
639 -- NB: we've already dealt with type variables and Notes,
640 -- so if one type is an App the other one jolly well better be too
641 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
642 = case tcSplitAppTy_maybe ty2 of
643 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
644 Nothing -> unifyMisMatch ps_ty1 ps_ty2
646 -- Now the same, but the other way round
647 -- Don't swap the types, because the error messages get worse
648 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
649 = case tcSplitAppTy_maybe ty1 of
650 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
651 Nothing -> unifyMisMatch ps_ty1 ps_ty2
653 -- Not expecting for-alls in unification
654 -- ... but the error message from the unifyMisMatch more informative
655 -- than a panic message!
657 -- Anything else fails
658 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
664 If you are tempted to make a short cut on synonyms, as in this
668 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
669 -- NO = if (con1 == con2) then
670 -- NO -- Good news! Same synonym constructors, so we can shortcut
671 -- NO -- by unifying their arguments and ignoring their expansions.
672 -- NO unifyTauTypeLists args1 args2
674 -- NO -- Never mind. Just expand them and try again
678 then THINK AGAIN. Here is the whole story, as detected and reported
679 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
681 Here's a test program that should detect the problem:
685 x = (1 :: Bogus Char) :: Bogus Bool
688 The problem with [the attempted shortcut code] is that
692 is not a sufficient condition to be able to use the shortcut!
693 You also need to know that the type synonym actually USES all
694 its arguments. For example, consider the following type synonym
695 which does not use all its arguments.
700 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
701 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
702 would fail, even though the expanded forms (both \tr{Int}) should
705 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
706 unnecessarily bind \tr{t} to \tr{Char}.
708 ... You could explicitly test for the problem synonyms and mark them
709 somehow as needing expansion, perhaps also issuing a warning to the
714 %************************************************************************
716 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
718 %************************************************************************
720 @uVar@ is called when at least one of the types being unified is a
721 variable. It does {\em not} assume that the variable is a fixed point
722 of the substitution; rather, notice that @uVar@ (defined below) nips
723 back into @uTys@ if it turns out that the variable is already bound.
726 uVar :: Bool -- False => tyvar is the "expected"
727 -- True => ty is the "expected" thing
729 -> TcTauType -> TcTauType -- printing and real versions
732 uVar swapped tv1 ps_ty2 ty2
733 = getTcTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
735 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
736 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
737 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
739 -- Expand synonyms; ignore FTVs
740 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
741 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
744 -- The both-type-variable case
745 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
747 -- Same type variable => no-op
751 -- Distinct type variables
752 -- ASSERT maybe_ty1 /= Just
754 = getTcTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
756 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
760 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
761 putTcTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
765 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
766 (putTcTyVar tv1 ps_ty2 `thenNF_Tc_`
771 update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
772 -- Try to get rid of open type variables as soon as poss
774 nicer_to_update_tv2 = isSigTyVar tv1
775 -- Don't unify a signature type variable if poss
776 || isSystemName (varName tv2)
777 -- Try to update sys-y type variables in preference to sig-y ones
779 -- Second one isn't a type variable
780 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
781 = -- Check that the kinds match
782 checkKinds swapped tv1 non_var_ty2 `thenTc_`
784 -- Check that tv1 isn't a type-signature type variable
785 checkTcM (not (isSigTyVar tv1))
786 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
788 -- Check that we aren't losing boxity info (shouldn't happen)
789 warnTc (not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1))
790 ((ppr tv1 <+> ppr (tyVarKind tv1)) $$
791 (ppr non_var_ty2 <+> ppr (typeKind non_var_ty2))) `thenNF_Tc_`
794 -- Basically we want to update tv1 := ps_ty2
795 -- because ps_ty2 has type-synonym info, which improves later error messages
800 -- f :: (A a -> a -> ()) -> ()
804 -- x = f (\ x p -> p x)
806 -- In the application (p x), we try to match "t" with "A t". If we go
807 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
808 -- an infinite loop later.
809 -- But we should not reject the program, because A t = ().
810 -- Rather, we should bind t to () (= non_var_ty2).
812 -- That's why we have this two-state occurs-check
813 zonkTcType ps_ty2 `thenNF_Tc` \ ps_ty2' ->
814 if not (tv1 `elemVarSet` tyVarsOfType ps_ty2') then
815 putTcTyVar tv1 ps_ty2' `thenNF_Tc_`
818 zonkTcType non_var_ty2 `thenNF_Tc` \ non_var_ty2' ->
819 if not (tv1 `elemVarSet` tyVarsOfType non_var_ty2') then
820 -- This branch rarely succeeds, except in strange cases
821 -- like that in the example above
822 putTcTyVar tv1 non_var_ty2' `thenNF_Tc_`
825 failWithTcM (unifyOccurCheck tv1 ps_ty2')
828 checkKinds swapped tv1 ty2
829 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
830 -- We need to check that we don't unify a lifted type variable with an
831 -- unlifted type: e.g. (id 3#) is illegal
832 | tk1 `eqKind` liftedTypeKind && tk2 `eqKind` unliftedTypeKind
833 = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
838 (k1,k2) | swapped = (tk2,tk1)
839 | otherwise = (tk1,tk2)
845 %************************************************************************
847 \subsection[Unify-fun]{@unifyFunTy@}
849 %************************************************************************
851 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
854 unifyFunTy :: TcType -- Fail if ty isn't a function type
855 -> TcM (TcType, TcType) -- otherwise return arg and result types
857 unifyFunTy ty@(TyVarTy tyvar)
858 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
860 Just ty' -> unifyFunTy ty'
861 other -> unify_fun_ty_help ty
864 = case tcSplitFunTy_maybe ty of
865 Just arg_and_res -> returnTc arg_and_res
866 Nothing -> unify_fun_ty_help ty
868 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
869 = newTyVarTy openTypeKind `thenNF_Tc` \ arg ->
870 newTyVarTy openTypeKind `thenNF_Tc` \ res ->
871 unifyTauTy ty (mkFunTy arg res) `thenTc_`
876 unifyListTy :: TcType -- expected list type
877 -> TcM TcType -- list element type
879 unifyListTy ty@(TyVarTy tyvar)
880 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
882 Just ty' -> unifyListTy ty'
883 other -> unify_list_ty_help ty
886 = case tcSplitTyConApp_maybe ty of
887 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
888 other -> unify_list_ty_help ty
890 unify_list_ty_help ty -- Revert to ordinary unification
891 = newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty ->
892 unifyTauTy ty (mkListTy elt_ty) `thenTc_`
897 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
898 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
899 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
901 Just ty' -> unifyTupleTy boxity arity ty'
902 other -> unify_tuple_ty_help boxity arity ty
904 unifyTupleTy boxity arity ty
905 = case tcSplitTyConApp_maybe ty of
906 Just (tycon, arg_tys)
908 && tyConArity tycon == arity
909 && tupleTyConBoxity tycon == boxity
911 other -> unify_tuple_ty_help boxity arity ty
913 unify_tuple_ty_help boxity arity ty
914 = newTyVarTys arity kind `thenNF_Tc` \ arg_tys ->
915 unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenTc_`
918 kind | isBoxed boxity = liftedTypeKind
919 | otherwise = openTypeKind
923 %************************************************************************
925 \subsection[Unify-context]{Errors and contexts}
927 %************************************************************************
933 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
934 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
935 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
936 returnNF_Tc (err ty1' ty2')
941 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
942 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
945 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
947 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
948 -- tv1 is zonked already
949 = zonkTcType ty2 `thenNF_Tc` \ ty2' ->
950 returnNF_Tc (err ty2')
952 err ty2 = (env2, ptext SLIT("When matching types") <+>
953 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
955 (pp_expected, pp_actual) | swapped = (pp2, pp1)
956 | otherwise = (pp1, pp2)
957 (env1, tv1') = tidyTyVar tidy_env tv1
958 (env2, ty2') = tidyOpenType env1 ty2
962 unifyMisMatch ty1 ty2
963 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
964 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
966 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
967 msg = hang (ptext SLIT("Couldn't match"))
968 4 (sep [quotes (ppr tidy_ty1),
969 ptext SLIT("against"),
970 quotes (ppr tidy_ty2)])
972 failWithTcM (env, msg)
974 unifyWithSigErr tyvar ty
975 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
976 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
978 (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
979 (env2, tidy_ty) = tidyOpenType env1 ty
981 unifyOccurCheck tyvar ty
982 = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
983 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
985 (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
986 (env2, tidy_ty) = tidyOpenType env1 ty