-unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM ()
-unifyTauTyLists [] [] = returnTc ()
-unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_`
- unifyTauTyLists tys1 tys2
-unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
-\end{code}
-
-@unifyTauTyList@ takes a single list of @TauType@s and unifies them
-all together. It is used, for example, when typechecking explicit
-lists, when all the elts should be of the same type.
-
-\begin{code}
-unifyTauTyList :: [TcTauType] -> TcM ()
-unifyTauTyList [] = returnTc ()
-unifyTauTyList [ty] = returnTc ()
-unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
- unifyTauTyList tys
-\end{code}
-
-%************************************************************************
-%* *
-\subsection[Unify-uTys]{@uTys@: getting down to business}
-%* *
-%************************************************************************
-
-@uTys@ is the heart of the unifier. Each arg happens twice, because
-we want to report errors in terms of synomyms if poss. The first of
-the pair is used in error messages only; it is always the same as the
-second, except that if the first is a synonym then the second may be a
-de-synonym'd version. This way we get better error messages.
-
-We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
-
-\begin{code}
-uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
- -- ty1 is the *expected* type
-
- -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
- -- ty2 is the *actual* type
- -> TcM ()
-
- -- Always expand synonyms (see notes at end)
- -- (this also throws away FTVs)
-uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
-uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
-
- -- Ignore usage annotations inside typechecker
-uTys ps_ty1 (UsageTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
-uTys ps_ty1 ty1 ps_ty2 (UsageTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
-
- -- Variables; go for uVar
-uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
-uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
- -- "True" means args swapped
-
- -- Predicates
-uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
- | n1 == n2 = uTys t1 t1 t2 t2
-uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
- | c1 == c2 = unifyTauTyLists tys1 tys2
-uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
- | tc1 == tc2 = unifyTauTyLists tys1 tys2
-
- -- Functions; just check the two parts
-uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
- = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
-
- -- Type constructors must match
-uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
- | con1 == con2 && equalLength tys1 tys2
- = unifyTauTyLists tys1 tys2
-
- | con1 == openKindCon
- -- When we are doing kind checking, we might match a kind '?'
- -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and
- -- (CCallable Int) and (CCallable Int#) are both OK
- = unifyOpenTypeKind ps_ty2
-
- -- Applications need a bit of care!
- -- They can match FunTy and TyConApp, so use splitAppTy_maybe
- -- NB: we've already dealt with type variables and Notes,
- -- so if one type is an App the other one jolly well better be too
-uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
- = case tcSplitAppTy_maybe ty2 of
- Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
- Nothing -> unifyMisMatch ps_ty1 ps_ty2
-
- -- Now the same, but the other way round
- -- Don't swap the types, because the error messages get worse
-uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
- = case tcSplitAppTy_maybe ty1 of
- Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
- Nothing -> unifyMisMatch ps_ty1 ps_ty2
-
- -- Not expecting for-alls in unification
- -- ... but the error message from the unifyMisMatch more informative
- -- than a panic message!
-
- -- Anything else fails
-uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
-\end{code}
-
-
-Notes on synonyms
-~~~~~~~~~~~~~~~~~
-If you are tempted to make a short cut on synonyms, as in this
-pseudocode...
-
-\begin{verbatim}
--- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
--- NO = if (con1 == con2) then
--- NO -- Good news! Same synonym constructors, so we can shortcut
--- NO -- by unifying their arguments and ignoring their expansions.
--- NO unifyTauTypeLists args1 args2
--- NO else
--- NO -- Never mind. Just expand them and try again
--- NO uTys ty1 ty2
-\end{verbatim}
-
-then THINK AGAIN. Here is the whole story, as detected and reported
-by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
-\begin{quotation}
-Here's a test program that should detect the problem:
-
-\begin{verbatim}
- type Bogus a = Int
- x = (1 :: Bogus Char) :: Bogus Bool
-\end{verbatim}
-
-The problem with [the attempted shortcut code] is that
-\begin{verbatim}
- con1 == con2
-\end{verbatim}
-is not a sufficient condition to be able to use the shortcut!
-You also need to know that the type synonym actually USES all
-its arguments. For example, consider the following type synonym
-which does not use all its arguments.
-\begin{verbatim}
- type Bogus a = Int
-\end{verbatim}
-
-If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
-the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
-would fail, even though the expanded forms (both \tr{Int}) should
-match.
-
-Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
-unnecessarily bind \tr{t} to \tr{Char}.
-
-... You could explicitly test for the problem synonyms and mark them
-somehow as needing expansion, perhaps also issuing a warning to the
-user.
-\end{quotation}
-
-
-%************************************************************************
-%* *
-\subsection[Unify-uVar]{@uVar@: unifying with a type variable}
-%* *
-%************************************************************************
-
-@uVar@ is called when at least one of the types being unified is a
-variable. It does {\em not} assume that the variable is a fixed point
-of the substitution; rather, notice that @uVar@ (defined below) nips
-back into @uTys@ if it turns out that the variable is already bound.
-
-\begin{code}
-uVar :: Bool -- False => tyvar is the "expected"
- -- True => ty is the "expected" thing
- -> TcTyVar
- -> TcTauType -> TcTauType -- printing and real versions
- -> TcM ()
-
-uVar swapped tv1 ps_ty2 ty2
- = getTcTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
- case maybe_ty1 of
- Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
- | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
- other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
-
- -- Expand synonyms; ignore FTVs
-uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
- = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
-
-
- -- The both-type-variable case
-uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
-
- -- Same type variable => no-op
- | tv1 == tv2
- = returnTc ()
-
- -- Distinct type variables
- -- ASSERT maybe_ty1 /= Just
- | otherwise
- = getTcTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
- case maybe_ty2 of
- Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
-
- Nothing | update_tv2
-
- -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
- putTcTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
- returnTc ()
- | otherwise
-
- -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
- (putTcTyVar tv1 ps_ty2 `thenNF_Tc_`
- returnTc ())
- where
- k1 = tyVarKind tv1
- k2 = tyVarKind tv2
- update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
- -- Try to get rid of open type variables as soon as poss
-
- nicer_to_update_tv2 = isSigTyVar tv1
- -- Don't unify a signature type variable if poss
- || isSystemName (varName tv2)
- -- Try to update sys-y type variables in preference to sig-y ones
-
- -- Second one isn't a type variable
-uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
- = -- Check that the kinds match
- checkKinds swapped tv1 non_var_ty2 `thenTc_`
-
- -- Check that tv1 isn't a type-signature type variable
- checkTcM (not (isSigTyVar tv1))
- (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
-
- -- Check that we aren't losing boxity info (shouldn't happen)
- warnTc (not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1))
- ((ppr tv1 <+> ppr (tyVarKind tv1)) $$
- (ppr non_var_ty2 <+> ppr (typeKind non_var_ty2))) `thenNF_Tc_`
-
- -- Occurs check
- -- Basically we want to update tv1 := ps_ty2
- -- because ps_ty2 has type-synonym info, which improves later error messages
- --
- -- But consider
- -- type A a = ()
- --
- -- f :: (A a -> a -> ()) -> ()
- -- f = \ _ -> ()
- --
- -- x :: ()
- -- x = f (\ x p -> p x)
- --
- -- In the application (p x), we try to match "t" with "A t". If we go
- -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
- -- an infinite loop later.
- -- But we should not reject the program, because A t = ().
- -- Rather, we should bind t to () (= non_var_ty2).
- --
- -- That's why we have this two-state occurs-check
- zonkTcType ps_ty2 `thenNF_Tc` \ ps_ty2' ->
- if not (tv1 `elemVarSet` tyVarsOfType ps_ty2') then
- putTcTyVar tv1 ps_ty2' `thenNF_Tc_`
- returnTc ()
- else
- zonkTcType non_var_ty2 `thenNF_Tc` \ non_var_ty2' ->
- if not (tv1 `elemVarSet` tyVarsOfType non_var_ty2') then
- -- This branch rarely succeeds, except in strange cases
- -- like that in the example above
- putTcTyVar tv1 non_var_ty2' `thenNF_Tc_`
- returnTc ()
- else
- failWithTcM (unifyOccurCheck tv1 ps_ty2')
-
-
-checkKinds swapped tv1 ty2
--- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
--- We need to check that we don't unify a lifted type variable with an
--- unlifted type: e.g. (id 3#) is illegal
- | tk1 `eqKind` liftedTypeKind && tk2 `eqKind` unliftedTypeKind
- = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
- unifyMisMatch k1 k2
- | otherwise
- = returnTc ()